/*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); var s = this.name; for (var count = 0; count < this.tag; count += 1) { s += "'"; } return s; }; 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); // } var res = left, x; while (stack.length) { x = stack.shift(); // res = new Lambda_app(res, x.eval_loop([], eta)); res = new Lambda_app(res, reduce(x, eta, false)); } return res; } // return unwind(this, stack); // trampoline to, args return [null, 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); // trampoline to, args return [this.left, 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_dotted(); if (as_atom) { return "(" + base + ")"; } else { return base; } }; this.to_dotted = function () { if (this.body.to_dotted) { return this.bound.to_string() + " " + this.body.to_dotted(); } 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)); var term = new Lambda_lam(this.bound, reduce(this.body, eta, false)); if (eta) { return [null, term.check_eta()]; } else { return [null, term]; } } else { var x = stack[0]; var xs = stack.slice(1); // return subst(this.bound, x, this.body).eval_loop(xs, eta); // trampoline to, args return [subst(this.bound, x, this.body), 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"; // } var res = 0, s = this.bound, z, cursor; if (this.body.variable && s.equal(this.body.variable)) { return 1; } else if (this.body.bound) { z = this.body.bound; cursor = this.body.body; while (cursor.left && cursor.left.variable && s.equal(cursor.left.variable)) { res += 1; cursor = cursor.right; } if (cursor.variable && z.equal(cursor.variable)) { return res; } } 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); // using trampoline to reduce call stack overflows var to_eval = expr, res = [[], eta]; while (to_eval !== null) { res = to_eval.eval_loop.apply(to_eval, res); to_eval = res.shift(); } return res[0]; } } 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) {} /* Chris's original // 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))); } */