push

main.ml

@@ -0,0 +1,54 @@
+type expr =
+  | Var of string           
+  | Lam of string * expr    
+  | App of expr * expr      
+
+let rec free_vars = function
+  | Var x -> [x]
+  | Lam (x, e) -> List.filter (fun y -> y <> x) (free_vars e)
+  | App (e1, e2) -> (free_vars e1) @ (free_vars e2)
+
+
+let rec substitute e x s =
+  match e with
+  | Var y -> if y = x then s else e
+  | Lam (y, body) ->
+      if y = x then e 
+      else if List.mem y (free_vars s) then
+        let y' = y ^ "'" in
+        let body' = substitute body y (Var y') in
+        Lam (y', substitute body' x s)
+      else
+        Lam (y, substitute body x s)
+  | App (e1, e2) -> App (substitute e1 x s, substitute e2 x s)
+
+let rec beta_reduce = function
+  | App (Lam (x, body), arg) -> substitute body x arg
+  | App (e1, e2) ->
+      let e1' = beta_reduce e1 in
+      if e1' <> e1 then App (e1', e2)
+      else App (e1, beta_reduce e2)
+  | Lam (x, body) -> Lam (x, beta_reduce body)
+  | Var x -> Var x
+
+let rec normalize e =
+  let e' = beta_reduce e in
+  if e' = e then e
+  else normalize e'
+
+let rec to_string = function
+  | Var x -> x
+  | Lam (x, e) -> "λ" ^ x ^ "." ^ to_string e
+  | App (e1, e2) ->
+      "(" ^ to_string e1 ^ " " ^ to_string e2 ^ ")"
+
+let () =
+  let id = Lam ("x", Var "x") in                   (* λx.x *)
+  let tru = Lam ("t", Lam ("f", Var "t")) in      (* λt.λf.t *)
+  let fls = Lam ("t", Lam ("f", Var "f")) in      (* λt.λf.f *)
+  let apply_id = App (id, Var "y") in             (* (λx.x y) *)
+
+  let reduced = normalize apply_id in
+
+  Printf.printf "Original: %s\n" (to_string apply_id);
+  Printf.printf "Reduced:  %s\n" (to_string reduced)