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

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

23269 次浏览
小开
最佳答案

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

  • Presburger 算法 是一阶逻辑 + 算法的一个可判断的片段。
  • 宇宙软件包为有限域的总函数提供了函数相等性测试。
  • 您可以检查函数在一大堆输入上是否相等，并将其视为未经测试的输入上是否相等的证据; 请检查 快速检查。
  • SMT 解决者尽最大努力，有时回答“不知道”而不是“相等”或“不相等”。有几个绑定到 SMT 解决方案的黑客攻击; 我没有足够的经验来建议一个最好的，但托马斯 M。杜布松建议 (法语)。
  • 关于判断函数相等性和紧凑函数上的其他事情，有一个有趣的研究方向; 这项研究的基础在博客文章 看似不可能的功能性程序中进行了描述。(请注意，紧凑性是一个非常强大和非常微妙的条件！它不是大多数 Haskell 函数所满足的。)
  • 如果知道函数是线性的，就可以找到源空间的基础; 那么每个函数都有唯一的矩阵表示。
  • 你可以尝试定义自己的表达语言，证明这种语言的等价性是可以确定的，然后将这种语言嵌入哈斯克尔。这是最灵活，但也是最困难的方式取得进展。
小开

除了在另一个答案中给出的实际例子外，让我们选择可以用有类型λ演算表示的函数子集，我们还可以允许乘积和和类型。虽然检查两个函数是否相等可以像 将它们应用于变量并比较结果一样简单，但是我们不能构建相等函数 在编程语言本身内部。

预计到达时间: ΛProlog是一种用于操作(有类型λ演算)函数的逻辑编程语言。

小开

两年过去了，但我想对这个问题补充一点意见。最初，我问是否有任何方法来判断 (λ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))都具有相同的标准形式。

小开

这在一般情况下是无法确定的，但是对于一个合适的子集，你确实可以今天使用 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

小开

在 Mathematica 这种有符号计算的语言中:

enter image description here

或者 C # 是 计算机代数库计算机代数库:

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


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


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

以上显示’真’在控制台。

小开

证明两个函数相等在一般情况下是不可判定的，但是在你的问题中的特殊情况下，一个函数仍然可以证明函数相等。

这里有一个精益的样本证明

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

提交答案