Klare, intuitive Ableitung des Festkomma-Kombinators (Y-Kombinator)?

cs.stackexchange https://cs.stackexchange.com/questions/9604

Frage

Der Festkommakombinator FIX (auch bekannt als Y-Kombinator) im (untypisierten) Lambda-Kalkül ($\lambda$) ist definiert als:

FIX $ riangleq \lambda f.(\lambda x.f~(\lambda y.x~x~y))~(\lambda x.f~(\lambda y.x~x~y))$

Ich verstehe seinen Zweck und kann die Ausführung seiner Anwendung vollkommen nachvollziehen. Ich würde gerne verstehen, wie man FIX aus ersten Prinzipien ableiten kann.

So weit komme ich, wenn ich versuche, es selbst abzuleiten:

  1. FIX ist eine Funktion:FIX $ riangleq \lambda_\ldots$
  2. FIX benötigt eine weitere Funktion, $f$, um es rekursiv zu machen:FIX $ riangleq \lambda f._\ldots$
  3. Das erste Argument der Funktion $f$ ist der „Name“ der Funktion, der verwendet wird, wenn eine rekursive Anwendung beabsichtigt ist.Daher sollten alle Vorkommen des ersten Arguments von $f$ durch eine Funktion ersetzt werden, und diese Funktion sollte die restlichen Argumente von $f$ erwarten (nehmen wir einfach an, dass $f$ ein Argument akzeptiert):FIX $ riangleq \lambda f._\ldots f~(\lambda y._\ldots y)$

An dieser Stelle weiß ich nicht, wie ich in meiner Argumentation „einen Schritt machen“ soll.Die kleinen Ellipsen zeigen an, wo meinem FIX etwas fehlt (obwohl ich das nur erkennen kann, indem ich es mit dem „echten“ FIX vergleiche).

Ich habe bereits gelesen Typen und Programmiersprachen, die nicht versucht, es direkt abzuleiten, sondern den Leser stattdessen darauf verweist Der kleine Intrigant für eine Ableitung.Ich habe das auch gelesen und seine „Ableitung“ war nicht so hilfreich.Darüber hinaus handelt es sich weniger um eine direkte Ableitung als vielmehr um die Verwendung eines sehr spezifischen Beispiels und einen Ad-hoc-Versuch, eine geeignete rekursive Funktion in $\lambda$ zu schreiben.

War es hilfreich?

Lösung

Ich habe das nirgendwo gelesen, aber ich glaube, $Y$ hätte so abgeleitet werden können:

Nehmen wir eine rekursive Funktion $f$, vielleicht eine Fakultät oder etwas Ähnliches.Informell definieren wir $f$ als Pseudo-Lambda-Term, wobei $f$ in seiner eigenen Definition vorkommt:

$$f = \ldots f \ldots f \ldots $$

Zunächst erkennen wir, dass der rekursive Aufruf als Parameter herausgerechnet werden kann:

$$f = \underbrace{(\lambda r .(\ldots r \ldots r \ldots))}_{M} f$$

Jetzt könnten wir $f$ definieren, wenn wir nur eine Möglichkeit hätten, es als Argument an sich selbst zu übergeben.Das ist natürlich nicht möglich, da wir kein $f$ zur Hand haben.Was wir zur Hand haben, ist $M$.Da $M$ alles enthält, was wir zum Definieren von $f$ benötigen, können wir versuchen, $M$ anstelle von $f$ als Argument zu übergeben und später daraus $f$ zu rekonstruieren.Unser erster Versuch sieht so aus:

$$f = \underbrace{(\lambda r .(\ldots r \ldots r \ldots))}_{M} \underbrace{(\lambda r .(\ldots r \ldots r \ldots))}_{M}$$

Dies ist jedoch nicht ganz richtig.Zuvor wurde $f$ innerhalb von $M$ durch $r$ ersetzt.Aber jetzt übergeben wir stattdessen $M$.Wir müssen irgendwie alle Stellen reparieren, an denen wir $r$ verwenden, damit sie $f$ aus $M$ rekonstruieren.Eigentlich ist das überhaupt nicht schwierig:Da wir nun wissen, dass $f = M M$, ersetzen wir es überall dort, wo wir $r$ verwenden, einfach durch $(r r)$.

$$f = \underbrace{(\lambda r .(\ldots (rr) \ldots (rr) \ldots))}_{M'} \underbrace{(\lambda r .(\ldots (rr) \ldots (rr) \ldots))}_{M'}$$

