(* Lambda Calculus Interpreter *)
(* First, a set signature and structure... *)
signature SET = sig
type ''a t
val empty : ''a t
val singleton : ''a -> ''a t
val fromList : ''a list -> ''a t
val toList : ''a t -> ''a list
val toString : (''a -> string) -> ''a t -> string
val isEmpty : ''a t -> bool
val member : ''a -> ''a t -> bool
val insert : ''a -> ''a t -> ''a t
val delete : ''a -> ''a t -> ''a t
val union : ''a t -> ''a t -> ''a t
val intersection : ''a t -> ''a t -> ''a t
val difference : ''a t -> ''a t -> ''a t
end
structure ListSet :> SET = struct
type ''a t = ''a list
val empty = []
fun singleton x = [x]
fun fromList xs = xs
fun toList xs = xs
fun toString f xs =
let fun stringify [] s = s
| stringify [x] s = (s ^ (f x))
| stringify (x::xs) s = stringify xs (s ^ (f x) ^ ", ")
in (stringify xs "{ ") ^ " }" end
fun isEmpty [] = true
| isEmpty _ = false
fun member x xs = List.exists (fn y => x=y) xs
fun insert x xs = if member x xs then xs else x::xs
fun delete x [] = []
| delete x (y::ys) = if x=y then ys else y :: delete x ys
fun union [] ys = ys
| union (x::xs) ys = union xs (insert x ys)
fun intersection xs [] = []
| intersection xs ys =
let fun i [] ys set = set
| i (x::xs) ys set = i xs ys (if member x ys then x::set else set)
in i xs ys [] end
fun difference xs [] = xs
| difference [] ys = []
| difference xs (y::ys) = difference (if member y xs
then delete y xs
else xs)
ys
end
(* Lambda Calculus abstract syntax. *)
type var = string
datatype expr = Var of var (* x *)
| Lambda of var * expr (* (\x.e) *)
| Apply of expr * expr (* (e1 e2) *)
(* Compute free variables of an expression. *)
fun free (Var x) = ListSet.singleton x
| free (Lambda (x,e)) = ListSet.delete x (free e)
| free (Apply (e1,e2)) = ListSet.union (free e1) (free e2)
(* alpha-renaming rule
Substitutes a fresh variable for all uses of the given variable
in the given expression. *)
val rename =
let val counter = ref 0
fun rename x e =
let val x' = x ^ "_" ^ (Int.toString (!counter))
val _ = counter := (!counter + 1)
fun rn (e as Var y) = if x=y then (Var x') else e
| rn (e as Lambda (y,el)) = if x=y
then e
else Lambda (y,rn el)
| rn (Apply (e1,e2)) = Apply (rn e1, rn e2)
in (x',rn e) end
in rename end
(* alias rename *)
val alpha = rename
(* Substitution rule
subst : expr -> var Set.t -> var -> expr -> expr *)
fun subst N fv x (v as Var y) = if x=y then N else v
| subst N fv x (l as Lambda (y,e)) =
if x=y then l else
let val (y',e') = if ListSet.member y fv
then rename y e
else (y,e)
in Lambda (y', subst N fv x e') end
| subst N fv x (Apply (e1,e2)) =
Apply (subst N fv x e1, subst N fv x e2)
(* eta-reduction rule
unwrap : *)
fun unwrap (l as Lambda (x,Apply (e,Var y))) =
unwrap (if x=y then e else l)
| unwrap (Lambda (x,e)) = Lambda (x, unwrap e)
| unwrap (Apply (e1,e2)) = Apply (unwrap e1, unwrap e2)
| unwrap e = e
val eta = unwrap
(* beta-reduction rule, with output describing steps.
reduce_show : expr -> string *)
fun reduce_show e =
let fun show e =
let fun show (Var x) = x
| show (Lambda (x,e)) = "(\\" ^ x ^ "." ^ (show e) ^ ")"
| show (Apply (e1,e2)) =
"(" ^ (show e1) ^ " " ^ (show e2) ^ ")"
in print ((show e) ^ "\n") end
fun reduce both pad (e as Var x) = e
| reduce both pad (l as Lambda (x,e)) =
let val _ = print (pad ^ "In lambda: ")
val _ = show l
val z = Lambda (x,reduce both (pad ^ "| ") e)
val _ = print (pad ^ "Yields: ")
val _ = show z
in z end
| reduce both pad (app as Apply (e1,e2)) =
let val _ = print (pad ^ "In: ")
val _ = show app
in
(case (reduce both (pad ^ "| ") e1,
if both then reduce both (pad ^ "| ") e2 else e2) of
(l as Lambda (x,e), a) =>
let val _ = print (pad ^ "Apply: ")
val _ = show (Apply (l, a))
val z = reduce both (pad ^ "| ") (subst a (free a) x e)
val _ = print (pad ^ "Yields: ")
val _ = show z
in z end
| e =>
let val _ = print (pad ^ "Apply: ")
val _ = show (Apply e)
val _ = print (pad ^ "Yields: ")
val _ = show (Apply e)
in Apply e end)
end
in reduce true "" (reduce false "" e) end
(* beta-reduction rule
reduce : expr -> string *)
fun reduce e =
let fun r _ (e as Var x) = e
| r both (l as Lambda (x,e)) = Lambda (x,r both e)
| r both (app as Apply (e1,e2)) =
(case (r both e1, if both then r both e2 else e2) of
(l as Lambda (x,e), a) => r both (subst a (free a) x e)
| e => Apply e)
in r true (r false e) end
(*********** Church encodings ***********)
(* Booleans and conditionals *)
val t = Lambda ("u", Lambda ("v", Var "u"))
val f = Lambda ("u", Lambda ("v", Var "v"))
val cond = Lambda ("u",
Lambda ("v",
Lambda ("w",
(Apply (Apply (Var "u",
Var "v"),
Var "w")))))
(* Pairs *)
val pair = Lambda ("m", Lambda ("n", Lambda ("b", Apply (Apply (Apply (cond, Var "b"), Var "m"), Var "n"))))
val first = Lambda ("p", Apply(Var "p", t))
val second = Lambda ("p", Apply(Var "p", f))
(* Function that takes an ML int and returns a Church Numeral for it. *)
fun n x =
let fun make 0 = Var "z"
| make x = Apply (Var "s", make (x-1))
in Lambda ("s", Lambda ("z", make x)) end
(* Successor *)
val succ = Lambda ("n", Lambda ("s", Lambda ("z", Apply (Var "s", Apply (Apply (Var "n", Var "s"), Var "z")))))
(* Addition *)
val plus = Lambda ("m", Lambda ("n", Lambda ("s", Lambda ("z", Apply (Apply (Var "m", Var "s"), Apply (Apply (Var "n", Var "s"), Var "z"))))))
(* Multiplication *)
val mult = Lambda ("n", Lambda ("m", Apply( Apply (Var "m", Apply (plus, Var "n")), n 0)))
(* check for zero *)
val isZero = Lambda ("n", Apply (Apply (Var "n", Lambda ("x", f)), t))
(* Support for subtraction *)
val pZero = Apply (Apply (pair, n 0), n 0)
val pSucc = Lambda ("n", Apply (Apply (pair, Apply (second, Var "n")),
Apply (succ, Apply (second, Var "n"))))
(* Predecessor *)
val pred = Lambda ("n", Apply (first, Apply (Apply (Var "n", pSucc), pZero)))
(* Y combinator. *)
val Y = Lambda ("f", Apply (Lambda ("x", Apply (Var "f", Apply (Var "x", Var "x"))),
Lambda ("x", Apply (Var "f", Apply (Var "x", Var "x")))))
(* Factorial: recursion using Y combinator. *)
val fact = Apply (Y, Lambda ("f", Lambda ("n", Apply (Apply (Apply (cond, Apply (isZero, Var "n")), n 1), Apply (Apply (mult, Var "n"), Apply (Var "f", Apply (pred, Var "n")))))))
(************** Numeral-aware show function *************)
fun show (Lambda (s, (Lambda (z, e)))) =
let fun sn (Var z') = if z=z' andalso String.isPrefix "z" z
then SOME 0 else NONE
| sn (Apply (Var s', e')) = if s=s' andalso String.isPrefix "s" s
then case sn e' of
SOME n => SOME (n + 1)
| NONE => NONE
else NONE
| sn _ = NONE
in case sn e of
SOME n => Int.toString n
| NONE => "(\\" ^ s ^ "." ^ "(\\" ^ z ^ "." ^ (show e) ^ "))"
end
| show (Var x) = x
| show (Lambda (x,e)) = "(\\" ^ x ^ "." ^ (show e) ^ ")"
| show (Apply (e1,e2)) =
"(" ^ (show e1) ^ " " ^ (show e2) ^ ")"
fun rs e =
let val _ = print ((show e) ^ "\n")
val e' = reduce e
val _ = print ("=> " ^ (show e') ^ "\n")
in e' end
val sr = rs