是否可以构造更高阶函数isAssociative
它接受另一个有两个参数的函数并确定该函数是否是关联的?
类似的问题,但也适用于其他属性,例如交换性。
如果这是不可能的,有没有办法用任何语言自动化它?如果有我感兴趣的 Agda、Coq 或 Prolog 解决方案。
我可以设想一个蛮力解决方案,它检查每个可能的参数组合并且永不终止。但是在这种情况下,“永不终止”是一个不受欢迎的属性。
最佳答案
我想到的第一个解决方案是使用 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 随机选择测试用例。
关于haskell - 自动和确定性地测试一个函数的关联性、交换性等,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/8652590/