Napisz interpreter dla nietypowego rachunku lambda

45

Wyzwanie polega na napisaniu interpretera dla niepisanego rachunku lambda w jak najmniejszej liczbie znaków. Nietypowy rachunek lambda definiujemy w następujący sposób:

Składnia

Istnieją następujące trzy rodzaje wyrażeń:

  • Wyrażenie lambda ma postać, w (λ x. e)której xmoże być dowolną nazwą zmiennej prawnej i edowolnym wyrażeniem prawnym. Tutaj xjest nazywany parametrem i enazywa ciało funkcji.

    Dla uproszczenia dodajemy dodatkowe ograniczenie, że nie może istnieć zmienna o takiej samej nazwie jak xobecnie w zakresie. A zaczyna być zmienne w zakresie, gdy pojawi się nazwa pomiędzy a .i zatrzymuje się w zakresie w odpowiedni ).

  • Aplikacja funkcji ma formę, (f a)gdzie fi asą wyrażeniami prawnymi. Tutaj fnazywa się funkcję i anazywa się argumentem.
  • Zmienna ma postać xgdzie xjest legalną nazwą zmiennej.

Semantyka

Funkcja jest stosowana przez zastąpienie każdego wystąpienia parametru w treści funkcji argumentem. Bardziej formalnie ekspresja formy ((λ x. e) a), w której xjest nazwą zmienne, ei asą wyrażeniami, ocenia się (lub zmniejsza) do ekspresji e', gdzie e'jest wynikiem zastąpienia w każdym wystąpieniu xw ez a.

Forma normalna jest wyrażeniem, którego nie można dalej oceniać.

Wyzwanie

Twoim zadaniem, jeśli zdecydujesz się to zaakceptować, jest napisanie interpretera, który jako dane wejściowe przyjmuje wyrażenie niepisanego rachunku lambda niezawierającego wolnych zmiennych i generuje jako wynik normalną formę wyrażenia (lub wyrażenie alfa zgodne z nim) . Jeśli wyrażenie nie ma normalnej postaci lub nie jest prawidłowym wyrażeniem, zachowanie jest niezdefiniowane.

Rozwiązanie o najmniejszej liczbie znaków wygrywa.

Kilka uwag:

  • Dane wejściowe można odczytać ze standardowego wejścia lub z nazwy pliku podanej jako argument wiersza poleceń (wystarczy zaimplementować jedno lub drugie - nie oba). Wyjście przechodzi na standardowe wyjście.
  • Alternatywnie możesz zdefiniować funkcję, która pobiera dane wejściowe jako ciąg znaków i zwraca dane wyjściowe jako ciąg znaków.
  • Jeśli występują problemy ze znakami spoza ASCII, możesz użyć znaku odwrotnego ukośnika ( \) zamiast λ.
  • Liczymy liczbę znaków, a nie bajtów, więc nawet jeśli plik źródłowy jest zakodowany jako Unicode λ, liczy się jako jeden znak.
  • Prawne nazwy zmiennych składają się z jednej lub większej liczby małych liter, tj. Znaków od a do z (nie trzeba obsługiwać nazw alfanumerycznych, wielkich liter lub liter spoza alfabetu łacińskiego - chociaż takie postępowanie oczywiście nie unieważnia rozwiązania).
  • Jeśli chodzi o to wyzwanie, nawiasy nie są opcjonalne. Każde wyrażenie lambda i każda aplikacja funkcji będzie otoczona dokładnie jedną parą nawiasów. Żadna nazwa zmiennej nie będzie otoczona nawiasami.
  • Cukier syntaktyczny, taki jak pisanie (λ x y. e)dla (λ x. (λ y. e)), nie musi być obsługiwany.
  • Jeśli do oceny funkcji wymagana jest głębokość rekurencji większa niż 100, zachowanie jest niezdefiniowane. To powinno być wystarczająco niskie, aby można je było wdrożyć bez optymalizacji we wszystkich językach, a jednocześnie wystarczająco duże, aby móc wykonywać większość wyrażeń.
  • Możesz także założyć, że odstępy będą takie jak w przykładach, tj. Bez spacji na początku i na końcu danych wejściowych lub przed a λlub .dokładnie jedną spacją po a .oraz między funkcją i jej argumentem a po a λ.

Przykładowe wejście i wyjście

  • Wejście: ((λ x. x) (λ y. (λ z. z)))

    Wynik: (λ y. (λ z. z))

  • Wejście: (λ x. ((λ y. y) x))

    Wynik: (λ x. x)

  • Wejście: ((λ x. (λ y. x)) (λ a. a))

    Wynik: (λ y. (λ a. a))

  • Wejście: (((λ x. (λ y. x)) (λ a. a)) (λ b. b))

    Wynik: (λ a. a)

  • Wejście: ((λ x. (λ y. y)) (λ a. a))

    Wynik: (λ y. y)

  • Wejście: (((λ x. (λ y. y)) (λ a. a)) (λ b. b))

    Wynik: (λ b. b)

  • Wejście: ((λx. (x x)) (λx. (x x)))

    Dane wyjściowe: cokolwiek (jest to przykład wyrażenia, które nie ma normalnej postaci)

  • Wejście: (((λ x. (λ y. x)) (λ a. a)) ((λx. (x x)) (λx. (x x))))

    Dane wyjściowe: (λ a. a)(Jest to przykład wyrażenia, które nie normalizuje się, jeśli oceniasz argumenty przed wywołaniem funkcji, i niestety przykład, dla którego moje próbowane rozwiązanie kończy się niepowodzeniem)

  • Wejście: ((λ a. (λ b. (a (a (a b))))) (λ c. (λ d. (c (c d)))))

    Dane wyjściowe: `(λ a. (λ b. (a (a (a (a (a (a (a (a b)))))))))) oblicza 2 ^ 3 w liczbach kościelnych.

sepp2k
źródło
1
Czy możemy założyć, że do łańcucha nie będzie wstawiana ani dołączana biała spacja, a biała spacja jest inna niż podano w przykładowym danych wejściowych? Oznacza to, że brak białych znaków między nawiasami, między kropką a nazwą parametru, a inne wystąpienia białych znaków to dokładnie 1 spacja.
JPvdMerwe,
@JPvdMerwe: Tak, dobra uwaga, możesz to założyć.
sepp2k
Czy są jakieś wolne zmienne? Mam na myśli zmienne niezwiązane przez lambda jak w wyrażeniu (\y. a).
FUZxxl,
3
Wiele lub wszystkie rozwiązania tutaj nie wdrażają substytucji pozwalającej uniknąć przechwytywania! Należy dodać przypadek testowy, taki jak ((λ f. (Λ x. (Fx))) (λ y. (Λ x. Y))), który powinien mieć wartość (λ x. (Λ z. X)), nie (λ x. (λ x. x)).
Anders Kaseorg
1
@ sepp2k Czy zastanawiałeś się nad dodaniem ((λ f. (λ x. (fx)))) (λ y. (λ x. y))) jako przypadku testowego i nie akceptujesz bieżącej odpowiedzi, która nieprawidłowo daje wynik (λ x. (λ x. x))?
Anders Kaseorg,

Odpowiedzi:

36

Najnowszy:

Zmniejszyłem go do 644 znaków , połączyłem części cEll w cOpy i Par; buforowane wywołania do komórki i cdr do tymczasowych zmiennych lokalnych i przeniesiono te zmienne lokalne do globalnych w funkcjach „terminalnych” (tj. nierekurencyjnych). Ponadto stałe dziesiętne są krótsze niż literały znakowe, a ten paskudny biznes ...

atom(x){
    return m[x]>>5==3;
}

... poprawnie identyfikuje małe litery (zakładając ASCII), ale akceptuje także dowolne z `{|} ~. (Ta sama obserwacja na temat ASCII znajduje się w tym doskonałym wideo o UTF-8 .)

