Äquivalenz von zwei Lambda-Ausdrücken für NOT

Ich habe zwei verschiedene Lambda-Ausdrücke für die logische NOT-Funktion gesehen.
Einer von ihnen wendet seinen Parameter nur auf Konstanten trueund falseintern in umgekehrter Reihenfolge an:

$NOT \;\;=\;\; \lambda x.\; x \; \mbox{false}\; \mbox{true} \;\;=\;\; \lambda x. \; x \; (\lambda t.\lambda f.f) \; (\lambda t. \lambda f. t )$

und der andere, der zwei weitere Parameter erfasst, anstatt sie extern an die zurückgegebene Funktion zu übergeben, und auch in umgekehrter Reihenfolge auf sie anwendet : $x$

$NOT \;\;=\;\; \lambda x. \; \lambda t.\lambda f.xft$

von denen der andere etwas einfacher erscheint (und es ist auch einfacher, wenn er binär codiert ist).

Meine Frage lautet also:
Gibt es eine Transformation, die mich von einer dieser Darstellungen zur anderen bringen könnte?

Ich sehe, dass sie "extensiv" gleichwertig sind, dh beide führen zu den gleichen Ergebnissen. Aber ich möchte es irgendwie durch algebraische Transformationen "beweisen", wie zum Beispiel für Alpha-, Beta- und Eta-Konvertierungen. Leider kann mir in diesem Fall nichts davon helfen: Alpha dient nur zum Umbenennen. Beta funktioniert nur für Funktionsaufrufe, aber wir haben hier keinen Funktionsaufruf, der reduziert werden könnte, da im Funktionskörper (allerdings nicht im gesamten Ausdruck) in all diesen Ausdrücken frei ist, bis wir tatsächlich etwas aufrufen . Das naheliegendste scheint das eta zu sein, das sich auf die Erweiterungsäquivalenz und die Weiterleitungsparameter bezieht, aber wenn die Parameter umgekehrt werden, ist es keine einfache Weiterleitung mehr und eta scheint hier nicht mehr zuzutreffen. $x$ NOT

Gibt es noch eine Konvertierungsregel, die mir fehlt?
(Nun, ich denke, sie werden nicht einfach zwei griechische Buchstaben ohne besonderen Grund überspringen, nicht wahr?)

PS: Diese Frage ist eigentlich eine Modellfrage, da es viele andere Definitionen für andere Funktionen gibt, die verschiedene Formen haben, die weitgehend äquivalent zu sein scheinen, sich jedoch in Bezug auf die bekannten Reduktionsregeln völlig unterscheiden. Ich habe das einfachste Beispiel für dieses Problem ausgewählt.

Bearbeiten:
Um besser zu verdeutlichen, was ich wissen möchte, ist hier ein Diagramm, das die Reduktionsschritte für beide Versionen der notFunktion zeigt: http://sasq.comyr.com/Stuff/Lambda/Not.png

Wie Sie sehen können, reduzieren sich beide wirklich auf die gleichen Ergebnisse (im Gegensatz zu dem, was @Jonathan Gallagher unten sagte). Das weiß ich bereits: Sie sind konfluent und daher Church-Rosser-Äquivalent. Was ich jedoch nicht weiß, ist, ob es eine Konvertierungsregel gibt (ähnlich wie Alpha, Beta und Eta), die es mir ermöglichen könnte, eine Form notin die andere umzuwandeln . Dies würde es mir ermöglichen, zumindest sicherzustellen, dass einige andere Funktionen (komplizierter als diese beiden hier) ebenfalls gleichwertig sind, was schwierig sein könnte, wenn sie auf mehr als nur zwei mögliche Antworten reduziert werden können. Ich würde gerne wissen, ob es eine Konvertierungsregel gibt, die es mir ermöglichen könnte, eine Intensionsdefinition in eine andere zu konvertieren, wennZwei Funktionen sind bereits weitgehend gleichwertig (dh sie liefern dieselben Ergebnisse für dieselben Parameter). Oder (was besser wäre), wenn eine Funktion irgendwie in die andere konvertiert werden kann, auch wenn ich nicht weiß, ob sie im Wesentlichen gleichwertig ist.

lambda-calculus SasQ
quelle

Sie können nichts nur mit diesen beiden Codierungen von NOT beweisen, aber das Ergebnis, das Sie möglicherweise beweisen möchten, wäre etwa: ein boolescher Lambda-Term gegeben ist, sollte auf den gleichen Normalwert reduziert werden Form, egal welche Kodierung von NICHT Sie wählen.

f

$f$

N O T f t r u e f a l s e

$NOT\ f\ true\ false$

