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

Question

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

Answer 1

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

• Presburger arithmetic 是一阶逻辑+算术的可判定片段。
• universe 包为有限域的所有函数提供函数相等性测试。
• 您可以检查您的函数在一大堆输入上是否相等，并将其视为未经测试的输入上相等的证据；查看QuickCheck。
• SMT 求解器尽最大努力，有时会回答“不知道”而不是“相等”或“不相等”。在 Hackage 上有几个与 SMT 求解器的绑定；我没有足够的经验来推荐一个最好的，但 Thomas M. DuBuisson 建议sbv。
• 关于确定函数相等性和其他关于紧凑函数的事情有一个有趣的研究方向；博客文章Seemingly impossible functional programs 中描述了这项研究的基础知识。 （请注意，紧凑性是一个非常强大且非常微妙的条件！大多数 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 演算中表达的函数子集；我们还可以允许 product 和 sum 类型。虽然检查两个函数是否相等可以像applying them to a variable and comparing results 这样简单，但我们无法构建相等函数within the programming language itself。

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)) 都具有相同的范式。

Answer 5

使用像 Mathematica 这样的符号计算语言：

或者带有computer algebra library的C#：

MathObject f(MathObject x) => x + x;
MathObject g(MathObject x) => 2 * x;

{
    var x = new Symbol("x");

    Console.WriteLine(f(x) == g(x));
}

上面在控制台显示'True'。

Answer 6

证明两个函数相等通常是不可判定的，但在特殊情况下仍然可以证明函数相等，如您的问题。

这是精益的示例证明

def foo : (λ x, 2 * x) = (λ x, x + x) :=
begin
  apply funext, intro x,
  cases x,
  { refl },
  { simp,
    dsimp [has_mul.mul, nat.mul],
    have zz : ∀ a : nat, 0 + a = a := by simp,
    rw zz }
end

你可以在其他依赖类型的语言中做同样的事情，例如 Coq、Agda、Idris。

以上是战术风格的证明。生成的foo（证明）的实际定义是相当多的手写：

def foo : (λ (x : ℕ), 2 * x) = λ (x : ℕ), x + x :=
funext
  (λ (x : ℕ),
     nat.cases_on x (eq.refl (2 * 0))
       (λ (a : ℕ),
          eq.mpr
            (id_locked
               ((λ (a a_1 : ℕ) (e_1 : a = a_1) (a_2 a_3 : ℕ) (e_2 : a_2 = a_3), congr (congr_arg eq e_1) e_2)
                  (2 * nat.succ a)
                  (nat.succ a * 2)
                  (mul_comm 2 (nat.succ a))
                  (nat.succ a + nat.succ a)
                  (nat.succ a + nat.succ a)
                  (eq.refl (nat.succ a + nat.succ a))))
            (id_locked
               (eq.mpr
                  (id_locked
                     (eq.rec (eq.refl (0 + nat.succ a + nat.succ a = nat.succ a + nat.succ a))
                        (eq.mpr
                           (id_locked
                              (eq.trans
                                 (forall_congr_eq
                                    (λ (a : ℕ),
                                       eq.trans
                                         ((λ (a a_1 : ℕ) (e_1 : a = a_1) (a_2 a_3 : ℕ) (e_2 : a_2 = a_3),
                                             congr (congr_arg eq e_1) e_2)
                                            (0 + a)
                                            a
                                            (zero_add a)
                                            a
                                            a
                                            (eq.refl a))
                                         (propext (eq_self_iff_true a))))
                                 (propext (implies_true_iff ℕ))))
                           trivial
                           (nat.succ a))))
                  (eq.refl (nat.succ a + nat.succ a))))))