Wie werden zwei Funktionen auf Äquivalenz verglichen, wie in (λx.2 * x) == (λx.x + x)?
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:
- Presburger-Arithmetik ist ein entscheidbares Fragment von Logik erster Ordnung + Arithmetik.
- Das niversum -Paket bietet Funktionsgleichheitstests für Gesamtfunktionen mit endlicher Domäne.
- Sie können überprüfen, ob Ihre Funktionen bei einer ganzen Reihe von Eingaben gleich sind, und dies als Beweis für die Gleichheit bei den nicht getesteten Eingaben behandeln. check out QuickCheck .
- SMT-Löser bemühen sich nach besten Kräften und antworten manchmal mit "Weiß nicht" anstelle von "Gleich" oder "Nicht gleich". Es gibt verschiedene Bindungen für SMT-Löser bei Hackage. Ich habe nicht genug Erfahrung, um eine beste vorzuschlagen, aber Thomas M. DuBuisson schlägt vor sbv .
- Es gibt eine Reihe spaßiger Recherchen zur Entscheidung über die Funktionsgleichheit und andere Aspekte für kompakte Funktionen. Die Grundlagen dieser Forschung sind im Blog-Beitrag Scheinbar unmögliche Funktionsprogramme beschrieben. (Beachten Sie, dass die Kompaktheit eine sehr starke und sehr subtile Bedingung ist. Die meisten Haskell-Funktionen erfüllen diese Bedingung nicht.)
- Wenn Sie wissen, dass Ihre Funktionen linear sind, können Sie eine Basis für den Quellraum finden. dann hat jede Funktion eine eindeutige Matrixdarstellung.
- Sie könnten versuchen, Ihre eigene Ausdruckssprache zu definieren, zu beweisen, dass die Äquivalenz für diese Sprache entscheidend ist, und diese Sprache dann in Haskell einbetten. Dies ist der flexibelste, aber auch der schwierigste Weg, um Fortschritte zu erzielen.
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))))))