Najprostsza kompletna para bazowa kombinacji dla wyrażeń płaskich

W artykule Chrisa Okasakiego „ Spłaszczające kombinatory: przetrwanie bez nawiasów ” pokazuje, że dwa kombinatory są wystarczające i konieczne jako podstawa do kodowania wyrażeń pełnych Turinga bez potrzeby użycia operatora lub nawiasów.

W porównaniu z kodowaniami kombinatorycznej logiki Johna Trumpa w „ Binary Lambda Calculus and Combinatory Logic ” poprzez kodowanie prefiksów S i K kombinatory z operatorem aplikacji, tylko dwa kombinatory dla wyrażeń płaskich zwiększają gęstość kodu do optymalności. Wynikowa numeracja Goedela odwzorowuje każdą liczbę całkowitą na prawidłowe, dobrze sformułowane wyrażenie zamknięte, w przeciwieństwie do większości esolangów obliczeniowych i o minimalnej długości opisu, których reprezentacje kanoniczne zwykle pozwalają na opis programów niepoprawnych pod względem składniowym.

Jednak kodowanie Okasaki miało być najbardziej pomocne w jednokierunkowym odwzorowaniu wyrażeń rachunku lambda na ciągi bitów, niekoniecznie na odwrót, ponieważ dwa kombinatory używane w tej redukcji są stosunkowo złożone, gdy są stosowane jako praktyczne instrukcje podstawiania.

Jaka jest najprostsza kompletna para bazowa kombinatora, która nie wymaga operatora aplikacji?

Wracając do tego prawie rok później, zdałem sobie sprawę, że przegapiłem kilka krytycznych badań przed opublikowaniem.

Jot wydaje się pasować do tego, o co prosiłem, z dwoma stosunkowo prostymi kombinatorami B & X, które można przedstawić za pomocą zwartej numeracji Goedel.

Uprościłem jego implementację referencyjną za pomocą Pythona:

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) zwraca wbudowaną funkcję oznaczającą program reprezentowany przez jego numer Goedel n.

B (odpowiednik mnożenia zakodowanego w kościele) pełni funkcję aplikacji funkcjonalnej (nawiasy) i może izolować połówki S / K jednoczynnikowego kombinatora Iota X.

Istnieje kilka ważnych właściwości tego języka, które (prawie) bezwstydnie kradnę ze strony wynalazcy języka Chrisa Barkera, około 2000 roku.

Jot jest językiem regularnym pod względem składniowym, ale kompletnym Turinga. Z implementacji J (n) widać, że jeśli język hosta obsługuje rekursję ogona, nie jest wymagane żadne miejsce na stosie do przeanalizowania formatu programu bitstringowego.

Dowód kompletności Turinga pochodzi również ze strony Chrisa, implementując już znaną logikę kombinacyjną Turinga za pomocą kombinatorów S i K:

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

Jot nie ma błędów składniowych, każdy program o numerze Goedel n jest poprawnym programem. Jest to prawdopodobnie najważniejszy aspekt moich własnych badań, ponieważ nie tylko upraszcza parsowanie do trywialności, ale także teoretycznie powinien sprawić, że Jot jest znacznie bardziej oszczędny niż jakiekolwiek kompletne kodowanie Turinga, które musi pomijać zniekształcone programy.

Napisałem kilka narzędzi do „rozwiązania” za pomocą brutalnej siły częściowo rozstrzygalnego problemu znalezienia złożoności funkcji Kołmogorowa w Jot. Działa, polegając na programiście, aby określił niektóre bardzo charakterystyczne przykłady szkolenia mapowania funkcji, a następnie wylicza wszystkie programy Jot, aż wszystkie przykłady szkolenia zostaną dopasowane, a na koniec próbuje udowodnić równość znalezionej funkcji z oryginalną implementacją szczegółową.

Obecnie działa tylko do ~ 40 bitów przy moich ograniczonych zasobach. Próbuję przepisać za pomocą narzędzia SAT, aby nauczyć się znacznie większych programów. Jeśli wiesz, jak rozwinąć zamknięte zagnieżdżone zamknięcia jako formułę logiczną, pomóż mi z moim nowym pytaniem .

Teraz kilka ciekawych porównań z Binary Lambda Calculus Johna Trompa, który jest znany ze zwięzłości, ale ma problem z możliwymi błędami składniowymi. Następujące programy zostały wygenerowane przez mój program do nauki w ciągu kilku sekund.

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

Na podstawie własnych eksperymentów powoli potwierdzana jest hipoteza, że ​​Jot prowadzi do mniejszych programów, ponieważ mój program uczy się prostych funkcji, komponuje je, a następnie uczy się większych funkcji z ulepszonego pułapu.