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.