1 /*jslint bitwise: true,
23 // substitution and translation algorithms from Chris Hankin, An Introduction to Lambda Calculi for Comptuer Scientists
25 function Db_free(variable) {
26 this.variable = variable;
27 this.subst = function (m, new_term) {
30 this.renumber = function (m, i) {
33 // we assume that other will have variable iff it's a Db_free
34 this.equal = function (other) {
35 return other.variable && this.variable.equal(other.variable);
37 this.contains = this.equal;
40 function Db_index(i) {
42 this.subst = function (m, new_term) {
45 } else if (this.index > m) {
46 return new Db_index(this.index - 1);
48 return new_term.renumber(this.index, 1);
51 this.renumber = function (m, i) {
55 return new Db_index(this.index + m - 1);
58 // we assume that other will have index iff it's a Db_index
59 this.equal = function (other) {
60 return this.index === other.index;
62 this.contains = this.equal;
65 function Db_app(left, right) {
68 this.subst = function (m, new_term) {
69 return new Db_app(this.left.subst(m, new_term), this.right.subst(m, new_term));
71 this.renumber = function (m, i) {
72 return new Db_app(this.left.renumber(m, i), this.right.renumber(m, i));
74 // we assume that other will have left iff it's a Db_app
75 this.equal = function (other) {
76 return other.left && this.left.equal(other.left) && this.right.equal(other.right);
78 this.contains = function (other) {
79 if (other.left && this.left.equal(other.left) && this.right.equal(other.right)) {
82 return this.left.contains(other) || this.right.contains(other);
87 function Db_lam(body) {
89 this.subst = function (m, new_term) {
90 return new Db_lam(this.body.subst(m + 1, new_term));
92 this.renumber = function (m, i) {
93 return new Db_lam(this.body.renumber(m, i + 1));
95 // we assume that other will have body iff it's a Db_lam
96 this.equal = function (other) {
97 return other.body && this.body.equal(other.body);
99 this.contains = function (other) {
100 if (other.body && this.body.equal(other.body)) {
103 return this.body.contains(other);
110 // substitution and normal-order evaluator based on Haskell version by Oleg Kisleyov
111 // http://okmij.org/ftp/Computation/lambda-calc.html#lambda-calculator-haskell
113 function Variable(name, tag) {
116 this.to_string = function () {
117 // append count copies of str to accum
118 // function markup(accum, count) {
119 // if (count === 0) {
122 // return markup(accum + "'", count - 1);
125 // return markup(this.name, this.tag);
127 for (var count = 0; count < this.tag; count += 1) {
132 this.equal = function (other) {
133 return (this.tag === other.tag) && (this.name === other.name);
135 // position of this in seq
136 this.position = function (seq) {
137 for (var i = 0; i < seq.length; i += 1) {
138 if (this.equal(seq[i])) {
139 return new Db_index(i + 1);
142 return new Db_free(this);
146 // if v occurs free_in term, returns Some v' where v' is the highest-tagged
147 // variable with the same name as v occurring (free or bound) in term
149 function free_in(v, term) {
150 var res = term.has_free(v);
151 return res[0] && res[1];
154 function subst(v, new_term, expr) {
155 if (new_term.variable && new_term.variable.equal(v)) {
158 return expr.subst(v, new_term);
162 function equal(expr1, expr2) {
163 return expr1.debruijn([]).equal(expr2.debruijn([]));
166 function contains(expr1, expr2) {
167 return expr1.debruijn([]).contains(expr2.debruijn([]));
171 function Lambda_var(variable) {
172 this.variable = variable;
173 this.debruijn = function (seq) {
174 return this.variable.position(seq);
176 this.to_string = function (as_atom) {
177 return this.variable.to_string();
179 this.has_free = function (v) {
180 if (v.name !== this.variable.name) {
182 } else if (v.tag === this.variable.tag) {
185 return [false, this.variable];
188 this.subst = function (v, new_term) {
189 if (this.variable.equal(v)) {
195 this.check_eta = function () {
198 this.eval_loop = function (stack, eta) {
199 function unwind(left, stack) {
200 // if (stack.length === 0) {
204 // var xs = stack.slice(1);
205 // return unwind(new Lambda_app(left, x.eval_loop([], eta)), xs);
208 while (stack.length) {
210 res = new Lambda_app(res, x.eval_loop([], eta));
214 return unwind(this, stack);
216 this.eval_cbv = function (aggressive) {
221 function Lambda_app(left, right) {
224 this.debruijn = function (seq) {
225 return new Db_app(this.left.debruijn(seq), this.right.debruijn(seq));
227 this.to_string = function (as_atom) {
229 if (this.left.left) {
230 base = this.left.to_string() + " " + this.right.to_string(true);
232 base = this.left.to_string(true) + " " + this.right.to_string(true);
235 return "(" + base + ")";
240 this.has_free = function (v) {
241 var left_res = this.left.has_free(v);
242 var right_res = this.right.has_free(v);
243 var left_bool = left_res[0];
244 var right_bool = right_res[0];
245 var left_tag = left_res[1].tag;
246 var right_tag = right_res[1].tag;
248 if (left_tag > right_tag) {
253 return [left_bool || right_bool, res];
255 this.subst = function (v, new_term) {
256 return new Lambda_app(subst(v, new_term, this.left), subst(v, new_term, this.right));
258 this.check_eta = function () {
261 this.eval_loop = function (stack, eta) {
262 var new_stack = stack.slice(0);
263 new_stack.unshift(this.right);
264 return this.left.eval_loop(new_stack, eta);
266 this.eval_cbv = function (aggressive) {
267 var left = this.left.eval_cbv(aggressive);
268 var right = this.right.eval_cbv(aggressive);
270 return subst(left.bound, right, left.body).eval_cbv(aggressive);
272 return new Lambda_app(left, right);
278 // (* if v occurs free_in term, returns Some v' where v' is the highest-tagged
279 // * variable with the same name as v occurring (free or bound) in term *)
282 function Lambda_lam(variable, body) {
283 this.bound = variable;
285 this.debruijn = function (seq) {
286 var new_seq = seq.slice(0);
287 new_seq.unshift(this.bound);
288 return new Db_lam(this.body.debruijn(new_seq));
290 this.to_string = function (as_atom) {
291 var base = "\\" + this.to_string_funct();
293 return "(" + base + ")";
298 this.to_string_funct = function () {
299 if (this.body.to_string_funct) {
300 return this.bound.to_string() + " " + this.body.to_string_funct();
302 return this.bound.to_string() + ". " + this.body.to_string();
305 this.has_free = function (v) {
306 if (this.bound.equal(v)) {
309 return this.body.has_free(v);
312 this.subst = function (v, new_term) {
313 function bump_tag(v1, v2) {
315 if (v1.tag > v2.tag) {
320 return new Variable(v1.name, max + 1);
322 function bump_tag2(v1, v2) {
323 if (v1.name !== v2.name) {
326 return bump_tag(v1, v2);
329 if (this.bound.equal(v)) {
332 var res = free_in(this.bound, new_term);
333 // if x is free in the inserted term new_term, a capture is possible
335 // this.bound is free in new_term, need to alpha-convert
336 var uniq_x = bump_tag2(bump_tag(this.bound, res), v);
337 var res2 = free_in(uniq_x, this.body);
339 uniq_x = bump_tag(uniq_x, res2);
341 var body2 = subst(this.bound, new Lambda_var(uniq_x), this.body);
342 return new Lambda_lam(uniq_x, subst(v, new_term, body2));
344 // this.bound not free in new_term, can substitute new_term for v without any captures
345 return new Lambda_lam(this.bound, subst(v, new_term, this.body));
349 this.check_eta = function () {
350 if (this.body.right && this.body.right.variable && this.bound.equal(this.body.right.variable) && !free_in(this.bound, this.body.left)) {
351 return this.body.left;
356 this.eval_loop = function (stack, eta) {
357 if (stack.length === 0) {
358 var term = new Lambda_lam(this.bound, this.body.eval_loop([], eta));
360 return term.check_eta();
366 var xs = stack.slice(1);
367 return subst(this.bound, x, this.body).eval_loop(xs, eta);
370 this.eval_cbv = function (aggressive) {
372 return new Lambda_lam(this.bound, this.body.eval_cbv(aggressive));
377 this.to_int = function (sofar) {
378 // if (this.body.body && this.body.body.variable && this.body.bound.equal(this.body.body.variable)) {
380 // } else if (this.body.variable && this.bound.equal(this.body.variable)) {
382 // } else if (this.body.body && this.body.body.left && this.body.body.left.variable && this.bound.equal(this.body.body.left.variable)) {
383 // var new_int = new Lambda_lam(this.bound, new Lambda_lam(this.body.bound, this.body.body.right));
384 // return new_int.to_int(1 + sofar);
386 // return "not a church numeral";
388 var res = 0, s = this.bound, z, cursor;
389 if (this.body.variable && s.equal(this.body.variable)) {
391 } else if (this.body.bound) {
393 cursor = this.body.body;
394 while (cursor.left && cursor.left.variable && s.equal(cursor.left.variable)) {
396 cursor = cursor.right;
398 if (cursor.variable && z.equal(cursor.variable)) {
402 return "not a church numeral";
408 ///////////////////////////////////////////////////////////////////////////////////
410 // cbv is false: use call-by-name
411 // cbv is 1: use call-by-value, don't descend inside lambda
412 // cbv is 2: applicative order
413 function reduce(expr, eta, cbv) {
415 return expr.eval_cbv(cbv > 1);
417 return expr.eval_loop([], eta);
421 function make_var(name) {
422 return new Variable(name);
424 function make_app(aa, bb) {
425 return new Lambda_app(aa, bb);
427 function make_lam(a, aa) {
428 return new Lambda_lam(a, aa);
432 if (console && console.debug) {
434 console.debug.apply(this, arguments);
441 let false = \x y. y in
442 let and = \l r. l r false in
443 let or = \l r. l true r in
444 let pair = \u v f. f u v in
445 let triple = \u v w f. f u v w in
446 let succ = \n s z. s (n s z) in
447 let pred = \n s z. n (\u v. v (u s)) (K z) I in
448 let ifzero = \n. n (\u v. v (u succ)) (K 0) (\n withp whenz. withp n) in
449 let add = \m n. n succ m in
450 let mul = \m n. n (\z. add m z) 0 in
451 let mul = \m n s. m (n s) in
452 let sub = (\mzero msucc mtail. \m n. n mtail (m msucc mzero) true) (pair 0 I) (\d. d (\a b. pair (succ a) (K d))) (\d. d false d) in
453 let min = \m n. sub m (sub m n) in
454 let max = \m n. add n (sub m n) in
455 let lt = (\mzero msucc mtail. \n m. n mtail (m msucc mzero) true (\x. true) false) (pair 0 I) (\d. d (\a b. pair (succ a) (K d))) (\d. d false d) in
456 let leq = (\mzero msucc mtail. \m n. n mtail (m msucc mzero) true (\x. false) true) (pair 0 I) (\d. d (\a b. pair (succ a) (K d))) (\d. d false d) in
457 let eq = (\mzero msucc mtail. \m n. n mtail (m msucc mzero) true (\x. false) true) (pair 0 (K (pair 1 I))) (\d. d (\a b. pair (succ a) (K d))) (\d. d false d) in
458 let divmod = (\mzero msucc mtail. \n divisor.
459 (\dhead. n (mtail dhead) (\sel. dhead (sel 0 0)))
460 (divisor msucc mzero (\a b c. c x))
461 (\d m a b c. pair d m) )
462 (triple succ (K 0) I)
463 (\d. triple I succ (K d))
464 (\dhead d. d (\dz mz df mf drest sel. drest dhead (sel (df dz) (mf mz)))) in
465 let div = \n d. divmod n d true in
466 let mod = \n d. divmod n d false in
467 let Y = \f. (\y. f(y y)) (\y. f(y y)) in
468 let Z = (\u f. f(u u f)) (\u f. f(u u f)) in
469 let fact = \y. y (\f n. ifzero n (\p. mul n (f p)) 1) in
475 // // Basic data structure, essentially a LISP/Scheme-like cons
476 // // pre-terminal nodes are expected to be of the form new cons(null, "string")
477 // function cons(car, cdr) {
482 // // takes a stack of symbols, returns a pair: a tree and the remaining symbols
483 // function parse(split) {
484 // if (split == null) return (new cons (null, null));
485 // if (split.length == 0) return (new cons (null, null));
486 // var token = split.shift();
487 // if (token == ")") return (new cons (null, split));
488 // var next = parse(split);
489 // if (token == "(") {
490 // var nextnext = parse(next.cdr);
491 // return (new cons ((new cons (next.car, nextnext.car)),
494 // return (new cons ((new cons ((new cons (null, token)),
499 // // substitute arg in for v in tree
500 // function sub(tree, v, arg) {
501 // if (tree == null) return (null);
502 // if (tree.car == null) if (tree.cdr == v) return (arg);
503 // if (tree.car == null) return (tree);
505 // // perform alpha reduction to prevent variable collision
506 // if (isBindingForm(tree))
507 // return (new cons (tree.car,
508 // sub(sub(tree.cdr, // inner sub = alpha reduc.
510 // fresh(tree.cdr.car.cdr)),
514 // return (new cons ((sub (tree.car, v, arg)),
515 // (sub (tree.cdr, v, arg))))
518 // // Guaranteed unique for each call as long as string is not empty.
520 // function fresh(string) {
522 // if (typeof(string) != "string") return (string);
523 // return (new cons (null,
524 // string.substring(0,1) + (i).toString()));
527 // // Keep reducing until there is no more change
528 // function fixedPoint (tree) {
529 // var t2 = reduce(tree);
530 // if (treeToString(tree) == treeToString(t2)) return (tree);
531 // return (fixedPoint (t2));
534 // // Reduce all the arguments, then try to do beta conversion on the whole
535 // function reduce(tree) {
536 // if (tree == null) return (tree);
537 // if (typeof(tree) == "string") return (tree);
538 // return (convert (new cons (reduce (tree.car), mapReduce (tree.cdr))));
541 // // Reduce all the arguments in a list
542 // function mapReduce(tree) {
543 // if (tree == null) return (tree);
544 // if (tree.car == null) return (tree);
545 // return (new cons (reduce (tree.car), mapReduce(tree.cdr )));
548 // // If the list is of the form ((lambda var body) arg), do beta reduc.
549 // function convert(tree) {
550 // if (isLet(tree)) {
551 // return (sub(tree.cdr.car, tree.car.cdr.car.cdr, tree.car.cdr.cdr.car));}
553 // if (isConvertable(tree)) {
554 // return (sub(tree.car.cdr.cdr.car, tree.car.cdr.car.cdr, tree.cdr.car));}
555 // else return(tree);
558 // // Is of form ((let var arg) body)?
559 // function isLet(tree) {
560 // if (tree == null) return (false);
561 // if (!(isBindingForm(tree.car))) return (false);
562 // if (tree.car.car.cdr != "let") return (false);
563 // if (tree.cdr == null) return (false);
564 // if (tree.cdr.car == null) return (false);
568 // // Is of form ((lambda var body) arg)?
569 // function isConvertable(tree) {
570 // if (tree == null) return (false);
571 // if (!(isBindingForm(tree.car))) return (false);
572 // if (tree.car.car.cdr != "lambda") return (false);
573 // if (tree.cdr == null) return (false);
574 // if (tree.cdr.car == null) return (false);
578 // // Is of form (lambda var body)?
579 // function isBindingForm(tree) {
580 // if (tree == null) return (false);
581 // if (tree.car == null) return (false);
582 // if (tree.car.car != null) return (false);
583 // if ((tree.car.cdr != "lambda")
584 // && (tree.car.cdr != "let")
585 // && (tree.car.cdr != "exists")
586 // && (tree.car.cdr != "forall")
587 // && (tree.car.cdr != "\u03BB")
588 // && (tree.car.cdr != "\u2200")
589 // && (tree.car.cdr != "\u2203")
592 // if (tree.car.cdr == null) return (false);
593 // if (tree.cdr.car == null) return (false);
594 // if (tree.cdr.car.car != null) return (false);
595 // if (tree.cdr.cdr == null) return (false);
599 // function treeToString(tree) {
600 // if (tree == null) return ("")
601 // if (tree.car == null) return (tree.cdr)
602 // if ((tree.car).car == null)
603 // return (treeToString(tree.car) + " " + treeToString(tree.cdr))
604 // return ("(" + treeToString(tree.car) + ")" + treeToString(tree.cdr))
607 // // use this instead of treeToString if you want to see the full structure
608 // function treeToStringRaw(tree) {
609 // if (tree == null) return ("@")
610 // if (typeof(tree) == "string") return (tree);
611 // return ("(" + treeToStringRaw(tree.car) + "." +
612 // treeToStringRaw(tree.cdr) + ")")
615 // // Make sure each paren will count as a separate token
616 // function stringToTree(input) {
617 // input = input.replace(/let/g, " ( ( let ");
618 // input = input.replace(/=/g, " ");
619 // input = input.replace(/in/g, " ) ");
620 // input = input.replace(/\(/g, " ( ");
621 // input = input.replace(/\)/g, " ) ");
622 // input = input.replace(/;.*\n/g," ");
623 // input = input.replace(/\^/g, " ^ ");
624 // input = input.replace(/[\\]/g, " lambda ");
625 // input = input.replace(/\u03BB/g, " lambda ");
626 // return ((parse(input.split(/[ \f\n\r\t\v]+/))).car)
629 // // Adjust spaces to print pretty
630 // function formatTree(tree) {
631 // output = treeToStringRaw (tree);
632 // output = output.replace(/^[ \f\n\r\t\v]+/, "");
633 // output = output.replace(/[ \f\n\r\t\v]+$/, "");
634 // output = output.replace(/[ \f\n\r\t\v]+\)/g, ")");
635 // output = output.replace(/\)([^)(])/g, ") $1");
636 // output = output.replace(/lambda/g, "\\");
637 // // output = output.replace(/lambda/g, "\u03BB");
638 // // output = output.replace(/exists/g, "\u2203");
639 // // output = output.replace(/forall/g, "\u2200");
643 // function mytry(form) {
645 // form.result.value = formatTree((stringToTree(form.input.value)));
646 // // form.result.value = formatTree(fixedPoint(stringToTree(form.input.value)));