Etola: |

#include<stdio.h>
#include<string.h>
#define X m[x]
#define R return
char*n,*m;int u,w,d;C(x,y){w=n-m;n+=sprintf(n,y?"(%s %s)":"(%s)",&X,m+y)+1;R w;}T(x){R X>>5==3;}
L(x){R X==92;}O(x,j){w=n-m;memcpy(n,&X,j);n+=j;*n++=0;R w;}E(x){X==' '?++x:0;R
X==41?0:L(x)?O(x,4):P(x);}P(x){d=0,w=x;do{X==40?d++:X==41?d--:0;++x;}while(d>0);R
O(w,x-w);}D(x){u=E(x+1);R u?E(x+1+strlen(m+u)):0;}V(x){int a=E(x+1),b=D(x);R
T(x)|T(a)?x:L(a)?C(a,V(b)):L(E(a+1))?V(S(V(b),E(a+3),D(a))):V(C(V(a),b?V(b):0));}S(w,y,x){R
T(x)?(X==m[y]?w:x):C(L(w+1)?E(x+1):S(w,y,E(x+1)),D(x)?S(w,y,D(x)):0);}
Y(char*s){n+=strlen(s=strcpy(n,s))+1;printf("%s\n%s\n\n",s,m+V(s-m));n=m+1;}

char*s[]={
"((\\ a. a) (b))",
"((\\ x. x) (\\ y. (\\ z. z)))",
"(\\ x. ((\\ y. y) x))",
"(((\\ x. (\\ y. x)) (\\ a. a)) (\\ b. b))",
"((\\ x. (\\ y. y)) (\\ a. a))",
"(((\\ x. (\\ y. y)) (\\ a. a)) (\\ b. b))",
"((\\x. (x x)) (\\x. (x x)))",0};
#include<unistd.h>
main(){char**k;n=m=sbrk(4096);*n++=0;for(k=s;*k;k++)Y(*k);R 0;}

Wcześniej:

Czy mogę dostać kilka głosów za wysiłek? Pracowałem nad tym dniem i nocą przez tydzień. Wykopałem oryginalny artykuł McCarthy'ego i byłem nękany przez błąd w samym dokumencie, dopóki nie przeczytałem dodatku do The Roots of Lisp Paula Grahama . Byłem tak rozproszony, że zamknąłem się z domu, a potem zupełnie zapomniałem, aż wróciłem do domu tej nocy o 12:30 (trochę późno, żeby zadzwonić do kierownika budowy, który mieszka daleko w hrabstwie), i musiałem spędzić noc u babci (rąbałam, aż bateria mojego laptopa wyczerpała się).

A po tym wszystkim nie jest nawet blisko zwycięskiego wejścia!

Nie jestem pewien, jak to skrócić; i użyłem wszystkich brudnych sztuczek, o których mogłem myśleć! Może nie da się tego zrobić w C.

Z pewną hojnością w liczeniu (pierwsza część bierze ciąg i wypisuje wynik), to 778 770 709 694 znaków. Ale żeby był samodzielny, musi mieć to sbrkwezwanie. Do obsługi bardziej skomplikowanych wyrażeń potrzebny jest także signalmoduł obsługi. I oczywiście nie można go przekształcić w moduł z dowolnym kodem, który próbuje użyć malloc.

Niestety, oto jest:

#include<stdio.h>
#include<string.h>
#define K(j) strncpy(n,m+x,j);n+=j;goto N;
#define R return
#define X m[x]
#define L =='\\'
char*m,*n;T(x){R islower(X);}V(x){int a=E(x+1);R
T(x)?x:T(a)?x:m[a]L?C(a,V(D(x))):m[E(a+1)]L?V(S(V(D(x)),E(a+3),D(a))):V(C(V(a),D(x)?V(D(x)):0));}
C(x,y){char*t=n;sprintf(n,y?"(%s %s)":"(%s)",m+x,m+y);n+=strlen(n)+1;R
t-m;}Y(char*s){char*t=strcpy(n,s);n+=strlen(n)+1;printf("%s=>%s\n",s,m+V(t-m));n=m+1;}S(x,y,z){R
T(z)?(m[z]==m[y]?x:z):C(m[z+1]L?E(z+1):S(x,y,E(z+1)),D(z)?S(x,y,D(z)):0);}D(x){R
E(x+1)?E(x+strlen(m+E(x+1))+1):0;}E(x){char*t=n,d=0;if(X==' ')++x;if(T(x)){K(1)}if(X
L){K(4)}do{d=X?(X=='('?d+1:(X==')'?d-1:d)):0;*n++=m[x++];}while(d);N:*n++=0;R t-m;}

char*samp[]={
    "a","a","b","b",
    "((\\ a. a) (b))", "(b)",
    "((\\ x. x) (\\ y. (\\ z. z)))", "(\\ y. (\\ z. z))",
    "(\\ x. ((\\ y. y) x))", "(\\ x. x)",
    "(((\\ x. (\\ y. x)) (\\ a. a)) (\\ b. b))", "(\\ a. a)",
    "((\\ x. (\\ y. y)) (\\ a. a))", "(\\ y. y)",
    "(((\\ x. (\\ y. y)) (\\ a. a)) (\\ b. b))", "(\\ b. b)",
    "((\\x. (x x)) (\\x. (x x)))", "undef",
    NULL};
#include<unistd.h>

unsigned sz;
#include<signal.h>
void fix(x){signal(SIGSEGV,fix);brk(m+(sz*=2));}
main(){
    char**t;
    signal(SIGSEGV,fix);
    m=n=sbrk(sz=10*getpagesize());
    *n++=0;
    for(t=samp;*t;t+=2){
        Y(*t);
        printf("s.b. => %s\n\n", t[1]);
    }
    return 0;
}

Oto blok tuż przed ostatecznymi obniżkami. Sztuczki tutaj to kursory liczb całkowitych zamiast wskaźników (wykorzystujące zachowanie „domyślnej int”) oraz użycie „pamięci scratch”: char*njest to wskaźnik „nowy” lub „następny” w wolnej przestrzeni. Ale czasami zapisuję ciąg do pamięci, a następnie wywołuję strlen i inkrementację n; efektywnie wykorzystując pamięć, a następnie przydzielając ją, po łatwiejszym obliczeniu rozmiaru. Widać, że jest to prawie prosto z artykułu McCarthy'ego, z wyjątkiem cell()interfejsów między funkcjami a ciągiem reprezentacji danych.

