From: Jim Pryor Date: Thu, 23 Sep 2010 05:50:15 +0000 (-0400) Subject: coverted Oleg's Haskell lib -> ML -> JS X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=98652627403eaa920f51cedc4d0cc68c1103b972 coverted Oleg's Haskell lib -> ML -> JS Signed-off-by: Jim Pryor --- diff --git a/code/lambda.ml b/code/lambda.ml index 146c9eb4..1eaca652 100644 --- a/code/lambda.ml +++ b/code/lambda.ml @@ -2,191 +2,204 @@ 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 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 - | `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 - 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 - | [] -> 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 - | `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 - 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 - 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 + (* 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 - | `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 +(* + * 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' - | `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 - 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 - | `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 + + + 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 - | `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 - | 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 - (* (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 - | `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 - - (* 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] - | `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) = @@ -228,10 +241,10 @@ module Private = struct ... | `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 - 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 -> [] - | `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 - | `App(t1,t2) -> + | `App(t1, t2) -> 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)) - | `App(t1,t2) -> + | `App(t1, 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(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 - | (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 = @@ -340,7 +353,7 @@ module Private = struct | `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)) @@ -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 - | `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") @@ -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 -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 index 00000000..09a1b5bc --- /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 index 00000000..7dcb53d2 --- /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))); +// }