# let id = Abs("x",Var "x");; # let k = Abs("x",Abs("y",Var "x"));; # let omega = App(Abs("x",App(Var "x",Var "x")),Abs("x",App(Var "x",Var "x")));; # let const z = Abs("x",Var z);;
# let rec string_of_term t = match t with Var x -> x | Abs (x,t') -> "\\" ^ x ^ "." ^ string_of_term t' | App (t0,t1) -> "(" ^ (string_of_term t0) ^ " " ^ (string_of_term t1) ^ ")";;
# print_string (string_of_term id);; # print_string (string_of_term k);; # print_string (string_of_term omega);;
# type 'a set = Set of 'a list;; # let emptyset = Set [];; # let rec member x s = match s with Set [] -> false | Set (y::s') -> x=y or (member x (Set s'));; # let rec union s t = match s with Set [] -> t | Set (x::s') -> (match union (Set s') t with Set t' -> if member x t then Set t' else Set (x::t'));; # let rec diff s x = match s with Set [] -> s | Set (y::s') -> (match diff (Set s') x with Set t' -> if x=y then Set s' else Set (y::t'));;
# let rec fv t = match t with Var x -> Set [x] | App(t0,t1) -> union (fv t0) (fv t1) | Abs(x,t0) -> diff (fv t0) x;;
# fv omega;; # fv (const "z");; # fv (Abs ("x", App(Var "x",Var "y")));;
# let count = ref(-1);; # let gensym = fun () -> count := !count +1; "x" ^ string_of_int (!count);; # let rec subst x t' t = match t with Var y -> if x=y then t' else Var y | App(t0,t1) -> App(subst x t' t0, subst x t' t1) | Abs(y,t0) when y=x -> Abs(x,t0) | Abs(y,t0) when y!=x && not (member y (fv t')) -> Abs(y, subst x t' t0) | Abs(y,t0) when y!=x && member y (fv t') -> let z = gensym() in Abs(z,subst x t' (subst z (Var y) t0));;
# let isredex t = match t with App(Abs(x,t0),t1) -> true | _ -> false;; # let rec hasredex t = match t with Var x -> false | Abs(x,t') -> hasredex t' | App(t0,t1) -> isredex t or hasredex t0 or hasredex t1;; # exception Error;; # let rec reduce1 t = if not (hasredex t) then t else match t with Abs(x,t') -> Abs(x,reduce1 t') | App(Abs(x,t0),t1) -> subst x t1 t0 | App(t0,t1) -> if hasredex t0 then App(reduce1 t0,t1) else App(t0,reduce1 t1);; # let rec reduce t k = if k=0 then t else let t' = reduce1 t in reduce t' (k-1);; # let rec reducefix t = let t' = reduce1 t in if t'=t then t' else reducefix t';; # reduce (App((const "z"),omega)) 1;;