X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=code%2Flambda.js;fp=code%2Flambda.js;h=f87b3559daaabf2acedd2261971a503f3c1507e5;hp=7dcb53d296ceacbfdab5f21a90528a1754c67005;hb=516417f5f9ac78553dd1788e263878ff6016f21d;hpb=7a8b2473541fe004b8c31d7238aaa337f24fa6f5

diff --git a/code/lambda.js b/code/lambda.js
index 7dcb53d2..f87b3559 100644
--- a/code/lambda.js
+++ b/code/lambda.js
@@ -1,108 +1,108 @@
 /*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,156 @@ 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);
-			}
-		}
-		return new Db_free(this);
-	};
+    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];
+    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);
-			}
-		}
-		return unwind(this, stack);
-	};
-	this.eval_cbv = function (aggressive) {
-		return this;
-	};
+    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);
-		}
-	};
+    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);
+        }
+    };
 }
 
 
@@ -269,112 +269,112 @@ 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_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";
-		}
-	};
+            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";
+        }
+    };
 }
 
 
@@ -385,29 +385,29 @@ 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);
+    }
 }
 
 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) {}