% 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.