#include<stdio.h>
#include<string.h>
char*m,*n;  //memory_base, memory_next
atom(x){  // x is an atom if it is a cursor to a lowercase alpha char.
    return x?(islower(m[x])?m[x]:0):0;
}
eq(x,y){  // x and y are equal if they are both atoms, the same atom.
    return x&&y&&atom(x)==atom(y);
}
cell(x){  // return a copy of the list-string by cursor, by parsing
    char*t=n,d=0;
    if(!x||!m[x])
        return 0;
    if(m[x]==' ')
        ++x;
    if(atom(x)){
        *n++=m[x];
        *n++=0;
        return(n-m)-2;
    }
    if(m[x]=='\\'){  // our lambda symbol
        memcpy(n,m+x,4);
        n+=4;
        *n++=0;
        return(n-m)-5;
    }
    do{  // um ...
        d=m[x]?(m[x]=='('?d+1:(m[x]==')'?d-1:d)):0;
        *n++=m[x++];
    }while(d);
    *n++=0;
    return t-m;
}
car(x){  // return (copy of) first element
    return x?cell(x+1):0;
}
cdr(x){  // return (copy of) rest of list
    return car(x)?cell(x+strlen(m+car(x))+1):0;
}
cons(x,y){  // return new list containing first x and rest y
    char*t=n;
    return x?(sprintf(n,y?"(%s %s)":"(%s)",m+x,m+y),n+=strlen(n)+1,t-m):0;
}
subst(x,y,z){  // substitute x for z in y
    if(!x||!y||!z)
        return 0;
    return atom(z)? (eq(z,y)?x:z):
        cons(m[z+1]=='\\'?car(z):
        subst(x,y,car(z)),cdr(z)?subst(x,y,cdr(z)):0);
}
eval(x){  // evaluate a lambda expression
    int a;
    return atom(x)?x:
        atom(a=car(x))?x:
        m[a]=='\\'?cons(a,eval(cdr(x))):
        m[car(a)]=='\\'?eval(subst(eval(cdr(x)),cell(a+3),cdr(a))):
        eval( cons(eval(a),cdr(x)?eval(cdr(x)):0));
}
try(char*s){  // handler
    char*t=strcpy(n,s);
    n+=strlen(n)+1;
    printf("input: %s\n", s);
    printf("eval => %s\n", m+eval(t-m));
    n=m+1;
}
luser droog
źródło
1
Znalazłem jeszcze kilka sztuczek, aby uratować jedną lub dwie postaci, ale nic radykalnego. sprintf(n,...);n+=strlen(n)+1;jest lepszy niż n+=sprintf(n,...)+1;Odwracanie składni tablicy x[m]zamiast m[x]zezwalam na zastąpienie wszystkich pośrednich makrami „postfiksowymi” #define M [m]... x Mco oszczędza 1 znak i daje „wolny” podział linii, ponieważ białe znaki są potrzebne do oddzielenia tokenów.
luser droog
Wygląda na to, że istnieją pewne podobieństwa do tego i jar.2 xlisp 4.0 z IOCCC 1989 .
luser droog
Próbowałem rozszerzyć to na pełniejszego interpretera Lisp .
luser droog
Skomentowany kod // um ...przechodzi przez ciąg i zlicza nawiasy, aż znajdzie pasujące ścisłe pareny na prawidłowym poziomie zagnieżdżenia.
luser droog
1
To niepoprawnie ocenia ((\ f. (\ X. (Fx))) (\ y. (\ X. Y))) do (\ x. (Fx)).
Anders Kaseorg
22

Binary Lambda Calculus 186

Program pokazany na zrzucie szesnastkowym poniżej

