(* ========================================================================= *) (* Untyped lambda calculus. *) (* *) (* Freek Wiedijk, Radboud University Nijmegen *) (* ========================================================================= *) open List;; let id x = x;; let ( ** ) f g x = f (g x);; let rec index s l = match l with [] -> raise Not_found | t::k -> if s = t then 0 else (index s k) + 1;; (* ------------------------------------------------------------------------- *) (* Type of lambda terms. *) (* ------------------------------------------------------------------------- *) type term = Const of string | App of term * term | Abstr of string * term | Var of int;; (* ------------------------------------------------------------------------- *) (* Reading lambda terms. *) (* ------------------------------------------------------------------------- *) let explode s = let rec explode1 n = try let s1 = String.make 1 s.[n] in s1::(explode1 (n + 1)) with Invalid_argument _ -> [] in explode1 0;; let implode l = fold_right (^) l "";; let lex l = let rec lex1 l = match l with [] -> [] | c::k -> if mem c [" "; "\t"; "\n"] then lex1 k else if mem c ["^"; "."; "("; ")"] then c::(lex1 k) else if c = "'" then failwith "lex" else lex2 [c] k and lex2 v l = match l with [] -> [implode v] | c::k -> if c = "'" then lex2 (v@[c]) k else (implode v)::(lex1 l) in lex1 l;; let parse l = let rec apps l = match l with [] -> failwith "parse" | [t] -> t | t::u::v -> apps (App(t,u)::v) in let rec parse1 c l = let t,k = parse2 c l in (apps t),k and parse2 c l = match l with [] -> [],[] | "^"::k -> let t,j = parse3 c k in [t],j | "."::_ -> failwith "parse" | "("::k -> (let t,j = parse1 c k in match j with ")"::i -> let u,h = parse2 c i in (t::u),h | _ -> failwith "parse") | ")"::_ -> [],l | s::k -> (let t = try Var(index s c) with Not_found -> Const(s) in let u,j = parse2 c k in (t::u),j) and parse3 c l = match l with [] -> failwith "parse" | "."::k -> parse1 c k | s::k -> if mem s ["^"; "("; ")"] then failwith "parse" else let t,j = parse3 (s::c) k in Abstr(s,t),j in let t,k = parse1 [] l in if k = [] then t else failwith "parse";; let term = parse ** lex ** explode;; (* ------------------------------------------------------------------------- *) (* Writing lambda terms. *) (* ------------------------------------------------------------------------- *) let term_to_string t = let rec term_to_string1 b1 b2 c t = match t with Const(s) -> s | Var(n) -> (try nth c n with Failure "nth" -> failwith "term_to_string") | App(f,x) -> let s = (term_to_string1 false true c f)^ (term_to_string1 true (not b1 & b2) c x) in if b1 then "("^s^")" else s | Abstr(v,a) -> let s = "^"^(term_to_string2 c t) in if b2 then "("^s^")" else s and term_to_string2 c t = match t with Abstr(v,a) -> v^(term_to_string2 (v::c) a) | _ -> "."^(term_to_string1 false false c t) in term_to_string1 false false [] t;; let alpha t = let rec occurs c t n v = match t with Const(w) -> v = w | Var(m) -> m > n & v = nth c m | App(f,x) -> (occurs c f n v) or (occurs c x n v) | Abstr(w,a) -> occurs (w::c) a (n + 1) v in let rec alpha1 c t = match t with App(f,x) -> App(alpha1 c f,alpha1 c x) | Abstr(v,a) -> alpha2 c a v | _ -> t and alpha2 c t v = if occurs (v::c) t 0 v then alpha2 c t (v^"'") else Abstr(v,alpha1 (v::c) t) in alpha1 [] t;; let print_term f t = Format.pp_print_string f ("term \""^(term_to_string (alpha t))^"\"");; (* #install_printer print_term;; *) (* ------------------------------------------------------------------------- *) (* Combinators. *) (* ------------------------------------------------------------------------- *) let combinators = ref (rev ["I", term "^x.x"; "K", term "^xy.x"; "S", term "^xyz.(xz)(yz)"; "B", term "^xyz.x(yz)"; "C", term "^xyz.xzy"; "W", term "^xy.xyy"; "1", term "^xy.xy"; "Y", term "^f.(^x.f(xx))(^x.f(xx))"; "T", term "^xy.x"; "F", term "^xy.y"; "D", term "^x.xx"; "J", term "^abcd.ab(adc)"; "C'", term "JII"]);; let unfold f = match f with Const(s) -> (try assoc s !combinators with Not_found -> f) | _ -> f;; (* ------------------------------------------------------------------------- *) (* Reduction. *) (* ------------------------------------------------------------------------- *) let rec lift d n t = match t with Var(m) -> if m >= n then Var(m + d) else Var(m) | App(f,x) -> App(lift d n f,lift d n x) | Abstr(v,a) -> Abstr(v,lift d (n + 1) a) | _ -> t;; let rec subst d n u t = match t with Var(m) -> if m = n then lift d 0 u else if m > n then Var(m - 1) else t | App(f,x) -> App(subst d n u f,subst d n u x) | Abstr(v,a) -> Abstr(v,subst (d + 1) (n + 1) u a) | _ -> t;; exception Normal;; let maybe f x = try f x with Normal -> x;; let beta i j t = match t with App(f,x) -> let f' = unfold f in (match f' with Abstr(_,a) -> subst 0 0 (maybe i x) (maybe i a) | _ -> if f' <> f then j (App(f',x)) else raise Normal) | _ -> raise Normal;; let current_beta = ref beta;; let current_eta = ref (fun i t -> raise Normal);; let rec leftmost_innermost t = match t with App(f,x) -> (try App(leftmost_innermost f,x) with Normal -> try App(f,leftmost_innermost x) with Normal -> !current_beta id leftmost_innermost t) | Abstr(v,a) -> (try Abstr(v,leftmost_innermost a) with Normal -> !current_eta id t) | _ -> raise Normal;; let rec leftmost_outermost t = match t with App(f,x) -> (try !current_beta id leftmost_outermost t with Normal -> try App(leftmost_outermost f,x) with Normal -> App(f,leftmost_outermost x)) | Abstr(v,a) -> (try !current_eta id t with Normal -> Abstr(v,leftmost_outermost a)) | _ -> raise Normal;; let rec parallel_outermost t = match t with App(f,x) -> (try !current_beta id parallel_outermost t with Normal -> try let g = parallel_outermost f in App(g,maybe parallel_outermost x) with Normal -> App(f,parallel_outermost x)) | Abstr(v,a) -> (try !current_eta id t with Normal -> Abstr(v,parallel_outermost a)) | _ -> raise Normal;; let rec gross_knuth t = match t with App(f,x) -> (try !current_beta gross_knuth gross_knuth t with Normal -> try let g = gross_knuth f in App(g,maybe gross_knuth x) with Normal -> App(f,gross_knuth x)) | Abstr(v,a) -> (try !current_eta gross_knuth t with Normal -> Abstr(v,gross_knuth a)) | _ -> raise Normal;; let rec reduce x z n t = if n = 0 then z else try let u = x t in t::(reduce x z (n - 1) u) with Normal -> [t];; let rec normal_form x t = try normal_form x (x t) with Normal -> t;; (* ------------------------------------------------------------------------- *) (* Abbrevs. *) (* ------------------------------------------------------------------------- *) let etc = [Const("...")];; let all = -1;; let nf = normal_form leftmost_outermost ** term;; let red n = reduce leftmost_outermost etc n ** term;; let red_eager n = reduce leftmost_innermost etc n ** term;; let red_par n = reduce parallel_outermost etc n ** term;; let red_gk n = reduce gross_knuth etc n ** term;; (* ------------------------------------------------------------------------- *) (* Examples. *) (* ------------------------------------------------------------------------- *) (* nf "(^x.fx)a";; nf "(KISS)(KISS)";; red_gk all "SKK";; red 7 "(^x.xx)(^x.xx)";; *) (* ========================================================================= *) (* Extra code for Jan-Willem *) (* ========================================================================= *) let rec free n t = match t with App(f,x) -> free n f && free n x | Abstr(_,t') -> free (n + 1) t' | Var(n') -> n <> n' | _ -> true;; let eta i t = match t with Abstr(_,App(f,Var(0))) -> if free 0 f then lift (-1) 0 (maybe i f) else raise Normal | _ -> raise Normal;; let translate e = let rec translate t = match t with App(f,x) -> App(translate f,translate x) | Abstr(v,u) -> if u = Var(0) then Const("I") else if free 0 u then App(Const("K"),translate (lift (-1) 0 u)) else (match translate u with Var(0) -> Const("I") | App(a,b) -> if e && b = Var(0) && free 0 a then lift (-1) 0 a else App(App(Const("S"),translate (Abstr(v,a))),translate (Abstr(v,b))) | _ -> failwith "translate") | _ -> t in translate;; let translate_henk e = let rec translate t = match t with App(f,x) -> App(translate f,translate x) | Abstr(v,u) -> if u = Var(0) then Const("I") else if free 0 u then App(Const("K"),translate (lift (-1) 0 u)) else (match translate u with Var(0) -> Const("I") | App(a,b) -> if free 0 a then if e && b = Var(0) then lift (-1) 0 a else App(App(Const("B"),lift (-1) 0 a),translate (Abstr(v,b))) else if free 0 b then App(App(Const("C"),translate (Abstr(v,a))),lift (-1) 0 b) else App(App(Const("S"),translate (Abstr(v,a))),translate (Abstr(v,b))) | _ -> failwith "translate") | _ -> t in translate;; let translate_church e = let tau = term "JII" in let _JI = term "JI" in let _J = term "J" in let _Jt = App(_J,tau) in let _Jtt = App(_Jt,tau) in let rec translate t = match t with App(f,x) -> App(translate f,translate x) | Abstr(v,u) -> if u = Var(0) then Const("I") else if free 0 u then App(Const("K"),translate (lift (-1) 0 u)) else (match translate u with Var(0) -> Const("I") | App(a,b) -> if free 0 a then if e && b = Var(0) then lift (-1) 0 a else App(App(App(_J,tau),translate (Abstr(v,b))), App(_JI,lift (-1) 0 a)) else if free 0 b then App(App(_Jt,lift (-1) 0 b),translate (Abstr(v,a))) else App(_Jtt,App(_JI,App(_Jtt, App(App(_Jt,translate (Abstr(v,b))), App(App(_Jt,translate (Abstr(v,a))),_J))))) | _ -> failwith "translate") | _ -> t in translate;; let rec term_size t = match t with App(f,x) -> term_size f + term_size x | Abstr(v,t') -> term_size t' + 1 | _ -> 1;; let rec equal t t' = if t = t' then true else let t = unfold t in let t' = unfold t' in match t with App(f,x) -> (match t' with App(f',x') -> equal f f' && equal x x' | _ -> false) | Abstr(_,u) -> (match t' with Abstr(_,u') -> equal u u' | _ -> false) | _ -> t = t';; let assoc' t l = let rec assoc' l = match l with [] -> raise Not_found | (v,t')::l' -> if equal t' t then v else assoc' l' in assoc' l;; let current_fold = ref id;; let rec fold t = try let v = assoc' t !combinators in Const(v) with _ -> match t with App(f,x) -> App(fold f,fold x) | Abstr(v,t') -> Abstr(v,fold t') | _ -> t;; let sub c1 c2 = implode ** map (fun c -> if c = c1 then c2 else c) ** explode;; let term_to_string' t = sub "^" "\\" (term_to_string (alpha t));; let rec occurs t' t = if equal t' t then true else match unfold t with App(f,x) -> occurs t' f || occurs t' x | Abstr(_,u) -> occurs t' u | _ -> false;; let rec flatten t = match t with App(f,x) -> let f',l' = flatten f in f',(l'@[x]) | _ -> t,[];; let rec unflatten (f,l) = match l with [] -> f | x::l' -> unflatten (App(f,x),l');; let rec lambda_count t = match t with Abstr(_,a) -> 1 + lambda_count a | _ -> 0;; let beta_combinator i j t = let rec red_combinator f l = if l = [] then f,l else match f with Abstr(_,a) -> (match l with [] -> failwith "beta_combinator" | x::l' -> red_combinator (subst 0 0 (maybe i x) a) l') | _ -> f,l in match t with App(f,x) -> (match f with Abstr(_,a) -> subst 0 0 (maybe i x) (maybe i a) | _ -> let f,l = flatten t in (match f with Const(_) -> let f' = unfold f in let n = lambda_count f' in let m = length l in if n = m then let f'',l' = red_combinator f' l in if l' = [] then f'' else failwith "beta_combinator" else if f' <> f && n = 0 then (match l with [x] -> App(f',x) | _ -> raise Normal) else raise Normal | _ -> raise Normal)) | _ -> raise Normal;; let current_term = ref None;; let current_history = ref [];; let current_future = ref [[]];; let current_strategy = ref leftmost_outermost;; let set_current_term t = current_term := Some t (* ; current_future := [[]] *) ;; let clear_current_term () = current_term := None;; let rec unfold_combinators t = match unfold t with App(f,x) -> App(unfold_combinators f,unfold_combinators x) | Abstr(v,u) -> Abstr(v,unfold_combinators u) | t -> t;; let unfold_combinator s' = let t' = assoc s' !combinators in let rec unfold_combinator t = match t with App(f,x) -> App(unfold_combinator f,unfold_combinator x) | Abstr(v,u) -> Abstr(v,unfold_combinator u) | Const(s) -> if s = s' then t' else t | _ -> t in unfold_combinator;; let add_combinator s = let l = lex (explode s) in match l with [v;"="] -> combinators := filter (fun x -> fst x <> v) !combinators; true | v::"="::l' -> (try let t = parse l' in try let t' = assoc v !combinators in print_string (" "^v^" already defined\n"^ " "^v^"="^(term_to_string' t')^"\n"); true with Not_found -> let s' = term_to_string' t in if occurs (Const(v)) t then (print_string (" cyclic definition: "^v^" occurs in "^s'^"\n"); true) else match t with Const _ -> print_string (" will not abbreviate single variable\n"); true | _ -> (print_string (" "^v^"="^s'^"\n"); combinators := (v,t)::!combinators; true) with Failure "parse" -> false) | ["^";v] -> (match v with "^" -> (match !current_term with Some t -> set_current_term (unfold_combinators t) | None -> print_string " no term to unfold\n"); true | "." -> false | "(" -> false | ")" -> false | _ -> (match !current_term with Some t -> (try set_current_term (unfold_combinator v t) with Not_found -> print_string (" no definition for "^v^"\n")) | None -> print_string " no term to unfold\n"); true) | _ -> false;; let rec split_last l = match l with [] -> raise Not_found | h::t -> let l,x = split_last t in (h::l),x;; let pop_history () = match !current_history with (t::l)::h -> current_history := l::h; current_term := Some t | _ -> raise Not_found;; let prev_history () = match !current_history with [] -> raise Not_found | [t]::h -> if h = [] then raise Not_found else current_history := h; (match !current_future with [] -> failwith "prev_history" | l'::h' -> current_future := []::(t::l')::h') | (t::l)::h -> current_history := l::h; (match !current_future with [] -> failwith "prev_history" | l'::h' -> current_future := (t::l')::h') | _ -> failwith "prev_history";; let next_history () = match !current_future with [[]] -> raise Not_found | []::(t::l)::h -> current_history := [t]::!current_history; current_future := l::h | (t::l)::h -> (match !current_history with [] -> failwith "next_history" | l'::h' -> current_history := (t::l')::h'; current_future := l::h) | _ -> failwith "next_history";; let prev_term () = try if !current_term <> None then prev_history(); pop_history() with Not_found -> print_string " no previous term\n";; let next_term () = try next_history(); pop_history() with Not_found -> print_string " no next term\n";; let at_input () = match !current_history with [_]::_ -> true | _ -> false;; let prev_input () = try if !current_term <> None then prev_history(); while not (at_input()) do prev_history() done; pop_history() with Not_found -> print_string " no previous input term\n";; let next_input () = try next_history(); while not (at_input()) do next_history() done; pop_history() with Not_found -> print_string " no next input term\n";; let interactive_normal_form () = let n = ref 0 in (try Sys.catch_break true; while true do match !current_term with Some t -> set_current_term (!current_strategy t); n := !n + 1 | None -> print_string " no term to normalize\n"; raise Normal done with Normal -> () | Sys.Break -> print_string " normalization interrupted\n"); print_string (" "^(string_of_int !n)^" reduction step"^ (if !n = 1 then "" else "s")^"\n"); Sys.catch_break false; match !current_term with Some t -> let m = term_size t in (if m > 1000 then print_string (" the term has "^(string_of_int m)^ " nodes, printing it might take very long\n")); flush stdout | None -> ();; let interactive_translate e () = match !current_term with Some t -> set_current_term (translate e (unfold t)) | None -> print_string " no term to translate\n";; let interactive_translate_henk e () = match !current_term with Some t -> set_current_term (translate_henk e (unfold t)) | None -> print_string " no term to translate\n";; let interactive_translate_church e () = match !current_term with Some t -> set_current_term (translate_church e (unfold t)) | None -> print_string " no term to translate\n";; let fold_current_term () = match !current_term with Some t -> set_current_term (fold t) | None -> print_string " no term to fold\n";; let rec help () = let _ = map (fun xy -> let x,y = xy in print_string (" "^x^"="^(term_to_string' y)^"\n")) (rev !combinators) in let _ = map (fun xy -> let x,(y,_) = xy in print_string (" "^x^" "^y^"\n")) commands in () and commands = [".li", ("leftmost innermost", fun () -> current_strategy := leftmost_innermost); ".lo", ("leftmost outermost [default]", fun () -> current_strategy := leftmost_outermost); ".po", ("parallel outermost", fun () -> current_strategy := parallel_outermost); ".gk", ("gross knuth", fun () -> current_strategy := gross_knuth); ".l", ("lambda reduction [default]", fun () -> current_beta := beta); ".c", ("combinator reduction", fun () -> current_beta := beta_combinator); ".ex", ("eta reduction", fun () -> current_eta := eta); ".in", ("no eta reduction [default]", fun () -> current_eta := fun i t -> raise Normal); "./", ("fold combinators", fold_current_term); "./IKS", ("translate to IKS", interactive_translate false); ".//IKS", ("translate to IKS using eta", interactive_translate true); "./IKBCS", ("translate to IKBCS", interactive_translate_henk false); ".//IKBCS", ("translate to IKBCS using eta", interactive_translate_henk true); "./IJK", ("translate to IJK", interactive_translate_church false); ".//IJK", ("translate to IJK using eta", interactive_translate_church true); "..", ("normalize", interactive_normal_form); ".<<", ("previous input term", prev_input); ".<", ("previous term", prev_term); ".>", ("next term", next_term); ".>>", ("next input term", next_input); ".?", ("help", help); ".", ("exit", fun () -> failwith "exit")];; let rec step_term n m = if n > 0 then match !current_term with Some t -> (try set_current_term (!current_strategy t); step_term (n - 1) (m + 1) with Normal -> m); | None -> m else m;; let main () = help(); while true do (let s = sub "\\" "^" (read_line()) in if s = "." then if !current_term = None then failwith "main" else clear_current_term () else try let _,y = assoc s commands in y() with Not_found -> if add_combinator s then () else (if s = "" then (if step_term 1 0 < 1 then clear_current_term ()) else try let m = step_term (int_of_string s) 0 in print_string (" "^(string_of_int m)^" reduction step"^ (if m = 1 then "" else "s")^"\n") with | Normal -> () | _ -> try let t = term s in set_current_term t; current_history := []::!current_history with Failure "parse" -> print_string " syntax error\n")); match !current_term with Some t -> let t = !current_fold t in current_term := Some t; (match !current_history with [] -> failwith "history" | l::h -> current_history := (t::l)::h); Sys.catch_break true; (try print_string (" "^(term_to_string' t)^" ") with Sys.Break -> print_string (" term printing interrupted\n"^ " [term with "^(string_of_int (term_size t))^" nodes] ")); Sys.catch_break false; | None -> () done;; try main() with Failure "main" -> () | End_of_file -> ();;