coverted Oleg's Haskell lib -> ML -> JS

Signed-off-by: Jim Pryor <profjim@jimpryor.net>

diff --git a/code/lambda.ml b/code/lambda.ml
index 146c9eb..1eaca65 100644 (file)
--- a/code/lambda.ml
+++ b/code/lambda.ml
@@ -2,191 +2,204 @@
 
 module Private =  struct
     type var_t = int*string
 
 module Private =  struct
     type var_t = int*string

-    let var v = (0,v)
-    let string_of_var (i,v) = v ^ String.make i '\''
-    let equal_var (i1,v1) (i2,v2) = i1 == i2 && (String.compare v1 v2 == 0)
+    let var v = (0, v)
+    let string_of_var (i, v) = v ^ String.make i '\''
+    let equal_var (i1, v1) (i2, v2) = i1 == i2 && (String.compare v1 v2 == 0)

 
     type lambda_t = [ `Var of var_t | `Lam of var_t * lambda_t | `App of lambda_t * lambda_t ]
 
 
     type lambda_t = [ `Var of var_t | `Lam of var_t * lambda_t | `App of lambda_t * lambda_t ]
 

-    type debruijn_t = [ `Var of var_t | `DVar of int | `DLam of debruijn_t | `DApp of debruijn_t*debruijn_t ]
+(* DeBruijn terms
+ * substitution and translation algorithms from Chris Hankin, An Introduction to Lambda Calculi for Comptuer Scientists
+ *)

 
 

-    let db_subst (expr : debruijn_t) (m : int) (repl : debruijn_t) =
-        let rec rename m i = function
-        | `Var _ as term -> term
-        | `DVar j as term when j < i -> term
-        | `DVar j -> `DVar (j + m - 1)
-        | `DApp(n1,n2) -> `DApp(rename m i n1, rename m i n2)
-        | `DLam n -> `DLam(rename m (i+1) n)
+    type debruijn_t = [ `Db_free of var_t | `Db_index of int | `Db_lam of debruijn_t | `Db_app of debruijn_t*debruijn_t ]
+
+    let debruijn_subst (expr : debruijn_t) (m : int) (new_term : debruijn_t) =
+        let rec renumber m i = function
+        | `Db_free _ as term -> term
+        | `Db_index j as term when j < i -> term
+        | `Db_index j -> `Db_index (j + m - 1)
+        | `Db_app(left, right) -> `Db_app(renumber m i left, renumber m i right)
+        | `Db_lam body -> `Db_lam(renumber m (i+1) body)

         in let rec loop m = function
         in let rec loop m = function

-        | `Var _ as term -> term
-        | `DVar n as term when n < m -> term
-        | `DVar n when n > m -> `DVar (n-1)
-        | `DVar n -> rename n 1 repl
-        | `DApp(m1,m2) -> `DApp(loop m m1, loop m m2)
-        | `DLam mterm -> `DLam(loop (m+1) mterm)
+        | `Db_free _ as term -> term
+        | `Db_index j as term when j < m -> term
+        | `Db_index j when j > m -> `Db_index (j-1)
+        | `Db_index j -> renumber j 1 new_term
+        | `Db_app(left, right) -> `Db_app(loop m left, loop m right)
+        | `Db_lam body -> `Db_lam(loop (m+1) body)

         in loop m expr
 
         in loop m expr
 

-    let db (expr : lambda_t) : debruijn_t =
-        let pos seq (target : var_t) handler default =
+    let debruijn (expr : lambda_t) : debruijn_t =
+        let pos seq (target : var_t) =

             let rec loop (i : int) = function
             let rec loop (i : int) = function

-            | [] -> default
-            | x::xs when equal_var x target -> handler i
+            | [] -> `Db_free target
+            | x::xs when equal_var x target -> `Db_index i

             | _::xs -> loop (i+1) xs
             in loop 1 seq
         in let rec loop seq = function
             | _::xs -> loop (i+1) xs
             in loop 1 seq
         in let rec loop seq = function

