5

任意のツリーが与えられた場合、シューベルトの番号付けを使用して、そのツリーに対してサブタイプの関係を構築できます。

constructH :: Tree a -> Tree (Type a)

whereTypeは元のラベルをネストし、さらに子/親 (またはサブタイプ) チェックを実行するために必要なデータを提供します。Schubert Numbering では、2 つの Int パラメータで十分です。

data Type a where !Int -> !Int -> a -> Type a

これは二項述語につながります

subtypeOf :: Type a -> Type a -> Bool

ここで、QuickCheck を使用して、これが実際にやりたいことを実行することをテストしたいと思います。ただし、次のプロパティは機能しません。QuickCheck があきらめるだけだからです。

subtypeSanity ∷ Tree (Type ()) → Gen Prop
subtypeSanity Node { rootLabel = t, subForest = f } =
  let subtypes = concatMap flatten f
  in (not $ null subtypes) ==> conjoin
     (forAll (elements subtypes) (\x → x `subtypeOf` t):(map subtypeSanity f))

への再帰呼び出しsubtypeSanity、つまり に渡すリストの末尾を省略したconjoin場合、プロパティは問題なく実行されますが、ツリーのルート ノードだけがテストされます。QuickCheck が新しいテスト ケースの生成をあきらめずに、データ構造に再帰的に降りるにはどうすればよいですか?

必要に応じて、シューベルト階層を構築するコードと のArbitraryインスタンスTree (Type a)を提供して、完全に実行可能な例を提供できますが、それはかなりの量のコードになります。私は、QuickCheck を「取得」していないだけでなく、ここで間違った方法で使用していると確信しています。

編集: 残念ながら、sized関数はここで問題を解決していないようです。最終的に同じ結果になります（J. Abrahamsonの回答へのコメントを参照してください）。

編集 II: 再帰的なステップを回避し、conjoin. ツリー内のすべてのノードのリストを作成し、それらの単一ノード プロパティ (最初から正常に機能していました) をテストします。

allNodes ∷ Tree a → [Tree a]
allNodes n@(Node { subForest = f }) = n:(concatMap allNodes f)

subtypeSanity ∷ Tree (Type ()) → Gen Prop
subtypeSanity tree = forAll (elements $ allNodes tree)
  (\(Node { rootLabel = t, subForest = f }) →
    let subtypes = concatMap flatten f
    in (not $ null subtypes) ==> forAll (elements subtypes) (\x → x `subtypeOf` t))

木のインスタンスを微調整してArbitraryも機能しませんでした。私がまだ使用している任意のインスタンスは次のとおりです。

instance (Arbitrary a, Eq a) ⇒ Arbitrary (Tree (Type a)) where
  arbitrary = liftM (constructH) $ sized arbTree

arbTree ∷ Arbitrary a ⇒ Int → Gen (Tree a)
arbTree n = do
  m ← choose (0,n)
  if m == 0
    then Node <$> arbitrary <*> (return [])
    else do part ← randomPartition n m
            Node <$> arbitrary <*> mapM arbTree part

-- this is a crude way to find a sufficiently random x1,..,xm,
-- such that x1 + .. + xm = n, for any n, m, with 0 < m.
randomPartition ∷ Int → Int → Gen [Int]
randomPartition n m' = do
  let m = m' - 1
  seed ← liftM ((++[n]) . sort) $ replicateM m (choose (0,n))
  return $ zipWith (-) seed (0:seed)

問題は「今のところ解決した」と考えていますが、誰かが再帰的なステップやconjoinQuickCheck をあきらめさせた理由を説明してくれたら (「0 個の」テストのみを通過した後)、感謝します。

4

2 に答える 2

3

この問題に出くわした人に役立つ場合: QuickCheck が「あきらめた」場合、( を使用して==>) 前提条件を満たすのが難しすぎるという兆候です。

QuickCheck は単純な拒否サンプリング手法を使用します。事前条件は値の生成に影響しません。QuickCheck は、通常のように一連のランダムな値を生成します。これらが生成された後True、事前条件を介して送信されます。結果がの場合、プロパティはその値でテストされます。の場合False、その値は破棄されます。前提条件が QuickCheck が生成した値のほとんどを拒否する場合、QuickCheck は「あきらめ」ます (統計的に疑わしい合格/不合格の主張をするよりも、完全にあきらめるほうがよいでしょう)。

特に、QuickCheck は、特定の前提条件を満たす値を生成しようとしません。使用している（arbitraryまたはそうでない）ジェネレーターが前提条件に合格する多くの値を生成することを確認するのはあなた次第です。

これがあなたの例でどのように現れているか見てみましょう:

subtypeSanity :: Tree (Type ()) -> Gen Prop
subtypeSanity Node { rootLabel = t, subForest = f } =
  let subtypes = concatMap flatten f
  in (not $ null subtypes) ==> conjoin
     (forAll (elements subtypes) (`subtypeOf` t):(map subtypeSanity f))

は 1 回しか出現し==>ないため、その前提条件 ( not $ null subtypes) を満たすには難しすぎるに違いありません。これは再帰呼び出しによるものです: 空のを持つmap subtypeSanity fものを拒否するだけでなく、(再帰により)に空のsを含むものを拒否し、s を含むsを含むものも拒否します。空の s など。TreesubForestTreesubForestTreesubForestTreesubForestTreesubForestTreesubForest

arbitraryあなたのインスタンスによると、 Trees は有限の深さまでしかネストされていません。最終的には常に空subForestの に到達するため、再帰的な前提条件は常に失敗し、QuickCheck はあきらめます。

于 2015-09-08T08:36:47.910 に答える