posted more about... for week 4
[lambda.git] / code / lambda.js
index 7dcb53d..955254b 100644 (file)
 /*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 */
+    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;
+    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;
+    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);
-               }
-       };
+    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);
-               }
-       };
+    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);
+        }
+    };
 }
 
 
@@ -111,156 +111,172 @@ function Db_lam(body) {
 // 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);
-                       }
+    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 new Db_free(this);
-       };
+               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];
+    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);
-       }
+    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([]));
+    return expr1.debruijn([]).equal(expr2.debruijn([]));
 }
 
 function contains(expr1, expr2) {
-       return expr1.debruijn([]).contains(expr2.debruijn([]));
+    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);
+    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 unwind(this, stack);
-       };
-       this.eval_cbv = function (aggressive) {
-               return this;
-       };
+                       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);
-       };
-       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);
-               }
-       };
+    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);
+        }
+    };
 }
 
 
@@ -269,112 +285,130 @@ function Lambda_app(left, right) {
 
 
 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);
+    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));
+            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 term.check_eta();
+                               return [null, term.check_eta()];
                        } else {
-                               return term;
+                               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;
                        }
-               } 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";
                }
-       };
+               return "not a church numeral";
+    };
 }
 
 
@@ -385,205 +419,216 @@ function Lambda_lam(variable, body) {
 // 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);
-       }
+    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);
+    return new Variable(name);
 }
 function make_app(aa, bb) {
-       return new Lambda_app(aa, bb);
+    return new Lambda_app(aa, bb);
 }
 function make_lam(a, aa) {
-       return new Lambda_lam(a, aa);
+    return new Lambda_lam(a, aa);
 }
 
 try {
-       if (console && console.debug) {
-               function print() {
-                       console.debug.apply(this, arguments);
-               }
-       }
+    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)));
+}
+
+*/
 
-// // 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)));
-// }