Evaluation contexts

anf.pl

/*
構文

x, y, z          変数
v ::=            値
　λ(x:T)t       ラムダ
s, t, u ::=      項
　x              変数
　v              値
　x y            関数適用
　let x = t in u let式

評価規則 t ---> t

        let x = v in e[x y] ---> let x = v in e[[z := y]t] if v=λ(z:T)t
             let x = y in t ---> [x::=y] t
let x = let y = s in t in u ---> let y = s in let x = t in u
                       e[t] ---> e[u]                      if t ---> u
                                 where e::=[] | let x = [] in t | let x = v in e
*/

:- initialization(main).
:- op(920, xfx, [ --->, -->> ]).
:- op(500, yfx, $).

v(X->_) :- atom(X).

% 答
a(V,V) :- v(V).
a(X,X) :- atom(X).
a(let(X=V,A),V) :- a(A,X).
a(let(_=_,A),A_) :- a(A,A_).

% 文脈、パラメータ取得
e(let(X=U,T),let(X=[],T),U):- \+v(U).
e(let(X=V,E),let(X=V,E_),H):- v(V), e(E,E_,H).
e(T,[],T).

subst(S,S_,S,S_).
subst(S,S_,X->T,X->T_) :- S \= X, subst(S,S_,T,T_).
subst(S,S_,T$U,T_$U_) :- subst(S,S_,T,T_), subst(S,S_,U,U_).
subst(S,S_,let(X=T,U),let(X=T_,U_)) :- S\=X,subst(S,S_,T,T_), subst(S,S_,U,U_).
subst(_,_,T,T).

       let(X=V,EXV) ---> let(X=V,ET_) :- e(EXV,E,(X$Y)), V=(Z->T), subst(Z,Y,T,T_), subst([],T_,E,ET_).
         let(X=Y,T) ---> T_ :- atom(Y), subst(X,Y,T,T_).
let(X=let(Y=S,T),U) ---> let(Y=S,let(X=T,U)).
                  T ---> T_ :- e(T,EC,U), T \= U, U ---> U_, subst([],U_,EC,T_).

% 複数ステップ実行
T -->> T_ :- writeln(T),T--->U,!,U-->>T_.
T -->> T_ :- a(T,T_),(T=T_;writeln(T_)),nl.

:- (x->x)-->>R,R=(x->x).
:- let(yy=(y->y),yy)-->>R,R=(y->y).
:- let(xx=(x->x),let(yy=(y->y),xx$yy))-->>R,R=(y->y).
:- let(xx=(x->x),let(yy=(y->y),let(zz=(z->z),let(yyzz=yy$zz,xx$yyzz))))-->>R,R=(z->z).
:- halt.

anf_env_and_smallstep.pl

/*
構文

x, y, z          変数
v ::=            値
　λ(x)t         ラムダ
s, t, u ::=      項
　x              変数
　v              値
　x y            関数適用
　let x = t in u let式

(Apply)
                         s | x y  -->  s | [z:=s(y)]t    if s(x) = lambda(z: T)t
(Let-Var)
              s | let x = y in t  -->  s | [x:=s(y)]t
(Let-Value)
              s | let x = v in t  -->  s, x = v | t
(Ctx)
                           s | t  -->  s' | t'
                  ------------------------------------
                  let x = t in u  -->  let x = t' in u
*/

% 値
v(lam(X,_)) :- atom(X).

% 答
a(lam(X,T),lam(X,T)).
a(let(_,_,A),A_) :- a(A,A_).

% 置換
subst(X,T,X,T).
subst(X,T,lam(X1,T1),lam(X1,T1_)) :- subst(X,T,T1,T1_), X \=X1.
subst(X,T,app(T1,T2),app(T1_,T2_)) :- subst(X,T,T1,T1_), subst(X,T,T2,T2_).
subst(X,T,let(X1,T1,T2),let(X1,T1_,T2_)) :- subst(X,T,T1,T1_), subst(X,T,T2,T2_), X\=X1.
subst(_,_,E,E).

% ワンステップ実行
eval1(S,app(X,Y), S,T_) :- member(X=lam(Z,T),S),member(Y=V,S),subst(Z,V,T,T_). % (Apply)
eval1(S,let(X,Y,T),S,T_):- member(Y=V,S),subst(X,V,T,T_).              % (Let-Var)
eval1(S,let(X,V,T),[X=V|S],T) :- v(V).                           % (Let-Value)
eval1(S,let(X,T,U),S_,let(X,T_,U)) :- eval1(S,T,S_,T_).          % (Ctx)

% 複数ステップ実行
eval(S,T,S_,T_) :- writeln(T),eval1(S,T,S1,T1),!,eval(S1,T1,S_,T_). 
eval(S,T,S,T) :- nl.

eval(T,T_) :- eval([],T,_,T1), a(T1,T_).

