From 3233e0fee04bb48a809c020b43ba23d78c95aea3 Mon Sep 17 00:00:00 2001
From: Jim Pryor <profjim@jimpryor.net>
Date: Thu, 23 Sep 2010 02:22:02 -0400
Subject: [PATCH] shift over to new parser and evaluator

Signed-off-by: Jim Pryor <profjim@jimpryor.net>
---
 code/{lambda2-test.js => lambda-test.js} |   2 +-
 code/lambda.js                           | 759 ++++++++++++++++++++++++-------
 code/lambda2.js                          | 589 ------------------------
 3 files changed, 589 insertions(+), 761 deletions(-)
 rename code/{lambda2-test.js => lambda-test.js} (99%)
 delete mode 100644 code/lambda2.js

diff --git a/code/lambda2-test.js b/code/lambda-test.js
similarity index 99%
rename from code/lambda2-test.js
rename to code/lambda-test.js
index 09a1b5bc..8f5fe4a6 100644
--- a/code/lambda2-test.js
+++ b/code/lambda-test.js
@@ -1,4 +1,4 @@
-load("lambda2.js");
+load("lambda.js");
 
 
 var g_eta = false;
diff --git a/code/lambda.js b/code/lambda.js
index c28a0c17..7dcb53d2 100644
--- a/code/lambda.js
+++ b/code/lambda.js
@@ -1,172 +1,589 @@
-// 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 fold(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 = fold(split);
-  if (token == "(") {
-    var nextnext = fold(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 ((fold(input.split(/[ \f\n\r\t\v]+/))).car)
-}
-
-// Adjust spaces to print pretty
-function formatTree(tree) {
-  output = treeToString (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(fixedPoint(stringToTree(form.input.value)));
+/*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)));
+// }
diff --git a/code/lambda2.js b/code/lambda2.js
deleted file mode 100644
index 7dcb53d2..00000000
--- a/code/lambda2.js
+++ /dev/null
@@ -1,589 +0,0 @@
-/*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)));
-// }
-- 
2.11.0