有没有办法比较两个函数的相等性？例如，(λx.2*x) == (λx.x+x)应该返回 true，因为它们显然是等价的。
问问题
22836 次
6 回答
128
众所周知，一般函数相等通常是不可判定的，因此您必须选择您感兴趣的问题的一个子集。您可以考虑以下部分解决方案：
- Presburger算术是一阶逻辑+算术的可判定片段。
- Universe包为具有有限域的总函数提供函数相等性测试。
- 您可以检查您的函数在一大堆输入上是否相等，并将其视为未经测试的输入上相等的证据；查看快速检查。
- SMT 求解器尽最大努力，有时会回答“不知道”而不是“相等”或“不相等”。在 Hackage 上有几个与 SMT 求解器的绑定；我没有足够的经验来推荐一个最好的，但 Thomas M. DuBuisson 建议sbv。
- 关于确定函数相等性和其他关于紧凑函数的事情，有一条有趣的研究路线；博客文章“看似不可能的功能程序”中描述了这项研究的基础知识。（请注意，紧凑性是一个非常强大且非常微妙的条件！它不是大多数 Haskell 函数都满足的条件。）
- 如果你知道你的函数是线性的，你可以找到源空间的基础；那么每个函数都有一个唯一的矩阵表示。
- 您可以尝试定义自己的表达语言，证明该语言的等价性是可判定的，然后将该语言嵌入到 Haskell 中。这是最灵活但也是最难取得进展的方式。
于 2013-06-11T14:06:30.660 回答
43
这通常是无法确定的，但是对于一个合适的子集，您今天确实可以使用 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
于 2017-09-13T20:32:05.447 回答
11
除了其他答案中给出的实际示例之外，让我们选择可在类型化 lambda 演算中表达的函数子集；我们还可以允许 product 和 sum 类型。尽管检查两个函数是否相等可以像将它们应用于变量并比较结果一样简单，但我们不能在编程语言本身中构建相等函数。
ETA：λProlog是一种用于操作（类型化 lambda 演算）函数的逻辑编程语言。
于 2013-06-11T18:33:41.003 回答
9
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))两者都具有相同的范式。
于 2015-08-02T20:48:21.263 回答
3
在像 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));
}
上面在控制台上显示“真”。
于 2017-09-14T21:28:22.020 回答
0
证明两个函数相等通常是无法确定的，但在特殊情况下仍然可以证明函数相等，如您的问题。
这是精益的示例证明
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))))))
于 2017-09-15T11:04:10.277 回答