Paire de bases de combinateur complète la plus simple pour les expressions plates

Dans l'article de Chris Okasaki « Aplatir les combinateurs: survivre sans parenthèses », il montre que deux combinateurs sont à la fois suffisants et nécessaires comme base pour coder des expressions complètes de Turing sans avoir besoin d'un opérateur d'application ou de parenthèses.

Comparé aux encodages de logique combinatoire de John Trump dans « Calcul lambda binaire et logique combinatoire » par le biais du codage de préfixe S et K combinateurs avec un opérateur d'application, le fait de n'avoir besoin que de deux combinateurs pour des expressions plates augmente la densité du code jusqu'à l'optimalité. La numérotation de Goedel résultante mappe chaque entier à une expression à terme fermé valide et bien formée, contrairement à la plupart des calculs et des esolangs pertinents de longueur de description minimale dont les représentations canoniques permettent généralement la description de programmes syntaxiquement invalides.

Cependant, le codage d'Okasaki était censé être le plus utile dans un mappage à sens unique des termes de calcul lambda aux chaînes de bits, pas nécessairement l'inverse, car les deux combinateurs utilisés dans cette réduction sont relativement complexes lorsqu'ils sont utilisés comme instructions de substitution pratiques.

Quelle est la paire de bases de combinaison complète la plus simple qui ne nécessite pas d'opérateur d'application?

Pour y revenir près d'un an plus tard, j'ai réalisé que j'avais raté certaines recherches critiques avant de poster.

Jot semble correspondre à la facture de ce que je demandais, avec deux combinateurs B & X relativement simples qui peuvent être représentés par une numérotation Goedel compacte.

J'ai simplifié son implémentation de référence avec Python:

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) renvoie la fonction intégrée indiquant le programme représenté par son nombre de Goedel n.

B (équivalent à la multiplication codée par Church) sert la fonction d'application fonctionnelle (parenthèses) et peut isoler les moitiés S / K du combinateur Iota à base unique X.

Il y a quelques propriétés importantes de cette langue que je vole (presque) sans vergogne au site Web de l'inventeur de la langue Chris Barker, vers 2000.

Jot est un langage régulier en syntaxe mais Turing-complet. Vous pouvez voir dans l'implémentation de J (n) que si un langage hôte prend en charge la récursivité de queue, il n'y a pas d'espace de pile requis pour analyser le format du programme de chaîne de bits.

La preuve de l'intégralité de Turing provient également du site de Chris, implémentant la logique combinatoire Turing-complete déjà connue à l'aide des combinateurs S et K:

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

Jot n'a pas d'erreurs de syntaxe, chaque programme étant donné son numéro de Goedel n est un programme valide. C'est probablement l'aspect le plus important de mes propres recherches, car il simplifie non seulement l'analyse de la trivialité, mais devrait également, en théorie, rendre Jot beaucoup plus parcimonieux que tout encodage Turing complet qui doit ignorer les programmes mal formés.

J'ai écrit quelques outils pour «résoudre» par force brute le problème semi-décidable de trouver la complexité de Kolmogorov d'une fonction dans Jot. Il fonctionne en s'appuyant sur le programmeur pour spécifier des exemples de formation très caractéristiques du mappage d'une fonction, puis énumère tous les programmes Jot jusqu'à ce que tous les exemples de formation correspondent, et tente enfin de prouver l'égalité d'une fonction trouvée avec l'implémentation verbeuse d'origine.

Il ne fonctionne actuellement que jusqu'à ~ 40 bits avec mes ressources limitées. J'essaie une réécriture avec un solveur SAT pour apprendre des programmes beaucoup plus grands. Si vous savez comment dérouler les fermetures imbriquées limitées en tant que formule booléenne, veuillez m'aider avec ma nouvelle question .

Maintenant, pour quelques comparaisons intéressantes avec le calcul binaire Lambda de John Tromp, qui est connu pour sa concision, mais qui a le problème d'erreurs de syntaxe possibles. Les programmes suivants ont été générés par mon programme d'apprentissage en quelques secondes.

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

De mes propres expériences, l'hypothèse que Jot conduit à des programmes plus petits se confirme lentement alors que mon programme apprend des fonctions simples, les compose, puis apprend des fonctions plus importantes à partir d'un plafond amélioré.