(* Michael R. Hansen, October 24, 2011 *) (* Revised October 21, 2013 *) (* Skeleton program for a simple lambda-calculus interpreter *) type Lambda = | L of string * Lambda | A of Lambda * Lambda | V of string | O of string | I of int | B of bool;; (* free: Lambda -> Set *) let rec free t = match t with | V x -> Set.singleton x | A(t1,t2) -> ... | L(x,t) -> ... | _ -> ... ;; (* nextVar: string -> string *) let nextVar = let n = ref 0 let f x = let s = x + "#" + string(!n) (n := !n+1; s) f;; (* subst: Lambda -> string -> Lambda -> Lambda *) let rec subst t x ta = match t with | L(y,t') when x=y -> ... | L(y,t') when Set.contains y (free ...) -> ... | L(y,t') -> ... | V y -> if x=y ... | A(t1,t2) -> ... | _ -> t;; (* One step normal-order reduction *) (* red: Lambda -> Lambda option *) let rec red t = match t with | A(A(O "=", I a), I b) -> Some(B(a=b)) | A(A(O "+", I a), I b) -> ... | A(A(O "-", I a), I b) -> ... | A(A(O "*", I a), I b) -> ... | A(A(A(O "ite", B true),t1),t2) -> ... | A(A(A(O "ite", B false),t1),t2) -> ... | L(x,t) -> match red t with | None -> ... | Some t' -> ... | A(L(x,t1),t2) -> ... | A(t1,t2) -> match red t1 with | Some t1' -> ... | None -> ... | _ -> None;; (* repeated normal-order reductions *) (* reduce: Lambda -> Lambda *) let rec reduce t = match red t with ... ;; let t1 = L("x",L("y", A(A(O "+", V "x"), V "y")));; let t2 = A(t1, I 3);; let t3 = A(t2, I 4);; let v3 = reduce t3;; let Y = let t = ... A(t,t);; let F = L("f",L("n",A( ... ;; let fact = A(Y,F);; let fac8 = A(fact,I 8);; let vfac8 = reduce fac8;;