shift/reset

shiftreset.pl

% shiftreset.pl
% http://pllab.is.ocha.ac.jp/~asai/cw2011tutorial/main-j.pdf

% 汎用構文定義用述語
:- op(1200,xfx,::=),op(600,xfx,∈).
G∈(G|_). G∈(_|G2):-!, G∈G2. G∈G. 
bnf(G,E):-G=..[O|Gs],E=..[O|Es],maplist(bnf,Gs,Es),!.
bnf(G,E):-(G::=Gs),!,G1∈Gs,bnf(G1,E),!.
bnf(i,I):-integer(I),!.
bnf(x,I):- atom(I),!.
% 汎用評価文脈用述語
hole([G|_]/G,[E|Es]/E,[H|Es]/H).
hole([_|Gs]/G,[E|Es]/E_,[E|Hs]/H):-hole(Gs/G,Es/E_,Hs/H).
evalctx([],E,E,H/H).
evalctx(G,E,V,H_/H):-G=..[O|Gs],E=..[O|Es],hole(Gs/G1,Es/E1,Hs/H1),
                     evalctx(G1,E1,V,H1/H),H_=..[O|Hs].
evalctx(G,E,V,H_/H):-(G::=Gs),G1∈Gs,evalctx(G1,E,V,H_/H).
% 汎用小ステップ評価用述語
small(F,G,E,E_):-evalctx(G,E,V,E_/H),call(F,V,H),writeln(E_).
all(F)-->call(F),all(F).
all(_)-->!.

% 構文
:- op(600, yfx, $), op(1000,xfx, ⇨).

v ::= i | x | λ(x,m).                                             % (値)
m ::= v | m+m | m $ m | let(x,m,m) | shift(x,m) | reset(m).       % (項)
f ::= f + m | v + f | f $ m | v $ f | let(x,f,m) | [].            % (純評価文脈)
e ::= e + m | v + e | e $ m | v $ e | let(x,e,m) | reset(e) | []. % (評価文脈)

fresh(Y):- retract(idval(X)),X1 is X+1,assert(idval(X1)),atomic_concat('_',X,Y).
subst(X,V,X,V):-!.
subst(X,_,λ(X,M),λ(X,M)):-!.
subst(X,V,λ(Y,M),λ(Y_,M_)):- fresh(Y_),subst(Y,Y_,M,M1),subst(X,V,M1,M_).
subst(X,V,M1$M2,M1_$M2_):- subst(X,V,M1,M1_),subst(X,V,M2,M2_).
subst(X,V,M1+M2,M1_+M2_):- subst(X,V,M1,M1_),subst(X,V,M2,M2_).
subst(X,V,let(X,M1,M2),let(X,M1_,M2)):-subst(X,V,M1,M1_).
subst(X,V,let(Y,M1,M2),let(Y_,M1_,M2_)):-subst(X,V,M1,M1_),fresh(Y_),subst(Y,Y_,M2,M21),subst(X,V,M21,M2_).
subst(X,_,shift(X,M),shift(X,M)):-!.
subst(X,V,shift(Y,M),shift(Y,M_)):-fresh(Y_),subst(Y,Y_,M,M1),subst(X,V,M1,M_).
subst(X,V,reset(M),reset(M_)):-subst(X,V,M,M_).
subst(_,_,M,M).

% 3.2 簡約規則

(λ(X, M)$ V) ⇨ M_                           :- bnf(v,V),subst(X,V,M,M_).
     I1 + I2 ⇨ I                            :- bnf(i,I1),bnf(i,I2), I is I1+I2.
let(X, V, M) ⇨ M_                           :- bnf(v,V), subst(X,V,M,M_).
    reset(V) ⇨ V                            :- bnf(v,V).
    reset(E) ⇨ reset(λ(K,V)$λ(X,reset(E_))) :- evalctx(f,E,shift(K,V),E_/X),
                                               fresh(X).

init():- retractall(idval(_)),assert(idval(0)).
run(M) :- run(M,_).
run(M,R) :- init(),bnf(m,M)->all(small(⇨,e),M,R);writeln(syntaxerror:M).

:- run((1+2+3)+4+5,R),!,R=15.
:- run(let(x,1+2+3,x),R),!,R=6.
:- run(λ(x,x+1)$1+2, R),!,R=4.
:- run(reset(1),R),!,R=1.
:- run(reset(1+1),R),!,R=2.
:- run(reset(shift(k,k)),R),R=λ(_0,reset(_0)).
:- run(reset(shift(k,k)+10)$1+2,R),R=13.
:- run(reset(shift(k,λ(x,k $ 5))+10)$1+2,R),R=15.
:- run(reset(shift(k,λ(x,k $ 5+x))+10)$1+2,R),R=18.

:- halt.