matthew arcus

Lambda Interpreter, Part II, Semantics

First thing, we need to be able to define identifiers, at least at the top level, for S, K, I, etc. A simple list of string-value pairs will do, we will fill in our default environment later:

fun getenv [] v = NONE
  | getenv ((v',e)::s) v =
    if (v = v') then SOME e else getenv s v;

(* Make an environment from a list of strings *)
fun mkenv [] k = k
  | mkenv (v::e::s) k = mkenv s ((v,parse e)::k)

We will define two evaluation mechanisms, one will reduce one redex at a time, with the index of the redex passed in to the function, the other will just reduce until a normal form is reached, if there is one.

It’s convenient to use option types to indicate if a subexpression has been reduced, and it’s even more convenient to define some monadic-style helper functions:

fun lift f NONE = NONE
  | lift f (SOME x) = SOME (f x);

fun bind f NONE = NONE
  | bind f (SOME a) = f a;

(* Apply f to a, if no result, apply g to b *)
fun try f a g b = case f a of r as SOME _ => r | NONE => g b;

fun get (SOME x) = x;

Here’s the single redex reducer: try to reduce each subexpression, keeping track of redex indexes. Return SOME(e') if a sub evaluation succeeds, else return NONE with some monadic trickery to handle the mechanics. We avoid expanding global identifiers unless they are in functional position.

fun reduce env n e =
    fun aux n (Var _) = NONE
      | aux 0 (App(Lambda(v,e1),e2)) = SOME (subst v e2 e1)
      | aux n (App(Lambda(v,e1),e2)) =
	try (lift (fn e1' => App(Lambda(v,e1'),e2)) o aux (n-1)) e1
	    (lift (fn e2' => App(Lambda(v,e1),e2')) o aux (n-1)) e2
      | aux n (App(e1 as Var v,e2)) =
	try (bind (fn e1' => aux n (App(e1',e2))) o getenv env) v
	    (lift (fn e2' => App(e1,e2')) o aux n) e2
      | aux n (App(e1,e2)) =
	try (lift (fn e1' => App(e1',e2)) o aux n) e1
	    (lift (fn e2' => App(e1,e2')) o aux n) e2
      | aux n (Lambda(v,e1)) =
	(lift (fn e1' => Lambda(v,e1')) o aux n) e1
      aux n e

That’s all very well for reducing individual redexes, let’s define something that will just let rip on an expression. We’d like to do a proper normal order evaluation, so we’ll use an evaluation stack: go down left branch of expression, reducing beta redexes as we go. When we have got to the end, there are no more top-level redexes, so recursively evaluate the items on the stack, and finally fold back up in into a single expression:

fun eval env e = 
    fun foldapp(e1::e2::s) = foldapp(App(e1,e2)::s)
      | foldapp ([e1]) = e1;
    fun aux (Lambda(v,e1)) (e2::s) = aux (subst v e2 e1) s
      | aux (Lambda(v,e1)) [] = Lambda(v, eval env e1)
      | aux (App(e1,e2)) s = aux e1 (e2::s)
      | aux (e as Var _) [] = e
      | aux (e as Var v) s = 
        (case getenv env v of
             SOME e' => aux e' s
           | _ => foldapp (map (eval env) (e::s)));
    aux e []

All we need now is a suitable environment, and we can start reducing.

val stdenv =
    mkenv ["S", "λxyz.(xz)(yz)",
	   "K", "λxy.x",
	   "I", "λx.x",
	   "Y", "λf.(λx.f(xx))(λx.f(xx))",
	   "M", "λxy.y(xy)",
	   "T", "λxy.x",
	   "F", "λxy.y",
	   "Z", "λn.n(λx.F)T",
	   "0", "λf.λn.n",
	   "N", "λn.λf.λx.f(nfx)",
	   "P", "λnfx.n(λgh.h(gf))(λu.x)(λu.u)",
	   "*", "λmnfx.m(nf)x",
	   "+", "λ",
	   "1", "N0",
	   "2", "N1",
	   "3", "N2",
	   "4", "N3",
	   "5", "N4",
	   "6", "N5",
	   "7", "N6",
	   "8", "N7",
	   "9", "N8",
	   "H", "Y(λgn.(Zn)1(*n(g(Pn))))"
	  ] [];

As well as the usual suspects, M is my favourite combinator. T and F help define conditionals, and there is the usual definition of Church numerals. H, obviously, is the factorial function.

Finally, we define some convenience functions:

fun run e =
  case reduce stdenv 0 (pp e) of
    SOME e' => run e'
  | NONE => e;

(* Evaluate first redex *)
fun e0 e = pp (get (reduce stdenv 0 e));
(* Evaluate second redex *)
fun e1 e = pp (get (reduce stdenv 1 e));
(* Evaluate a symbol *)
fun esym s = pp (get (getenv stdenv s));
(* Evaluate to normal form *)
fun e s = pp (eval stdenv (parse s));

And now at last we can do some reductions:

First we probably should check that variable capture is handled properly:

- e "(\\abcd.abcd)xyzw";
val it = App (App (App #,Var #),Var "w") : Exp
- e "(\\vxx'x''.vxx'x'')xyzw";
val it = App (App (App #,Var #),Var "w") : Exp

It’s interesting that in the first reduction of the latter, there is a sort of cascade of primes being added:

- e0 (parse "(\\vxx'x''.vxx'x'')xyzw");
val it = App (App (App #,Var #),Var "w") : Exp

Anyway, that seems to check out so we can move on to something more interesting. Let’s derive the Turing fixpoint combinator from M and Y:

- e1(e1(e0(parse"YM")));
val it = App (Lambda ("x",Lambda #),Lambda ("x",Lambda #)) : Exp

Nice. And we can do factorials:

- e "H4";
val it = Lambda ("f",Lambda ("x",App #)) : Exp

The output is a little big to put inline, but the enthusiastic can try:

run (parse "H2");

See [[here]] for output.