impl alpha reduction

src/cui.ml

@@ -5,8 +5,28 @@ exception Error of string
 
 let err s = raise (Error s)
 
-let initial_env =
-  Environment.extend "id" (Abstraction ("_x", Var "_x")) Environment.empty
+let parse s = Parser.main Lexer.main (Lexing.from_string (s ^ "\n"))
+
+let initial_env = Environment.from_list [
+  ("test", parse "λl. λm. λn. l m n");
+  ("tru", parse "λt. λf. t");
+  ("fls", parse "λt. λf. f");
+  ("iszro", parse "λm. m (λx. fls) tru");
+  ("c0", parse "λs. λz. z");
+  ("c1", parse "λs. λz. s z");
+  ("scc", parse "λn. λs. λz. s (n s z)");
+  ("plus", parse "λm. λn. λs. λz. m s (n s z)");
+  ("times", parse "λm. λn. m (plus n) c0");
+  ("pair", parse "λf. λs. λb. b f s");
+  ("fst", parse "λp. p tru");
+  ("snd", parse "λp. p fls");
+  ("prd", parse "λm. fst (m (λp. pair (snd p) (plus c1 (snd p))) (pair c0 c0))");
+  ("fix", parse "λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))");
+  ("factorial", parse "fix (λf. λn. test (iszro n) (λx. c1) (λx. (times n (f (prd n)))) c0)");
+  ("nil", parse "λc. λn. n");
+  ("cons", parse "λh. λt. λc. λn. c h (t c n)");
+  ("head", parse "λh. λt. λc. λn. c h (t c n)");
+]
 
 
 (* read eval print *)

src/environment.ml

@@ -16,4 +16,13 @@ let rec map f = function
 let rec fold_right f env a =
   match env with
     [] -> a
-  | (_, v)::rest -> f v (fold_right f rest a)
+  | hd::rest -> f hd (fold_right f rest a)
+
+let rec from_list = function
+  [] -> empty
+| (id, v) :: tl -> 
+  if List.mem_assoc id tl then
+    raise (Bound_Several_Times
+    ("Variable " ^ id ^ " is bound several times"))
+  else
+    extend id v (from_list tl)

src/environment.mli

@@ -8,4 +8,5 @@ val empty : 'a t
 val extend : Syntax.id -> 'a -> 'a t -> 'a t
 val lookup : Syntax.id -> 'a t -> 'a
 val map : ('a -> 'b) -> 'a t -> 'b t
