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

• Presburger arithmetic是一阶逻辑+算术的可判定片段。
• universe软件包提供有限域的总函数的函数相等性测试。
• 你可以检查你的函数在一大堆输入上是否相等，并将其视为在未测试的输入上相等的证据;查看QuickCheck。
• SMT解算器尽了最大努力，有时响应“不知道”而不是“相等”或“不相等”。Hackage上有几个SMT解算器的绑定;我没有足够的经验来建议一个最好的，但托马斯M。DuBuisson建议sbv。
• 有一条有趣的研究路线是关于决定函数等式和其他关于紧函数的事情;这项研究的基础知识在博客文章Seemingly impossible functional programs中进行了描述。（注意，紧凑性是一个非常强大和非常微妙的条件！它不是大多数Haskell函数都能满足的。
• 如果你知道你的函数是线性的，你就能找到源空间的基;那么每个函数都有唯一的矩阵表示。
• 您可以尝试定义自己的表达式语言，证明该语言的等价性是可判定的，然后将该语言嵌入到Haskell中。这是最灵活但也是最难取得进展的方法。

这通常是不可判定的，但对于合适的子集，您今天确实可以使用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

除了在另一个答案中给出的实际例子之外，让我们挑选在类型lambda演算中可表达的函数子集;我们还可以允许乘积和和类型。虽然检查两个函数是否相等可以像applying them to a variable and comparing results一样简单，但我们不能构建相等函数within the programming language itself。
ETA：λProlog是一种逻辑编程语言，用于操作（类型化lambda演算）函数。

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

在像Mathematica这样的符号计算语言中：

或者C#中的computer algebra library：

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

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

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

上面的命令在控制台上显示“True”。

证明两个函数相等在一般情况下是不可判定的，但在特殊情况下仍然可以证明函数相等，如您的问题。
这里有一个样本证明在精益

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