+++ /dev/null
-/*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)));
-}
-
-*/
-