如何比较两个函数的等价性,如(λx.2*x)==(λx.x+ x)？

Question

有没有办法比较两个函数的相等性？例如,(?x.2*x) == (?x.x+x)应该返回true,因为那些显然是等价的.

Answer 1

众所周知,一般的函数相等性一般是不可判定的,因此您必须选择您感兴趣的问题的一个子集.您可以考虑以下部分解决方案:

• Presburger算术是一阶逻辑+算术的可判定片段.
• 在宇宙包提供了功能相等测试与有限域总功能.
• 您可以检查您的函数在一大堆输入上是否相等,并将其视为未经测试输入上相等的证据; 查看 QuickCheck.
• SMT解决方案尽最大努力,有时回应"不知道"而不是"平等"或"不平等".Hackage上的SMT求解器有几种绑定; 我没有足够的经验,建议最好之一,但托马斯M DuBuisson暗示SBV.
• 关于在紧凑函数上决定函数相等性和其他事物,有一个有趣的研究方向; 博客文章看似不可能的功能程序中描述了这项研究的基础知识.(请注意,紧凑性是一个非常强大且非常微妙的条件!它不是大多数Haskell函数满足的.)
• 如果你知道你的函数是线性的,你可以找到源空间的基础; 然后每个函数都有一个唯一的矩阵表示.
• 您可以尝试定义自己的表达式语言,证明该语言的等价性是可判定的,然后将该语言嵌入Haskell中.这是最灵活但也是最困难的进步方式.

Answer 2

这通常是不可判定的,但是对于合适的子集,您今天确实可以使用SMT求解器有效地完成它:

$ ghci
GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
Prelude> :m Data.SBV
Prelude Data.SBV> (\x ->  2 * x) === (\x -> x + x :: SInteger)
Q.E.D.
Prelude Data.SBV> (\x ->  2 * x) === (\x -> 1 + x + x :: SInteger)
Falsifiable. Counter-example:
  s0 = 0 :: Integer

有关详细信息,请参阅:https://hackage.haskell.org/package/sbv

Answer 3

除了在另一个答案中给出的实际例子之外,让我们选择在类型化的lambda演算中可表达的函数子集; 我们还可以允许产品和总和类型.虽然检查两个函数是否相等可以简单到将它们应用于变量并比较结果,但我们无法在编程语言本身内构建相等函数.

ETA:λProlog是一种用于操作(类型化的lambda演算)函数的逻辑编程语言.

Answer 4

2年过去了,但我想对这个问题加一点评论.最初,我问是否有任何方法可以判断是否(?x.2*x)等于(?x.x+x).λ演算的加法和乘法可以定义为:

add = (a b c -> (a b (a b c)))
mul = (a b c -> (a (b c)))

现在,如果您规范化以下术语:

add_x_x = (?x . (add x x))
mul_x_2 = (mul (?f x . (f (f x)))

你得到:

result = (a b c -> (a b (a b c)))

对于这两个项目.由于它们的正常形式相同,因此两个程序显然是相等的.虽然这在一般情况下不起作用,但它在实践中确实适用于许多术语.(?x.(mul 2 (mul 3 x))例如,(?x.(mul 6 x))两者都具有相同的正常形式.