Wie modelliere ich die Ausgabe des binären Lambda-Kalküls?

Question

Ich versuche, einen Interpreter für John Tromp's binary lambda calculus

ich Code geschrieben habe, zu schreiben, wie folgt vorgehen:

1. Analysieren Sie den binären Eingang in eine Datenstruktur, die das reguläre untypisierten Lambda-Kalkül
2. Beta-reduce dieser Begriff

Was passiert dann?

• Wie wird die "Ausgabe" interpretiert?
• ist die Ausgabe
  • a) die sich ergebende Term zurück in binäre über die gleiche Codierung übersetzt,
  • oder b) der Bitstrom durch eine Liste von Falsch-termini booleans kodiert?
• (Und was passiert, wenn der Ausgang nicht, eine solche Liste bildet?)

Oder bin ich Missverständnis, wie BLC funktioniert?

Answer 1

Ich würde vorschlagen, http://www.ioccc.org/2012/tromp/hint.html als Ihre primäre Referenz verwenden. Die Wikipedia-Seite ist wahrscheinlich in Ordnung, aber seine ursprünglichen Anmerkungen zu BLC sind ziemlich gut.

Zum Thema Ein- und Ausgang, hat er folgendes zu sagen:

Insbesondere definiert sie eine Universalmaschine, die von einem Eingangsstrom von Bits, die binäre Codierung eines Lambda-Kalkül parst Begriff, gilt das für den Rest der Eingabe (übersetzt in eine faule Liste von Booleans, die eine Standarddarstellung in Lambda-Kalkül haben) und übersetzt das ausgewertete Ergebnis zurück in einen Strom von auszugebenden Bits.