7

是否可以构造一个高阶函数isAssociative，它接受另一个有两个参数的函数并确定该函数是否是关联的？

类似的问题，但也适用于其他属性，例如交换性。

如果这是不可能的，有没有办法用任何语言自动化它？如果有我感兴趣的 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

f我们正在测试的函数在哪里。它既不能证明结合性也不能证明交换性；这只是编写您一直在考虑的蛮力解决方案的最简单方法。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 回答