-        | `Var v as term -> pos seq v (fun i -> `DVar i) term
-        | `Lam (v,t) -> `DLam(loop (v::seq) t)
-        | `App (t1,t2) -> `DApp(loop seq t1, loop seq t2)
+        | `Var v -> pos seq v
+        | `Lam (v, body) -> `Db_lam(loop (v::seq) body)
+        | `App (left, right) -> `Db_app(loop seq left, loop seq right)

         in loop [] expr
 
         in loop [] expr
 

-    let rec db_equal (t1 : debruijn_t) (t2 : debruijn_t) = match (t1,t2) with
-    | (`Var v1,`Var v2) -> equal_var v1 v2
-    | (`DVar i1, `DVar i2) -> i1 == i2
-    | (`DApp(m1,m2),`DApp(n1,n2)) -> db_equal m1 n1 && db_equal m2 n2
-    | (`DLam(t1),`DLam(t2)) -> db_equal t1 t2
+    let rec dbruijn_equal (t1 : debruijn_t) (t2 : debruijn_t) = match (t1, t2) with
+    | (`Db_free v1, `Db_free v2) -> equal_var v1 v2
+    | (`Db_index j1, `Db_index j2) -> j1 == j2
+    | (`Db_app(left1, right1), `Db_app(left2, right2)) -> dbruijn_equal left1 left2 && dbruijn_equal right1 right2
+    | (`Db_lam(body1), `Db_lam(body2)) -> dbruijn_equal body1 body2

     | _ -> false
 
     | _ -> false
 

-    let rec db_contains (t1 : debruijn_t) (t2 : debruijn_t) = match (t1,t2) with
-    | (`Var v1,`Var v2) -> equal_var v1 v2
-    | (`DVar i1, `DVar i2) -> i1 == i2
-    | (`DApp(m1,m2),`DApp(n1,n2)) when db_equal m1 n1 && db_equal m2 n2 -> true
-    | (`DApp(m1,m2), term) -> db_contains m1 term || db_contains m2 term
-    | (`DLam(t1),`DLam(t2)) when db_equal t1 t2 -> true
-    | (`DLam(t1), term) -> db_contains t1 term
+    let rec debruijn_contains (t1 : debruijn_t) (t2 : debruijn_t) = match (t1, t2) with
+    | (`Db_free v1, `Db_free v2) -> equal_var v1 v2
+    | (`Db_index j1, `Db_index j2) -> j1 == j2
+    | (`Db_app(left1, right1), `Db_app(left2, right2)) when dbruijn_equal left1 left2 && dbruijn_equal right1 right2 -> true
+    | (`Db_app(left, right), term2) -> debruijn_contains left term2 || debruijn_contains right term2
+    | (`Db_lam(body1), `Db_lam(body2)) when dbruijn_equal body1 body2 -> true
+    | (`Db_lam(body1), term2) -> debruijn_contains body1 term2

     | _ -> false
 
     | _ -> false
 

+

     (* non-normalizing string_of_lambda *)
     let string_of_lambda (expr : lambda_t) =
         let rec top = function
             | `Var v -> string_of_var v
     (* non-normalizing string_of_lambda *)
     let string_of_lambda (expr : lambda_t) =
         let rec top = function
             | `Var v -> string_of_var v

-            | `Lam _ as t -> "fun " ^ funct t
-            | `App ((`App _ as t1),t2) -> top t1 ^ " " ^ atom t2
-            | `App (t1,t2) -> atom t1 ^ " " ^ atom t2
+            | `Lam _ as term -> "fun " ^ dotted term
+            | `App ((`App _ as left), right) -> top left ^ " " ^ atom right
+            | `App (left, right) -> atom left ^ " " ^ atom right

         and atom = function
             | `Var v -> string_of_var v
         and atom = function
             | `Var v -> string_of_var v

-            | `Lam _ as t -> "(fun " ^ funct t ^ ")"
-            | `App _ as t -> "(" ^ top t ^ ")"
-        and funct = function
-            | `Lam (v,(`Lam _ as t)) -> (string_of_var v) ^ " " ^ funct t
-            | `Lam (v,t) -> (string_of_var v) ^ " -> " ^ top t
+            | `Lam _ as term -> "(fun " ^ dotted term ^ ")"
+            | `App _ as term -> "(" ^ top term ^ ")"
+        and dotted = function
+            | `Lam (v, (`Lam _ as body)) -> (string_of_var v) ^ " " ^ dotted body
+            | `Lam (v, body) -> (string_of_var v) ^ " -> " ^ top body

         in top expr
 
         in top expr
 

+(*
+ * substitution and normal-order evaluator based on Haskell version by Oleg Kisleyov
+ * http://okmij.org/ftp/Computation/lambda-calc.html#lambda-calculator-haskell
+ *)

 
 

-    (* evaluator based on http://okmij.org/ftp/Haskell/Lambda_calc.lhs *)
-
-    (* if v occurs free_in term, returns Some v' where v' is the highest-tagged
-     * variable with the same name as v occurring (free or bound) in term *)
-
+(* if v occurs free_in term, returns Some v' where v' is the highest-tagged
+ * variable with the same name as v occurring (free or bound) in term
+ *)

     let free_in ((tag, name) as v) term =
         let rec loop = function
         | `Var((tag', name') as v') ->
                 if name <> name' then false, v
                 else if tag = tag' then true, v
                 else false, v'
     let free_in ((tag, name) as v) term =
         let rec loop = function
         | `Var((tag', name') as v') ->
                 if name <> name' then false, v
                 else if tag = tag' then true, v
                 else false, v'

-        | `App(t1, t2) ->
-                let b1, ((tag1, _) as v1) = loop t1 in
-                let b2, ((tag2, _) as v2) = loop t2 in
-                b1 || b2, if tag1 > tag2 then v1 else v2
-        | `Lam(x, _) when x = v -> (false, v)
+        | `App(left, right) ->
+                let left_bool, ((left_tag, _) as left_v) = loop left in
+                let right_bool, ((right_tag, _) as right_v) = loop right in
+                left_bool || right_bool, if left_tag > right_tag then left_v else right_v
+        | `Lam(v', _) when equal_var v v' -> (false, v)

         | `Lam(_, body) -> loop body
         in match loop term with
         | false, _ -> None
         | true, v -> Some v
 
         | `Lam(_, body) -> loop body
         in match loop term with
         | false, _ -> None
         | true, v -> Some v
 

-    let rec subst v st = function
-        | term when st = `Var v -> term
-        | `Var x when x = v -> st
-        | `Var _ as term -> term
-        | `App(t1,t2) -> `App(subst v st t1, subst v st t2)
-        | `Lam(x, _) as term when x = v -> term
-        (* if x is free in the inserted term st, a capture is possible
-         * we handle by ...
-         *)
-        | `Lam(x, body) ->
-                (match free_in x st with
-                (* x not free in st, can substitute st for v without any captures *)
-                | None -> `Lam(x, subst v st body)
-                (* x free in st, need to alpha-convert `Lam(x, body) *)
-                | Some max_x ->  
-                    let bump_tag (tag, name) (tag', _) =
-                        (max tag tag') + 1, name in
-                    let bump_tag' ((_, name) as v1) ((_, name') as v2) =
-                        if name = name' then bump_tag v1 v2 else v1 in
-                    (* bump x > max_x from st, then check whether
-                     * it also needs to be bumped > v
-                     *)
-                    let uniq_x = bump_tag' (bump_tag x max_x) v in
-                    let uniq_x' = (match free_in uniq_x body with
-                        | None -> uniq_x
-                        (* bump uniq_x > max_x' from body *)
-                        | Some max_x' -> bump_tag uniq_x max_x'
-                    ) in
-                    (* alpha-convert body *)
-                    let body' = subst x (`Var uniq_x') body in
-                    (* now substitute st for v *)
-                    `Lam(uniq_x', subst v st body')
-                )
+    let rec subst v new_term term = match new_term with
+        | `Var v' when equal_var v v' -> term
+        | _ -> (match term with
+            | `Var v' when equal_var v v' -> new_term
+            | `Var _ -> term
+            | `App(left, right) -> `App(subst v new_term left, subst v new_term right)
+            | `Lam(v', _) when equal_var v v' -> term
+            (* if x is free in the inserted term new_term, a capture is possible *)
+            | `Lam(v', body) ->
+                    (match free_in v' new_term with
+                    (* v' not free in new_term, can substitute new_term for v without any captures *)
+                    | None -> `Lam(v', subst v new_term body)
+                    (* v' free in new_term, need to alpha-convert *)
+                    | Some max_x ->  
+                        let bump_tag (tag, name) (tag', _) =
+                            (max tag tag') + 1, name in
+                        let bump_tag' ((_, name) as v1) ((_, name') as v2) =
+                            if (String.compare name name' == 0) then bump_tag v1 v2 else v1 in
+                        (* bump v' > max_x from new_term, then check whether
+                         * it also needs to be bumped > v
+                         *)
+                        let uniq_x = bump_tag' (bump_tag v' max_x) v in
+                        let uniq_x' = (match free_in uniq_x body with
+                            | None -> uniq_x
+                            (* bump uniq_x > max_x' from body *)
+                            | Some max_x' -> bump_tag uniq_x max_x'
+                        ) in
+                        (* alpha-convert body *)
+                        let body' = subst v' (`Var uniq_x') body in
+                        (* now substitute new_term for v *)
+                        `Lam(uniq_x', subst v new_term body')
+                    )
+        )

 
     let check_eta = function
 
     let check_eta = function

-        | `Lam(v, `App(t, `Var u)) when v = u && free_in v t = None -> t
+        | `Lam(v, `App(body, `Var u)) when equal_var v u && free_in v body = None -> body

         | (_ : lambda_t) as term -> term
 
         | (_ : lambda_t) as term -> term
 

+
+
+

     exception Lambda_looping;;
 
     let eval ?(eta=false) (expr : lambda_t) : lambda_t =
         let rec looping (body : debruijn_t) = function
     exception Lambda_looping;;
 
     let eval ?(eta=false) (expr : lambda_t) : lambda_t =
         let rec looping (body : debruijn_t) = function

-        | [] -> false
-        | x::xs when db_equal body x -> true
+          | [] -> false
+        | x::xs when dbruijn_equal body x -> true

         | _::xs -> looping body xs
         in let rec loop (stack : lambda_t list) (body : lambda_t) = 
             match body with
             | `Var v as term -> unwind term stack
         | _::xs -> looping body xs
         in let rec loop (stack : lambda_t list) (body : lambda_t) = 
             match body with
             | `Var v as term -> unwind term stack

-            | `App(t1, t2) as term -> loop (t2::stack) t1
+            | `App(left, right) -> loop (right::stack) left

             | `Lam(v, body) -> (match stack with
                 | [] ->
                     let term = (`Lam(v, loop [] body)) in
                         if eta then check_eta term else term
             | `Lam(v, body) -> (match stack with
                 | [] ->
                     let term = (`Lam(v, loop [] body)) in
                         if eta then check_eta term else term

-                | t::rest -> loop rest (subst v t body)
+                | x::xs -> loop xs (subst v x body)

             )
             )

-        and unwind t1 = function
-        | [] -> t1
-        | t2::ts -> unwind (`App(t1, loop [] t2)) ts
+        and unwind left = function
+        | [] -> left
+        | x::xs -> unwind (`App(left, loop [] x)) xs

         in loop [] expr
 
 
         in loop [] expr
 
 

-    (* (Oleg's version of) Ken's evaluator; doesn't seem to work -- requires laziness? *)
+    let cbv ?(aggressive=true) (expr : lambda_t) : lambda_t =
+        let rec loop = function
+        | `Var v as term -> term
+        | `App(left, right) ->
+                let right' = loop right in
+                (match loop left with
+                | `Lam(v, body) -> loop (subst v right' body)
+                | _ as left' -> `App(left', right')
+                )
+        | `Lam(v, body) as term ->
+                if aggressive then `Lam(v, loop body)
+                else term
+        in loop expr
+
+
+

 
 

+
+    (*
+    
+     (* (Oleg's version of) Ken's evaluator; doesn't seem to work -- requires laziness? *)

     let eval' ?(eta=false) (expr : lambda_t) : lambda_t =
         let rec loop = function
         | `Var v as term -> term
         | `Lam(v, body) ->
                 let term = (`Lam(v, loop body)) in
                     if eta then check_eta term else term
     let eval' ?(eta=false) (expr : lambda_t) : lambda_t =
         let rec loop = function
         | `Var v as term -> term
         | `Lam(v, body) ->
                 let term = (`Lam(v, loop body)) in
                     if eta then check_eta term else term

-        | `App(`App _ as t1, t2) ->
-            (match loop t1 with
-                | `Lam _ as redux -> loop (`App(redux, t2))
-                | nonred_head -> `App(nonred_head, loop t2)
+        | `App(`App _ as left, right) ->
+            (match loop left with
+                | `Lam _ as redux -> loop (`App(redux, right))
+                | nonred_head -> `App(nonred_head, loop right)

             )
             )

-        | `App(t1, t2) -> `App(t1, loop t2)
-        in loop expr
-
-    let cbv ?(aggressive=true) (expr : lambda_t) : lambda_t =
-        let rec loop = function
-        | `Var x as term -> term
-        | `App(t1,t2) ->
-                let t2' = loop t2 in
-                (match loop t1 with
-                | `Lam(x, t) -> loop (subst x t2' t)
-                | _ as term -> `App(term, t2')
-                )
-        | `Lam(x, t) as term ->
-                if aggressive then `Lam(x, loop t)
-                else term
+        | `App(left, right) -> `App(left, loop right)

         in loop expr
 
 
         in loop expr
 
 

-
-    (*

         module Sorted = struct
             let rec cons y = function
                 | x :: _ as xs when x = y -> xs
         module Sorted = struct
             let rec cons y = function
                 | x :: _ as xs when x = y -> xs


@@ -215,8 +228,8 @@ module Private =  struct
         let free_vars (expr : lambda_t) : string list =
             let rec loop = function
                 | `Var x -> [x]
         let free_vars (expr : lambda_t) : string list =
             let rec loop = function
                 | `Var x -> [x]

-                | `Lam(x,t) -> Sorted.remove x (loop t)
-                | `App(t1,t2) -> Sorted.merge (loop t1) (loop t2)
+                | `Lam(x, t) -> Sorted.remove x (loop t)
+                | `App(t1, t2) -> Sorted.merge (loop t1) (loop t2)

             in loop expr
 
         let free_in v (expr : lambda_t) =
             in loop expr
 
         let free_in v (expr : lambda_t) =


@@ -228,10 +241,10 @@ module Private =  struct
 
         ...
         | `Lam(x, body) as term when not (free_in v body) -> term
 
         ...
         | `Lam(x, body) as term when not (free_in v body) -> term

-        | `Lam(y, body) when not (free_in y st) -> `Lam(y, subst v st body)
+        | `Lam(y, body) when not (free_in y new_term) -> `Lam(y, subst v new_term body)

         | `Lam(y, body) ->
             let z = new_var () in
         | `Lam(y, body) ->
             let z = new_var () in

-            subst v st (`Lam(z, subst y (`Var z) body))
+            subst v new_term (`Lam(z, subst y (`Var z) body))

     *)
 
 
     *)
 
 


@@ -241,14 +254,14 @@ module Private =  struct
     let bound_vars (expr : lambda_t) : string list =
         let rec loop = function
             | `Var x -> []
     let bound_vars (expr : lambda_t) : string list =
         let rec loop = function
             | `Var x -> []

-            | `Lam(x,t) -> Sorted.cons x (loop t)
-            | `App(t1,t2) -> Sorted.merge (loop t1) (loop t2)
+            | `Lam(x, t) -> Sorted.cons x (loop t)
+            | `App(t1, t2) -> Sorted.merge (loop t1) (loop t2)

         in loop expr
 
     let reduce_cbv ?(aggressive=true) (expr : lambda_t) : lambda_t =
         let rec loop = function
         | `Var x as term -> term
         in loop expr
 
     let reduce_cbv ?(aggressive=true) (expr : lambda_t) : lambda_t =
         let rec loop = function
         | `Var x as term -> term

-        | `App(t1,t2) ->
+        | `App(t1, t2) ->

                 let t2' = loop t2 in
                 (match loop t1 with
                 | `Lam(x, t) -> loop (subst x t2' t)
                 let t2' = loop t2 in
                 (match loop t1 with
                 | `Lam(x, t) -> loop (subst x t2' t)


@@ -264,7 +277,7 @@ module Private =  struct
         | `Var x as term -> term
         | `Lam(v, body) ->
                 check_eta (`Lam(v, loop body))
         | `Var x as term -> term
         | `Lam(v, body) ->
                 check_eta (`Lam(v, loop body))

-        | `App(t1,t2) ->
+        | `App(t1, t2) ->

                 (match loop t1 with
                 | `Lam(x, t) -> loop (subst x t2 t)
                 | _ as term -> `App(term, loop t2)
                 (match loop t1 with
                 | `Lam(x, t) -> loop (subst x t2 t)
                 | _ as term -> `App(term, loop t2)


@@ -305,13 +318,13 @@ module Private =  struct
             | `Lam(x, body) ->
                 (fun env ->
                     let v = new_var () in
             | `Lam(x, body) ->
                 (fun env ->
                     let v = new_var () in

-                    `Lam(v, inner body ((x,`Var v) :: env)))
+                    `Lam(v, inner body ((x, `Var v) :: env)))

         in inner expr ([] : env_t)
 
     let pp_env env =
         let rec loop acc = function
             | [] -> acc
         in inner expr ([] : env_t)
 
     let pp_env env =
         let rec loop acc = function
             | [] -> acc

-            | (x,term)::es -> loop ((x ^ "=" ^ string_of_lambda term) :: acc) es
+            | (x, term)::es -> loop ((x ^ "=" ^ string_of_lambda term) :: acc) es

         in "[" ^ (String.concat ", " (loop [] (List.rev env))) ^ "]"
 
     let eval (strategy : strategy_t) (expr : lambda_t) : lambda_t =
         in "[" ^ (String.concat ", " (loop [] (List.rev env))) ^ "]"
 
     let eval (strategy : strategy_t) (expr : lambda_t) : lambda_t =


@@ -340,7 +353,7 @@ module Private =  struct
             | `Lam(x, body) ->
                 (fun env ->
                     let v = new_var () in
             | `Lam(x, body) ->
                 (fun env ->
                     let v = new_var () in

-                    `Lam(v, inner body ((x,`Var v) :: env)))
+                    `Lam(v, inner body ((x, `Var v) :: env)))

             in
             (fun env -> 
                 (Printf.printf "%s with %s => %s\n" (string_of_lambda term) (pp_env env) (string_of_lambda (res env)); res env))
             in
             (fun env -> 
                 (Printf.printf "%s with %s => %s\n" (string_of_lambda term) (pp_env env) (string_of_lambda (res env)); res env))


