haskell - 自动和确定性地测试一个函数的关联性、交换性等

Question

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

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

如果这是不可能的，有没有办法用任何语言自动化它？如果有我感兴趣的 Agda、Coq 或 Prolog 解决方案。

我可以设想一个蛮力解决方案，它检查每个可能的参数组合并且永不终止。但是在这种情况下，“永不终止”是一个不受欢迎的属性。

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 随机选择测试用例。