Sequenzierung oder Fortsetzung im reinen Lambda-Kalkül
Ich versuche die folgende Übung hier zu lösen .
Betrachten Sie die folgende Zahlendarstellung. Wie definiere ich den Zusatz?
|0| = λx.x
|1| = λx.λx.x
...
|n + 1| = λx.|n|
Die Nachfolge- und Vorgängeroperatoren sind einfach zu definieren:
Succ n = λx.n
Pred n = n (λx.x)
Eine "offensichtliche" Lösung zum Definieren der Addition besteht darin, die Nachfolgeoperation plus den Test für Null zusammen mit dem Festpunktkombinator zu verwenden, wie (YF) für F unten angegeben (der Operator if und die Booleschen Werte sind wie üblich definiert):
F = λf.(λm n. if (Is0 m) n (Succ (f (Pred m) n))
Die Definition von Is0 scheint jedoch nicht trivial zu sein. Das Problem ist, dass eine Ziffer | N | verbraucht N + 1 Argumente und N Argumente werden einfach dadurch gelöscht. Wenn ich eine solche Funktion anwende, erscheint es daher vernünftig, ihre Anwendung zu beenden, wenn klar wird, dass die Ziffer, z. B. keine Identität ist. Ich denke, es ist eine Art Fortsetzung, aber ich kann mir nicht vorstellen, wie ich es im reinen Lambda-Kalkül modellieren soll. Vielleicht kennt jemand irgendwelche Tipps, die helfen können?
Ein Sequenzierungsoperator kann auch beim Definieren der Addition helfen. Wenn eine Anwendung einer Ziffer | m | wird verzögert, bis eine Ziffer | n | Wird auf alle Argumente angewendet , ist das Ergebnis genau eine Ziffer | n + m | . Vielleicht gibt es eine Variante eines solchen Sequenzierungskombinators im reinen Lambda-Kalkül?
Die Antwort, die vom Autor der Übung gegeben wird, verwendet eine nicht reine Operation (nämlich IsProcedure, die prüft, ob das Argument eine Funktion ist).
UPD: Es ist nicht schwer, ein CPS in Lambda-Kalkül durchzuführen (Details zu CBV finden Sie hier ). Scheint nicht genug zu sein, um das Problem zu lösen.
UPD : Wenn wir eine Version von Quote-Eval- Funktionen für den reinen Lambda-Kalkül haben, muss es eine Funktion geben$eq$, der erkennt, ob die zitierten Lambda-Ausdrücke syntaktisch gleich sind, und wir können Is0 mit konstruieren$eq$. Aber das bezweifle ich$eq$ist definierbar. Der Grund ist "Genericity Lemma" (Barendregt-Buch, Lemma 14.3.24). Wenn wir die Gleichheit mit den angegebenen Lambda-Begriffen testen könnten, dann ($eq$( Zitat $\Omega$) ( Zitat $\lambda x.x$)) würden zurückkehren $False$und die Großzügigkeit impliziert, dass ($eq$( Zitat $\lambda x.x$) ( Zitat $\lambda x.x$)) würde auch zurückkehren $False$. Widerspricht das einer Möglichkeit, ein Zitat im reinen Lambda-Kalkül zu konstruieren ?
Antworten
Ich glaube nicht, dass Sie im reinen Lambda-Kalkül finden werden, wonach Sie suchen. Der Schlüssel ist diese Aussage, die Sie gemacht haben:
Ein Sequenzierungsoperator kann auch beim Definieren der Addition helfen. Wenn eine Anwendung einer Ziffer | m | wird verzögert, bis eine Ziffer | n | wird auf alle seine Argumente angewendet, ...
Nun, Modelle des Lambda-Kalküls sollen sein wie:
$$U \cong U^U$$
Und der Punkt dabei ist, dass jeder semantische Wert$u \in U$kann auf etwas angewendet werden. Es macht also keinen Sinn, über etwas zu sprechen, das "auf alle seine Argumente angewendet wird". Es gibt keinen Wert, der nicht auf weitere Argumente im reinen Lambda-Kalkül angewendet werden kann.
Ich weiß nicht ohne weiteres von einem Modell / Argument, dass diese Darstellung von Naturmenschen eine Implementierung unmöglich macht IsZero, obwohl einige Überlegungen darüber es unwahrscheinlich erscheinen lassen. Wenn es jedoch im reinen Lambda-Kalkül möglich sein soll, muss es semantisch sinnvoll sein und darf nicht auf Begriffen beruhen, die nur syntaktisch sind.
Bearbeiten: Hier ist eine Skizze eines Arguments. Eine Definition von$\mathsf{IsZero}$ muss eventuell reduzieren wie:
$$\mathsf{IsZero}\ n \rightsquigarrow^* n \overrightarrow v$$
Der Grund dafür ist, dass das Anwenden auf eine bestimmte Anzahl von Werten der einzige Mechanismus in der Lambda-Rechnung ist, um tatsächlich zwischen Zahlen zu unterscheiden. Es muss der Fall sein, dass:$$0 \overrightarrow v = \mathsf{true} \\ \mathsf{s}n \overrightarrow v = \mathsf{false}$$ Jedoch für jeden $\overrightarrow v$ es ist der Fall, dass: $$||\overrightarrow v| + k|\overrightarrow v = |k|$$ (wo $|\overrightarrow v|$ ist die Länge von $\overrightarrow v$). Aber nur$|1| = \mathsf{false}$(wenn dies die gewählte Konvention ist). Im Englischen gibt es keine Begrenzung für die Anzahl der Begriffe, die erforderlich sind, um einen Booleschen Wert durch Anwenden einer Ziffer zu erhalten. Es kann also keine geben$\overrightarrow v$ das erfüllt die Gleichungen für alle Ziffern und somit $\mathsf{IsZero}$ kann nicht definiert werden.