@@ -356,7 +369,7 @@ module Private =  struct
 
     let rec to_int expr = match expr with
         | `Lam(s, `Lam(z, `Var z')) when z' = z -> 0
 
     let rec to_int expr = match expr with
         | `Lam(s, `Lam(z, `Var z')) when z' = z -> 0

-        | `Lam(s, `Var s') when s = s' -> 1
+        | `Lam(s, `Var s') when equal_var s s' -> 1

         | `Lam(s, `Lam(z, `App (`Var s', t))) when s' = s -> 1 + to_int (`Lam(s, `Lam(z, t)))
         | _ -> failwith (normal_string_of_lambda expr ^ " is not a church numeral")
 
         | `Lam(s, `Lam(z, `App (`Var s', t))) when s' = s -> 1 + to_int (`Lam(s, `Lam(z, t)))
         | _ -> failwith (normal_string_of_lambda expr ^ " is not a church numeral")
 


@@ -369,8 +382,8 @@ type lambda_t = Private.lambda_t
 open Private
 let var = var
 let pp, pn, pi = string_of_lambda, normal_string_of_lambda, int_of_lambda
 open Private
 let var = var
 let pp, pn, pi = string_of_lambda, normal_string_of_lambda, int_of_lambda

-let pnv,piv= (fun expr -> string_of_lambda (cbv expr)), (fun expr -> to_int (cbv expr))
-let db, db_equal, db_contains = db, db_equal, db_contains
+let pnv, piv= (fun expr -> string_of_lambda (cbv expr)), (fun expr -> to_int (cbv expr))
+let debruijn, dbruijn_equal, debruijn_contains = debruijn, dbruijn_equal, debruijn_contains

 
 

-let alpha_eq x f = db_equal (db x) (db y)
+let alpha_eq x y = dbruijn_equal (debruijn x) (debruijn y)

 
 

diff --git a/code/lambda2-test.js b/code/lambda2-test.js
new file mode 100644 (file)
index 0000000..09a1b5b
--- /dev/null
+++ b/code/lambda2-test.js
@@ -0,0 +1,651 @@
+load("lambda2.js");
+
+
+var g_eta = false;
+var g_cbv = false;
+
+function to_int(expr) {
+       var reduced = reduce(expr, g_eta, g_cbv);
+       if (reduced.to_int) {
+               return reduce(reduced, false, false).to_int(0);
+       } else {
+               return "not a church numeral";
+       }
+}
+
+function to_string(expr) {
+       var reduced = reduce(expr, g_eta, g_cbv);
+       return reduced.to_string();
+}
+
+
+function test() {
+
+       function make_lam2(a, b, aa) {
+               return make_lam(a, make_lam(b, aa));
+       }
+       function make_lam3(a, b, c, aa) {
+               return make_lam(a, make_lam(b, make_lam(c, aa)));
+       }
+       function make_lam4(a, b, c, d, aa) {
+               return make_lam(a, make_lam(b, make_lam(c, make_lam(d, aa))));
+       }
+       function make_lam5(a, b, c, d, e, aa) {
+               return make_lam(a, make_lam(b, make_lam(c, make_lam(d, make_lam(e, aa)))));
+       }
+       function make_app3(aa, bb, cc) {
+               return make_app(make_app(aa, bb), cc);
+       }
+       function make_app4(aa, bb, cc, dd) {
+               return make_app(make_app(make_app(aa, bb), cc), dd);
+       }
+       function make_app5(aa, bb, cc, dd, ee) {
+               return make_app(make_app(make_app(make_app(aa, bb), cc), dd), ee);
+       }
+
+       var s = make_var("s");
+       var z = make_var("z");
+       var m = make_var("m");
+       var n = make_var("n");
+       var u = make_var("u");
+       var v = make_var("v");
+       var d = make_var("d");
+       var ss = new Lambda_var(s);
+       var zz = new Lambda_var(z);
+       var mm = new Lambda_var(m);
+       var nn = new Lambda_var(n);
+       var uu = new Lambda_var(u);
+       var vv = new Lambda_var(v);
+       var dd = new Lambda_var(d);
+       var succ = make_lam3(m, s, z, make_app(ss, make_app3(mm, ss, zz)));
+       var tt = make_lam2(m, n, mm);
+       var ff = make_lam2(m, n, nn);
+       var kk = tt;
+       var get1 = tt;
+       var get2 = ff;
+       var id = make_lam(s, ss);
+       var ww = make_lam(s, make_app(ss, ss));
+       var pair = make_lam3(m, n, s, make_app3(ss, mm, nn));
+       var zero = make_lam2(s, z, zz);
+       var one = make_lam2(s, z, make_app(ss, zz));
+       var two = make_lam2(s, z, make_app(ss, make_app(ss, zz)));
+       var three = make_lam2(s, z, make_app(ss, make_app(ss, make_app(ss, zz))));
+       var four = make_lam2(s, z, make_app(ss, make_app(ss, make_app(ss, make_app(ss, zz)))));
+       var five = make_lam2(s, z, make_app(ss, make_app(ss, make_app(ss, make_app(ss, make_app(ss, zz))))));
+       var iszero = make_lam(m, make_app3(mm, make_lam(s, ff), tt));
+       var add = make_lam2(m, n, make_app3(mm, succ, nn));
+       var mul = make_lam3(m, n, s, make_app(mm, make_app(nn, ss)));
+       var pred1 = make_lam3(n, s, z, make_app4(nn, make_lam2(u, v, make_app(vv, make_app(uu, ss))), make_app(kk, zz), id));
+
+       var shift = make_lam(s, make_app(ss, make_lam2(m, n, make_app3(pair, make_app(succ, mm), mm))));
+       var pred2 = make_lam(n, make_app4(nn, shift, make_app3(pair, zero, zero), get2));
+
+
+       function make_sub() {
+               var mzero = make_app(make_app(pair, zero), id);
+               var msucc = make_lam(s, make_app(ss, make_lam(m, make_lam(n, make_app(make_app(pair, make_app(succ, mm)), make_app(kk, ss))))));
+               var mtail = make_lam(s, make_app(make_app(ss, get2), ss));
+               return make_lam(m, make_lam(n, make_app(make_app(make_app(nn, mtail), make_app(make_app(mm, msucc), mzero)), get1)));
+       }
+       var sub = make_sub();
+
+       var min = make_lam(m, make_lam(n, make_app(make_app(sub, mm), make_app(make_app(sub, mm), nn))));
+       var max = make_lam(m, make_lam(n, make_app(make_app(add, nn), make_app(make_app(sub, mm), nn))));
+
+       function make_lt() {
+               var mzero = make_app(make_app(pair, zero), id);
+               var msucc = make_lam(s, make_app(ss, make_lam(m, make_lam(n, make_app(make_app(pair, make_app(succ, mm)), make_app(kk, ss))))));
+               var mtail = make_lam(s, make_app(make_app(ss, get2), ss));
+               return make_lam(n, make_lam(m, make_app(make_app(make_app(make_app(make_app(nn, mtail), make_app(make_app(mm, msucc), mzero)), get1), make_lam(s, tt)), ff)));
+       }
+       var lt = make_lt();
+
+       function make_leq() {
+               var mzero = make_app(make_app(pair, zero), id);
+               var msucc = make_lam(s, make_app(ss, make_lam(m, make_lam(n, make_app(make_app(pair, make_app(succ, mm)), make_app(kk, ss))))));
+               var mtail = make_lam(s, make_app(make_app(ss, get2), ss));
+               return make_lam(m, make_lam(n, make_app(make_app(make_app(make_app(make_app(nn, mtail), make_app(make_app(mm, msucc), mzero)), get1), make_lam(s, ff)), tt)));
+       }
+       var leq = make_leq();
+
+       function make_eq() {
+               var mzero = make_app(make_app(pair, zero), make_app(kk, make_app(make_app(pair, one), id)));
+               var msucc = make_lam(s, make_app(ss, make_lam(m, make_lam(n, make_app(make_app(pair, make_app(succ, mm)), make_app(kk, ss))))));
+               var mtail = make_lam(s, make_app(make_app(ss, get2), ss));
+               return make_lam(m, make_lam(n, make_app(make_app(make_app(make_app(make_app(nn, mtail), make_app(make_app(mm, msucc), mzero)), get1), make_lam(s, ff)), tt)));
+       }
+       var eq = make_eq();
+
+       function make_divmod() {
+               var triple = make_lam4(m, n, z, s, make_app4(ss, mm, nn, zz));
+               var mzero = make_app4(triple, succ, make_app(kk, zero), id);
+               var msucc = make_lam(u, make_app4(triple, id, succ, make_app(kk, uu)));
+               // mtail is open in d
+               var mtail = make_lam(s, make_app(ss, make_lam5(m, n, u, v, z, make_lam(s, make_app3(zz, dd, make_app3(ss, make_app(uu, mm), make_app(vv, nn)))))));
+               var res = make_lam2(n, u, make_app3(
+                               make_lam(d, make_app3(nn, mtail, make_lam(s, make_app(dd, make_app3(ss, zero, zero))))),
+                               make_app4(uu, msucc, mzero, make_lam3(m, n, s, make_app(ss, zz))),
+                               make_lam5(m, n, u, v, s, make_app3(pair, mm, nn))
+                       ));
+               return res;
+       }
+       var divmod = make_divmod();
+       var div = make_lam2(n, m, make_app4(divmod, nn, mm, get1));
+       var mod = make_lam2(n, m, make_app4(divmod, nn, mm, get2));
+
+       var yhalf = make_lam(u, make_app(vv, make_app(uu, uu)));
+       var y = make_lam(v, make_app(yhalf, yhalf));
+       var yyhalf = make_lam(u, make_app(vv, make_lam(n, make_app3(uu, uu, nn))))
+       var yy = make_lam(v, make_app(yyhalf, yyhalf));
+
+       var turinghalf = make_lam2(u, v, make_app(vv, make_app3(uu, uu, vv)));
+       var turing = make_app(turinghalf, turinghalf);
+       var tturinghalf = make_lam2(u, v, make_app(vv, make_lam(m, make_app4(uu, uu, vv, mm))));
+       var tturing = make_app(tturinghalf, tturinghalf);
+
+       var ifzero = make_lam(n, make_app4(nn, make_lam2(u, v, make_app(vv, make_app(uu, succ))), make_app(kk, zero), make_lam3(m, s, z, make_app(ss, mm) )));
+
+       var fact1 = make_app(ww, make_lam2(u, n, make_app4(ifzero, nn, make_lam(s, make_app3(mul, nn, make_app3(uu, uu, ss))), one)));
+       function make_fact(y) {
+               return make_app(y, make_lam2(u, n, make_app4(ifzero, nn, make_lam(s, make_app3(mul, nn, make_app(uu, ss))), one)));
+       }
+       var fact2 = make_fact(y);
+       var fact3 = make_fact(yy);
+       var fact4 = make_fact(turing);
+       var fact5 = make_fact(tturing);
+
+       function check(expect, formula) {
+               var i = to_int(formula);
+               print(expect, expect === i);
+       }
+
+       function checkbool(expect, index, formula) {
+               if (expect) {
+                       print(index, equal(reduce(formula, g_eta, g_cbv), tt));
+               } else {
+                       print(index, equal(reduce(formula, g_eta, g_cbv), ff));
+               }
+       }
+
+       check(0, zero);
+       check(1, one);
+       check(2, two);
+       check(3, three);
+       check(4, four);
+       check(5, five);
+
+       check(1, make_app(succ, zero));
+       check(2, make_app(succ, make_app(succ, zero)));
+       check(3, make_app(succ, make_app(succ, make_app(succ, zero))));
+       check(4, make_app(succ, make_app(succ, make_app(succ, make_app(succ, zero)))));
+       check(5, make_app(succ, make_app(succ, make_app(succ, make_app(succ, make_app(succ, zero))))));
+
+
+       check(2, make_app(succ, one));
+       check(3, make_app(succ, make_app(succ, one)));
+       check(4, make_app(succ, make_app(succ, make_app(succ, one))));
+       check(5, make_app(succ, make_app(succ, make_app(succ, make_app(succ, one)))));
+
+       check(3, make_app(succ, two));
+       check(4, make_app(succ, make_app(succ, two)));
+       check(5, make_app(succ, make_app(succ, make_app(succ, two))));
+
+       print("checking iszero");
+       checkbool(true, 0, make_app(iszero, zero));
+       checkbool(true, 1, make_app(iszero, one));
+       checkbool(true, 2, make_app(iszero, two));
+       checkbool(true, 3, make_app(iszero, three));
+       checkbool(true, 4, make_app(iszero, four));
+       checkbool(true, 5, make_app(iszero, five));
+
+       print("checking add");
+       check(0, make_app(make_app(add, zero), zero));
+       check(1, make_app(make_app(add, zero), one));
+       check(2, make_app(make_app(add, zero), two));
+       check(3, make_app(make_app(add, zero), three));
+       check(4, make_app(make_app(add, zero), four));
+       check(5, make_app(make_app(add, zero), five));
+       check(1, make_app(make_app(add, one), zero));
+       check(2, make_app(make_app(add, one), one));
+       check(3, make_app(make_app(add, one), two));
+       check(4, make_app(make_app(add, one), three));
+       check(5, make_app(make_app(add, one), four));
+       check(6, make_app(make_app(add, one), five));
+       check(2, make_app(make_app(add, two), zero));
+       check(3, make_app(make_app(add, two), one));
+       check(4, make_app(make_app(add, two), two));
+       check(5, make_app(make_app(add, two), three));
+       check(6, make_app(make_app(add, two), four));
+       check(7, make_app(make_app(add, two), five));
+       check(3, make_app(make_app(add, three), zero));
+       check(4, make_app(make_app(add, three), one));
+       check(5, make_app(make_app(add, three), two));
+       check(6, make_app(make_app(add, three), three));
+       check(7, make_app(make_app(add, three), four));
+       check(8, make_app(make_app(add, three), five));
+       check(4, make_app(make_app(add, four), zero));
+       check(5, make_app(make_app(add, four), one));
+       check(6, make_app(make_app(add, four), two));
+       check(7, make_app(make_app(add, four), three));
+       check(8, make_app(make_app(add, four), four));
+       check(9, make_app(make_app(add, four), five));
+
+       print("checking mul");
+       check(0, make_app(make_app(mul, zero), zero));
+       check(0, make_app(make_app(mul, zero), one));
+       check(0, make_app(make_app(mul, zero), two));
+       check(0, make_app(make_app(mul, zero), three));
+       check(0, make_app(make_app(mul, zero), four));
+       check(0, make_app(make_app(mul, zero), five));
+       check(0, make_app(make_app(mul, one), zero));
+       check(1, make_app(make_app(mul, one), one));
+       check(2, make_app(make_app(mul, one), two));
+       check(3, make_app(make_app(mul, one), three));
+       check(4, make_app(make_app(mul, one), four));
+       check(5, make_app(make_app(mul, one), five));
+       check(0, make_app(make_app(mul, two), zero));
+       check(2, make_app(make_app(mul, two), one));
+       check(4, make_app(make_app(mul, two), two));
+       check(6, make_app(make_app(mul, two), three));
+       check(8, make_app(make_app(mul, two), four));
+       check(10, make_app(make_app(mul, two), five));
+       check(0, make_app(make_app(mul, three), zero));
+       check(3, make_app(make_app(mul, three), one));
+       check(6, make_app(make_app(mul, three), two));
+       check(9, make_app(make_app(mul, three), three));
+       check(12, make_app(make_app(mul, three), four));
+       check(15, make_app(make_app(mul, three), five));
+       check(0, make_app(make_app(mul, four), zero));
+       check(4, make_app(make_app(mul, four), one));
+       check(8, make_app(make_app(mul, four), two));
+       check(12, make_app(make_app(mul, four), three));
+       check(16, make_app(make_app(mul, four), four));
+       check(20, make_app(make_app(mul, four), five));
+
+
+       function check_pred(pred) {
+               check(0, make_app(pred, zero));
+               check(0, make_app(pred, make_app(pred, zero)));
+               check(0, make_app(pred, make_app(pred, make_app(pred, zero))));
+               check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, zero)))));
+               check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, zero))))));
+
+               check(0, make_app(pred, one));
+               check(0, make_app(pred, make_app(pred, one)));
+               check(0, make_app(pred, make_app(pred, make_app(pred, one))));
+               check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, one)))));
+               check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, one))))));
+
+               check(1, make_app(pred, two));
+               check(0, make_app(pred, make_app(pred, two)));
+               check(0, make_app(pred, make_app(pred, make_app(pred, two))));
+               check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, two)))));
+               check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, two))))));
+
+               check(2, make_app(pred, three));
+               check(1, make_app(pred, make_app(pred, three)));
+               check(0, make_app(pred, make_app(pred, make_app(pred, three))));
+               check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, three)))));
+               check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, three))))));
+
+               check(3, make_app(pred, four));
+               check(2, make_app(pred, make_app(pred, four)));
+               check(1, make_app(pred, make_app(pred, make_app(pred, four))));
+               check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, four)))));
+               check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, four))))));
+
+               check(4, make_app(pred, five));
+               check(3, make_app(pred, make_app(pred, five)));
+               check(2, make_app(pred, make_app(pred, make_app(pred, five))));
+               check(1, make_app(pred, make_app(pred, make_app(pred, make_app(pred, five)))));
+               check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, five))))));
+       }
+
+       print("checking pred1");
+       check_pred(pred1);
+
+       print("checking pred2");
+       check_pred(pred2);
+
+       print("checking sub");
+       check(0, make_app(make_app(sub, zero), zero));
+       check(0, make_app(make_app(sub, zero), one));
+       check(0, make_app(make_app(sub, zero), two));
+       check(0, make_app(make_app(sub, zero), three));
+       check(0, make_app(make_app(sub, zero), four));
+       check(0, make_app(make_app(sub, zero), five));
+       check(1, make_app(make_app(sub, one), zero));
+       check(0, make_app(make_app(sub, one), one));
+       check(0, make_app(make_app(sub, one), two));
+       check(0, make_app(make_app(sub, one), three));
+       check(0, make_app(make_app(sub, one), four));
+       check(0, make_app(make_app(sub, one), five));
+       check(2, make_app(make_app(sub, two), zero));
+       check(1, make_app(make_app(sub, two), one));
+       check(0, make_app(make_app(sub, two), two));
+       check(0, make_app(make_app(sub, two), three));
+       check(0, make_app(make_app(sub, two), four));
+       check(0, make_app(make_app(sub, two), five));
+       check(3, make_app(make_app(sub, three), zero));
+       check(2, make_app(make_app(sub, three), one));
+       check(1, make_app(make_app(sub, three), two));
+       check(0, make_app(make_app(sub, three), three));
+       check(0, make_app(make_app(sub, three), four));
+       check(0, make_app(make_app(sub, three), five));
+       check(4, make_app(make_app(sub, four), zero));
+       check(3, make_app(make_app(sub, four), one));
+       check(2, make_app(make_app(sub, four), two));
+       check(1, make_app(make_app(sub, four), three));
+       check(0, make_app(make_app(sub, four), four));
+       check(0, make_app(make_app(sub, four), five));
+       check(5, make_app(make_app(sub, five), zero));
+       check(4, make_app(make_app(sub, five), one));
+       check(3, make_app(make_app(sub, five), two));
+       check(2, make_app(make_app(sub, five), three));
+       check(1, make_app(make_app(sub, five), four));
+       check(0, make_app(make_app(sub, five), five));
+
+       print("checking min");
+       check(0, make_app(make_app(min, zero), zero));
+       check(0, make_app(make_app(min, zero), one));
+       check(0, make_app(make_app(min, zero), two));
+       check(0, make_app(make_app(min, zero), three));
+       check(0, make_app(make_app(min, zero), four));
+       check(0, make_app(make_app(min, zero), five));
+       check(0, make_app(make_app(min, one), zero));
+       check(1, make_app(make_app(min, one), one));
+       check(1, make_app(make_app(min, one), two));
+       check(1, make_app(make_app(min, one), three));
+       check(1, make_app(make_app(min, one), four));
+       check(1, make_app(make_app(min, one), five));
+       check(0, make_app(make_app(min, two), zero));
+       check(1, make_app(make_app(min, two), one));
+       check(2, make_app(make_app(min, two), two));
+       check(2, make_app(make_app(min, two), three));
+       check(2, make_app(make_app(min, two), four));
+       check(2, make_app(make_app(min, two), five));
+       check(0, make_app(make_app(min, three), zero));
+       check(1, make_app(make_app(min, three), one));
+       check(2, make_app(make_app(min, three), two));
+       check(3, make_app(make_app(min, three), three));
+       check(3, make_app(make_app(min, three), four));
+       check(3, make_app(make_app(min, three), five));
+       check(0, make_app(make_app(min, four), zero));
+       check(1, make_app(make_app(min, four), one));
+       check(2, make_app(make_app(min, four), two));
+       check(3, make_app(make_app(min, four), three));
+       check(4, make_app(make_app(min, four), four));
+       check(4, make_app(make_app(min, four), five));
+       check(0, make_app(make_app(min, five), zero));
+       check(1, make_app(make_app(min, five), one));
+       check(2, make_app(make_app(min, five), two));
+       check(3, make_app(make_app(min, five), three));
+       check(4, make_app(make_app(min, five), four));
+       check(5, make_app(make_app(min, five), five));
+
+       print("checking max");
+       check(0, make_app(make_app(max, zero), zero));
+       check(1, make_app(make_app(max, zero), one));
+       check(2, make_app(make_app(max, zero), two));
+       check(3, make_app(make_app(max, zero), three));
+       check(4, make_app(make_app(max, zero), four));
+       check(5, make_app(make_app(max, zero), five));
+       check(1, make_app(make_app(max, one), zero));
+       check(1, make_app(make_app(max, one), one));
+       check(2, make_app(make_app(max, one), two));
+       check(3, make_app(make_app(max, one), three));
+       check(4, make_app(make_app(max, one), four));
+       check(5, make_app(make_app(max, one), five));
+       check(2, make_app(make_app(max, two), zero));
+       check(2, make_app(make_app(max, two), one));
+       check(2, make_app(make_app(max, two), two));
+       check(3, make_app(make_app(max, two), three));
+       check(4, make_app(make_app(max, two), four));
+       check(5, make_app(make_app(max, two), five));
+       check(3, make_app(make_app(max, three), zero));
+       check(3, make_app(make_app(max, three), one));
+       check(3, make_app(make_app(max, three), two));
+       check(3, make_app(make_app(max, three), three));
+       check(4, make_app(make_app(max, three), four));
+       check(5, make_app(make_app(max, three), five));
+       check(4, make_app(make_app(max, four), zero));
+       check(4, make_app(make_app(max, four), one));
+       check(4, make_app(make_app(max, four), two));
+       check(4, make_app(make_app(max, four), three));
+       check(4, make_app(make_app(max, four), four));
+       check(5, make_app(make_app(max, four), five));
+       check(5, make_app(make_app(max, five), zero));
+       check(5, make_app(make_app(max, five), one));
+       check(5, make_app(make_app(max, five), two));
+       check(5, make_app(make_app(max, five), three));
+       check(5, make_app(make_app(max, five), four));
+       check(5, make_app(make_app(max, five), five));
+
+       print("checking lt");
+       checkbool(false, 0, make_app(make_app(lt, zero), zero));
+       checkbool(true, 0, make_app(make_app(lt, zero), one));
+       checkbool(true, 0, make_app(make_app(lt, zero), two));
+       checkbool(true, 0, make_app(make_app(lt, zero), three));
+       checkbool(true, 0, make_app(make_app(lt, zero), four));
+       checkbool(true, 0, make_app(make_app(lt, zero), five));
+       checkbool(false, 1, make_app(make_app(lt, one), zero));
+       checkbool(false, 1, make_app(make_app(lt, one), one));
+       checkbool(true, 1, make_app(make_app(lt, one), two));
+       checkbool(true, 1, make_app(make_app(lt, one), three));
+       checkbool(true, 1, make_app(make_app(lt, one), four));
+       checkbool(true, 1, make_app(make_app(lt, one), five));
+       checkbool(false, 2, make_app(make_app(lt, two), zero));
+       checkbool(false, 2, make_app(make_app(lt, two), one));
+       checkbool(false, 2, make_app(make_app(lt, two), two));
+       checkbool(true, 2, make_app(make_app(lt, two), three));
+       checkbool(true, 2, make_app(make_app(lt, two), four));
+       checkbool(true, 2, make_app(make_app(lt, two), five));
+       checkbool(false, 3, make_app(make_app(lt, three), zero));
+       checkbool(false, 3, make_app(make_app(lt, three), one));
+       checkbool(false, 3, make_app(make_app(lt, three), two));
+       checkbool(false, 3, make_app(make_app(lt, three), three));
+       checkbool(true, 3, make_app(make_app(lt, three), four));
+       checkbool(true, 3, make_app(make_app(lt, three), five));
+       checkbool(false, 4, make_app(make_app(lt, four), zero));
+       checkbool(false, 4, make_app(make_app(lt, four), one));
+       checkbool(false, 4, make_app(make_app(lt, four), two));
+       checkbool(false, 4, make_app(make_app(lt, four), three));
+       checkbool(false, 4, make_app(make_app(lt, four), four));
+       checkbool(true, 4, make_app(make_app(lt, four), five));
+       checkbool(false, 5, make_app(make_app(lt, five), zero));
+       checkbool(false, 5, make_app(make_app(lt, five), one));
+       checkbool(false, 5, make_app(make_app(lt, five), two));
+       checkbool(false, 5, make_app(make_app(lt, five), three));
+       checkbool(false, 5, make_app(make_app(lt, five), four));
+       checkbool(false, 5, make_app(make_app(lt, five), five));
+
+       print("checking leq");
+       checkbool(true, 0, make_app(make_app(leq, zero), zero));
+       checkbool(true, 0, make_app(make_app(leq, zero), one));
+       checkbool(true, 0, make_app(make_app(leq, zero), two));
+       checkbool(true, 0, make_app(make_app(leq, zero), three));
+       checkbool(true, 0, make_app(make_app(leq, zero), four));
+       checkbool(true, 0, make_app(make_app(leq, zero), five));
+       checkbool(false, 1, make_app(make_app(leq, one), zero));
+       checkbool(true, 1, make_app(make_app(leq, one), one));
+       checkbool(true, 1, make_app(make_app(leq, one), two));
+       checkbool(true, 1, make_app(make_app(leq, one), three));
+       checkbool(true, 1, make_app(make_app(leq, one), four));
+       checkbool(true, 1, make_app(make_app(leq, one), five));
+       checkbool(false, 2, make_app(make_app(leq, two), zero));
+       checkbool(false, 2, make_app(make_app(leq, two), one));
+       checkbool(true, 2, make_app(make_app(leq, two), two));
+       checkbool(true, 2, make_app(make_app(leq, two), three));
+       checkbool(true, 2, make_app(make_app(leq, two), four));
+       checkbool(true, 2, make_app(make_app(leq, two), five));
+       checkbool(false, 3, make_app(make_app(leq, three), zero));
+       checkbool(false, 3, make_app(make_app(leq, three), one));
+       checkbool(false, 3, make_app(make_app(leq, three), two));
+       checkbool(true, 3, make_app(make_app(leq, three), three));
+       checkbool(true, 3, make_app(make_app(leq, three), four));
+       checkbool(true, 3, make_app(make_app(leq, three), five));
+       checkbool(false, 4, make_app(make_app(leq, four), zero));
+       checkbool(false, 4, make_app(make_app(leq, four), one));
+       checkbool(false, 4, make_app(make_app(leq, four), two));
+       checkbool(false, 4, make_app(make_app(leq, four), three));
+       checkbool(true, 4, make_app(make_app(leq, four), four));
+       checkbool(true, 4, make_app(make_app(leq, four), five));
+       checkbool(false, 5, make_app(make_app(leq, five), zero));
+       checkbool(false, 5, make_app(make_app(leq, five), one));
+       checkbool(false, 5, make_app(make_app(leq, five), two));
+       checkbool(false, 5, make_app(make_app(leq, five), three));
+       checkbool(false, 5, make_app(make_app(leq, five), four));
+       checkbool(true, 5, make_app(make_app(leq, five), five));
+
+       print("checking eq");
+       checkbool(true, 0, make_app(make_app(eq, zero), zero));
+       checkbool(false, 0, make_app(make_app(eq, zero), one));
+       checkbool(false, 0, make_app(make_app(eq, zero), two));
+       checkbool(false, 0, make_app(make_app(eq, zero), three));
+       checkbool(false, 0, make_app(make_app(eq, zero), four));
+       checkbool(false, 0, make_app(make_app(eq, zero), five));
+       checkbool(false, 1, make_app(make_app(eq, one), zero));
+       checkbool(true, 1, make_app(make_app(eq, one), one));
+       checkbool(false, 1, make_app(make_app(eq, one), two));
+       checkbool(false, 1, make_app(make_app(eq, one), three));
+       checkbool(false, 1, make_app(make_app(eq, one), four));
+       checkbool(false, 1, make_app(make_app(eq, one), five));
+       checkbool(false, 2, make_app(make_app(eq, two), zero));
+       checkbool(false, 2, make_app(make_app(eq, two), one));
+       checkbool(true, 2, make_app(make_app(eq, two), two));
+       checkbool(false, 2, make_app(make_app(eq, two), three));
+       checkbool(false, 2, make_app(make_app(eq, two), four));
+       checkbool(false, 2, make_app(make_app(eq, two), five));
+       checkbool(false, 3, make_app(make_app(eq, three), zero));
+       checkbool(false, 3, make_app(make_app(eq, three), one));
+       checkbool(false, 3, make_app(make_app(eq, three), two));
+       checkbool(true, 3, make_app(make_app(eq, three), three));
+       checkbool(false, 3, make_app(make_app(eq, three), four));
+       checkbool(false, 3, make_app(make_app(eq, three), five));
+       checkbool(false, 4, make_app(make_app(eq, four), zero));
+       checkbool(false, 4, make_app(make_app(eq, four), one));
+       checkbool(false, 4, make_app(make_app(eq, four), two));
+       checkbool(false, 4, make_app(make_app(eq, four), three));
+       checkbool(true, 4, make_app(make_app(eq, four), four));
+       checkbool(false, 4, make_app(make_app(eq, four), five));
+       checkbool(false, 5, make_app(make_app(eq, five), zero));
+       checkbool(false, 5, make_app(make_app(eq, five), one));
+       checkbool(false, 5, make_app(make_app(eq, five), two));
+       checkbool(false, 5, make_app(make_app(eq, five), three));
+       checkbool(false, 5, make_app(make_app(eq, five), four));
+       checkbool(true, 5, make_app(make_app(eq, five), five));
+
+       print("checking div");
+       check(0, make_app(make_app(div, zero), one));
+       check(0, make_app(make_app(div, zero), two));
+       check(0, make_app(make_app(div, zero), three));
+       check(0, make_app(make_app(div, zero), four));
+       check(0, make_app(make_app(div, zero), five));
+       check(1, make_app(make_app(div, one), one));
+       check(0, make_app(make_app(div, one), two));
+       check(0, make_app(make_app(div, one), three));
+       check(0, make_app(make_app(div, one), four));
+       check(0, make_app(make_app(div, one), five));
+       check(2, make_app(make_app(div, two), one));
+       check(1, make_app(make_app(div, two), two));
+       check(0, make_app(make_app(div, two), three));
+       check(0, make_app(make_app(div, two), four));
+       check(0, make_app(make_app(div, two), five));
+       check(3, make_app(make_app(div, three), one));
+       check(1, make_app(make_app(div, three), two));
+       check(1, make_app(make_app(div, three), three));
+       check(0, make_app(make_app(div, three), four));
+       check(0, make_app(make_app(div, three), five));
+       check(4, make_app(make_app(div, four), one));
+       check(2, make_app(make_app(div, four), two));
+       check(1, make_app(make_app(div, four), three));
+       check(1, make_app(make_app(div, four), four));
+       check(0, make_app(make_app(div, four), five));
+       check(5, make_app(make_app(div, five), one));
+       check(2, make_app(make_app(div, five), two));
+       check(1, make_app(make_app(div, five), three));
+       check(1, make_app(make_app(div, five), four));
+       check(1, make_app(make_app(div, five), five));
+
+       print("checking mod");
+       check(0, make_app(make_app(mod, zero), one));
+       check(0, make_app(make_app(mod, zero), two));
+       check(0, make_app(make_app(mod, zero), three));
+       check(0, make_app(make_app(mod, zero), four));
+       check(0, make_app(make_app(mod, zero), five));
+       check(0, make_app(make_app(mod, one), one));
+       check(1, make_app(make_app(mod, one), two));
+       check(1, make_app(make_app(mod, one), three));
+       check(1, make_app(make_app(mod, one), four));
+       check(1, make_app(make_app(mod, one), five));
+       check(0, make_app(make_app(mod, two), one));
+       check(0, make_app(make_app(mod, two), two));
+       check(2, make_app(make_app(mod, two), three));
+       check(2, make_app(make_app(mod, two), four));
+       check(2, make_app(make_app(mod, two), five));
+       check(0, make_app(make_app(mod, three), one));
+       check(1, make_app(make_app(mod, three), two));
+       check(0, make_app(make_app(mod, three), three));
+       check(3, make_app(make_app(mod, three), four));
+       check(3, make_app(make_app(mod, three), five));
+       check(0, make_app(make_app(mod, four), one));
+       check(0, make_app(make_app(mod, four), two));
+       check(1, make_app(make_app(mod, four), three));
+       check(0, make_app(make_app(mod, four), four));
+       check(4, make_app(make_app(mod, four), five));
+       check(0, make_app(make_app(mod, five), one));
+       check(1, make_app(make_app(mod, five), two));
+       check(2, make_app(make_app(mod, five), three));
+       check(1, make_app(make_app(mod, five), four));
+       check(0, make_app(make_app(mod, five), five));
+
+       if (!g_cbv) {
+               print("checking fact1");
+               check(1, make_app(fact1, zero));
+               check(1, make_app(fact1, one));
+               check(2, make_app(fact1, two));
+               check(6, make_app(fact1, three));
+               check(24, make_app(fact1, four));
+       }
+
+       if (!g_cbv) {
+               print("checking fact2");
+               check(1, make_app(fact2, zero));
+               check(1, make_app(fact2, one));
+               check(2, make_app(fact2, two));
+               check(6, make_app(fact2, three));
+               check(24, make_app(fact2, four));
+       }
+
+       if (g_cbv<2) {
+               print("checking fact3");
+               check(1, make_app(fact3, zero));
+               check(1, make_app(fact3, one));
+               check(2, make_app(fact3, two));
+               check(6, make_app(fact3, three));
+               check(24, make_app(fact3, four));
+       }
+
+       if (!g_cbv) {
+               print("checking fact4");
+               check(1, make_app(fact4, zero));
+               check(1, make_app(fact4, one));
+               check(2, make_app(fact4, two));
+               check(6, make_app(fact4, three));
+               check(24, make_app(fact4, four));
+       }
+
+       if (g_cbv<2) {
+               print("checking fact5");
+               check(1, make_app(fact5, zero));
+               check(1, make_app(fact5, one));
+               check(2, make_app(fact5, two));
+               check(6, make_app(fact5, three));
+               check(24, make_app(fact5, four));
+       }
+
+}
+
+
+test();
+