:- eval(lam(x,x),R),R=lam(x,x).
:- eval(let(xx,lam(x,x),let(yy,lam(y,y),app(xx,yy))),R),R=lam(y,y).
:- eval(let(xx,lam(x,x),let(yy,lam(y,y),let(zz,lam(z,z),let(yyzz,app(yy,zz),app(xx,yyzz))))),R),R=lam(z,z).
:- halt.

cbn.pl

% 値
v(N) :- integer(N).
v(lam(X,_)) :- atom(X).

% 式を文脈と、パラメータに分ける
e(E,[],E).
e(app(E,T),app(E2,T),H):-e(E,E2,H).
e(add(V,E),add(V,E2),H):-v(V),e(E,E2,H).
e(add(E,T),add(E2,T),H):-e(E,E2,H).

% 置換
subst(X,T,X,T).
subst(X,T,lam(X1,T1),lam(X1,T1_)) :- subst(X,T,T1,T1_), X \=X1.
subst(X,T,app(T1,T2),app(T1_,T2_)) :- subst(X,T,T1,T1_), subst(X,T,T2,T2_).
subst(X,T,add(T1,T2),add(T1_,T2_)) :- subst(X,T,T1,T1_), subst(X,T,T2,T2_).
subst(_,_,E,E).

% ワンステップ実行
eval1(app(lam(X,T),U), T_) :- subst(X,U, T,T_).
eval1(add(V1,V2), V) :- v(V1),v(V2), V is V1 + V2.
% 評価文脈を使った実行
eval1(Et,Et_) :-
	e(Et,E,T1), Et \= T1, % 文脈を取り出すけど、EtとT1が同じだと無限ループするので排除
	eval1(T1,T1_),!,
	subst([],T1_,E,Et_). % 文脈の穴を置き換える

% 複数ステップ実行
eval(T,T_) :- writeln(T),eval1(T,T1),eval(T1,T_). 
eval(T,T) :- nl.

:- eval(lam(x,x),R),R=lam(x,x).
:- eval(app(lam(x,x),lam(y,y)),R),R=lam(y,y).
:- eval(app(lam(x,x),1),R),R=1.
:- eval(app(lam(x,x),app(lam(y,y),lam(z,z))),R),R=lam(z,z).
:- eval(app(lam(x,x),app(lam(y,y),1)),R),R=1.
:- eval(app(lam(x,add(x,x)),app(lam(y,y),1)),R),R=2.
:- eval(app(app(lam(x,lam(y,add(x,y))),1),2),R),R=3.
:- halt.

cbv.pl

% 値
v(N) :- integer(N).
v(lam(X,_)) :- atom(X).

% 式を文脈と、パラメータに分ける
e(E,[],E).
e(app(V,E),app(V,E2),H):-v(V),e(E,E2,H).
e(app(E,T),app(E2,T),H):-e(E,E2,H).
e(add(V,E),add(V,E2),H):-v(V),e(E,E2,H).
e(add(E,T),add(E2,T),H):-e(E,E2,H).

% 置換
subst(X,T,X,T).
subst(X,T,lam(X1,T1),lam(X1,T1_)) :- subst(X,T,T1,T1_), X \=X1.
subst(X,T,app(T1,T2),app(T1_,T2_)) :- subst(X,T,T1,T1_), subst(X,T,T2,T2_).
subst(X,T,add(T1,T2),add(T1_,T2_)) :- subst(X,T,T1,T1_), subst(X,T,T2,T2_).
subst(_,_,E,E).

% ワンステップ実行
eval1(app(lam(X,T),V), T_) :- v(V), subst(X,V, T,T_).
eval1(add(V1,V2), V) :- V is V1 + V2.

% 評価文脈を使った実行
eval1(Et,Et_) :-
	e(Et,E,T1), Et \= T1, % 文脈を取り出し、無限ループ防止
	eval1(T1,T1_),!,
	subst([],T1_,E,Et_). % 文脈の穴を置き換える

% 複数ステップ実行
eval(T,T_) :- writeln(T),eval1(T,T1),eval(T1,T_). 
eval(T,T) :- nl.

:- eval(lam(x,x),R), R=lam(x,x).
:- eval(app(lam(x,x),lam(y,y)),R), R=lam(y,y).
:- eval(app(lam(x,x),1),R), R=1.
:- eval(app(lam(x,x),app(lam(y,y),lam(z,z))),R), R=lam(z,z).
:- eval(app(lam(x,x),app(lam(y,y),1)),R), R=1.
:- eval(app(lam(x,add(x,x)),app(lam(y,y),1)),R), R=2.
:- eval(app(app(lam(x,lam(y,add(x,y))),1),2),R), R=3.
:- halt.

standard_call_by_need.pl

