open List;; type lambda = Var of string | App of (lambda * lambda) | Abs of (string * lambda) | Nil;; let y_term = Abs ("f", App (Abs ("x", App (Var ("f"), (App (Var ("x"), Var ("x"))))), Abs ("x", App (Var ("f"), (App (Var ("x"), Var ("x")))))));; let xred = App (Abs ("x", Abs ("y", Var "x")), Var "y");; let i = Abs ("x", Var "x");; let w_term = Abs ("x", App (Var "x", Var "x"));; let s = Abs ("x", Abs ("y", Abs ("z", App (App (Var "x", Var "z"), App (Var "y", Var "z")))));; let k = Abs ("x", Abs ("y", Var "x"));; let paral_term = App (App (i, i), App (i, i));; let paral_term2 = App (w_term, App (App (i, i), Var "a"));; let print_list = iter (fun x -> print_string (x ^ "\n"));; let fst (x, y) = x;; let scd (x, y) = y;; let rec string_of_lambda t = match t with Var a -> a |Abs (a, Var b) when a = b -> "I" |Abs (a, App (Var b, Var c)) when a = b && a = c -> "w" |Abs (x, Abs (y, Abs (z, App (App (Var a, Var c), App (Var b, Var d))))) when a = x && b = y && c = z && c = d -> "S" |Abs (x, Abs (y, Var z)) when x = z -> "K" |App (a, b) -> "(" ^ (string_of_lambda a) ^ " " ^ (string_of_lambda b) ^ ")" |Abs (a, b) -> "(\\" ^ a ^ "." ^ (string_of_lambda b) ^ ")" |Nil -> "NIL";; let rec isin l a = match l with [] -> false |l1::ls -> if l1 = a then true else isin ls a;; let exclude a l = filter ((<>) a) l;; let unique z = let rec unique' l acc = match l with [] -> acc |l1::ls -> if isin acc l1 then (unique' ls acc) else (unique' ls (l1::acc)) in unique' z [];; let union a b = a @ filter (fun x -> not (isin a x)) b;; let intersect c d = fold_left (fun x y -> if isin d y then y::x else x) [] c;; let fv z = let rec fv' exp = match exp with Var a -> [a] |App (a, b) -> (fv' a) @ (fv' b) |Abs (a, b) -> filter (fun z -> (z <> a)) (fv' b) |Nil -> [] in unique (fv' z);; let cx y z = let rec cx' a x = if (not (isin (fv a) x)) then [] else ( match a with Var b -> [] |App (b, c) -> (cx' b x) @ (cx' c x) |Abs (b, c) -> (cx' c x) @ [b] |Nil -> [] ) in unique (cx' y z);; let rec replace a x b = if (not (isin (fv a) x)) then a else ( match a with Var z -> b |App (p, q) -> App (replace p x b, replace q x b) |Abs (y, r) -> Abs (y, replace r x b) |Nil -> Nil );; let rec (=@) a b = match (a, b) with (Var x, Var y) -> x = y |(App (p1, q1), App (p2, q2)) -> (p1 =@ p2) && (q1 =@ q2) |(Abs (x, p1), Abs (y, p2)) -> (replace p1 x (Var y)) =@ p2 |_ -> false;; let rec bound_replace a x y = match a with Abs (z, q) -> if z = x then (Abs (y, bound_replace (replace q z (Var y)) x y)) else Abs (z, bound_replace q x y) |App (p, q) -> App (bound_replace p x y, bound_replace q x y) |Var z -> Var z |Nil -> Nil;; (* The following piece of code is not copyrighted by me *) let union a b = a @ filter (fun x -> not (isin a x)) b;; let rec new_name v except = if isin except v then new_name (v ^ "'") except else v;; let rec all_vars expr = match expr with Var b -> [b] |App (p, q) -> union (all_vars p) (all_vars q) |Abs (x, q) -> union (all_vars q) [x] |Nil -> ["Nil"];; (* End of non-copyrighted code *) let rec conv_red a x b = let cross = (intersect (cx a x) (fv b)) in match cross with [] -> a |l1::ls -> conv_red (bound_replace a l1 ( new_name l1 (all_vars a) )) x b;; let redex_reduction c = match c with App (Abs (x, a), b) -> if ((intersect (cx a x) (fv b)) = []) then (replace a x b) else (replace (conv_red a x b) x b) |_ -> Nil;; let reduct_once z = let rec red' t = match t with Var a -> (false, Var a) |Nil -> (false, Nil) |(App (Abs (x, a), b)) as c -> let (p, q) = (red' a, red' b) in if (not (fst p)) && (not (fst q)) then (true, redex_reduction c) else (if (fst p) then (true, App (Abs (x, scd p), b)) else (true, App (Abs (x, a), scd q))) |(App (a, b)) as c -> let (p, q) = (red' a, red' b) in if (not (fst p)) && (not (fst q)) then (false, c) else (if (fst p) then (true, App (scd p, b)) else (true, App (a, scd q))) |(Abs (x, b)) as c -> let q = red' b in if not (fst q) then (false, c) else (true, Abs (x, scd q)) in scd (red' z);; let parallel_reduction z = let rec red' t = match t with Var b -> [Var b] |App (Abs (x, p), q) -> let processed = (flatten ( map (fun a -> map (fun b -> App (Abs (x, a), b)) (red' q)) (red' p) )) in processed @ (map (redex_reduction) processed) |App (p, q) -> flatten ( map (fun a -> map (fun b -> App (a, b)) (red' q)) (red' p) ) |Abs (x, r) -> map (fun a -> Abs (x, a)) (red' r) |Nil -> [Nil] in (red' z);; let parallel_reduction2 z = let rec red' t = match t with Var b -> Var b |App (Abs (x, p), q) -> redex_reduction (App (Abs (x, red' p), red' q)) |App (p, q) -> App (red' p, red' q) |Abs (x, q) -> Abs (x, red' q) |Nil -> Nil in (red' z);; let normal_reduction z = let rec red' t n = if n > 0 then ( match t with Var a -> (false, Var a) |Nil -> (false, Nil) |(App (Abs (x, a), b)) as c -> (true, redex_reduction c) |(App (a, b)) as c -> let (p, q) = (red' a (n - 1), red' b (n - 1)) in if (not (fst p)) && (not (fst q)) then (false, c) else if (fst p) then (true, App (scd p, b)) else (true, App (a, scd q)) |(Abs (x, b)) as c -> let q = red' b (n - 1) in if not (fst q) then (false, c) else (true, Abs (x, scd q)) ) else (false, t) in red' z 10;; let rec normal_form t n = let nr = normal_reduction t in if not (fst nr) || n = 0 then t else normal_form (scd nr) (n - 1);; let normal_forming z = let rec f t acc n = let nr = normal_reduction t in if not (fst nr) || n = 0 || isin acc (scd nr) then acc else f (scd nr) (scd nr::acc) (n - 1) in rev (f z [] 10);; let output redex = print_string ("\n\nOriginal:\n" ^ (string_of_lambda redex) ^ "\n\nReducted:\n"); print_list (map (string_of_lambda) (normal_forming redex)(* ^ "\n\n"*));; output (App (App (s, App (k, k)), k));; output (App (w_term, w_term));;