Lambda-Kalkül durch JavaScript, Teil 3

Dieser Artikel wurde ursprünglich auf 47deg.com am 14. Januar 2021 veröffentlicht.

Wir kommen in dieser Serie über Lambda-Kalküle schnell voran! In Teil 1 haben wir die Grundlagen für die Arbeit mit JavaScript als Lambda-Kalkül gelegt, und in Teil 2 haben wir Boolesche Operatoren und Zahlen zu unserem Repertoire hinzugefügt. Aber seien wir mal ehrlich, die Definition von Addition und Multiplikation war eine Art Zaubertrick. In diesem Beitrag befassen wir uns mit der vertrauteren Technik der Rekursion, die uns zu festen Punkten und schließlich in die Sümpfe der Nichtterminierung führt.

Meine Lieblingsgeschichte über Gauß

Wenn Sie schon einmal einem meiner Anfängervorträge zugehört haben, haben Sie diese Geschichte bestimmt schon gehört, denn ich liebe sie. Es heißt, dass Carl Friedrich Gauß als Kind - nennen wir ihn von nun an "Kleiner Gauß" - ein wenig ungezogen war. Zur Strafe verlangte sein Lehrer von ihm, alle Zahlen von 1 bis 100 zu addieren, was er auch in Windeseile tat. Und wie? indem er eine einfache Formel dafür entwickelte. Habe ich schon erwähnt, dass Gauß wegen seiner weitreichenden Fortschritte in vielen Bereichen der Mathematik als "Prinz der Mathematik" gilt?

Geschichten beiseite, unser Ziel ist es, dem kleinen Gauß bei seiner Bestrafung zu helfen. Nicht indem wir eine Formel entwickeln, sondern indem wir den Computer so programmieren, dass er die Summe ausführt. Wenn wir nicht über Lambda-Kalkül sprechen würden, wäre die Lösung ganz einfach:

const littleGaussHelper = n => n === 0 ? 0 : n + littleGaussHelper(n - 1)

Wir wissen bereits, wie wir einige der Elemente darstellen können, nämlich das Konditional, die Zahl 0 und die Addition. Was uns fehlt, ist eine Möglichkeit, herauszufinden, ob eine Zahl Null ist, und den Vorgänger einer Zahl zu erhalten.

Sind Sie eine Null?

Um uns auf unsere erste Aufgabe zu konzentrieren, wollen wir eine Funktion isZero(n) definieren, die true (unseren kodierten Booleschen Wert) zurückgibt, wenn n gleich Null ist, und andernfalls false. Denken Sie daran, dass Church-Zahlen selbst Funktionen sind. Wie in Teil 2 werden wir herausfinden, welche Argumente unknown_f und unknown_x gegeben werden müssen, um das gewünschte Ergebnis zu erhalten.

const isZero = n => n(unknown_f)(unknown_x)

Wenn n die Zahl zero ist, kollabiert die Definition in unknown_x, da Null sein erstes Argument nicht anwendet.

isZero(zero) = zero(unknown_f)(unknown_x) = unknown_x

Auf der anderen Seite wissen wir, dass isZero(zero) gleich true_ sein sollte, also muss unknownx gleich true sein.

Am Ende von Teil 2 haben wir verstanden, wie eine Kirchenzahl als wiederholte Anwendung einer Funktion betrachtet werden kann. Das heißt, wann immer n ist nicht zero, das Ergebnis von isZero(n) wird die Anwendung von unknownf entweder zu true (der Wert, den wir für unknownx) oder eine andere rekursive Anwendung von unknownf. Und in beiden Fällen muss das Endergebnis false sein. Eine solche Wahl ist die konstant-falsche Funktion . Folglich wird unsere Definition von isZero:

const isZero = n => n(x => false_)(true_)

Diese Denkweise - eine unvollständige Funktion zu betrachten und durch Überprüfung des Ergebnisses für jedes Argument die Definition zu verfeinern - wird Programmberechnung genannt. Graham Hutton ist der absolute Meister dieser Technik. In diesem Video - skillsmatter.com/skillscasts/8491-calculating-correct-compilers - weitet er diese Technik auf die Berechnung eines Compilers aus!

Probleme mit dem Vorgänger

Die Funktion, die n => n - 1 berechnet - in der Regel die Vorgängerfunktion genannt - ist ein ziemliches Monstrum:

const pred = n => (f => x => n(g => h => h(g(f)))(u => x)(u => u)

Warum sie funktioniert und wie man sie ableitet, würde den Fokus auf unsere Aufgabe der Rekursion verlieren; außerdem werden wir bald einfachere Möglichkeiten kennenlernen, mit Zahlen zu arbeiten. Für diejenigen, die sich dafür interessieren, wird die Vorgängerfunktion in dem entsprechenden Wikipedia-Artikel sorgfältig erklärt. Ein wichtiger Punkt ist auf jeden Fall, dass die äußere Anwendung von n nicht direkt die Zahl berechnet, sondern eine Funktion, die dann die Zahl berechnet. Aus diesem Grund sieht es so aus, als hätte n drei Argumente, während es formal nur zwei hat.

Ein bisschen meta sein

Es sieht so aus, als wären wir bereit, unsere Funktion zu schreiben. Erinnern Sie sich, dass in normalem JavaScript littleGaussHelper wie folgt aussieht:

const littleGaussHelper = n => n === 0 ? 0 : n + littleGaussHelper(n - 1)

Die Übersetzung kann viele verschiedene Formen annehmen, je nachdem, wie viel von den eigentlichen Definitionen von if_ und den übrigen Komponenten Sie einbringen möchten. Hier ist eine Möglichkeit:

const littleGaussHelper = n => if_(isZero(n))(zero)(add(n)(littleGaussHelper(pred(n))))

"Erledigt!", höre ich Sie denken. Nicht wirklich, denn hier rufen wir littleGaussHelper von sich aus auf. Und das ist nach unseren Regeln nicht erlaubt.

Aber warum ist littleGaussHelper plötzlich nicht mehr erlaubt, während if, zero, oder pred kein Problem darstellen? Wären wir absolute Puristen, würde auch letzteres nicht akzeptiert werden, da unsere Regeln für den Lambda-Kalkül nur Funktionen x => something und Anwendungen f(something) zulassen. Wir erlauben uns jedoch, die Möglichkeiten von JavaScript als Sprache zu nutzen, um Definitionen aufzuzeichnen und zu ersetzen: Wenn wir zum Beispiel if schreiben, sollten Sie an die erweiterte Version denken, in der if_ durch seine Definition ersetzt wird. Zum Beispiel sollte isZero erweitert werden zu:

const isZero = n => n(x => t => f => f)(t => f => t)

Dieser einfache Mechanismus bricht zusammen, wenn wir eine rekursive Funktion haben, da wir die Ersetzung von Namen durch ihre Definitionen nie beenden würden. Wir müssen einen Weg finden - innerhalb unserer strengen Regeln - die Rekursion in eine nicht-rekursive Form umzuschreiben. Die Sache mit den Definitionen in der Lambda-Kalkulation wird noch subtiler, wenn Sie sich in andere Ecken des Lambda-Würfels mit mächtigen Formen der Typisierung begeben (einfach typisierte Lambda-Kalkulation, System F, abhängige Typen). Das Buch Typentheorie und formale Beweise widmet ein ganzes Kapitel der Diskussion darüber!

Normalerweise sagen wir in dieser Situation, dass JavaScript die Host- oder Makrosprache und Lambda Calculus die Objektsprache ist. Wir sagen auch, dass JavaScript Meta-Programmierfunktionen für Lambda-Kalküle bereitstellt, wobei "Meta" hier "Programmierung der Programme" bedeutet.

Rekursion-als-Funktion

Unerwarteterweise brauchen wir kein neues Element im Lambda-Kalkül, um rekursive Funktionen einzuführen. Stattdessen werden wir eine Funktion fix definieren, die sich um den gesamten Rekursionsmechanismus kümmert (Haskeller erkennen vielleicht die ähnlich benannte Funktion.). Wenn Sie diesen Trick noch nie gesehen haben, macht der letzte Satz vielleicht keinen Sinn: Wie kann sich eine Funktion um eine Rekursion "kümmern"?

Lassen Sie uns noch einmal die Funktion betrachten, die wir implementieren möchten:

const littleGaussHelper = n => if_(isZero(n))(zero)(add(n)(littleGaussHelper(pred(n))))

So sieht es aus, wenn Sie fix verwenden:

const littleGaussHelper = fix(lhg => n => if_(isZero(n))(zero)(add(n)(lhg(pred(n)))))

Das Argument für die Funktion fix erhält ein zusätzliches Argument lhg im Vergleich zum ursprünglichen littleGaussHelper. Wann immer Sie diese Funktion im Körper von fix aufrufen, wird dies schließlich den rekursiven Aufruf darstellen. Aber beachten Sie, dass das Argument für jetzt keine Rekursion mehr hat; alles ist einfach ein Argument für die Funktion. Die Funktion fix ist für die Ausarbeitung der Rekursion verantwortlich; dieser Vorgang wird gewöhnlich als Eingabe des Knotens oder Eingabe der rekursiven Schleife bezeichnet.

Der Y-Kombinator

Hier kommt der Y-Kombinator ins Spiel, ein sehr seltsam aussehender Begriff in der Lambda-Kalkulation. Beachten Sie, dass wir in diesem Fall die untypisierte Natur der Sprache voll ausnutzen, da wir eine Funktion x auf sich selbst anwenden.

const Y = g => (x => g(x(x))) (x => g(x(x)))

Der Y-Kombinator gehört zu einer Familie von Begriffen, die Fixpunkt-Kombinatoren genannt werden. Mathematiker bezeichnen oft diejenigen Werte x einer Funktion f als Fixpunkte, für die x = f(x) gilt. Zum Beispiel sind 0 und 1 Fixpunkte der Funktion x => x * x. Der Y-Kombinator, der auf eine beliebige Funktion f angewendet wird, führt zu einem Fixpunkt derselben Funktion.

Y(f) = (x => f(x(x))) (x => f(x(x)))
     = f ( (x => f(x(x))) (x => f(x(x))) )
     = f ( Y(f) )

Das ist der Clou: Y combinator wendet am Ende f rekursiv an! Y kann also als Definition für fix verwendet werden, nach der wir gesucht haben. Da dies manchmal schwer zu glauben ist, lassen Sie uns littleGaussHelper(two) ausführen:

littleGaussHelper(two)
  = fix(lhg => n => if_(isZero(n))(zero)(add(n)(lhg(pred(n))))) (two)
  // since fix(f) = f(fix(f))
  = (n => if_(isZero(n))(zero)(add(n)(fix(lhg => ...)(pred(n))))) (two)
  = if_(isZero(two))(zero)(add(two)(fix(lhg => ...)(pred(two))))
  = add(two)(fix(lhg => ...)(one))
  // since fix(f) = f(fix(f))
  = add(two)(if_(isZero(one))(zero)(add(one)(fix(lhg => ...)(pred(one)))))
  = add(two)(add(one)(fix(lhg => ...)(zero)))
  // since fix(f) = f(fix(f))
  = add(two)(add(one)(if_(isZero(zero))(zero)(add(zero)(fix(lhg => ...)(pred(zero))))))
  = add(two)(add(one)(zero))

Der nicht enden wollende Begriff

Die Rekursion hat ihre eigenen Tücken: Sie müssen sehr vorsichtig sein, um sicherzustellen, dass jede rekursive Funktion schließlich terminiert. Nicht jede Funktion im (untypisierten) Lambda-Kalkül endet. Ein wichtiges Beispiel heißt Ω und entsteht durch die Spezialisierung von Y auf die Identitätsfunktion:

const Ω = (x => x(x)) (x => x(x))

Eine bestechende Eigenschaft von Ω ist, dass es sich selbst auswertet. Wenn Sie einen Schritt weiter gehen und das Argument (x => x(x)) in der Funktion (x => x(x)) ersetzen, erhalten Sie das gleiche Ergebnis.

Diese Arten von Begriffen sind mit dem Halteproblem . Es kann (mathematisch) bewiesen werden, dass es keinen Algorithmus gibt, der für einen beliebigen Begriff im Lambda-Kalkül entscheidet, ob die Auswertung dieses Begriffs endet oder unendlich oft wiederholt wird. Wir sagen, dass das Problem unentscheidbar ist. Historisch gesehen hat die Tatsache, dass es unentscheidbare Probleme gibt, die Idee eines "universellen Theorem-Entscheiders"(Entscheidungsproblem, wie es gewöhnlich genannt wird) zu Grabe getragen.

Genug für heute

Boolesche Operatoren und Konditionale Operatoren, Zahlen, Wiederholungen und Rekursionen - das sind alles nette Werkzeuge für die Programmierung. Aber um eine schöne Struktur zu erhalten, verwendet man oft Datentypen, und das wäre unser nächstes Ziel: Wie können wir Listen oder Bäume in unserem kleinen Lambda-Kalkül darstellen? Bleiben Sie dran!