% Domaci ukol: nahradte vsechny todo tak, aby prosly testy. todo :- writeln("Unimplemented!"), fail. % testy si muzete spustit pomoci test1 a test2 (viz. dole). % Uplne dole je bonus. % pomucka -- jako member/2, ale vybere _jen_ prvni vyraz, % ktery jde unifikovat s X. first_member(X,[X|_]) :- !. first_member(X,[_|Xs]) :- first_member(X,Xs). %%%%%%%%% % Generovani vsech moznych lambda vyrazu bez volbych promennych. % (syntax pouzijte jako vzor pro parsovani: % λx.A v prologu budeme reprezentovat jako lam(x,A), % AB jako app(A,B), % promennou x jako var(x). % lambda_terms(X) :- lambda_terms(X,0). lambda_terms(X,N) :- lambda_term(X,[],N); N1 is N+1, lambda_terms(X, N1). lambda_term(var(V),Vs,_) :- member(V,Vs). lambda_term(app(L,R),Vs,N) :- N>0, N0 is N-1, lambda_term(L,Vs,N0), lambda_term(R,Vs,N0). lambda_term(lam(X,B),Vs,N) :- N>0, N0 is N-1, is_var_name(X), \+ member(X,Vs), !, lambda_term(B,[X|Vs],N0). %%%%%%%%% % Parsovani lambda vyrazu ze stringu % Lambdu λ budeme pro jednoduchost psat jako lomitko / % % is_var_name zjisti, jestli je pismeno vhodne jako jmeno promenne % (mame jen jednopismenne promenne) is_var_name(X) :- string_chars("abcdefghijklmnopqrstuvwxyz",Cs), member(X,Cs). % simple_lambda naparsuje "jednoduche lambda vyrazy", % tj.: % - povolenou jednopismennou promennou (viz. vyse) % - jiny vyraz v (zavorkach), na vnitrni vyraz pouzijte % nize definovany parser lambda/3 simple_lambda(L) --> {todo}. % lambda abstrakce λx.vyraz, ve stringu "/x.vyraz" abstraction(A) --> {todo}. % lambda aplikace se zavorkuji zleva. Kvuli tomu normalni parsery bohuzel % selzou na nekonecnou levou rekurzi. Misto toho muzeme radu lambda vyrazu % naparsovat do obycejneho seznamu, a ten pak obratit. % % lambda_list by mela string "abc(/x.x)" naparsovat do: % [ var(a), var(b), var(c), lam(x,var(x)) ] lambda_list([A]) --> {todo}. lambda_list([H|T]) --> {todo}. % lambdas_apply vezme seznam lambda vyrazu z predchozi funkce, a vyrobi seznam % lambda aplikaci uzavorkovany zleva: % lambdas_apply( % [ a, a, b, lam(x, var(x))], %vstupni seznam % app(app(app(a, a), b), lam(x, var(x))) %vystupni lambda vyraz % ). % % Hint: funkce nikdy nedostane prazdny seznam, a na aplikaci jsou v seznamu % potreba minimalne 2 prvky. lambdas_apply(List, Lam) :- todo. % parser na slozeny lambda vyraz lambda(A) --> lambda_list(X), {lambdas_apply(X,A)}; abstraction(A). % konverze string -> lambda vyraz parse_lambda(String, L) :- todo. %%%%%%%%% % Vypocet lambda kalkulu. % % Nejvetsi nebezpeci pri vypoctu je kolize promennych (dosadite x do vyrazu, % kde ma jiny vyznam nez puvodne). Nebezpeci je podobne jako pri substituci v % predikatove logice. % % Reseni: uniquify_vars prejmenuje vsechny promenne. Misto znaku na promenne % pouzijte cisla (v prologu to je jedno, a cisla jdou lepe generovat). % % Ukazka: % ?- parse_lambda("(/x.xx)(/x.x(/x.x)x)",L), uniquify_vars(L,U). % L = app(lam(x, app(var(x), var(x))), lam(x, app(app(var(x), lam(x, var(x))), var(x)))), % U = app(lam(0, app(var(0), var(0))), lam(1, app(app(var(1), lam(2, var(2))), var(1)))). % uniquify_vars(L,L2) :- todo. % Hint: pouzijte pomocnou funkci: % uniquify_vars( % +Vstup, % -Vystup, % +SeznamDvojicPrecislovanychPromennych, % +CisloDalsiPromenneVeVyrazu, % -UpdatovaneCisloDalsiPromenne). % beta_reduce_once najde ve vyrazu prvni podvyraz zleva, kde jde dosadit do % lambdy, a provede dosazeni. beta_reduce_once(app(lam(V,A),B),L1) :- !,subst(A,V,B,L1). beta_reduce_once(app(L,R), app(L1,R)) :- beta_reduce_once(L,L1),!. beta_reduce_once(app(L,R), app(L,R1)) :- beta_reduce_once(R,R1). beta_reduce_once(lam(V,A),lam(V,A1)) :- beta_reduce_once(A,A1). % Substituce. Do vyrazu Vstup dosad vyraz SubstVyraz misto _vsech volnych_ % promennych SubstPromenna, vysledek vrat na Vystupu. % % Pozor na backtracking -- vysledek by nemel byt substituovany jen castecne. subst(Vstup, SubstPromenna, SubstVyraz, Vystup) :- todo. %%%%%%%%% % Tady konci domaci ukol, zbytek programu je ciste demonstracni/testovaci. % % lambda vyraz obsahuje redex prave kdyz v nem je neco, co jde dosadit contains_redex(X) :- beta_reduce_once(X,_), !. % aplikuje beta redukci dokud je co redukovat, vysledek se bud zacykli, % nebo je opravdu "vysledek". normal_form(L, L) :- \+ contains_redex(L). normal_form(L, NF) :- contains_redex(L), beta_reduce_once(L,L1), uniquify_vars(L1,L2), normal_form(L2,NF). % Primitivni implementace jednoducheho typoveho systemu lambda kalkulu type(var(V), Ctx, T) :- first_member(t(V,T), Ctx). type(lam(V,E), Ctx, fun(TV,T)) :- type(E, [t(V,TV)|Ctx], T). type(app(X,Y), Ctx, T) :- type(Y, Ctx, TY), type(X, Ctx, TX), TX = fun(TY,T). %reprezentuje typ funkce TY -> T % Pozn. po pridani occur-checku do unifikaci bychom dostali standardni STLC. %%%%%%%%%% % Testy % test1 :- parse_lambda("(/a.a)(/a.a)", V), write("Parsed out: "), print_term(V,[]), nl, uniquify_vars(V,U), write("Uniquified: "), print_term(U,[]), nl, U = app(lam(X1,var(X1)), lam(X2,var(X2))), X1 \== X2, contains_redex(U), writeln("Contains a redex!"), beta_reduce_once(U,U1), write("Beta reduced: "), print_term(U1,[]), nl, \+ contains_redex(U1), writeln("Contains no more redexes!"), type(U,[],T), type(U1,[],T), %typ vyrazu by se pri vyhodnocovani nemel zmenit! write("Type is: "), print_term(T,[]), nl, T = fun(TV,TV), var(TV). test2 :- % Trochu komplikovanejsi test: program se zacykli, pokud se pokusi % spocitat spatny podvyraz. Nastesti to neni potreba ke spocitani % celeho vyrazu. % % (Pozn.: beta_reduce_once se zvladne nezacyklit diky tomu, ze provadi % lazy vyhodnocovani -- prvni vyhodnocuje vzdycky nejvic levy regex, % takze nikdy nevyhodnoti nic, co by opravdu nebylo potreba). parse_lambda("(/a./b.(/a./b.b)((/x.xx)(/x.xx))(/a./b.a)ab)",V), write("Parsed out: "), print_term(V,[]), nl, uniquify_vars(V,U), write("Uniquified: "), print_term(U,[]), nl, normal_form(U,NF), write("Normal form: "), print_term(NF,[]), nl, type(NF,[],T), write("Type: "), print_term(T,[]), nl, %check the final type T = fun(A,fun(B,A)), var(A), var(B), A\==B. % bonus: pomoci definovanych funkci mechanicky najdete lambda vyraz, ktery se % po jedne beta redukci zmeni, ale po druhe se vrati do puvodniho stavu % (pozor na precislovani promennych). bonus(X) :- todo.