Wie implementiert man eine rekursive Funktion im Lambda-Kalkül mit einer Teilmenge der Clojure-Sprache?

Für strenge Sprachen benötigen Sie anstelle des Y-Kombinators den Z-Kombinator . Es ist die gleiche Grundidee, aber ersetzen (x x) durch (fn [v] (x x) v) , so dass die Selbstreferenz in ein Lambda gewickelt wird, was bedeutet, dass es nur bei Bedarf ausgewertet wird.

Sie müssen auch Ihre Definition von booleschen Werten korrigieren, damit sie in einer strengen Sprache funktionieren: Sie können nicht einfach die zwei Werte übergeben, die Ihnen wichtig sind, und zwischen ihnen auswählen. Stattdessen übergeben Sie es für die Berechnung der beiden Werte, die Ihnen wichtig sind, und rufen Sie die entsprechende Funktion mit einem Dummy-Argument auf. Das heißt, genau wie Sie den Y-Kombinator durch eta-Erweiterung des rekursiven Aufrufs reparieren, reparieren Sie boolesche Werte, indem Sie die beiden Zweige von if und eta eta-reduzieren - reduzieren Sie den boolean selbst (ich bin nicht 100% sicher, dass eta-reduzierend ist der richtige Ausdruck hier).

Beachten Sie, dass beide Zweige des if jetzt mit (fn [_] ...) umschlossen sind und das if selbst mit (... b) umhüllt ist, wobei b ein Wert ist, den ich willkürlich zum Übergeben auswähle; Sie könnten stattdessen zero übergeben oder irgendetwas anderes.

Das Problem, das ich sehe, ist, dass Sie eine starke Verbindung zwischen Ihrem Clojure-Programm und Ihrem Lambda-Kalkül-Programm haben

1. Sie verwenden Clojure-Lambdas, um LC-Lambdas darzustellen
2. Sie verwenden Clojure-Variablen / Definitionen zur Darstellung von LC-Variablen / Definitionen
3. Sie verwenden Clojures Anwendungsmechanismus (Clojures Evaluator) als LC-Anwendungsmechanismus

Sie schreiben also ein Clojure-Programm (kein LC-Programm), das den Auswirkungen des Clojure-Compilers / Evaluators unterliegt - was strict evaluation bedeutet non -Konstant-Raumrichtungsrekursion. Schauen wir uns an:

Als Clojure-Programm, in einer streng evaluierten Umgebung, jeder Zeit nennen wir add2 , werten wir

1. (zero? b) als value1
2. (value1 a) als value2
3. (succ a) als value3
4. (f value2) als value4
5. (pred b) als value5
6. (value2 value4) als value6
7. (value6 value5)

Wir können nun sehen, dass der Aufruf von add2 immer zum Aufruf des Rekursionsmechanismus f führt - natürlich wird das Programm niemals beendet und wir bekommen einen Stack-Überlauf!

Sie haben ein paar Optionen

1. per @ amalloy's Vorschläge, benutze Thunks, um die Auswertung bestimmter Ausdrücke zu verzögern und zwinge sie dann, wenn du bereit bist, die Berechnung fortzusetzen - das denke ich nicht Das wird dir viel beibringen

2. Sie können Clojures loop / recur oder trampoline für Konstanten-Raum-Rekursionen verwenden, um Ihren Y oder Z Kombinator zu implementieren - es gibt hier einen kleinen Haken, weil Sie nur wollen Unterstützung von Single-Parameter-Lambdas, und es wird schwierig (vielleicht unmöglich), dies in einem strengen Evaluator zu tun, der keine Tail-Aufrufe optimiert.

   Ich mache eine Menge dieser Art von Arbeit in JS, weil die meisten JS-Maschinen das gleiche Problem haben; Wenn Sie daran interessiert sind, Homebrew-Workarounds zu sehen, gehen Sie folgendermaßen vor: Wie ersetze ich while-Schleifen mit einer funktionalen Programmieralternative ohne Tail-Call-Optimierung?

