% Lambda Calculus with call/comp / 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. And the reduction rules for delimited % continuations are taken from "How to remove a dynamic prompt" by % Oleg Kiselyov. % ---- Notations defop '\$', left, 2500. % application % ---- Grammar % x := typedef x(L) :- atom(L). % v := lambda x.e ... abstraction % | succ ... successor function % | ... constant % | call/comp ... capture delimited continuation % | comp M ... delimited continuation object typedef v(L) { L = lambda(X, E) :- x(X), e(E). L = succ. :- int(L). L = call_comp. L = comp(Hole, Body) :- m(Hole, Body). } % e := e e ... application % | x ... variable % | v ... value % | reset e ... prompt typedef e(L) { L = E1 \$ E2 :- e(E1), e(E2). :- x(L). :- v(L). L = reset \$ E :- e(E). } % --- Evaluation Context % M := [] | M e | v M typedef m(Redex, Body) { Body = Redex. Body = M \$ E :- m(Redex, M), e(E). Body = V \$ M :- v(V), m(Redex, M). } % C := M | C[reset M] typedef c(Redex, Body) { :- m(Redex, Body). Redex2 = reset \$ M :- c(Redex2, Body), m(Redex, M). } % --- 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[reset M[call/comp v]] -> C[reset (v (comp M))] expr = \$c[reset \$ \$m[call_comp \$ \$v]] :- c(\$c), m(\$m), v(\$v) | expr = \$c[reset \$ (\$v \$ comp(Hole, \$m[Hole]))]. % C[reset v] -> C[v] expr = \$c[reset \$ \$v] :- c(\$c), v(\$v) | expr = \$c[\$v]. % C[(comp M) v] -> C[reset M[v]] expr = \$c[comp(Hole, \$m[Hole]) \$ \$v] :- c(\$c), m(\$m), v(\$v) | expr = \$c[reset \$ \$m[\$v]]. % --- Example expr = succ \$ (reset \$ (succ \$ (call_comp \$ lambda(x, x \$ (x \$ 1))))).