Tpecatte

Hmm, sooo ... Sie schlagen vor, das Church-Rosser-Theorem zu verwenden, um den Zusammenfluss beider Reduktionen zu zeigen? Aber deutet das nicht darauf hin, dass es sich um eine Transformation handeln könnte? (vielleicht einige, die noch nicht entdeckt wurden)

SasQ

Ich bin mir nicht sicher, ob es sich um eine Transformation handelt. Der Zusammenfluss bedeutet nur, dass die Wahl von nicht wirklich wichtig ist. Es ist dasselbe wie bei Church Integer. Sie können die beiden Parameter austauschen, um Ganzzahlen zu definieren. Beide sind gültig und in gewisser Weise gleichwertig, wenn sie "ausgewertet" werden, aber nicht gleichwertig mit Transformationen.

Tpecatte

Antworten:

Um zu beweisen, dass die beiden NICHT-Formulare im Allgemeinen nicht gleichwertig sind, müssen Sie lediglich einen Begriff finden, der bei jeder Anwendung ein anderes Ergebnis zurückgibt, z.

$NOT1 \; \lambda x.\; x \; \;\;=\;\; (\lambda x. \; x \; (\lambda t.\lambda f.f) \; (\lambda t. \lambda f. t )) \; \lambda x.\; x \;\; =\;\; \lambda x. \; x \;$

$NOT2 \; \lambda x.\; x \; \;\;=\;\; (\lambda x.\lambda t.\lambda f.xft) \; \lambda x.\; x\;\; =\;\; \lambda t.\lambda f. ft \;$

Dansalmo
quelle

-3

Das erste sei nicht not1 und das zweite not2. Dann haben Sie folgendes:

n o t 1 M \to_{β} M f a l s e t r u e

$\mathsf{not1} \, M \to_\beta M \, \mathsf{false} \, \mathsf{true}$ und

n o t 2 M \to_{β} λ t f . M f t \to_{η} λ t . M t \to_{η} M

$\mathsf{not2} \, M \to_\beta \lambda t \, f . M \, f \, t \to_\eta \lambda t . M \, t \to_\eta M$

Nun, wenn wir das annehmen

M = t r u e

$M = \mathsf{true}$ dann würde die obere Reduktion uns falsch geben, während die untere Reduktion uns wahr geben würde - so dass die Identifizierung ein seltsames Ergebnis zu liefern scheint.

Jonathan Gallagher
quelle

Das liegt daran, dass Sie einen Fehler gemacht haben. Soweit ich weiß, kann man das nicht auf diese Weise reduzieren.

n o t 2 M \to_{β} λ t f . M f t

$\mathsf{not2} \, M \to_\beta \lambda t \, f . M \, f \, t$ ist in Ordnung, und dies ist die richtige Normalform, bis Sie wissen

M

$M$ . Das ist aber nicht:

λ t f . M f t \to_{η} λ t . M t

$\lambda t \, f . M \, f \, t \to_\eta \lambda t . M \, t$ ;; Sie können nicht loswerden

λ f

$\lambda f$ weil es nicht der letzte Parameter in der untergeordneten Funktionsanwendung ist. Wenn Sie die auf diese Weise reduzierte Funktion mit denselben Parametern aufrufen, wird sie zurückgegeben

M t

$M t$ , die wiederum für den anderen Parameter (früher) aufgerufen wird

f

$f$ ), was gibt

M t f

$M t f$ nicht

M f t

$M f t$ .

SasQ

Ich glaube du bist falsch. Eta ist eine Neufassung, daher muss es eine Kongruenz sein - geschlossen unter Substitution und Kontext. Dies sollte die angegebene Reduzierung ermöglichen. Ich kann es auch anders machen, wenn du magst. einstellen

S = λ f . M f)

$S = \lambda f . M f)$ . Dann

λ t . S t \to^{η} S

$\lambda t . S t \to^{\eta} S$ und dann wieder,

λ f . M f \to^{η} M

$\lambda f . M f \to^{\eta} M$ .

Jonathan Gallagher

@ JonathanGallagher:

λ t f . M f t

$\lambda t f . M f t$ sollte gelesen werden als

λ t . λ f . ((M f) t)

$\lambda t . \lambda f . ((M f) t)$ und nicht als

λ t . (λ f . (M f)) t

$\lambda t. (\lambda f . (M f)) t$ . Sie haben Ihre Parenheses falsch verstanden, weshalb Sie glauben, dass Sie das durchführen können

η

$\eta$ -die Ermäßigung.

Andrej Bauer

Ah. Aha. Danke für die Abklärung. Meine Antwort ist falsch.

Jonathan Gallagher