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 = let 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 in aux n e end;

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 = let 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))); in aux e [] end;

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", "+", "λmnfx.mf(nfx)", "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"; xyzw val it = App (App (App #,Var #),Var "w") : Exp - e "(\\vxx'x''.vxx'x'')xyzw"; 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"); (λx'x''x'''.xx'x''x''')yzw 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"))); (λx.M(xx))(λx.M(xx)) (λxy.y(xxy))(λx.M(xx)) (λxy.y(xxy))(λxy.y(xxy)) val it = App (Lambda ("x",Lambda #),Lambda ("x",Lambda #)) : Exp

Nice. And we can do factorials:

- e "H4"; λfx.f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(fx))))))))))))))))))))))) 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.