(* 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;;
*)
**