/*
Standard call-by-need reduction.

Syntactic Domains

Variables           x,y,z
Values              V,W   ::= λx.T
Terms               S,T,U ::= V | T U
Answers             A,Ai  ::= λx.T | let x = T in A
Evaluation Contexts E,Ei  ::= [] | E T | let x = T in E
                                 | let x = E0 in E1[x]

Standard Reduction Rules

(Is) (λx.T) U                        -> let x = U in T
(Vs) let x = V in E[x]                -> let x = V in E[V]
(Cs) (let x = S in A) U               -> let x = S in A U
(As) let y = (let x = S in A) in E[y] -> let x = S in let y = A in E[y]

References

[1] Z. M. Ariola and M. Felleisen. The call-by-need lambda calculus.
Journal of Functional Programming, 7(3):265–301, 1997.
[2] Z. M. Ariola, M. Felleisen, J. Maraist, M. Odersky, and P. Wadler.
A call-by-need lambda calculus. In P. Lee, editor, Proceedings of
the Twenty-Second Annual ACM Symposium on Principles of Programming
Languages, pages 233–246, San Francisco, California, Jan.
1995. ACM Press.
[3] DANVY, Olivier; ZERNY, Ian. A synthetic operational account of
call-by-need evaluation. In: Proceedings of the 15th Symposium on
Principles and Practice of Declarative Programming.
ACM, 2013. p. 97-108.
*/
:- initialization(main).
:- op(920, xfx, [ --->, -->> ]).
:- op(500, yfx, $).
:- op(1200, xfx, [ -- ]).
term_expansion(A -- B, B :- A).

% Values
v(X) :- atom(X).
v(X->_) :- atom(X).
v(N) :- integer(N).

% Answers
a(N,N) :- integer(N).
a(X->T,X->T).
a(let(_=_,A),A_) :- a(A,A_).

% e(expression,evaluation contexts,param)
e(E,[],E).
e(let(X=T,E),let(X=T,E_),H):- e(E,E_,H).
e(let(X=E0,E1x),let(X=E0_,E1x),H):- e(E0,E0_,H), e(E1x,_,X).
e(E$T,E_$T,H):-e(E,E_,H).
e(E+T,E_+T,H):-e(E,E_,H).
e(T+E,T+E_,H):-e(E,E_,H).

subst(X,T,X,T).
subst(X,T,X1->T1,X1->T1_) :- subst(X,T,T1,T1_), X \=X1.
subst(X,T,T1$T2,T1_$T2_) :- subst(X,T,T1,T1_), subst(X,T,T2,T2_).
subst(X,T,T1+T2,T1_+T2_) :- subst(X,T,T1,T1_), subst(X,T,T2,T2_).
subst(X,T,let(X1=T1,T2),let(X1=T1_,T2_)) :- subst(X,T,T1,T1_), subst(X,T,T2,T2_), X\=X1.
subst(_,_,E,E).

% one step
/*(Is)*/            (X->T)$U ---> let(X=U,T).
/*(Vs)*/         let(X=V,Ex) ---> let(X=V,EV) :- v(V),e(Ex,E,X),subst([],V,E,EV).
/*(Cs)*/        let(X=S,A)$U ---> let(X=S,A$U) :- a(A,_).
/*(As)*/let(Y=let(X=S,A),Ey) ---> let(X=S,let(Y=A,Ey)) :-a(A,_),e(Ey,_,Y).
                       A1+A2 ---> N :- a(A1,N1),a(A2,N2), integer(N1),integer(N2), N is N1 + N2.
/*evaluation contexts*/   Et ---> Et_ :- e(Et,E,T), Et \= T, T ---> T_,!, subst([],T_,E,Et_).

% multi step
T -->> T_ :- writeln(T),T ---> T1,!,T1 -->> T_. 
T -->> T_ :- a(T,T_),(T=T_;writeln(T_)),nl,!.

% tests
:- e(let(x=(y->y),x),E,P), E:P=let(x=(y->y),[]):x.
:- e(let(x=(y->y),x$x),E,P), E:P=let(x=(y->y),[]$x):x; writeln("error";E:P),fail.
:- e(y->y,E,P), E:P=[]:(y->y).
:- e(let(y=(z->z),y),E,P), E:P=let(y=[],y):(z->z); writeln("error";E:P),fail.
:- e(let(x=let(y=(z->z),y),x),E,P), E:P=let(x=let(y=[],y),x):(z->z);writeln("error";E:P),fail.

:- (x->x) -->> R, R=(x->x).
:- (x->x)$(y->y) -->> R, R=(y->y).
:- (x->x)$((y->y)$(z->z)) -->> R, R=(z->z).
:- 1 -->> R, R=1.
:- (x->x)$((y->y)$1)-->>R, R=1.
:- ((x->x+x)$((y->y)$1))+((z->z)$10)-->>R, R=12.
:- (x->y->x+y)$1$2-->>R, R=3.
:- let(x=let(y=2,y+1),((z->z)$x+1)+let(y=x,y+x))-->>R, R=10.
:- ((z->z)$1)+((z->z)$2)-->>R, R=3.
:- let(x=1,(z->z)$x)+let(x=2,(z->z)$x)-->>R, R=3.
:- halt.