% Lambda Calculus with call/cc / Kota Nara, Ueda Lab. % The example is taken from "A Semantics for Context-Sensitive % Reduction Semantics" by Casey Klein, Jay McCarthy, Steven Jaconette, % and Robert Bruce Findler. % ---- Notations defop '\$', left, 2500. % application % ---- Grammar % x := typedef x(L) :- atom(L). % v := lambda x.e ... abstraction % | succ ... successor function % | ... constant % | call/cc ... capture continuation % | cont C ... continuation object typedef v(L) { L = lambda(X, E) :- x(X), e(E). L = succ. :- int(L). L = call_cc. L = cont(Hole, Body) :- c(Hole, Body). } % e := e e ... application % | x ... variable % | v ... value typedef e(L) { L = E1 \$ E2 :- e(E1), e(E2). :- x(L). :- v(L). } % --- Evaluation Context % C := [] | C e | v C typedef c(Redex, Body) { Body = Redex. Body = C \$ E :- c(Redex, C), e(E). Body = V \$ C :- v(V), c(Redex, C). } % --- Utility Rules (substitution) % (e1 e2){x/v} = e1{x/v} e2{x/v} define Ret = subst(E1 \$ E2, \$x, \$v) :- ground(\$x, \$v) | Ret = subst(E1, \$x, \$v) \$ subst(E2, \$x, \$v). % (lambda x1 e){x2/v} = lambda x1 e (if x1 = x2) % | lambda x1 e{x2/v} (otherwise) define Ret = subst(lambda(\$x1, E), \$x2, \$v) :- { \$x1 == \$x2, ground(\$v) | Ret = lambda(\$x1, E). ground(\$x1, \$x2, \$v) | Ret = lambda(\$x1, subst(E, \$x2, \$v)). } % x1[x2/v] = v (if x1 = x2) % | x1 (otherwise) define Ret = subst(\$x1, \$x2, \$v) :- { \$x1 == \$x2, ground(\$v) | Ret = \$v. atom(\$x1), ground(\$x2, \$v) | Ret = \$x1. } % --- Reduction Rules % C[(lambda x.e1) e2] -> C[e1{x/e2}] expr = \$c[lambda(X, E1) \$ E2] :- c(\$c) | expr = \$c[subst(E1, X, E2)]. % C[succ v] -> C[v + 1] expr = \$c[succ \$ \$v] :- c(\$c), int(\$v) | expr = \$c[\$v + 1]. % C[call/cc v] -> C[v (cont C)] expr = \$c[call_cc \$ \$v] :- c(\$c), v(\$v) | expr = \$c[\$v \$ cont(Hole, \$c[Hole])]. % C_1[(cont C_2) v] -> C_2[v] expr = \$c1[cont(Hole, \$c2[Hole]) \$ \$v] :- c(\$c1), c(\$c2), v(\$v) | expr = \$c2[\$v]. % --- Example expr = succ \$ (call_cc \$ lambda(cc, succ \$ (cc \$ 1))).