code/lambda.js

   1 /*jslint bitwise: true,
   2     eqeqeq: true,
   3     immed: true,
   4     newcap: true,
   5     nomen: true,
   6     onevar: true,
   7     plusplus: true,
   8     regexp: true,
   9     rhino: true,
  10     browser: false,
  11     undef: true,
  12     white: true,
  13
  14     evil: false,
  15     regexp: false,
  16     sub: true,
  17     laxbreak: true,
  18     onevar: false,
  19     debug: true */
  20
  21
  22 // DeBruijn terms
  23 // substitution and translation algorithms from Chris Hankin, An Introduction to Lambda Calculi for Comptuer Scientists
  24 //
  25 function Db_free(variable) {
  26     this.variable = variable;
  27     this.subst = function (m, new_term) {
  28         return this;
  29     };
  30     this.renumber = function (m, i) {
  31         return this;
  32     };
  33     // we assume that other will have variable iff it's a Db_free
  34     this.equal = function (other) {
  35         return other.variable && this.variable.equal(other.variable);
  36     };
  37     this.contains = this.equal;
  38 }
  39
  40 function Db_index(i) {
  41     this.index = i;
  42     this.subst = function (m, new_term) {
  43         if (this.index < m) {
  44             return this;
  45         } else if (this.index > m) {
  46             return new Db_index(this.index - 1);
  47         } else {
  48             return new_term.renumber(this.index, 1);
  49         }
  50     };
  51     this.renumber = function (m, i) {
  52         if (this.index < i) {
  53             return this;
  54         } else {
  55             return new Db_index(this.index + m - 1);
  56         }
  57     };
  58     // we assume that other will have index iff it's a Db_index
  59     this.equal = function (other) {
  60         return this.index === other.index;
  61     };
  62     this.contains = this.equal;
  63 }
  64
  65 function Db_app(left, right) {
  66     this.left = left;
  67     this.right = right;
  68     this.subst = function (m, new_term) {
  69         return new Db_app(this.left.subst(m, new_term), this.right.subst(m, new_term));
  70     };
  71     this.renumber = function (m, i) {
  72         return new Db_app(this.left.renumber(m, i), this.right.renumber(m, i));
  73     };
  74     // we assume that other will have left iff it's a Db_app
  75     this.equal = function (other) {
  76         return other.left && this.left.equal(other.left) && this.right.equal(other.right);
  77     };
  78     this.contains = function (other) {
  79         if (other.left && this.left.equal(other.left) && this.right.equal(other.right)) {
  80             return true;
  81         } else {
  82             return this.left.contains(other) || this.right.contains(other);
  83         }
  84     };
  85 }
  86
  87 function Db_lam(body) {
  88     this.body = body;
  89     this.subst = function (m, new_term) {
  90         return new Db_lam(this.body.subst(m + 1, new_term));
  91     };
  92     this.renumber = function (m, i) {
  93         return new Db_lam(this.body.renumber(m, i + 1));
  94     };
  95     // we assume that other will have body iff it's a Db_lam
  96     this.equal = function (other) {
  97         return other.body && this.body.equal(other.body);
  98     };
  99     this.contains = function (other) {
 100         if (other.body && this.body.equal(other.body)) {
 101             return true;
 102         } else {
 103             return this.body.contains(other);
 104         }
 105     };
 106 }
 107
 108
 109 // lambda terms
 110 // substitution and normal-order evaluator based on Haskell version by Oleg Kisleyov
 111 // http://okmij.org/ftp/Computation/lambda-calc.html#lambda-calculator-haskell
 112 //
 113 function Variable(name, tag) {
 114     this.name = name;
 115     this.tag = tag || 0;
 116     this.to_string = function () {
 117         // append count copies of str to accum
 118         function markup(accum, count) {
 119             if (count === 0) {
 120                 return accum;
 121             } else {
 122                 return markup(accum + "'", count - 1);
 123             }
 124         }
 125         return markup(this.name, this.tag);
 126     };
 127     this.equal = function (other) {
 128         return (this.tag === other.tag) && (this.name === other.name);
 129     };
 130     // position of this in seq
 131     this.position = function (seq) {
 132         for (var i = 0; i < seq.length; i += 1) {
 133             if (this.equal(seq[i])) {
 134                 return new Db_index(i + 1);
 135             }
 136         }
 137         return new Db_free(this);
 138     };
 139 }
 140
 141 // if v occurs free_in term, returns Some v' where v' is the highest-tagged
 142 // variable with the same name as v occurring (free or bound) in term
 143 //
 144 function free_in(v, term) {
 145     var res = term.has_free(v);
 146     return res[0] && res[1];
 147 }
 148
 149 function subst(v, new_term, expr) {
 150     if (new_term.variable && new_term.variable.equal(v)) {
 151         return expr;
 152     } else {
 153         return expr.subst(v, new_term);
 154     }
 155 }
 156
 157 function equal(expr1, expr2) {
 158     return expr1.debruijn([]).equal(expr2.debruijn([]));
 159 }
 160
 161 function contains(expr1, expr2) {
 162     return expr1.debruijn([]).contains(expr2.debruijn([]));
 163 }
 164
 165
 166 function Lambda_var(variable) {
 167     this.variable = variable;
 168     this.debruijn = function (seq) {
 169         return this.variable.position(seq);
 170     };
 171     this.to_string = function (as_atom) {
 172         return this.variable.to_string();
 173     };
 174     this.has_free = function (v) {
 175         if (v.name !== this.variable.name) {
 176             return [false, v];
 177         } else if (v.tag === this.variable.tag) {
 178             return [true, v];
 179         } else {
 180             return [false, this.variable];
 181         }
 182     };
 183     this.subst = function (v, new_term) {
 184         if (this.variable.equal(v)) {
 185             return new_term;
 186         } else {
 187             return this;
 188         }
 189     };
 190     this.check_eta = function () {
 191         return this;
 192     };
 193     this.eval_loop = function (stack, eta) {
 194         function unwind(left, stack) {
 195             if (stack.length === 0) {
 196                 return left;
 197             } else {
 198                 var x = stack[0];
 199                 var xs = stack.slice(1);
 200                 return unwind(new Lambda_app(left, x.eval_loop([], eta)), xs);
 201             }
 202         }
 203         return unwind(this, stack);
 204     };
 205     this.eval_cbv = function (aggressive) {
 206         return this;
 207     };
 208 }
 209
 210 function Lambda_app(left, right) {
 211     this.left = left;
 212     this.right = right;
 213     this.debruijn = function (seq) {
 214         return new Db_app(this.left.debruijn(seq), this.right.debruijn(seq));
 215     };
 216     this.to_string = function (as_atom) {
 217         var base;
 218         if (this.left.left) {
 219             base = this.left.to_string() + " " + this.right.to_string(true);
 220         } else {
 221             base = this.left.to_string(true) + " " + this.right.to_string(true);
 222         }
 223         if (as_atom) {
 224             return "(" + base + ")";
 225         } else {
 226             return base;
 227         }
 228     };
 229     this.has_free = function (v) {
 230         var left_res = this.left.has_free(v);
 231         var right_res = this.right.has_free(v);
 232         var left_bool = left_res[0];
 233         var right_bool = right_res[0];
 234         var left_tag = left_res[1].tag;
 235         var right_tag = right_res[1].tag;
 236         var res;
 237         if (left_tag > right_tag) {
 238             res = left_res[1];
 239         } else {
 240             res = right_res[1];
 241         }
 242         return [left_bool || right_bool, res];
 243     };
 244     this.subst = function (v, new_term) {
 245         return new Lambda_app(subst(v, new_term, this.left), subst(v, new_term, this.right));
 246     };
 247     this.check_eta = function () {
 248         return this;
 249     };
 250     this.eval_loop = function (stack, eta) {
 251         var new_stack = stack.slice(0);
 252         new_stack.unshift(this.right);
 253         return this.left.eval_loop(new_stack, eta);
 254     };
 255     this.eval_cbv = function (aggressive) {
 256         var left = this.left.eval_cbv(aggressive);
 257         var right = this.right.eval_cbv(aggressive);
 258         if (left.body) {
 259             return subst(left.bound, right, left.body).eval_cbv(aggressive);
 260         } else {
 261             return new Lambda_app(left, right);
 262         }
 263     };
 264 }
 265
 266
 267 //     (* if v occurs free_in term, returns Some v' where v' is the highest-tagged
 268 //      * variable with the same name as v occurring (free or bound) in term *)
 269
 270
 271 function Lambda_lam(variable, body) {
 272     this.bound = variable;
 273     this.body = body;
 274     this.debruijn = function (seq) {
 275         var new_seq = seq.slice(0);
 276         new_seq.unshift(this.bound);
 277         return new Db_lam(this.body.debruijn(new_seq));
 278     };
 279     this.to_string = function (as_atom) {
 280         var base = "\\" + this.to_string_funct();
 281         if (as_atom) {
 282             return "(" + base + ")";
 283         } else {
 284             return base;
 285         }
 286     };
 287     this.to_string_funct = function () {
 288         if (this.body.to_string_funct) {
 289             return this.bound.to_string() + " " + this.body.to_string_funct();
 290         } else {
 291             return this.bound.to_string() + ". " + this.body.to_string();
 292         }
 293     };
 294     this.has_free = function (v) {
 295         if (this.bound.equal(v)) {
 296             return [false, v];
 297         } else {
 298             return this.body.has_free(v);
 299         }
 300     };
 301     this.subst = function (v, new_term) {
 302         function bump_tag(v1, v2) {
 303             var max;
 304             if (v1.tag > v2.tag) {
 305                 max = v1.tag;
 306             } else {
 307                 max = v2.tag;
 308             }
 309             return new Variable(v1.name, max + 1);
 310         }
 311         function bump_tag2(v1, v2) {
 312             if (v1.name !== v2.name) {
 313                 return v1;
 314             } else {
 315                 return bump_tag(v1, v2);
 316             }
 317         }
 318         if (this.bound.equal(v)) {
 319             return this;
 320         } else {
 321             var res = free_in(this.bound, new_term);
 322             // if x is free in the inserted term new_term, a capture is possible
 323             if (res) {
 324                 // this.bound is free in new_term, need to alpha-convert
 325                 var uniq_x = bump_tag2(bump_tag(this.bound, res), v);
 326                 var res2 = free_in(uniq_x, this.body);
 327                 if (res2) {
 328                     uniq_x = bump_tag(uniq_x, res2);
 329                 }
 330                 var body2 = subst(this.bound, new Lambda_var(uniq_x), this.body);
 331                 return new Lambda_lam(uniq_x, subst(v, new_term, body2));
 332             } else {
 333                 // this.bound not free in new_term, can substitute new_term for v without any captures
 334                 return new Lambda_lam(this.bound, subst(v, new_term, this.body));
 335             }
 336         }
 337     };
 338     this.check_eta = function () {
 339         if (this.body.right && this.body.right.variable && this.bound.equal(this.body.right.variable) && !free_in(this.bound, this.body.left)) {
 340             return this.body.left;
 341         } else {
 342             return this;
 343         }
 344     };
 345     this.eval_loop = function (stack, eta) {
 346         if (stack.length === 0) {
 347             var term = new Lambda_lam(this.bound, this.body.eval_loop([], eta));
 348             if (eta) {
 349                 return term.check_eta();
 350             } else {
 351                 return term;
 352             }
 353         } else {
 354             var x = stack[0];
 355             var xs = stack.slice(1);
 356             return subst(this.bound, x, this.body).eval_loop(xs, eta);
 357         }
 358     };
 359     this.eval_cbv = function (aggressive) {
 360         if (aggressive) {
 361             return new Lambda_lam(this.bound, this.body.eval_cbv(aggressive));
 362         } else {
 363             return this;
 364         }
 365     };
 366     this.to_int = function (sofar) {
 367         if (this.body.body && this.body.body.variable && this.body.bound.equal(this.body.body.variable)) {
 368             return 0 + sofar;
 369         } else if (this.body.variable && this.bound.equal(this.body.variable)) {
 370             return 1 + sofar;
 371         } else if (this.body.body && this.body.body.left && this.body.body.left.variable && this.bound.equal(this.body.body.left.variable)) {
 372             var new_int = new Lambda_lam(this.bound, new Lambda_lam(this.body.bound, this.body.body.right));
 373             return new_int.to_int(1 + sofar);
 374         } else {
 375             return "not a church numeral";
 376         }
 377     };
 378 }
 379
 380
 381
 382 ///////////////////////////////////////////////////////////////////////////////////
 383
 384 // cbv is false: use call-by-name
 385 // cbv is 1: use call-by-value, don't descend inside lambda
 386 // cbv is 2: applicative order
 387 function reduce(expr, eta, cbv) {
 388     if (cbv) {
 389         return expr.eval_cbv(cbv > 1);
 390     } else {
 391         return expr.eval_loop([], eta);
 392     }
 393 }
 394
 395 function make_var(name) {
 396     return new Variable(name);
 397 }
 398 function make_app(aa, bb) {
 399     return new Lambda_app(aa, bb);
 400 }
 401 function make_lam(a, aa) {
 402     return new Lambda_lam(a, aa);
 403 }
 404
 405 try {
 406     if (console && console.debug) {
 407         function print() {
 408             console.debug.apply(this, arguments);
 409         }
 410     }
 411 } catch (e) {}
 412
 413 /*
 414 let true = K in
 415 let false = \x y. y in
 416 let and = \l r. l r false in
 417 let or = \l r. l true r in
 418 let pair = \u v f. f u v in
 419 let triple = \u v w f. f u v w in
 420 let succ = \n s z. s (n s z) in
 421 let pred = \n s z. n (\u v. v (u s)) (K z) I in
 422 let ifzero = \n. n (\u v. v (u succ)) (K 0) (\n withp whenz. withp n) in
 423 let add = \m n. n succ m in
 424 let mul = \m n. n (\z. add m z) 0 in
 425 let mul = \m n s. m (n s) in
 426 let sub = (\mzero msucc mtail. \m n. n mtail (m msucc mzero) true) (pair 0 I) (\d. d (\a b. pair (succ a) (K d))) (\d. d false d) in
 427 let min = \m n. sub m (sub m n) in
 428 let max = \m n. add n (sub m n) in
 429 let lt = (\mzero msucc mtail. \n m. n mtail (m msucc mzero) true (\x. true) false) (pair 0 I) (\d. d (\a b. pair (succ a) (K d))) (\d. d false d) in
 430 let leq = (\mzero msucc mtail. \m n. n mtail (m msucc mzero) true (\x. false) true) (pair 0 I) (\d. d (\a b. pair (succ a) (K d))) (\d. d false d) in
 431 let eq = (\mzero msucc mtail. \m n. n mtail (m msucc mzero) true (\x. false) true) (pair 0 (K (pair 1 I))) (\d. d (\a b. pair (succ a) (K d))) (\d. d false d) in
 432 let divmod = (\mzero msucc mtail. \n divisor.
 433                (\dhead. n (mtail dhead) (\sel. dhead (sel 0 0)))
 434               (divisor msucc mzero (\a b c. c x))
 435               (\d m a b c. pair d m) )
 436           (triple succ (K 0) I)
 437           (\d. triple I succ (K d))
 438           (\dhead d. d (\dz mz df mf drest sel. drest dhead (sel (df dz) (mf mz)))) in
 439 let div = \n d. divmod n d true in
 440 let mod = \n d. divmod n d false in
 441 let Y = \f. (\y. f(y y)) (\y. f(y y)) in
 442 let Z = (\u f. f(u u f)) (\u f. f(u u f)) in
 443 let fact = \y. y (\f n. ifzero n (\p. mul n (f p)) 1) in
 444 fact Z 3
 445 */
 446
 447
 448
 449 // // Basic data structure, essentially a LISP/Scheme-like cons
 450 // // pre-terminal nodes are expected to be of the form new cons(null, "string")
 451 // function cons(car, cdr) {
 452 //   this.car = car;
 453 //   this.cdr = cdr;
 454 // }
 455
 456 // // takes a stack of symbols, returns a pair: a tree and the remaining symbols
 457 // function parse(split) {
 458 //   if (split == null) return (new cons (null, null));
 459 //   if (split.length == 0) return (new cons (null, null));
 460 //   var token = split.shift();
 461 //   if (token == ")") return (new cons (null, split));
 462 //   var next = parse(split);
 463 //   if (token == "(") {
 464 //     var nextnext = parse(next.cdr);
 465 //     return (new cons ((new cons (next.car, nextnext.car)),
 466 //                       nextnext.cdr));
 467 //   }
 468 //   return (new cons ((new cons ((new cons (null, token)),
 469 //                                next.car)),
 470 //                     next.cdr))
 471 // }
 472
 473 // // substitute arg in for v in tree
 474 // function sub(tree, v, arg) {
 475 //   if (tree == null) return (null);
 476 //   if (tree.car == null) if (tree.cdr == v) return (arg);
 477 //   if (tree.car == null) return (tree);
 478
 479 //   // perform alpha reduction to prevent variable collision
 480 //   if (isBindingForm(tree))
 481 //     return (new cons (tree.car,
 482 //                       sub(sub(tree.cdr,         // inner sub = alpha reduc.
 483 //                               tree.cdr.car.cdr,
 484 //                               fresh(tree.cdr.car.cdr)),
 485 //                           v,
 486 //                           arg)));
 487
 488 //   return (new cons ((sub (tree.car, v, arg)),
 489 //                     (sub (tree.cdr, v, arg))))
 490 // }
 491
 492 // // Guaranteed unique for each call as long as string is not empty.
 493 // var i = 0;
 494 // function fresh(string) {
 495 //   i = i+1;
 496 //   if (typeof(string) != "string") return (string);
 497 //   return (new cons (null,
 498 //                     string.substring(0,1) + (i).toString()));
 499 // }
 500
 501 // // Keep reducing until there is no more change
 502 // function fixedPoint (tree) {
 503 //   var t2 = reduce(tree);
 504 //   if (treeToString(tree) == treeToString(t2)) return (tree);
 505 //   return (fixedPoint (t2));
 506 // }
 507
 508 // // Reduce all the arguments, then try to do beta conversion on the whole
 509 // function reduce(tree) {
 510 //   if (tree == null) return (tree);
 511 //   if (typeof(tree) == "string") return (tree);
 512 //   return (convert (new cons (reduce (tree.car), mapReduce (tree.cdr))));
 513 // }
 514
 515 // // Reduce all the arguments in a list
 516 // function mapReduce(tree) {
 517 //   if (tree == null) return (tree);
 518 //   if (tree.car == null) return (tree);
 519 //   return (new cons (reduce (tree.car), mapReduce(tree.cdr )));
 520 // }
 521
 522 // // If the list is of the form ((lambda var body) arg), do beta reduc.
 523 // function convert(tree) {
 524 //     if (isLet(tree)) {
 525 //       return (sub(tree.cdr.car, tree.car.cdr.car.cdr, tree.car.cdr.cdr.car));}
 526 //     else
 527 //       if (isConvertable(tree)) {
 528 //         return (sub(tree.car.cdr.cdr.car, tree.car.cdr.car.cdr, tree.cdr.car));}
 529 //       else return(tree);
 530 // }
 531
 532 // // Is of form ((let var arg) body)?
 533 // function isLet(tree) {
 534 //   if (tree == null) return (false);
 535 //   if (!(isBindingForm(tree.car))) return (false);
 536 //   if (tree.car.car.cdr != "let") return (false);
 537 //   if (tree.cdr == null) return (false);
 538 //   if (tree.cdr.car == null) return (false);
 539 //   return(true);
 540 // }
 541
 542 // // Is of form ((lambda var body) arg)?
 543 // function isConvertable(tree) {
 544 //   if (tree == null) return (false);
 545 //   if (!(isBindingForm(tree.car))) return (false);
 546 //   if (tree.car.car.cdr != "lambda") return (false);
 547 //   if (tree.cdr == null) return (false);
 548 //   if (tree.cdr.car == null) return (false);
 549 //   return(true);
 550 // }
 551
 552 // // Is of form (lambda var body)?
 553 // function isBindingForm(tree) {
 554 //   if (tree == null) return (false);
 555 //   if (tree.car == null) return (false);
 556 //   if (tree.car.car != null) return (false);
 557 //   if ((tree.car.cdr != "lambda")
 558 //       && (tree.car.cdr != "let")
 559 //       && (tree.car.cdr != "exists")
 560 //       && (tree.car.cdr != "forall")
 561 //       && (tree.car.cdr != "\u03BB")
 562 //       && (tree.car.cdr != "\u2200")
 563 //       && (tree.car.cdr != "\u2203")
 564 //      )
 565 //     return (false);
 566 //   if (tree.car.cdr == null) return (false);
 567 //   if (tree.cdr.car == null) return (false);
 568 //   if (tree.cdr.car.car != null) return (false);
 569 //   if (tree.cdr.cdr == null) return (false);
 570 //   return (true);
 571 // }
 572
 573 // function treeToString(tree) {
 574 //   if (tree == null) return ("")
 575 //   if (tree.car == null) return (tree.cdr)
 576 //   if ((tree.car).car == null)
 577 //     return (treeToString(tree.car) + " " + treeToString(tree.cdr))
 578 //   return ("(" + treeToString(tree.car) + ")" + treeToString(tree.cdr))
 579 // }
 580
 581 // // use this instead of treeToString if you want to see the full structure
 582 // function treeToStringRaw(tree) {
 583 //   if (tree == null) return ("@")
 584 //   if (typeof(tree) == "string") return (tree);
 585 //   return ("(" + treeToStringRaw(tree.car) + "." +
 586 //                 treeToStringRaw(tree.cdr) + ")")
 587 // }
 588
 589 // // Make sure each paren will count as a separate token
 590 // function stringToTree(input) {
 591 //   input = input.replace(/let/g, " ( ( let ");
 592 //   input = input.replace(/=/g, " ");
 593 //   input = input.replace(/in/g, " ) ");
 594 //   input = input.replace(/\(/g, " ( ");
 595 //   input = input.replace(/\)/g, " ) ");
 596 //   input = input.replace(/;.*\n/g," ");
 597 //   input = input.replace(/\^/g, " ^ ");
 598 //   input = input.replace(/[\\]/g, " lambda ");
 599 //   input = input.replace(/\u03BB/g, " lambda ");
 600 //   return ((parse(input.split(/[ \f\n\r\t\v]+/))).car)
 601 // }
 602
 603 // // Adjust spaces to print pretty
 604 // function formatTree(tree) {
 605 //   output = treeToStringRaw (tree);
 606 //   output = output.replace(/^[ \f\n\r\t\v]+/, "");
 607 //   output = output.replace(/[ \f\n\r\t\v]+$/, "");
 608 //   output = output.replace(/[ \f\n\r\t\v]+\)/g, ")");
 609 //   output = output.replace(/\)([^)(])/g, ") $1");
 610 //   output = output.replace(/lambda/g, "\\");
 611 // //  output = output.replace(/lambda/g, "\u03BB");
 612 // //  output = output.replace(/exists/g, "\u2203");
 613 // //  output = output.replace(/forall/g, "\u2200");
 614 //   return (output)
 615 // }
 616
 617 // function mytry(form) {
 618 //   i = 0;
 619 //   form.result.value = formatTree((stringToTree(form.input.value)));
 620 //   // form.result.value = formatTree(fixedPoint(stringToTree(form.input.value)));
 621 // }