(* Normalization by evaluation for untyped lambda terms AM Pitts 30/05/03 *) (* syntax *) type t;; type var = t name;; type term = Var of var | Lam of <>term | App of term*term;; (* semantics *) type sem = L of ((unit -> sem) -> sem) | N of neu and neu = V of var | A of neu*sem;; (* reification reify : sem -> term *) let rec reify d = match d with L f -> let x=fresh in Lam(<>(reify(f(function () -> N(V x))))) | N n -> reifyn n and reifyn n = match n with V x -> Var x | A(n',d') -> App(reifyn n', reify d');; (* evals : (var * (unit->sem))list -> term -> sem *) let rec evals env t = match t with Var x -> (match env with [] -> N(V x) | (x',v)::env -> if x=x' then v() else evals env (Var x)) | Lam(<>t) -> L(function v -> evals ((x,v)::env) t) | App(t1,t2) -> (match evals env t1 with L f -> f(function () -> evals env t2) | N n -> N(A(n,evals env t2)));; (* evaluation eval : term -> sem *) let rec eval t = evals [] t;; (* normalisation norm:lam -> lam *) let norm t = reify(eval t);; (* equal : term * term -> bool Claim: equal(t1,t2)=true iff t1 and t2 are normalisable and have the same normal form, up to alpha-equivalence *) let equal(t1,t2) = ((norm t1)=(norm t2));; (* examples *) let a,b,c=fresh,fresh,fresh;; let s = Lam(<>( Lam(<>( Lam(<>( App(App(Var a,Var c), App(Var b,Var c))))))));; let k = Lam(<>(Lam(<>(Var a))));; let i = Lam(<>(Var a));; let l = Lam(<>i);; let p = Lam(<>( Lam(<>( Lam(<>( App(App(Var c,Var a),Var b)))))));; let p1 = Lam(<>(App(Var c,k)));; let p2 = Lam(<>(App(Var c,l)));; let omega = Lam(<>(App(Var a, Var a)));; let y = Lam(<>( App(Lam(<>(App(Var a, App(Var b,Var b)))), Lam(<>(App(Var a, App(Var b,Var b)))))));; (* tests *) let t = App(App(App(s,k),k),i);; (* the normal form of this is i *) (norm t) = i;; let i1 = App(p2,App(App(p,s),k));;(* the normal form of this is k *) (norm i1) = k;; let tm = App(l, App(omega,omega));; (* the normal form of this is i *) (norm tm) = i;; let loop = App(y,i);; (* fixpoint of the identity, has no normal form *) (* so don't try this at home norm loop;; *)