-val fold_right : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+val fold_right : ((Syntax.id * 'a) -> 'b -> 'b) -> 'a t -> 'b -> 'b
+val from_list : (Syntax.id * 'a) list -> 'a t

src/evaluation.ml

@@ -4,26 +4,50 @@ exception Error of string
 
 let err s = raise (Error s)
 
+(* alpha reduction
+  substitute id with id ^ "'"
+*)
+let rec alpha id exp = 
+  let new_id = id ^ "'" in
+  match exp with
+    Var i -> if i = id then Var new_id else exp
+  | Abstraction (i, e) -> if i = id then Abstraction (new_id, alpha id e) else Abstraction (i, alpha id e)
+  | Application (e1, e2) -> Application (alpha id e1, alpha id e2)
+
+(* whether the id is free var or not in t *)
+let is_fv id t =
+  let rec is_fv2 id t binded = match t with
+      Var i -> i = id && not (List.exists ((=) id) binded)
+    | Abstraction (i, t2) -> is_fv2 id t2 (i :: binded)
+    | Application (e1, e2) -> is_fv2 id e1 binded && is_fv2 id e2 binded
+  in is_fv2 id t []
+
 (* [x → t]exp *)
 let rec substitute x t exp = match exp with
     Var id -> if x = id then t else exp
-  | Abstraction (id, ex) -> 
-    Abstraction (id, substitute x t ex)
+  | Abstraction (id, ex) ->
+    if id <> x && not (is_fv id t) then
+    (* when id ≠ x and id ∉ FV(t) *)
+    Abstraction (id, substitute x t ex) else
+    (* when id = x or id ∈ FV(t) *)
+    let new_abst = alpha id exp in
+    substitute x t new_abst
   | Application (ex1, ex2) ->
     Application (substitute x t ex1, substitute x t ex2)
 
 (* call-by-value beta reduction
   only outermost redexes are reduced and where a redex is reduced only when its right-hand side has already been reduced to a value
   (λx. t1) t2 -> [x → t2]t1
 *)
-let rec beta env = function
+let rec beta = function
     Application (Abstraction (x, t1), exp2) ->
-      let t2 = beta env exp2 in
+      let t2 = beta exp2 in
       substitute x t2 t1
+  | Application (Var x, exp2) -> Application (Var x, beta exp2)
   | Application (exp1, exp2) ->
-      let t = beta env exp1 in
+      let t = beta exp1 in
       Application (t, exp2)
-  | Var id -> Environment.lookup id env
+  | Abstraction (i, e) -> Abstraction (i, beta e)
   | e -> e
 
 (* 
@@ -33,6 +57,7 @@ let rec beta env = function
     - set timeout
 *)
 let rec eval env t =
-  let b = beta env t in
+  let t1 = Environment.fold_right (fun (x, t) exp -> substitute x t exp) env t in
+  let b = beta t1 in
   if (string_of_exp b) = (string_of_exp t)
   then [t] else t :: (eval env b)

src/lexer.mll

@@ -6,6 +6,6 @@ rule main = parse
 | "(" { Parser.LPAREN }
 | ")" { Parser.RPAREN }
 | "." { Parser.DOT }
-| ['a'-'z'] ['a'-'z' '0'-'9' '_' '\'']*
+| ['a'-'z' '_'] ['a'-'z' '0'-'9' '_']*
     { Parser.ID (Lexing.lexeme lexbuf) }
 | ['\n'] { Parser.EOL }

test/lambda_test.ml

@@ -23,8 +23,36 @@ let tests = [
   { 
     input = "(λx. x x) (λx. x x)"; 
     expected = Application (
-      Abstraction ("x", Application (Var "x", Var "x")), 
-      Abstraction ("x", Application (Var "x", Var "x"))) 
+      Abstraction ("x", Application (Var "x", Var "x")),
+      Abstraction ("x", Application (Var "x", Var "x")))
+  };
+  { input = "(λx. (λx. x)) y"; expected = Abstraction ("x'", Var "x'") };
+  { input = "(λx. (λx. (λx. x))) y z"; expected = Abstraction ("x''", Var "x''") };
+  { input = "(λx. (λz. x)) z"; expected = Abstraction ("z'", Var "z") };
+  { input = "(λx. (λz. x)) z"; expected = Abstraction ("z'", Var "z") };
+  { 
+    input = "(λn. λs. λz. s (n s z)) (λs. λz. z)"; 
+    expected = Abstraction ("s", Abstraction ("z", Application (Var "s", Var "z")))
+  };
+  { 
+    input = "(λm. λn. λs. λz. m s (n s z)) (λs. λz. s z) ((λn. λs. λz. s (n s z)) (λs. λz. z))"; 
+    expected = Abstraction ("s", Abstraction ("z", Application (Var "s", Application (Var "s", Var "z"))))
+  };
+  { 
+    input = "(λm. λn. m ((λm. λn. λs. λz. m s (n s z)) n) (λs. λz. z)) (λs. λz. s z) (λs. λz. s(s z))"; 
+    expected = Abstraction ("s", Abstraction ("z'", Application (Var "s", Application (Var "s", Var "z'"))))
+  };
+  { 
+    input = "(λp. p (λt. λf. t)) ((λf. λs. λb. b f s) x y)"; 
+    expected = Var "x"
+  };
+  { 
+    input = "(λp. p (λt. λf. f)) ((λf. λs. λb. b f s) x y)"; 
+    expected = Var "y"
+  };
+  { 
+    input = "(λm. (((m (λp. ((λs. (λb. ((b (p (λt. (λf. f)))) s))) (((λm. (λn. (λs. (λz. ((m s) ((n s) z)))))) (λs. (λz. (s z)))) ((λp. (p (λt. (λf. f)))) p))))) (((λf. (λs. (λb. ((b f) s)))) (λs. (λz. z))) (λs. (λz. z)))) (λt. (λf. t)))) ((λn. λs. λz. s (n s z)) (λs. λz. s z))";
+    expected = Abstraction ("s", Abstraction ("z''", Application (Var "s", Var "z''")))
   };
 ]
 
@@ -34,7 +62,7 @@ let suite = "test suite for lambda" >:::
     let e = Syntax.string_of_exp tt.expected in
     tt.input >:: (fun _ -> assert_equal
     ~printer: (fun x -> x)
-    i e)
+    e i)
     ) tests
 
 let _ = run_test_tt_main suite