7

isAssociative2 つの引数を持つ別の関数を取り、その関数が連想的かどうかを判断する高階関数を構築することは可能ですか?

同様の質問ですが、交換性などの他のプロパティについても同様です。

これが不可能な場合、任意の言語で自動化する方法はありますか? Agda、Coq、または Prolog ソリューションがあれば、興味があります。

考えられるすべての引数の組み合わせをチェックし、決して終了しないブルート フォース ソリューションを思い描くことができます。しかし、「決して終了しない」は、このコンテキストでは望ましくないプロパティです。

4

2 に答える 2

9

私の頭に浮かぶ最初の解決策は、QuickCheckを使用することです。

quickCheck $ \(x, y, z) -> f x (f y z) == f (f x y) z
quickCheck $ \(x, y) -> f x y == f y x

wherefはテスト中の関数です。結合性も交換性も証明しません。これは、あなたが考えてきたブルート フォース ソリューションを作成する最も簡単な方法です。QuickCheck の利点は、テストされたコードのコーナー ケースとなることが期待されるテストのパラメーターを選択できることです。

isAssociativeあなたが求めている は次のように定義できます

isAssociative
  :: (Arbitrary t, Show t, Eq t) => (t -> t -> t) -> IO ()
isAssociative f = quickCheck $ \(x, y, z) -> f x (f y z) == f (f x y) z

これはIO、QuickCheck がランダムにテスト ケースを選択するためです。

于 2011-12-28T06:53:05.883 に答える
3

Haskell はそのようなことにはあまり適していないと思います。通常、チェックとはまったく逆のことを行います。オブジェクトにいくつかのプロパティがあり、特別な方法で使用できることを宣言します ( Data.Foldableを参照)。システムをプロモートしたい場合があります:

import Control.Parallel
import Data.Monoid

pmconcat :: Monoid a => [a] -> a
pmconcat [x] = x
pmconcat xs = pmconcat (pairs xs) where
    pairs [] = []
    pairs [x] = [x]
    pairs (x0 : x1 : xs') = y `par` (y : ys) where
        y = x0 `mappend` x1
        ys = pairs xs'

data SomeType

associativeSlowFold = undefined :: SomeType -> SomeType -> SomeType

data SlowFold = SlowFoldId
              | SlowFold { getSlowFold :: SomeType }

instance Monoid SlowFold where
    mempty = SlowFoldId
    SlowFoldId `mappend` x = x
    x `mappend` SlowFoldId = x
    x0 `mappend` x1 = SlowFold y where
        y = (getSlowFold x0) `associativeSlowFold` (getSlowFold x1)
    mconcat = pmconcat

証明システムが本当に必要な場合は、あなたが言及した証明アシスタントも参照することをお勧めします。Prolog - は論理言語であり、それにもあまり適していないと思います。しかし、単純なアシスタントを作成するために使用される可能性があります。つまり、結合規則を適用して、より低いレベルでは等価性を導き出すことが不可能であることを確認します。

于 2011-12-28T07:52:56.543 に答える