Einfachstes vollständiges Kombinator-Basenpaar für flache Ausdrücke

In Chris Okasakis Artikel " Abflachen von Kombinatoren: Überleben ohne Klammern " zeigt er, dass zwei Kombinatoren ausreichend und notwendig sind, um Turing-vollständige Ausdrücke zu codieren, ohne dass ein Anwendungsoperator oder Klammern erforderlich sind.

Im Vergleich zu John Trumps Codierungen der kombinatorischen Logik in " Binary Lambda Calculus and Combinatory Logic " durch Präfixcodierung von S- und K-Kombinatoren mit einem Anwendungsoperator erhöht die Notwendigkeit von nur zwei Kombinatoren für flache Ausdrücke die Codedichte auf Optimalität. Die resultierende Goedel-Nummerierung ordnet jede Ganzzahl einem gültigen, wohlgeformten Ausdruck mit geschlossenem Begriff zu, im Gegensatz zu den meisten Kalkülen und relevanten Esolangs mit minimaler Beschreibungslänge, deren kanonische Darstellungen normalerweise Beschreibungen syntaktisch ungültiger Programme ermöglichen.

Die Codierung von Okasaki sollte jedoch bei einer Einweg-Zuordnung von Lambda-Kalkül-Begriffen zu Bitstrings am hilfreichsten sein, nicht unbedingt umgekehrt, da die beiden in dieser Reduktion verwendeten Kombinatoren als praktische Substitutionsanweisungen relativ komplex sind.

Was ist das einfachste vollständige Kombinator-Basenpaar, für das kein Anwendungsoperator erforderlich ist?

Als ich fast ein Jahr später darauf zurückkam, stellte ich fest, dass ich vor dem Posten einige kritische Nachforschungen verpasst hatte.

Jot scheint genau das zu sein, wonach ich gefragt habe, mit zwei relativ einfachen Kombinatoren B & X, die durch eine kompakte Goedel-Nummerierung dargestellt werden können.

Ich habe seine Referenzimplementierung mit Python vereinfacht:

def S(x): return lambda y: lambda z: x(z)(y(z))
def K(x): return lambda y: x
def X(x): return x(S)(K)
def B(x): return lambda y: lambda z: x(y(z))
def I(x): return x
def J(n): return (B if n & 1 else X)(J(n >> 1)) if n else I

J (n) gibt die aufgebaute Funktion zurück, die das Programm bezeichnet, das durch seine Goedel-Nummer n dargestellt wird.

B (entspricht Church-codierter Multiplikation) hat die Funktion der funktionalen Anwendung (Klammern) und kann die S / K-Hälften des Iota-Kombinators X auf Einzelbasis isolieren.

Es gibt einige wichtige Eigenschaften dieser Sprache, die ich (fast) schamlos von der Website des Erfinders der Sprache, Chris Barker, um 2000, stehle.

Jot ist eine reguläre Sprache in der Syntax, aber Turing-vollständig. Sie können der Implementierung von J (n) entnehmen, dass, wenn eine Hostsprache die Schwanzrekursion unterstützt, kein Stapelspeicher erforderlich ist, um das Bitstring-Programmformat zu analysieren.

Der Beweis für die Vollständigkeit von Turing stammt ebenfalls von Chris 'Website, die die bereits bekannte kombinatorische Logik von Turing-vollständig unter Verwendung der S- und K-Kombinatoren implementiert:

K  ==> 11100
S  ==> 11111000
AB ==> 1[A][B], where A & B are arbitrary CL combinators built up from K & S

Jot hat keine Syntaxfehler, jedes Programm mit seiner Goedel-Nummer n ist ein gültiges Programm. Dies ist wahrscheinlich der wichtigste Aspekt meiner eigenen Forschung, da es nicht nur das Parsen auf Trivialität vereinfacht, sondern Jot theoretisch weitaus sparsamer machen sollte als jede Turing-vollständige Codierung, die fehlerhafte Programme überspringen muss.

Ich habe ein paar Werkzeuge geschrieben, um das halbentscheidbare Problem, die Kolmogorov-Komplexität einer Funktion in Jot zu finden, mit brutaler Gewalt zu „lösen“. Es funktioniert, indem es sich darauf verlässt, dass der Programmierer einige sehr charakteristische Trainingsbeispiele für die Zuordnung einer Funktion spezifiziert, dann alle Jot-Programme auflistet, bis alle Trainingsbeispiele übereinstimmen, und schließlich versucht, die Gleichheit einer gefundenen Funktion mit der ursprünglichen ausführlichen Implementierung nachzuweisen.

Es funktioniert derzeit nur für bis zu ~ 40 Bit mit meinen begrenzten Ressourcen. Ich versuche ein Umschreiben mit einem SAT-Solver, um viel größere Programme zu lernen. Wenn Sie wissen, wie Sie begrenzte verschachtelte Abschlüsse als boolesche Formel abrollen können, helfen Sie mir bitte bei meiner neuen Frage .

Nun zu einigen interessanten Vergleichen mit John Tromps Binary Lambda Calculus, der für seine Prägnanz bekannt ist, aber das Problem möglicher Syntaxfehler aufweist. Die folgenden Programme wurden von meinem Lernprogramm in wenigen Sekunden generiert.

Function    Jot       Binary Lambda Calculus   |J| |B|
--------|----------|--------------------------|---|---
SUCC      J(18400)  "000000011100101111011010" 15  24
CHURCH_0  J(154)    "000010"                    8   6
CHURCH_1  J(0)      "00000111010"               1  11
CHURCH_2  J(588826) "0000011100111010"         20  16
IS_ZERO   J(5)      "00010110000000100000110"   3  23
MUL       J(280)    "0000000111100111010"       9  19
EXP       J(18108)  "00000110110"              15  11
S         J(8)      "00000001011110100111010"   4  23
K         J(4)      "0000110"                   3   7
AND       J(16)     "0000010111010000010"       5  19
OR        J(9050)   "00000101110000011010"     14  20

Aus meinen eigenen Experimenten wird die Hypothese, dass Jot zu kleineren Programmen führt, langsam bestätigt, da mein Programm einfache Funktionen lernt, sie komponiert und dann größere Funktionen von einer verbesserten Obergrenze lernt.