自动确定测试函数的结合性、交换性等

Question

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

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

如果这是不可能的，有没有办法在任何语言中自动化它?如果有一个Agda, Coq或Prolog解决方案，我感兴趣。

我可以想象一个蛮力解决方案，检查每一个可能的参数组合，永远不会终止。但是"never terminates"在这种情况下是一个不受欢迎的属性。

Answer 1

我想到的第一个解决方案是使用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随机选择测试用例

Answer 2

我猜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

如果你真的想要证明系统，你可能也想看看你提到的那些证明助手。前言-是逻辑语言，我不认为它也很适合。但它可能被用来编写一些简单的助手。即应用结合律，发现在较低的层次上不可能推导出等式。