% Left-to-Right Lambda Calculus / 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 typedef v(L) { L = lambda(X, E) :- x(X), e(E). L = succ. :- int(L). } % 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]. % --- Example expr = lambda(x, lambda(y, x \$ y)) \$ lambda(x, succ \$ 2) \$ 3.