Как сравнить две функции для эквивалентности, как в (λx.2 * x) = = (λx.x+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

в дополнение к практическим примерам, приведенным в другом ответе, давайте выберем подмножество функций, выражаемых в типизированном лямбда-исчислении; мы также можем разрешить типы произведений и сумм. Хотя проверить, равны ли две функции, можно так же просто, как применение их к переменной и сравнение результатов, мы не можем построить функцию равенства в самом языке программирования.

ETA:λProlog это логический язык программирования для манипулирование (типизированное лямбда-исчисление) функциями.

Прошло 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# с библиотека компьютерной алгебры:

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

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

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

выше отображается 'True' на консоли.

доказательство двух равных функций неразрешимо в целом, но все же можно доказать функциональное равенство в особых случаях, как в вашем вопросе.

вот образец доказательства в 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))))))