Diese Lösung ist gut, aber wir mussten $M$ darin ändern.Das ist nicht sehr praktisch.Wir können dies eleganter machen, ohne $M$ ändern zu müssen, indem wir ein weiteres $\lambda$ einführen, das sein auf sich selbst angewendetes Argument an $M$ sendet:Indem wir $M'$ als $\lambda x.M(xx)$ ausdrücken, erhalten wir

$$f = (\lambda x.\underbrace{(\lambda r .(\ldots r \ldots r \ldots))}_{M}(xx)) (\lambda x.\underbrace{(\lambda r .(\ldots r \ldots r \ldots))}_{M}(xx))$$

Wenn $x$ durch $M$ ersetzt wird, wird $r$ durch $MM$ ersetzt, was per Definition gleich $f$ ist.Dies gibt uns eine nicht rekursive Definition von $f$, ausgedrückt als gültiger Lambda-Term!

Der Übergang zu $Y$ ist jetzt einfach.Wir können anstelle von $M$ einen beliebigen Lambda-Term nehmen und diese Prozedur darauf ausführen.Wir können also $M$ herausrechnen und definieren

$$Y = \lambda m .(\lambda x.m(xx)) (\lambda x.m(xx))$$

Tatsächlich reduziert sich $Y M$ auf $f$, wie wir es definiert haben.

Notiz: Ich habe $Y$ so abgeleitet, wie es in der Literatur definiert ist.Der von Ihnen beschriebene Kombinator ist eine Variante von $Y$ für Call-by-Value Sprachen, manchmal auch $Z$ genannt.Sehen dieser Wikipedia-Artikel.

Andere Tipps

Wie Yuval betont hat, gibt es nicht nur einen Festkommaoperator.Es gibt viele davon.Mit anderen Worten: Die Gleichung für den Festkommasatz hat keine einzige Antwort.Sie können den Operator also nicht daraus ableiten.

Es ist, als würde man fragen, wie Menschen $(x,y)=(0,0)$ als Lösung für $x=y$ ableiten.Das tun sie nicht!Die Gleichung hat keine eindeutige Lösung.

Nur für den Fall, dass Sie wissen möchten, wie der erste Fixpunktsatz entdeckt wurde.Lassen Sie mich sagen, dass ich mich auch gefragt habe, wie sie auf die Fixpunkt-/Rekursionstheoreme gekommen sind, als ich sie zum ersten Mal sah.Es scheint so genial.Insbesondere in der Form der Berechenbarkeitstheorie.Anders als Yuval sagt, ist es nicht so, dass die Leute herumgespielt haben, bis sie etwas gefunden haben.Folgendes habe ich gefunden:

Soweit ich mich erinnere, geht der Satz ursprünglich auf S.C. zurück.Kleene.Kleene entwickelte den ursprünglichen Fixpunktsatz, indem er den Beweis der Inkonsistenz von Churchs ursprünglichem Lambda-Kalkül rettete.Churchs ursprünglicher Lambda-Kalkül litt unter einem Russel-Paradoxon.Die modifizierte Lambda-Rechnung vermied das Problem.Kleene untersuchte den Beweis der Inkonsistenz, wahrscheinlich um zu sehen, wie die modifizierte Lambda-Kalküle unter einem ähnlichen Problem leiden würde, und verwandelte den Beweis der Inkonsistenz in einen nützlichen Satz für die modifizierte Lambda-Kalküle.Durch seine Arbeiten zur Äquivalenz der Lambada-Rechnung mit anderen Rechenmodellen (Turingmaschinen, rekursive Funktionen usw.) übertrug er diese auf andere Rechenmodelle.

Wie leitet man den Operator ab, fragen Sie sich vielleicht?So behalte ich es im Hinterkopf.Beim Fixpunktsatz geht es um die Entfernung der Selbstreferenz.

Jeder kennt das Lügnerparadoxon:

Ich bin ein Versteck.

Oder in der sprachlicheren Form:

Dieser Satz ist falsch.

Nun denken die meisten Leute, dass das Problem bei diesem Satz in der Selbstreferenz liegt.Es ist nicht!Der Selbstbezug kann eliminiert werden (das Problem liegt bei der Wahrheit, eine Sprache kann nicht allgemein über die Wahrheit ihrer eigenen Sätze sprechen, siehe Tarskis Undefinierbarkeitssatz der Wahrheit).Das Formular, in dem die Selbstreferenz entfernt wird, lautet wie folgt:

Wenn Sie das folgende Zitat zweimal schreiben, das zweite Mal in Anführungszeichen, ist der resultierende Satz falsch:„Wenn Sie das folgende Zitat zweimal schreiben, das zweite Mal in Anführungszeichen, ist der resultierende Satz falsch:“

Keine Selbstreferenz, wir haben Anweisungen, wie man einen Satz bildet und dann etwas daraus macht.Und der Satz, der konstruiert wird, entspricht den Anweisungen.Beachten Sie, dass wir in der $\lambda$-Kalküle keine Anführungszeichen benötigen, da es keinen Unterschied zwischen Daten und Anweisungen gibt.

Wenn wir das nun analysieren, haben wir $MM$, wobei $Mx$ die Anweisungen sind, um $xx$ zu konstruieren und etwas damit zu tun.

$Mx = f(xx)$

Also ist $M$ $\lambda x.f(xx)$ und wir haben

$MM = (\lambda x.f(xx))(\lambda x.f(xx))$

Dies gilt für ein festes $f$.Wenn Sie daraus einen Operator machen möchten, fügen wir einfach $\lambda f$ hinzu und wir erhalten $Y$:

$Y = \lambda f.(MM) = \lambda f.((\lambda x.f(xx))(\lambda x.f(xx)))$

Deshalb behalte ich einfach das Paradoxon ohne Selbstreferenz im Hinterkopf und das hilft mir zu verstehen, worum es bei $Y$ geht.

Sie müssen also einen Festkommakombinator definieren

fix f = f (fix f)
      = f (f (fix f))
      = f (f (f ... ))

aber ohne explizite Rekursion.Beginnen wir mit dem einfachsten irreduziblen Kombinator

omega = (\x. x x) (\x. x x)
      = (\x. x x) (\x. x x)
      = ...

Der x Dabei wird das erste Lambda wiederholt durch das zweite Lambda ersetzt.Eine einfache Alpha-Konvertierung macht diesen Prozess klarer:

omega =  (\x. x x) (\x. x x)
      =α (\x. x x) (\y. y y)
      =β (\y. y y) (\y. y y)
      =α (\y. y y) (\z. z z)
      =β (\z. z z) (\z. z z)

D.h.Die Variable im ersten Lambda verschwindet immer.Wenn wir also ein hinzufügen f zum ersten Lambda

(\x. f (x x)) (\y. y y)

Die f wird aufspringen

f ((\y. y y) (\y. y y))

Wir haben unsere omega zurück.Es sollte jetzt klar sein, dass, wenn wir eine hinzufügen f zum zweiten Lambda, dann das f wird im ersten Lambda erscheinen und dann wird es auf und ab gehen:

Y f = (\x. x x)     (\x. f (x x))
      (\x. f (x x)) (\x. f (x x)) -- the classical definition of Y

Seit 

(\x. s t) z = s ((\x. t) z), if `x' doesn't occur free in `s'

Wir können den Ausdruck umschreiben als

f ((\x. x x) (\x. f (x x))

Das ist gerecht

f (Y f)

und wir haben unsere Gleichung Y f = f (Y f).Also die Y Kombinator ist im Wesentlichen

  1. das Doppelte f
  2. mach das erste f aufgetaucht
  3. wiederholen

Möglicherweise haben Sie das klassische Beispiel einer Gleichung ohne Normalform gesehen:

$$(\lambda x.xx)(\lambda x.xx) riangleright (\lambda x.xx)(\lambda x.xx)$$

Eine ähnliche Gleichung wird für die allgemeine Rekursion vorgeschlagen:

$$ begin {array} {rr} & ( lambda xr (xx)) ( lambda xr (xx)) ~ triangleright & r (~ ( lambda xr (xx)) ( lambda xr (xx (xx )) ~) triangleright & r (r (~ ( lambda xr)) ( lambda xr (xx)) ~) triangleright & dots end {Array} Tag {a} $$

(A) ist eine Möglichkeit, allgemeine rekursive Gleichungen in der Lambda-Rechnung zu schreiben (über die primitive Rekursivität hinaus).Wie löst man also die Gleichung $Yf = f(Yf)$ ?Setzen Sie $f$ für $R$ in die obige Gleichung ein, um Folgendes zu erhalten:

$$ yf = ( lambda xf (xx)) ( lambda xf (xx)) $$ $$ y = lambda f. ( Lambda xf (xx)) ( lambda xf (xx)) $$

Lizenziert unter: CC-BY-SA mit Zuschreibung
Nicht verbunden mit cs.stackexchange
scroll top