diff --git a/code/lambda2.js b/code/lambda2.js
new file mode 100644 (file)
index 0000000..7dcb53d
--- /dev/null
+++ b/code/lambda2.js
@@ -0,0 +1,589 @@
+/*jslint bitwise: true,
+       eqeqeq: true,
+       immed: true,
+       newcap: true,
+       nomen: true,
+       onevar: true,
+       plusplus: true,
+       regexp: true,
+       rhino: true,
+       browser: false,
+       undef: true,
+       white: true,
+
+       evil: false,
+       regexp: false,
+       sub: true,
+       laxbreak: true,
+       onevar: false,
+       debug: true */
+
+
+// DeBruijn terms
+// substitution and translation algorithms from Chris Hankin, An Introduction to Lambda Calculi for Comptuer Scientists
+//
+function Db_free(variable) {
+       this.variable = variable;
+       this.subst = function (m, new_term) {
+               return this;
+       };
+       this.renumber = function (m, i) {
+               return this;
+       };
+       // we assume that other will have variable iff it's a Db_free
+       this.equal = function (other) {
+               return other.variable && this.variable.equal(other.variable);
+       };
+       this.contains = this.equal;
+}
+
+function Db_index(i) {
+       this.index = i;
+       this.subst = function (m, new_term) {
+               if (this.index < m) {
+                       return this;
+               } else if (this.index > m) {
+                       return new Db_index(this.index - 1);
+               } else {
+                       return new_term.renumber(this.index, 1);
+               }
+       };
+       this.renumber = function (m, i) {
+               if (this.index < i) {
+                       return this;
+               } else {
+                       return new Db_index(this.index + m - 1);
+               }
+       };
+       // we assume that other will have index iff it's a Db_index
+       this.equal = function (other) {
+               return this.index === other.index;
+       };
+       this.contains = this.equal;
+}
+
+function Db_app(left, right) {
+       this.left = left;
+       this.right = right;
+       this.subst = function (m, new_term) {
+               return new Db_app(this.left.subst(m, new_term), this.right.subst(m, new_term));
+       };
+       this.renumber = function (m, i) {
+               return new Db_app(this.left.renumber(m, i), this.right.renumber(m, i));
+       };
+       // we assume that other will have left iff it's a Db_app
+       this.equal = function (other) {
+               return other.left && this.left.equal(other.left) && this.right.equal(other.right);
+       };
+       this.contains = function (other) {
+               if (other.left && this.left.equal(other.left) && this.right.equal(other.right)) {
+                       return true;
+               } else {
+                       return this.left.contains(other) || this.right.contains(other);
+               }
+       };
+}
+
+function Db_lam(body) {
+       this.body = body;
+       this.subst = function (m, new_term) {
+               return new Db_lam(this.body.subst(m + 1, new_term));
+       };
+       this.renumber = function (m, i) {
+               return new Db_lam(this.body.renumber(m, i + 1));
+       };
+       // we assume that other will have body iff it's a Db_lam
+       this.equal = function (other) {
+               return other.body && this.body.equal(other.body);
+       };
+       this.contains = function (other) {
+               if (other.body && this.body.equal(other.body)) {
+                       return true;
+               } else {
+                       return this.body.contains(other);
+               }
+       };
+}
+
+
+// lambda terms
+// substitution and normal-order evaluator based on Haskell version by Oleg Kisleyov
+// http://okmij.org/ftp/Computation/lambda-calc.html#lambda-calculator-haskell
+//
+function Variable(name, tag) {
+       this.name = name;
+       this.tag = tag || 0;
+       this.to_string = function () {
+               // append count copies of str to accum
+               function markup(accum, count) {
+                       if (count === 0) {
+                               return accum;
+                       } else {
+                               return markup(accum + "'", count - 1);
+                       }
+               }
+               return markup(this.name, this.tag);
+       };
+       this.equal = function (other) {
+               return (this.tag === other.tag) && (this.name === other.name);
+       };
+       // position of this in seq
+       this.position = function (seq) {
+               for (var i = 0; i < seq.length; i += 1) {
+                       if (this.equal(seq[i])) {
+                               return new Db_index(i + 1);
+                       }
+               }
+               return new Db_free(this);
+       };
+}
+
+// if v occurs free_in term, returns Some v' where v' is the highest-tagged
+// variable with the same name as v occurring (free or bound) in term
+//
+function free_in(v, term) {
+       var res = term.has_free(v);
+       return res[0] && res[1];
+}
+
+function subst(v, new_term, expr) {
+       if (new_term.variable && new_term.variable.equal(v)) {
+               return expr;
+       } else {
+               return expr.subst(v, new_term);
+       }
+}
+
+function equal(expr1, expr2) {
+       return expr1.debruijn([]).equal(expr2.debruijn([]));
+}
+
+function contains(expr1, expr2) {
+       return expr1.debruijn([]).contains(expr2.debruijn([]));
+}
+
+
+function Lambda_var(variable) {
+       this.variable = variable;
+       this.debruijn = function (seq) {
+               return this.variable.position(seq);
+       };
+       this.to_string = function (as_atom) {
+               return this.variable.to_string();
+       };
+       this.has_free = function (v) {
+               if (v.name !== this.variable.name) {
+                       return [false, v];
+               } else if (v.tag === this.variable.tag) {
+                       return [true, v];
+               } else {
+                       return [false, this.variable];
+               }
+       };
+       this.subst = function (v, new_term) {
+               if (this.variable.equal(v)) {
+                       return new_term;
+               } else {
+                       return this;
+               }
+       };
+       this.check_eta = function () {
+               return this;
+       };
+       this.eval_loop = function (stack, eta) {
+               function unwind(left, stack) {
+                       if (stack.length === 0) {
+                               return left;
+                       } else {
+                               var x = stack[0];
+                               var xs = stack.slice(1);
+                               return unwind(new Lambda_app(left, x.eval_loop([], eta)), xs);
+                       }
+               }
+               return unwind(this, stack);
+       };
+       this.eval_cbv = function (aggressive) {
+               return this;
+       };
+}
+
+function Lambda_app(left, right) {
+       this.left = left;
+       this.right = right;
+       this.debruijn = function (seq) {
+               return new Db_app(this.left.debruijn(seq), this.right.debruijn(seq));
+       };
+       this.to_string = function (as_atom) {
+               var base;
+               if (this.left.left) {
+                       base = this.left.to_string() + " " + this.right.to_string(true);
+               } else {
+                       base = this.left.to_string(true) + " " + this.right.to_string(true);
+               }
+               if (as_atom) {
+                       return "(" + base + ")";
+               } else {
+                       return base;
+               }
+       };
+       this.has_free = function (v) {
+               var left_res = this.left.has_free(v);
+               var right_res = this.right.has_free(v);
+               var left_bool = left_res[0];
+               var right_bool = right_res[0];
+               var left_tag = left_res[1].tag;
+               var right_tag = right_res[1].tag;
+               var res;
+               if (left_tag > right_tag) {
+                       res = left_res[1];
+               } else {
+                       res = right_res[1];
+               }
+               return [left_bool || right_bool, res];
+       };
+       this.subst = function (v, new_term) {
+               return new Lambda_app(subst(v, new_term, this.left), subst(v, new_term, this.right));
+       };
+       this.check_eta = function () {
+               return this;
+       };
+       this.eval_loop = function (stack, eta) {
+               var new_stack = stack.slice(0);
+               new_stack.unshift(this.right);
+               return this.left.eval_loop(new_stack, eta);
+       };
+       this.eval_cbv = function (aggressive) {
+               var left = this.left.eval_cbv(aggressive);
+               var right = this.right.eval_cbv(aggressive);
+               if (left.body) {
+                       return subst(left.bound, right, left.body).eval_cbv(aggressive);
+               } else {
+                       return new Lambda_app(left, right);
+               }
+       };
+}
+
+
+//     (* if v occurs free_in term, returns Some v' where v' is the highest-tagged
+//      * variable with the same name as v occurring (free or bound) in term *)
+
+
+function Lambda_lam(variable, body) {
+       this.bound = variable;
+       this.body = body;
+       this.debruijn = function (seq) {
+               var new_seq = seq.slice(0);
+               new_seq.unshift(this.bound);
+               return new Db_lam(this.body.debruijn(new_seq));
+       };
+       this.to_string = function (as_atom) {
+               var base = "\\" + this.to_string_funct();
+               if (as_atom) {
+                       return "(" + base + ")";
+               } else {
+                       return base;
+               }
+       };
+       this.to_string_funct = function () {
+               if (this.body.to_string_funct) {
+                       return this.bound.to_string() + " " + this.body.to_string_funct();
+               } else {
+                       return this.bound.to_string() + ". " + this.body.to_string();
+               }
+       };
+       this.has_free = function (v) {
+               if (this.bound.equal(v)) {
+                       return [false, v];
+               } else {
+                       return this.body.has_free(v);
+               }
+       };
+       this.subst = function (v, new_term) {
+               function bump_tag(v1, v2) {
+                       var max;
+                       if (v1.tag > v2.tag) {
+                               max = v1.tag;
+                       } else {
+                               max = v2.tag;
+                       }
+                       return new Variable(v1.name, max + 1);
+               }
+               function bump_tag2(v1, v2) {
+                       if (v1.name !== v2.name) {
+                               return v1;
+                       } else {
+                               return bump_tag(v1, v2);
+                       }
+               }
+               if (this.bound.equal(v)) {
+                       return this;
+               } else {
+                       var res = free_in(this.bound, new_term);
+            // if x is free in the inserted term new_term, a capture is possible
+                       if (res) {
+                               // this.bound is free in new_term, need to alpha-convert
+                               var uniq_x = bump_tag2(bump_tag(this.bound, res), v);
+                               var res2 = free_in(uniq_x, this.body);
+                               if (res2) {
+                                       uniq_x = bump_tag(uniq_x, res2);
+                               }
+                               var body2 = subst(this.bound, new Lambda_var(uniq_x), this.body);
+                               return new Lambda_lam(uniq_x, subst(v, new_term, body2));
+                       } else {
+                               // this.bound not free in new_term, can substitute new_term for v without any captures
+                               return new Lambda_lam(this.bound, subst(v, new_term, this.body));
+                       }
+               }
+       };
+       this.check_eta = function () {
+               if (this.body.right && this.body.right.variable && this.bound.equal(this.body.right.variable) && !free_in(this.bound, this.body.left)) {
+                       return this.body.left;
+               } else {
+                       return this;
+               }
+       };
+       this.eval_loop = function (stack, eta) {
+               if (stack.length === 0) {
+                       var term = new Lambda_lam(this.bound, this.body.eval_loop([], eta));
+                       if (eta) {
+                               return term.check_eta();
+                       } else {
+                               return term;
+                       }
+               } else {
+                       var x = stack[0];
+                       var xs = stack.slice(1);
+                       return subst(this.bound, x, this.body).eval_loop(xs, eta);
+               }
+       };
+       this.eval_cbv = function (aggressive) {
+               if (aggressive) {
+                       return new Lambda_lam(this.bound, this.body.eval_cbv(aggressive));
+               } else {
+                       return this;
+               }
+       };
+       this.to_int = function (sofar) {
+               if (this.body.body && this.body.body.variable && this.body.bound.equal(this.body.body.variable)) {
+                       return 0 + sofar;
+               } else if (this.body.variable && this.bound.equal(this.body.variable)) {
+                       return 1 + sofar;
+               } else if (this.body.body && this.body.body.left && this.body.body.left.variable && this.bound.equal(this.body.body.left.variable)) {
+                       var new_int = new Lambda_lam(this.bound, new Lambda_lam(this.body.bound, this.body.body.right));
+                       return new_int.to_int(1 + sofar);
+               } else {
+                       return "not a church numeral";
+               }
+       };
+}
+
+
+
+///////////////////////////////////////////////////////////////////////////////////
+
+// cbv is false: use call-by-name
+// cbv is 1: use call-by-value, don't descend inside lambda
+// cbv is 2: applicative order
+function reduce(expr, eta, cbv) {
+       if (cbv) {
+               return expr.eval_cbv(cbv > 1);
+       } else {
+               return expr.eval_loop([], eta);
+       }
+}
+
+function make_var(name) {
+       return new Variable(name);
+}
+function make_app(aa, bb) {
+       return new Lambda_app(aa, bb);
+}
+function make_lam(a, aa) {
+       return new Lambda_lam(a, aa);
+}
+
+try {
+       if (console && console.debug) {
+               function print() {
+                       console.debug.apply(this, arguments);
+               }
+       }
+} catch (e) {}
+
+
+
+
+
+// // Basic data structure, essentially a LISP/Scheme-like cons
+// // pre-terminal nodes are expected to be of the form new cons(null, "string")
+// function cons(car, cdr) {
+//   this.car = car;
+//   this.cdr = cdr;
+// }
+
+// // takes a stack of symbols, returns a pair: a tree and the remaining symbols
+// function parse(split) {
+//   if (split == null) return (new cons (null, null));
+//   if (split.length == 0) return (new cons (null, null));
+//   var token = split.shift();
+//   if (token == ")") return (new cons (null, split));
+//   var next = parse(split);
+//   if (token == "(") {
+//     var nextnext = parse(next.cdr);
+//     return (new cons ((new cons (next.car, nextnext.car)),
+//                       nextnext.cdr));
+//   }
+//   return (new cons ((new cons ((new cons (null, token)),
+//                                next.car)),
+//                     next.cdr))
+// }
+
+// // substitute arg in for v in tree
+// function sub(tree, v, arg) {
+//   if (tree == null) return (null);
+//   if (tree.car == null) if (tree.cdr == v) return (arg);
+//   if (tree.car == null) return (tree);
+
+//   // perform alpha reduction to prevent variable collision
+//   if (isBindingForm(tree)) 
+//     return (new cons (tree.car, 
+//                       sub(sub(tree.cdr,         // inner sub = alpha reduc.
+//                               tree.cdr.car.cdr, 
+//                               fresh(tree.cdr.car.cdr)),
+//                           v,
+//                           arg)));
+
+//   return (new cons ((sub (tree.car, v, arg)),
+//                     (sub (tree.cdr, v, arg))))
+// }
+
+// // Guaranteed unique for each call as long as string is not empty.
+// var i = 0;
+// function fresh(string) {
+//   i = i+1;
+//   if (typeof(string) != "string") return (string);
+//   return (new cons (null,  
+//                     string.substring(0,1) + (i).toString()));
+// }
+
+// // Keep reducing until there is no more change
+// function fixedPoint (tree) {
+//   var t2 = reduce(tree);
+//   if (treeToString(tree) == treeToString(t2)) return (tree);
+//   return (fixedPoint (t2));
+// }
+
+// // Reduce all the arguments, then try to do beta conversion on the whole
+// function reduce(tree) {
+//   if (tree == null) return (tree);
+//   if (typeof(tree) == "string") return (tree);
+//   return (convert (new cons (reduce (tree.car), mapReduce (tree.cdr))));
+// }
+
+// // Reduce all the arguments in a list
+// function mapReduce(tree) {
+//   if (tree == null) return (tree);
+//   if (tree.car == null) return (tree);
+//   return (new cons (reduce (tree.car), mapReduce(tree.cdr )));
+// }
+
+// // If the list is of the form ((lambda var body) arg), do beta reduc.
+// function convert(tree) {
+//     if (isLet(tree)) {
+//       return (sub(tree.cdr.car, tree.car.cdr.car.cdr, tree.car.cdr.cdr.car));}
+//     else 
+//       if (isConvertable(tree)) {
+//         return (sub(tree.car.cdr.cdr.car, tree.car.cdr.car.cdr, tree.cdr.car));}
+//       else return(tree);
+// } 
+
+// // Is of form ((let var arg) body)?
+// function isLet(tree) {
+//   if (tree == null) return (false);
+//   if (!(isBindingForm(tree.car))) return (false);
+//   if (tree.car.car.cdr != "let") return (false);
+//   if (tree.cdr == null) return (false);
+//   if (tree.cdr.car == null) return (false);
+//   return(true);
+// }  
+
+// // Is of form ((lambda var body) arg)?
+// function isConvertable(tree) {
+//   if (tree == null) return (false);
+//   if (!(isBindingForm(tree.car))) return (false);
+//   if (tree.car.car.cdr != "lambda") return (false);
+//   if (tree.cdr == null) return (false);
+//   if (tree.cdr.car == null) return (false);
+//   return(true);
+// }  
+
+// // Is of form (lambda var body)?
+// function isBindingForm(tree) {
+//   if (tree == null) return (false);
+//   if (tree.car == null) return (false);
+//   if (tree.car.car != null) return (false);
+//   if ((tree.car.cdr != "lambda") 
+//       && (tree.car.cdr != "let")
+//       && (tree.car.cdr != "exists")
+//       && (tree.car.cdr != "forall")
+//       && (tree.car.cdr != "\u03BB")
+//       && (tree.car.cdr != "\u2200")
+//       && (tree.car.cdr != "\u2203")
+//      )
+//     return (false);
+//   if (tree.car.cdr == null) return (false);
+//   if (tree.cdr.car == null) return (false);
+//   if (tree.cdr.car.car != null) return (false);
+//   if (tree.cdr.cdr == null) return (false);
+//   return (true);
+// }
+
+// function treeToString(tree) {
+//   if (tree == null) return ("")
+//   if (tree.car == null) return (tree.cdr)
+//   if ((tree.car).car == null) 
+//     return (treeToString(tree.car) + " " + treeToString(tree.cdr))
+//   return ("(" + treeToString(tree.car) + ")" + treeToString(tree.cdr))
+// }
+
+// // use this instead of treeToString if you want to see the full structure
+// function treeToStringRaw(tree) {
+//   if (tree == null) return ("@")
+//   if (typeof(tree) == "string") return (tree);
+//   return ("(" + treeToStringRaw(tree.car) + "." + 
+//                 treeToStringRaw(tree.cdr) + ")")
+// }
+
+// // Make sure each paren will count as a separate token
+// function stringToTree(input) {
+//   input = input.replace(/let/g, " ( ( let ");
+//   input = input.replace(/=/g, " ");
+//   input = input.replace(/in/g, " ) ");
+//   input = input.replace(/\(/g, " ( ");
+//   input = input.replace(/\)/g, " ) ");
+//   input = input.replace(/;.*\n/g," ");
+//   input = input.replace(/\^/g, " ^ ");
+//   input = input.replace(/[\\]/g, " lambda ");
+//   input = input.replace(/\u03BB/g, " lambda ");
+//   return ((parse(input.split(/[ \f\n\r\t\v]+/))).car)
+// }
+
+// // Adjust spaces to print pretty
+// function formatTree(tree) {
+//   output = treeToStringRaw (tree);
+//   output = output.replace(/^[ \f\n\r\t\v]+/, "");
+//   output = output.replace(/[ \f\n\r\t\v]+$/, "");
+//   output = output.replace(/[ \f\n\r\t\v]+\)/g, ")");
+//   output = output.replace(/\)([^)(])/g, ") $1");
+//   output = output.replace(/lambda/g, "\\");
+// //  output = output.replace(/lambda/g, "\u03BB");
+// //  output = output.replace(/exists/g, "\u2203");
+// //  output = output.replace(/forall/g, "\u2200");
+//   return (output)
+// }
+
+// function mytry(form) { 
+//   i = 0;
+//   form.result.value = formatTree((stringToTree(form.input.value)));
+//   // form.result.value = formatTree(fixedPoint(stringToTree(form.input.value)));
+// }