Gibt es eine Möglichkeit, zwei Funktionen auf Gleichheit zu vergleichen? Zum Beispiel, (λx.2*x) == (λx.x+x)
sollte true zurückgeben, da diese offensichtlich äquivalent sind.
Es ist allgemein bekannt, dass die allgemeine Funktionsgleichheit im Allgemeinen nicht entscheidbar ist. Daher müssen Sie eine Teilmenge des Problems auswählen, an dem Sie interessiert sind. Sie können einige der folgenden Teillösungen in Betracht ziehen:
Dies ist im Allgemeinen nicht zu entscheiden, aber für eine geeignete Teilmenge können Sie es heute tatsächlich effektiv mit SMT-Solvern tun:
$ 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
Weitere Informationen finden Sie unter: https://hackage.haskell.org/package/sbv
Lassen Sie uns zusätzlich zu den praktischen Beispielen in der anderen Antwort die Teilmenge der Funktionen auswählen, die in der typisierten Lambda-Rechnung ausgedrückt werden können. Wir können auch Produkt- und Summentypen zulassen. Obwohl die Überprüfung, ob zwei Funktionen gleich sind, so einfach sein kann wie Anwenden auf eine Variable und Vergleichen der Ergebnisse , können wir die Gleichheitsfunktion innerhalb der Programmiersprache selbst nicht erstellen.
ETA: λProlog ist eine logische Programmiersprache zur Manipulation von Funktionen (typisierte Lambda-Rechnung).
2 Jahre sind vergangen, aber ich möchte dieser Frage eine kleine Bemerkung hinzufügen. Ursprünglich habe ich gefragt, ob es eine Möglichkeit gibt, festzustellen, ob (λx.2*x)
entspricht (λx.x+x)
. Addition und Multiplikation auf dem λ-Kalkül können definiert werden als:
add = (a b c -> (a b (a b c)))
mul = (a b c -> (a (b c)))
Wenn Sie nun die folgenden Begriffe normalisieren:
add_x_x = (λx . (add x x))
mul_x_2 = (mul (λf x . (f (f x)))
Du erhältst:
result = (a b c -> (a b (a b c)))
Für beide Programme. Da ihre normalen Formen gleich sind, sind beide Programme offensichtlich gleich. Während dies im Allgemeinen nicht funktioniert, funktioniert es in der Praxis für viele Begriffe. (λx.(mul 2 (mul 3 x))
und (λx.(mul 6 x))
haben zum Beispiel beide die gleichen Normalformen.
In einer Sprache mit symbolischer Berechnung wie Mathematica:
Oder C # mit einem Computer-Algebra-Bibliothek :
MathObject f(MathObject x) => x + x;
MathObject g(MathObject x) => 2 * x;
{
var x = new Symbol("x");
Console.WriteLine(f(x) == g(x));
}
Oben wird an der Konsole "True" angezeigt.
Die Gleichheit von zwei Funktionen zu beweisen, ist im Allgemeinen unentscheidbar, aber in besonderen Fällen kann man immer noch die Gleichheit der Funktionen beweisen, wie in Ihrer Frage.
Hier ist ein Beispiel für einen Proof in 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
Das Gleiche kann man in einer anderen, abhängig getippten Sprache wie Coq, Agda, Idris tun.
Das Obige ist ein taktischer Stilbeweis. Die eigentliche Definition von foo
(der Beweis), die generiert wird, ist ein ziemlicher Handgriff:
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))))))