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

Question

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

- MaiaVictor

---

你真的需要算术函数吗？还是只是对比较函数感到好奇？如果是后者，可以看一下类型λ演算中的归一化。 - lukstafi

@lukstafi 只是好奇，但我会看一下。 - MaiaVictor

你的连接词"but"放错位置了，应该使用"so"。;-) - lukstafi

@lukstafi 你是对的。 - MaiaVictor

@IvanCastellanos 听起来很不错，直到你想证明两个二进制函数的等价性，突然这40亿个域大小变成了16万亿，而你之前的1分钟测试套件变成了一个需要10000年才能完成的测试套件。 - Daniel Wagner

Answer 1

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

• Presburger算术是一阶逻辑和算术的可判定片段。
• universe包为具有有限定义域的总函数提供函数相等性测试。
• 您可以检查函数在大量输入上是否相等，并将其视为未经测试的输入相等的证据；请查看QuickCheck。
• SMT求解器尽力而为，有时会回答“不知道”而不是“相等”或“不相等”。Hackage上有几个与SMT求解器绑定的工具包；我没有足够的经验建议最好的工具包，但Thomas M. DuBuisson建议使用sbv。
• 有一个有趣的研究领域，关于如何在紧凑的函数上判断函数相等性等问题；这项研究的基础在博客文章Seemingly impossible functional programs中描述。（请注意，紧凑性是一个非常强大且非常微妙的条件！这不是大多数Haskell函数所满足的条件。）
• 如果您知道您的函数是线性的，可以为源空间找到一组基；然后每个函数都有一个唯一的矩阵表示。
• 您可以尝试定义自己的表达式语言，证明此语言的等价性是可判定的，然后将该语言嵌入Haskell。这是最灵活但也最困难的进展方式。

- Daniel Wagner

---

他是不是只是在寻找sbv或quickcheck？使用SBV测试：prove $ \(x::SInt32) -> 2*x .== x + x 的结果是 Q.E.D.。请确认一下。 - Thomas M. DuBuisson

@ThomasM.DuBuisson 好建议！我会把它加入到答案中。 - Daniel Wagner

我实际上正在寻找更深入的问题概述，正如丹尼尔所提供的那样。 - MaiaVictor

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

- alias

Answer 3

除了其他答案中给出的实际例子外，让我们选择可在类型化λ演算中表达的函数子集；我们还可以允许积类型和和类型。虽然检查两个函数是否相等可能只需将它们应用于变量并比较结果，但我们无法在编程语言本身内部构建相等函数。

ETA：λProlog是一种用于操作（类型化λ演算）函数的逻辑编程语言。

- lukstafi

---

你说，“检查两个函数是否相等可以简单地将它们应用于变量并比较结果。”但我很难相信这一点。举个简单的例子，这确实能验证 (\x -> 2*x) == (\x -> x*2) 相等吗？ - Daniel Wagner

"(\x -> 2x) == (\x -> x2)" 这个表达式并不一定成立，它取决于你如何解释 "*" 和 "2"。例如，你可以在某些术语重写系统下将 "==" 定义为恒等式。 - lukstafi

Answer 4

两年过去了，但我想在这个问题上增加一点评论。最初，我的问题是是否有任何方法可以判断(λ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))都具有相同的标准形式。

- MaiaVictor

---

有一种技术叫做 "超级编译"（我建议阅读这篇 论文）。我猜测一个成熟的超级编译器可以统一你的函数，即使它们是通过递归和模式匹配定义的。 - effectfully

@user3237465 提供的链接已经失效。这篇研究论文可以在这里获取：https://www.academia.edu/2718995/Rethinking_supercompilation - Stephane Rolland

已经过去了4年，我想再加一点注释：虽然在这种情况下这个方法可行，但这种情况大多是例外。函数可以以非常不同的方式定义，仍然是等效的，因此手动操纵等式的方式非常有用。 - MaiaVictor

Answer 5

在像Mathematica这样具有符号计算能力的语言中：

或者使用带有 计算机代数库 的 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”。

- dharmatech

---

但是，然而(x \[Function] x + x) == (y \[Function] 2 y)是某些东西，它甚至不尝试。 - user5920214

Answer 6

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

这里是 Lean 中的一个示例证明：

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))))))

- Slavomir Kaslev