00000000  18 18 18 18 18 18 44 45  1a 10 18 18 45 7f fb cf  |......DE....E...|
00000010  f0 b9 fe 00 78 7f 0b 6f  cf f8 7f c0 0b 9f de 7e  |....x..o.......~|
00000020  f2 cf e1 b0 bf e1 ff 0e  6f 79 ff d3 40 f3 a4 46  |[email protected]|
00000030  87 34 0a a8 d0 80 2b 0b  ff 78 16 ff fe 16 fc 2d  |.4....+..x.....-|
00000040  ff ff fc ab ff 06 55 1a  00 58 57 ef 81 15 bf bf  |......U..XW.....|
00000050  0b 6f 02 fd 60 7e 16 f7  3d 11 7f 3f 00 df fb c0  |.o..`~..=..?....|
00000060  bf f9 7e f8 85 5f e0 60  df 70 b7 ff ff e5 5f f0  |..~.._.`.p...._.|
00000070  30 30 6f dd 80 5b b3 41  be 85 bf ff ca a3 42 0a  |00o..[.A......B.|
00000080  c2 bc c0 37 83 00 c0 3c  2b ff 9f f5 10 22 bc 03  |...7...<+...."..|
00000090  3d f0 71 95 f6 57 d0 60  18 05 df ef c0 30 0b bf  |=.q..W.`.....0..|
000000a0  7f 01 9a c1 70 2e 80 5b  ff e7 c2 df fe e1 15 55  |....p..[.......U|
000000b0  75 55 41 82 0a 20 28 29  5c 61                    |uUA.. ()\a|
000000ba

nie akceptuje całkowicie proponowanego formatu. Raczej oczekuje terminu lambda w formacie binarnego rachunku lambda (blc). Jednak pokazuje każdy krok w normalnej redukcji formy, używając minimalnych nawiasów.

Przykład: obliczenie 2 ^ 3 cyframi kościelnymi

Zapisz powyższy zrzut heksowy za pomocą xxd -r> symbolic.Blc

Weź interpretera blc ze strony http://tromp.github.io/cl/uni.c

cc -O2 -DM=0x100000 -m32 -std=c99 uni.c -o uni
echo -n "010000011100111001110100000011100111010" > threetwo.blc
cat symbolic.Blc threetwo.blc | ./uni
(\a \b a (a (a b))) (\a \b a (a b))
\a (\b \c b (b c)) ((\b \c b (b c)) ((\b \c b (b c)) a))
\a \b (\c \d c (c d)) ((\c \d c (c d)) a) ((\c \d c (c d)) ((\c \d c (c d)) a) b)
\a \b (\c (\d \e d (d e)) a ((\d \e d (d e)) a c)) ((\c \d c (c d)) ((\c \d c (c d)) a) b)
\a \b (\c \d c (c d)) a ((\c \d c (c d)) a ((\c \d c (c d)) ((\c \d c (c d)) a) b))
\a \b (\c a (a c)) ((\c \d c (c d)) a ((\c \d c (c d)) ((\c \d c (c d)) a) b))
\a \b a (a ((\c \d c (c d)) a ((\c \d c (c d)) ((\c \d c (c d)) a) b)))
\a \b a (a ((\c a (a c)) ((\c \d c (c d)) ((\c \d c (c d)) a) b)))
\a \b a (a (a (a ((\c \d c (c d)) ((\c \d c (c d)) a) b))))
\a \b a (a (a (a ((\c (\d \e d (d e)) a ((\d \e d (d e)) a c)) b))))
\a \b a (a (a (a ((\c \d c (c d)) a ((\c \d c (c d)) a b)))))
\a \b a (a (a (a ((\c a (a c)) ((\c \d c (c d)) a b)))))
\a \b a (a (a (a (a (a ((\c \d c (c d)) a b))))))
\a \b a (a (a (a (a (a ((\c a (a c)) b))))))
\a \b a (a (a (a (a (a (a (a b)))))))

Ponieważ zrzut heksowy jest raczej nieczytelny, tutaj jest wersja „zdemontowana”

@10\\@10\\@10\\@10\\@10\\@10\@\@\@\@@\@1010\@\\\@10\\@10\@\@@@1111111111101
1110@11111110\@@110@11111110\\\\@1110\@1111110\@@101101111110@111111110\@111
111110\\\\@@110@111111011110@11111011110@@10@1111110\@10110\@@111111110\@111
111110\@110@101111011110@1111111111010@1010\\@1110@11010@\@\@1010\@110@1010\
\@@@@@\@1010\@\\\\@@@10\@@111111111011110\\@@101111111111111110\@@101111110\
@@10111111111111111111111110@@@@1111111110\\110@@@@\@1010\\\\@@10\@@@1111101
11110\\@\@@@10111111101111110\@@1011011110\\@@11111010110\\@111110\@@1011110
1110@111010\10\1011111110@111110\\\@101111111111011110\\@@11111111110@@11111
0111110\10\@@@@11111110\\@10\\1101111101110\@@1011111111111111111111110@@@@1
11111110\\@10\\@10\\11011111101110110\\\@@101110110@1010\\11011111010\@@1011
111111111111110@@@@\@1010\@\\@@@10\@@@1110@10\\\@1011110\\110\\\@10\\\@1110\
@@@11111111110@1111111101010\10\\@\@@@1110\\\@10@1110111110\\1110\110@@@1111
0110@@@1111010\\110\\\@10\\\@@1101111111101111110\\\@10\\\@@1101111110111111
10\\\110@1010110\\101110\\@@11010\\\@@1011111111111110@11110\@@1011111111111
101110\@\@@@@@@@@11010101010101010\\110\\10\\1010\10\\\1010\\1010@@@110\110\
@

zamiana 00 (lambda) na \ i 01 (aplikacja) na @ Teraz jest prawie tak czytelna, jak pieprzenie mózgu :-)

Zobacz także http://www.ioccc.org/2012/tromp/hint.html

John Tromp
źródło
7
BLC po prostu używa alfabetu binarnego. 00 to lambda, 01 to aplikacja, a 1 ^ {n} 0 to zmienna jednostka. Kompilacja nie jest wymagana.
John Tromp,
3
Skąd bierze się współczynnik x3? Właściwie podnosisz rację w tym, że języki o mniejszych źródłach alfabetu, takie jak BF, są karane. Dla uczciwego porównania wszystkie rozmiary powinny być wyrażone w bitach, a znaki BF przyjmują tylko 3 bity każdy. Większość innych języków potrzebuje 7 bitów do ASCII, niektóre używają wszystkich 8.
John Tromp
1
BTW +1 To jest cholernie fajne!
luser droog,
1
Jeśli frranran w frranran jest akceptowalny, nie rozumiem, dlaczego miałby to być w ogóle problem. Nie możesz tego przeczytać? Chcesz? Uczyć się!
luser droog,
1
Co trzeba zrobić, aby odczytał rzeczywisty format wejściowy? Myślę, że tam tracisz potencjalne głosy poparcia.
luser droog
14

Haskell, 342 323 317 305 znaków

W chwili pisania tego tekstu jest to jedyne rozwiązanie, które ocenia ((λ f. (Λ x. (Fx)))) (λ y. (Λ x. Y))) do prawidłowego wyniku (λ x. (Λ z. x)) zamiast (λ x. (λ x. x)). Prawidłowa implementacja rachunku lambda wymaga podstawienia unikającego przechwytywania , nawet w ramach uproszczenia tego problemu, że żadna zmienna nie cienia innej zmiennej w swoim zakresie. (Mój program działa nawet bez tej gwarancji).

data T=T{a::T->T,(%)::ShowS}
i d=T(i. \x v->'(':d v++' ':x%v++")")d
l f=f`T`\v->"(λ "++v++". "++f(i(\_->v))%('x':v)++")"
(?)=q.lex
q[(v,s)]k|v/="("=k(maybe T{}id.lookup v)s|'λ':u<-s,[(w,_:t)]<-lex u=t? \b->k(\e->l$b.(:e).(,)w).tail|0<1=s? \f->(?(.tail).k. \x z->f z`a`x z)
main=interact(? \f->(f[]%"x"++))

Uwagi:

  • Działa to w GHC 7.0, zgodnie z wymaganiami, ponieważ to wyzwanie zostało ustawione w styczniu 2011 roku. Byłbym o 13 znaków krótszy, gdyby pozwolono mi założyć GHC 7.10.

Wersja bez golfa z dokumentacją.

Anders Kaseorg
źródło
twój prog w ideone haskell kompilator do wejścia ((\ x. x) (\ y. (\ z. z))) zwraca „błąd czasu wykonania” nawet w ((\\ x. x) (\\ y. ( \\ z. z))) ... co to znaczy „lex” w Haskell?
RosLuP
2
@RosLuP Mój program akceptuje λ, a nie \.
Anders Kaseorg,
wpisz ten imput ((λ x. x) (λ y. (λ z. z))) w ideone.com return: Czas błędu czasu wykonania: 0 pamięć: 4876 sygnał: -1
RosLuP
1
@RosLuP Ideone wydaje się mieć zepsutą obsługę Unicode. Wypróbuj wiersz poleceń lub inny internetowy tłumacz (działa na przykład w Rextester ).
Anders Kaseorg,
2
@codeshot Autor pytania skomentował już, że ((λ f. (λ x. (fx)))) (λ y. (λ x. y))) ↦ (λ x. (λ z. x)) jest poprawne dla ten problem (tak jak prawdziwy rachunek lambda).
Anders Kaseorg
13

Python - 321 320

Oto moja (naprawiona) próba:

l="("
def S(s):
 if s[0]!=l:return s
 if s[1]=="\\":g=s.find('.');return"(\\ %s. %s)"%(s[3:g],S(s[g+2:-1]))
 i=2;c=s[1]==l
 while c:c+=(s[i]==l)-(s[i]==')');i+=1
 t=S(s[1:i])
 z=s[i+1:-1]
 if l!=t[0]:return"(%s %s)"%(t,S(z))
 g=t.find('.')
 t=S(t[g+2:-1]).replace(t[3:g],z)
 if t!=s:t=S(t)
 return t
print S(raw_input())
JPvdMerwe
źródło
Wygląda to ładnie, ale nie działa. Dodałem kilka przykładowych danych wejściowych i wyjściowych, dla których kod generuje nieprawidłowe wyniki.
sepp2k
1
Nie powoduje to zamiany unikania przechwytywania. Na przykład (((\ f. (\ X. (Fx)))) (\ y. (\ X. Y))) niepoprawnie ocenia się na (\ x. (\ X. X)).
Anders Kaseorg
1
Dlaczego jest to oznaczone jako odpowiedź, gdy ledwo działa? Czy wypróbowałeś dane wejściowe i wyjściowe autora?
rbaleksandar
1
Dostarczone przez autora przypadki testowe są niewystarczające do wykazania błędów w tej odpowiedzi.
Anders Kaseorg,
1
Ta odpowiedź nie jest ani poprawna, ani najkrótsza. Nie udaje się uniknąć przechwytywania i zawiera błędy zastępowania łańcucha.
Richard Padley,
6

Ruby 254 znaków

f=->u,r{r.chars.take_while{|c|u+=c==?(?1:c==?)?-1:0;u>0}*''}
l=->x{x=~/^(\(*)\(\\ (\w+)\. (.*)/&&(b,v,r=$1,$2,$3;e=f[1,r];(e==s=l[e])?b==''?x:(s=f[2,r];(x==y=b.chop+e.gsub(v,s[2+e.size..-1])+r[1+s.size..-1])?x:l[y]):(b+'(\\ '+v+'. '+s+r[e.size..-1]))||x}

Może być używany jak

puts l["((\\ x. (\\ y. x)) (\\ a. a))"]    # <= (\ y. (\ a. a))

Rozwiązanie nie jest jeszcze w pełni zagrane w golfa, ale jest już prawie nieczytelne.

Howard
źródło
cześć zazdrość, mój stary przyjacielu :)
luser droog
Nie powoduje to zamiany unikania przechwytywania. Na przykład (((\ f. (\ X. (Fx)))) (\ y. (\ X. Y))) niepoprawnie ocenia się na (\ x. (\ X. X)).
Anders Kaseorg
Oprócz powyższego błędu przechwytywania, to również niepoprawnie ocenia (\ y. (\ Xx. ((\ X. Xx) y)))) do (\ y. (\ Xx. Yy)), gdzie wytworzono nadmierne zastąpienie łańcucha nieistniejąca zmienna yy.
Anders Kaseorg,
3

Edycja: sprawdź moją odpowiedź poniżej pod kątem 250 w czystym JavaScript.

2852 243 znaków przy użyciu LiveScript (bez Regex! Nie w pełni golfowy - można poprawić)

L=(.0==\\)
A=->it.forEach?&&it.0!=\\
V=(.toFixed?)
S=(a,b,t=-1,l=0)->|L a=>[\\,S(a.1,b,t,l+1)];|A a=>(map (->S(a[it],b,t,l)),[0 1]);|a==l+-1=>S(b,0,l+-1,0)||a|l-1<a=>a+t;|_=>a
R=(a)->|L a=>[\\,R a.1]|(A a)&&(L a.0)=>R(S(R(a.0),R(a.1)).1)|_=>a

Test:

a = [\\,[\\,[1 [1 0]]]]
b = [\\,[\\,[1 [1 [1 0]]]]]
console.log R [a, b]
# outputs ["\\",["\\",[1,[1,[1,[1,[1,[1,[1,[1,[1,0]]]]]]]]]]]

Który jest 3^2=9, jak stwierdzono w OP.

Jeśli ktoś jest ciekawy, oto rozszerzona wersja z kilkoma komentarzami:

# Just type checking
λ = 100
isλ = (.0==λ)
isA = -> it.forEach? && it.0!=λ
isV = (.toFixed?)

# Performs substitutions in trees
# a: trees to perform substitution in
# b: substitute bound variables by this, if != void
# f: add this value to all unbound variables
# l: internal (depth)
S = (a,b,t=-1,l=0) ->
    switch
    | isλ a             => [λ, (S a.1, b, t, l+1)]
    | isA a             => [(S a.0, b, t, l), (S a.1, b, t, l)]
    | a == l - 1        => (S b, 0, (l - 1), 0) || a
    | l - 1 < a < 100   => a + t
    | _                 => a

# Performs the beta-reduction
R = (a) ->
    switch
    | (isλ a)               => [λ,R a.1]
    | (isA a) && (isλ a.0)  => R(S(R(a.0),R(a.1)).1)
    | _                     => a

# Test
a = [λ,[λ,[1 [1 0]]]]
b = [λ,[λ,[1 [1 [1 0]]]]]
console.log show R [a, b]
MaiaVictor
źródło
Nie jest to zgodne ze specyfikacjami wejściowymi i wyjściowymi problemu.
Anders Kaseorg
3

Łuk Waterhouse - 140 znaków

(=
f[is cons?&car._'λ]n[if
atom._ _
f._ `(λ,_.1,n:_.2)(=
c n:_.0
e _)(if
f.c(n:deep-map[if(is
c.1 _)e.1
_]c.2)(map n
_))]λ[n:read:rem #\._])
Ogrzewany
źródło
Gdzie mogę dostać Waterhouse Arc?
Anders Kaseorg
1
Nigdzie nie można znaleźć niepoprawnego jako tłumacza
kot
@AndersKaseorg tutaj
tylko ASCII
@ Tylko ASCII Wiem, co to jest Arc, ale część „Waterhouse” zasugerowała mi, że jakiś szczególny dialekt był konieczny. Czy już go uruchomiłeś?
Anders Kaseorg
@AndersKaseorg Nieważne. Znaleziono
tylko ASCII
2

C 1039 bajtów

#define F for
#define R return
#define E if(i>=M||j>=M)R-1;
enum{O='(',C,M=3999};signed char Q[M],D[M],t[M],Z,v,*o=Q,*d=D,*T;int m,n,s,c,w,x,y;K(i,j,k){!Z&&(Z=t[O]=1)+(t[C]=-1);E;if(!o[i]){d[j]=0;R 0;}if((c=t[o[i]]+t[o[i+1]])!=2||o[i+2]!='\\'){d[j++]=o[i++];R K(i,j,i);}F(i+=2,y=w=0;i<M&&o[i]&&c;++i)c+=t[o[i]],!w&&c==1?w=i:0,!y&&o[i]=='.'?y=i+2:0;E;if(c){F(;d[j++]=o[i++];)E;R 0;}F(c=y;c<w;++c)if(o[c]=='\\')F(n=0,m=w+2;m<i;++m){if(o[m]==o[c+2]){F(x=0;o[m+x]&&isalpha(o[m+x])&&o[m+x]==o[c+2+x];++x);if(o[c+2+x]!='.'||isalpha(o[m+x]))continue;if(v>'Z')R-1;F(n=c+2;n<w;++n)if(o[n]==o[m]){F(x=0; o[m+x]&&isalpha(o[m+x])&&o[m+x]==o[n+x];++x);if(o[m+x]=='.'&&!isalpha(o[n+x]))F(;--x>=0;) o[n+x]=v;}++v;}}F(c=y;c<w&&j<M;++c){F(x=0;o[c+x]&&o[c+x]==o[k+4+x]&&isalpha(o[c+x]); ++x);if(o[k+4+x]=='.'&&!isalpha(o[c+x])){F(m=w+2;m<i-1&&j<M;++m)d[j++]=o[m];c+=x-1;}else d[j++]=o[c];}E;Z=2;R K(i,j,i);}char*L(char*a){F(s=n=0;n<M&&(o[n]=a[n]);++n);if(n==M)R 0;v='A';F(;++s<M;){Z=0;n=K(0,0,0);if(Z==2&&n!=-1)T=d,d=o,o=T;else break;}R n==-1||s>=M?0:d;}

Zmienne zezwalają jako dane wejściowe przy użyciu małych liter [od a..z] sys może generować zmienne przy użyciu wielkich liter [od A..Z], jeśli jest taka potrzeba na wyjściu ... Załóżmy, że konfiguracja znaków ascii.

#define P printf
main()
{char  *r[]={ "((\\ abc. (\\ b. (abc (abc (abc b))))) (\\ cc. (\\ dd. (cc (cc dd)))))",
              "((\\ fa. (\\ abc. (fa abc))) (\\ yy. (\\ abc. yy)))",
              "((\\ x. x) z)", 
              "((\\ x. x) (\\ y. (\\ z. z)))", 
              "(\\ x. ((\\ y. y) x))", 
              "((\\ x. (\\ y. x)) (\\ a. a))", 
              "(((\\ x. (\\ y. x)) (\\ a. a)) (\\ b. b))",
              "((\\ x. (\\ y. y)) (\\ a. a))",
              "(((\\ x. (\\ y. y)) (\\ a. a)) (\\ b. b))",             
              "((\\ x. (x x)) (\\ x. (x x)))",
              "(((\\ x. (\\ y. x)) (\\ a. a)) ((\\ x. (x x)) (\\ x. (x x))))",
             0}, *p;
 int    w;

 for(w=0; r[w] ;++w)
   {p=L(r[w]);
    P("o=%s d=%s\n", r[w], p==0?"Error ":p);
   }
 R  0;
}

/*1.039*/
RosLuP
źródło
Specyfikacja wymaga \ lub λ, a nie /. Wymaga to również obsługi wieloliterowych nazw zmiennych.
Anders Kaseorg,
„\ n” itd. symbol „\” ma inne zastosowania, lepiej zamiast tego użyć „/”
RosLuP
1
Jednak wyzwaniem jest spełnienie specyfikacji, a nie poprawienie jej.
Anders Kaseorg,
napisałem coś, żeby było trochę bardziej zgodne ... ale rozmiar eksploduje ...
RosLuP
1
932 bajty
ceilingcat
1

Haskell 456 C.

Może być znacznie krótszy, jeśli w pełni wykorzystana jest leniwa funkcja oceny Haskell. Niestety nie wiem jak to zrobić.

Ponadto wiele znaków jest marnowanych na etapie analizy.

data T=A[Char]|B[Char]T|C T T
(!)=(++)
s(A a)=a
s(B a b)="(λ "!a!". "!s b!")"
s(C a b)='(':s a!" "!s b!")"
e d(A a)=maybe(A a)id(lookup a d)
e d(B a b)=B a.e d$b
e d(C a b)=f d(e d a)(e d b)
f d(B x s)q=e((x,q):d)s
f d p q=C p q
d=tail
p('(':'λ':s)=let(A c,t)=p(d s);(b,u)=p(d.d$t);in(B c b,d u)
p('(':s)=let(a,t)=p s;(b,u)=p(d t)in(C a b,d u)
p(c:s)|elem c" .)"=(A "",c:s)|1<2=let((A w),t)=p s in(A(c:w),t)
r=s.e[].fst.p
main=do l<-getLine;putStrLn$r l

Wersja bez golfa

data Expression = Literal String 
                | Lambda String Expression
                | Apply Expression Expression
                deriving Show

type Context = [(String, Expression)]

show' :: Expression -> String
show' (Literal a) = a
show' (Lambda x e) = "(λ " ++ x ++ ". " ++ show' e ++ ")"
show' (Apply e1 e2) = "(" ++ show' e1 ++ " " ++ show' e2 ++ ")"

eval :: Context -> Expression -> Expression
eval context e@(Literal a) = maybe e id (lookup a context)
eval context (Lambda x e) = Lambda x (eval context e)
eval context (Apply e1 e2) = apply context (eval context e1) (eval context e2)

apply :: Context -> Expression -> Expression -> Expression
apply context (Lambda x e) e2 = eval ((x, e2):context) e
apply context e1 e2 = Apply e1 e2

parse :: String -> (Expression, String)
parse ('(':'λ':s) = let
    (Literal a, s') = parse (tail s)
    (e, s'') = parse (drop 2 s')
    in (Lambda a e, tail s'')

parse ('(':s) = let
    (e1, s') = parse s
    (e2, s'') = parse (tail s')
    in (Apply e1 e2, tail s'')

parse (c:s) | elem c " .)" = (Literal "", c:s)
            | otherwise    = let ((Literal a), s') = parse s 
                             in (Literal (c:a), s')

run :: String -> String
run = show' . eval [] . fst . parse
main = do
  line <- getLine
  putStrLn$ run line
Promień
źródło
3
Nie powoduje to zamiany unikania przechwytywania. Na przykład ((λ f. (Λ x. (Fx))) (λ y. (Λ x. Y))) niepoprawnie ocenia się na (λ x. (Λ x. X)).
Anders Kaseorg
1

Masz 231 z JavaScript / bez Regex

(function f(a){return a[0]?(a=a.map(f),1===a[0][0]?f(function d(b,a,e,c){return b[0]?1===b[0]?[1,d(b[1],a,e,c+1)]:2===b[0]?b[1]===c-1?d(a,0,c-1,0)||b:c-1<b[1]?[2,b[1]+e]:b:[d(b[0],a,e,c),d(b[1],a,e,c)]:b}(a[0],a[1],-1,0)[1]):a):a})

Odbiera tablice 2-elementowe. 1oznacza λi 2 oznacza zmienną indeksu bruijn.

Test:

zero = [1,[1,[2,0]]]; // λλ0
succ = [1,[1,[1,[[2,1],[[[2,2],[2,1]],[2,0]]]]]]; // λλλ(1 ((2 1) 0))
console.log(JSON.stringify(reduce([succ,[succ,[succ,zero]]]))); // 0+1+1+1
// Output: [1,[1,[[2,1],[[2,1],[[2,1],[2,0]]]]]] = λλ(1(1(1 0))) = number 3
MaiaVictor
źródło
Nie jest to zgodne ze specyfikacjami wejściowymi i wyjściowymi problemu.
Anders Kaseorg
1

Python: 1266 znaków (mierzonych za pomocą wc)

from collections import *;import re
A,B,y,c=namedtuple('A',['l','r']),namedtuple('B',['i','b']),type,list.pop
def ab(t):c(t,0);p=c(t,0);c(t,0);return B(p,tm(t))
def tm(t):return ab(t)if t[0]=='\\'else ap(t)
def at(t):
    if t[0]=='(':c(t,0);r=tm(t);c(t,0);return r
    if 96<ord(t[0][0])<123:return c(t,0)
    if t[0]=='\\':return ab(t)
def ap(t):
    l = at(t)
    while 1:
        r = at(t)
        if not r:return l
        l = A(l,r)
def P(s):return tm(re.findall(r'(\(|\)|\\|[a-z]\w*|\.)',s)+['='])
def V(e):o=y(e);return V(e.b)-{e.i} if o==B else V(e.l)|V(e.r)if o==A else{e}
def R(e,f,t):return B(e.i,R(e.b,f,t)) if y(e)==B else A(R(e.l,f,t),R(e.r,f,t))if y(e)==A else t if e==f else e
def N(i,e):return N(chr(97+(ord(i[0])-96)%26),e) if i in V(e)else i
def S(i,e,a): return A(S(i,e.l,a),S(i,e.r,a)) if y(e)==A else(e if e.i==i else B(N(e.i,a),S(i,R(e.b,e.i,N(e.i,a)),a)))if y(e)==B else a if e==i else e
def T(e):
    if y(e)==A:l,r=e;return S(l.i,l.b,r)if y(l)==B else A(T(l),r)if y(l)==A else A(l,T(r))
    if y(e)==B:return B(e.i,T(e.b))
    q
def F(e):o=y(e);return r'(\%s. %s)'%(e.i,F(e.b))if o==B else'(%s %s)'%(F(e.l),F(e.r)) if o==A else e
def E(a):
    try: return E(T(a))
    except NameError:print(F(a))
E(P(input()))

Nie najkrótszy z długiego ujęcia, ale poprawnie obsługuje zmianę nazwy alfa i wszystkie przykłady wymienione w poście PO.

Björn Lindqvist
źródło
Możesz skrócić niektóre z tych nazw funkcji i zamienić niektóre z nich na lambdas. Masz tu też nadmiar białych znaków
Jo King
(1) Zastąpienie wcięcia 4 spacjami pojedynczym spacją zaoszczędzi sporo bajtów. (2) Czy możesz wymienić na except NameErrorjust except? (3) Nazwy funkcji dwuznakowych można zmienić na nazwy jednoznakowe. (4) Istnieje kilka miejsc, w których masz zadania, które mają spacje wokół =. (5) if t[0]=='c'można zastąpić if'c'==t[0].
Esolanging Fruit
1045 bajtów dzięki głównie zmianom formatowania, takim jak wcięcia i lambda
Jo King,
0

C ++ (gcc) ,782 766 758 731 bajtów

#include <string>
#include <map>
#define A return
#define N new E
using S=std::string;using C=char;using I=int;S V(I i){A(i>8?V(i/9):"")+C(97+i%9);}S W(C*&s){C*b=s;while(*++s>96);A{b,s};}struct E{I t,i;E*l,*r;E(E&o,I d,I e){t=o.t;i=o.i+(o.i>=d)*e;t?l=N{*o.l,d,e},t-1?r=N{*o.r,d,e}:0:0;}E(I d,std::map<S,I>m,C*&s){t=*s-40?i=m[W(s)],0:*++s-92?l=N{d,m,s},r=N{d,m,++s},++s,2:(m[W(s+=2)]=d,l=N{d+1,m,s+=2},++s,1);}I R(I d){A t?t-1?l->t==1?l->l->s(d,0,*r),*this=*l->l,1:l->R(d)||r->R(d):l->R(d+1):0;}I s(I d,I e,E&v){t?t-1?l->s(d,e,v),r->s(d,e,v):l->s(d,e+1,v):i==d?*this={v,d,e},0:i-=i>d;}S u(I d){A t?t-1?S{"("}+l->u(d)+' '+r->u(d)+')':S{"(\\ "}+V(d)+". "+l->u(d+1)+')':V(i);}};S f(C*s){E a{0,{},s};for(I c=999;a.R(0)&&c--;);A a.u(0);}

Wypróbuj online!

Podstawową ideą jest to, że kod wykorzystuje wewnętrzną reprezentację opartą na idei indeksów de Bruijna - z tym wyjątkiem, że odwracam wskaźniki, aby wskazać głębokość lambda wiązania danej zmiennej. W kodzie:

  • E::treprezentuje typ węzła - 0 dla zmiennego węzła liścia, 1 dla węzła lambda i 2 dla węzła aplikacji funkcji. (Dobiera się tak, że pokrywa się z Arity węzła, który okazuje się być możliwe.) A E::li E::rsą dzieci, zgodnie z (tylko E::ldla węzła lambda), i E::ijest indeksem lambda głębokość zmienną węzła liścia.
  • Konstruktor E::E(E&o,int d,int e)klonuje podwyrażenie, które początkowo znajdowało się na głębokości lambda, w dcelu wklejenia w nowym miejscu na głębokości lambda d+e. Obejmuje to zachowanie zmiennych na głębokości lambda mniejszej niż dpodczas zwiększania zmiennych na głębokości lambda przynajmniej do e.
  • E::sma podstawienie podwyrażenie vdo różnej liczby dw *thisnatomiast zmniejszanie liczby zmiennych powyżej d(oraz ejest wewnętrznym Detal śledzenia przyrost lambda głębokość gdy musi skorzystać E::c).
  • E::Rszuka pojedynczej redukcji beta do wykonania, preferując najwyższe lub najbardziej lewe wystąpienia, zgodnie z wyszukiwaniem w przedsprzedaży AST. Zwraca wartość niezerową, jeśli znalazł redukcję do wykonania lub zero, jeśli nie znalazła żadnej.
  • E::ujest to_stringoperacją typu, która odtwarza łańcuch „czytelny dla człowieka” przy użyciu syntetycznych nazw zmiennych. (Pamiętaj, że z powodu niewielkiej gry w golfa w Vfunkcji pomocnika będzie generować tylko nazwy zawierające aprzelot i).
  • Konstruktor E::E(int d, std::map<std::string, int> m, char*&s)analizuje ciąg wejściowy sdo wyrażenia AST w oparciu o odwzorowanie maktualnie powiązanych nazw zmiennych na wskaźniki głębokości lambda.
  • f to główna funkcja odpowiadająca na pytanie.

(Jak widać na łączu TIO, kod obsługuje nazwy zmiennych z wieloma znakami, a także otrzymuje poprawną odpowiedź (\ a. (\ b. a))na ((\ f. (\ x. (f x))) (\ y. (\ x. y))). Zdarza się również, że parsowanie kodu może obsługiwać cieniowanie zmiennych bez dodatkowych kosztów.)


-16 bajtów częściowo z powodu pomysłu autorstwa ceilingcat (który sam wymyśliłem niezależnie), a częściowo z powodu zmiany E*a=new E;na, E&a=*new E;a następnie zmiany a->naa.

-8 więcej bajtów z powodu innego komentarza użytkownika ceilingcat (pomiń przypisanie z trójki a.t)

-27 bajtów z konwersji parsera i klonowania do konstruktorów E

Daniel Schepler
źródło
-1

C 637 bajtów

#define R return
#define E if(i>=M||j>=M)R-1;
#define H d[j++]
enum{O=40,C,M=3999};signed char Q[M],D[M],t[M],Z,*o=Q,*d=D,*T;int m,n,s,c,w;K(i,j,k){!Z&&(Z=t[O]=1)+(t[C]=-1);E;if(!o[i]){H=0;R 0;}if((c=t[o[i]]+t[o[i+1]])!=2||o[i+2]!=92){H=o[i++];R K(i,j,i);}for(i+=2,w=0;i<M&&o[i]&&c;++i)c+=t[o[i]],!w&&c==1?w=i:0;E;if(c){for(;H=o[i++];)E;R 0;}for(c=k+7,n=j;c<w&&j<M;++c)if(o[c]==o[k+4]){if(o[c+1]==46){d[n++]=o[k++];R K(k,n,k);}for(m=w+2;m<i-1&&j<M;)H=o[m++];}else H=o[c];E;Z=2;R K(i,j,i);}char*L(char*a){for(s=n=0;n<M&&(o[n]=a[n]);++n);if(n==M)R 0;for(;++s<M;){Z=0;if((n=K(0,0,0))!=-1&&Z==2)T=d,d=o,o=T;else break;}R n==-1||s>=M?0:d;}

Ta wersja nie używa zmiennych pomocniczych (więc nie wynika to w 100% z tego, co mówi rachunek lambda ... jak wiele innych tutaj ...). Każda zmienna musi mieć długość 1 znaków (tak jak inne tutaj). Kod testowy:

#define P printf

main()
{char  *r[]={ "((\\ x. x) z)", 
              "((\\ x. x) (\\ y. (\\ z. z)))", 
              "(\\ x. ((\\ y. y) x))", 
              "((\\ x. (\\ y. x)) (\\ a. a))", 
              "(((\\ x. (\\ y. x)) (\\ a. a)) (\\ b. b))",
              "((\\ x. (\\ y. y)) (\\ a. a))",
              "(((\\ x. (\\ y. y)) (\\ a. a)) (\\ b. b))",
              "((\\ x. (x x)) (\\ x. (x x)))",
              "(((\\ x. (\\ y. x)) (\\ a. a)) ((\\ x. (x x)) (\\ x. (x x))))",
              "((\\ a. (\\ b. (a (a (a b))))) (\\ c. (\\ d. (c (c d)))))",
              "((\\ f. (\\ x. (f x))) (\\ y. (\\ x. y)))",
             0}, *y;
 int    w;

 for(w=0; r[w] ;++w)
   {y=L(r[w]);
    P("o=%s d=%s\n", r[w], y==0?"Error ":y);
   }
 R  0;
}

wyniki:

/*
637
o=((\ x. x) z) d=z
o=((\ x. x) (\ y. (\ z. z))) d=(\ y. (\ z. z))
o=(\ x. ((\ y. y) x)) d=(\ x. x)
o=((\ x. (\ y. x)) (\ a. a)) d=(\ y. (\ a. a))
o=(((\ x. (\ y. x)) (\ a. a)) (\ b. b)) d=(\ a. a)
o=((\ x. (\ y. y)) (\ a. a)) d=(\ y. y)
o=(((\ x. (\ y. y)) (\ a. a)) (\ b. b)) d=(\ b. b)
o=((\ x. (x x)) (\ x. (x x))) d=Error
o=(((\ x. (\ y. x)) (\ a. a)) ((\ x. (x x)) (\ x. (x x)))) d=(\ a. a)
o=((\ a. (\ b. (a (a (a b))))) (\ c. (\ d. (c (c d))))) d=(\ b. (\ d. (b (b (b (b (b (b (b (b d))))))))))
o=((\ f. (\ x. (f x))) (\ y. (\ x. y))) d=(\ x. (\ x. x))
*/

to jest pół-niemęski:

#define R return
#define E if(i>=M||j>=M)R-1;
#define H d[j++]
enum{O=40,C,M=3999}; // assume ascii
signed char Q[M],D[M],t[M],Z,*o=Q,*d=D,*T;
int m,n,s,c,w;

K(i,j,k)
{!Z&&(Z=t[O]=1)+(t[C]=-1); //inizializza tabelle

 E;if(!o[i]){H=0;R 0;}
 if((c=t[o[i]]+t[o[i+1]])!=2||o[i+2]!=92)
      {H=o[i++]; R K(i,j,i);}
 for(i+=2,w=0;i<M&&o[i]&&c;++i)
         c+=t[o[i]],!w&&c==1?w=i:0;
 E;
 if(c){for(;H=o[i++];)E;R 0;} 
//  01234567w12 i
//  ((/ x. x) z)
//   x                 w              z
// o[k+4]..o[k+5];  o[k+7]..o[w];  o[w+2]..o[i-1]

// sostituzione
// sostituisce a x z in w e lo scrive in d
for(c=k+7,n=j;c<w&&j<M;++c)
      if(o[c]==o[k+4])
         {if(o[c+1]==46) // non puo' sostituire una variabile dove c'e' lambda
             {d[n++]=o[k++]; R K(k,n,k);}
          for(m=w+2;m<i-1&&j<M;++m)
                H=o[m];
         }
      else H=o[c];
 E;
 Z=2;
 R K(i,j,i);
}

char*L(char*a)
{for(s=n=0;n<M&&(o[n]=a[n]);++n);
 if(n==M)R 0;
 for(;++s<M;)
   {Z=0;
    n=K(0,0,0);
//    if(Z==2)printf("n=%d>%s\n", n, d);
    if(Z==2&&n!=-1)T=d,d=o,o=T;
    else break;
   }
 R n==-1||s>=M?0:d; 
}
RosLuP
źródło
Specyfikacja wymaga \ lub λ, a nie /. Wymaga to również obsługi wieloliterowych nazw zmiennych. Dodatkowo (wiem, że zdajesz sobie z tego sprawę, ale tak, nadal jest źle), to niepoprawnie ocenia ((/ f. (/ X. (Fx))) (/ y. (/ X. Y))) do ( / x. (/ x. x)).
Anders Kaseorg,
Zmieniam / na \ jest problem, który nie pozwala na wieloznakową zmienną. jeśli przetestujesz jakiś inny, jest to również dla innego rozwiązania
RosLuP