3. Schreiben Sie einen tatsächlichen Evaluator - das bedeutet, Sie können die Darstellung Ihres Lambda-Kalkül-Programms von den Datentypen und Verhaltensweisen von Clojure und Clojures Compiler / Evaluator entkoppeln - Sie erhalten wählen wie diese Dinge funktionieren, weil Sie bin derjenige, der den Evaluator schreibt

   Ich habe diese Übung nie in Clojure gemacht, aber ich habe es ein paar Mal in JavaScript gemacht - die Lernerfahrung ist transformativ. Erst letzte Woche schrieb ich Ссылка , das ein normales Ordnungssubstitutionsmodell der Auswertung verwendet. Der Evaluator ist hier nicht stacksicher für große LC-Programme, aber Sie können sehen, dass die Rekursion über Currys Y in Zeile 113 unterstützt wird - er unterstützt die gleiche Rekursionstiefe im LC-Programm, wie die zugrunde liegende JS-Maschine unterstützt. Hier ist ein anderer Evaluator, der memoization und das bekanntere Umgebungsmodell verwendet: Ссылка - erbt auch das Rekursionslimit der zugrunde liegenden JS-Maschine

   Die Rekursion stack-safe ist in JavaScript wirklich schwierig, da ich oben verlinkt habe und (manchmal) beträchtliche Umwandlungen in deinem Code stattfinden müssen, bevor du es stack-safe machen kannst. Es hat mich zwei Monate lang viele schlaflose Nächte gekostet, um dies an einen stack-sicheren, normalen Call-by-Need-Evaluator anzupassen: Ссылка - das ist wie Haskell oder Rackets #lang lazy

   Wie in Clojure, könnte der JavaScript-Code leicht angepasst werden, aber ich weiß nicht genug Clojure, um Ihnen zu zeigen, wie ein sinnvolles Evaluator-Programm aussehen könnte - In dem Buch < a href="https://github.com/sarabander/sicp"> Struktur und Interpretation von Computerprogrammen , (Kapitel 4), die Autoren zeigen Ihnen, wie Sie mit Scheme selbst einen Evaluator für Scheme (ein Lisp) schreiben. Natürlich ist das 10-mal komplizierter als primitiver Lambda-Kalkül, daher liegt es nahe, dass Sie, wenn Sie einen Scheme-Evaluator schreiben können, auch einen LC schreiben können. Dies könnte hilfreicher für Sie sein, da die Codebeispiele eher Clojure

   ähneln

ein Startpunkt

Ich habe ein wenig Clojure für dich studiert und bin dazu gekommen - es ist nur der Anfang eines strengen Evaluators, aber es sollte dir eine Vorstellung davon geben, wie wenig Arbeit es braucht, um einer funktionierenden Lösung ziemlich nahe zu kommen.

Beachten Sie, dass wir fn verwenden, wenn wir eine 'lambda auswerten, aber dieses Detail wird dem Benutzer des Programms nicht angezeigt. Dasselbe gilt für env , dh das env ist nur ein Implementierungsdetail und sollte nicht vom Benutzer berücksichtigt werden.

Um ein totes Pferd zu besiegen, können Sie sehen, dass sowohl der Substitutionsbewerter als auch der umweltbasierte Evaluator zu den entsprechenden Antworten für das gleiche Eingabeprogramm kommen - ich kann nicht genug betonen, wie diese Entscheidungen bis zu Sie - In SICP wechseln die Autoren sogar den Evaluator, um ein einfaches registerbasiertes Modell für das Binden von Variablen und das Aufrufen von Procs zu verwenden. Die Möglichkeiten sind endlos weil wir gewählt haben, die Auswertung zu kontrollieren; alles in Clojure zu schreiben (wie du es ursprünglich getan hast) gibt uns diese Art von Flexibilität nicht.