Как сравнить две функции для эквивалентности, как в (λx.2 * x) == (λx.x + x)?

Ответ 1

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

• Ассемблер пресбергера является разрешимым фрагментом логики первого порядка + арифметика.
• Пакет universe предлагает тесты равенства функций для полных функций с конечным доменом.
• Вы можете проверить, что ваши функции равны по целому набору входных данных и рассматривать это как доказательство равенства на непроверенных входах; проверьте QuickCheck.
• Решения SMT прикладывают максимум усилий, иногда реагируя "не знаю", а не "равно" или "не равно". Существует несколько привязок к решателям SMT в Hackage; У меня недостаточно опыта, чтобы предложить лучший, но Thomas M. DuBuisson предлагает sbv.
• Там интересная линия исследований по решению равенства функций и других вещей на компактных функциях; основы этого исследования описаны в сообщении блога Похоже, что невозможные функциональные программы. (Заметим, что компактность - очень сильное и очень тонкое условие! Это не то, что удовлетворяют большинство функций Хаскелла.)
• Если вы знаете, что ваши функции линейны, вы можете найти основу для исходного пространства; то каждая функция имеет уникальное матричное представление.
• Вы можете попытаться определить свой собственный язык выражения, доказать, что эквивалентность разрешима для этого языка, а затем встроить этот язык в Haskell. Это самый гибкий, но также самый сложный способ добиться прогресса.

Ответ 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

Ответ 3

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

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

Ответ 4

Прошло 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)) оба имеют одинаковые нормальные формы, например.

Ответ 5

На языке с символическим вычислением, таким как Mathematica:

Или С# с библиотекой компьютерных алгебр :

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

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

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

В верхней части экрана отображается "True" на консоли.

Ответ 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))))))