code/lambda2.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
 415
 416
 417 // // Basic data structure, essentially a LISP/Scheme-like cons
 418 // // pre-terminal nodes are expected to be of the form new cons(null, "string")
 419 // function cons(car, cdr) {
 420 //   this.car = car;
 421 //   this.cdr = cdr;
 422 // }
 423
 424 // // takes a stack of symbols, returns a pair: a tree and the remaining symbols
 425 // function parse(split) {
 426 //   if (split == null) return (new cons (null, null));
 427 //   if (split.length == 0) return (new cons (null, null));
 428 //   var token = split.shift();
 429 //   if (token == ")") return (new cons (null, split));
 430 //   var next = parse(split);
 431 //   if (token == "(") {
 432 //     var nextnext = parse(next.cdr);
 433 //     return (new cons ((new cons (next.car, nextnext.car)),
 434 //                       nextnext.cdr));
 435 //   }
 436 //   return (new cons ((new cons ((new cons (null, token)),
 437 //                                next.car)),
 438 //                     next.cdr))
 439 // }
 440
 441 // // substitute arg in for v in tree
 442 // function sub(tree, v, arg) {
 443 //   if (tree == null) return (null);
 444 //   if (tree.car == null) if (tree.cdr == v) return (arg);
 445 //   if (tree.car == null) return (tree);
 446
 447 //   // perform alpha reduction to prevent variable collision
 448 //   if (isBindingForm(tree))
 449 //     return (new cons (tree.car,
 450 //                       sub(sub(tree.cdr,         // inner sub = alpha reduc.
 451 //                               tree.cdr.car.cdr,
 452 //                               fresh(tree.cdr.car.cdr)),
 453 //                           v,
 454 //                           arg)));
 455
 456 //   return (new cons ((sub (tree.car, v, arg)),
 457 //                     (sub (tree.cdr, v, arg))))
 458 // }
 459
 460 // // Guaranteed unique for each call as long as string is not empty.
 461 // var i = 0;
 462 // function fresh(string) {
 463 //   i = i+1;
 464 //   if (typeof(string) != "string") return (string);
 465 //   return (new cons (null,
 466 //                     string.substring(0,1) + (i).toString()));
 467 // }
 468
 469 // // Keep reducing until there is no more change
 470 // function fixedPoint (tree) {
 471 //   var t2 = reduce(tree);
 472 //   if (treeToString(tree) == treeToString(t2)) return (tree);
 473 //   return (fixedPoint (t2));
 474 // }
 475
 476 // // Reduce all the arguments, then try to do beta conversion on the whole
 477 // function reduce(tree) {
 478 //   if (tree == null) return (tree);
 479 //   if (typeof(tree) == "string") return (tree);
 480 //   return (convert (new cons (reduce (tree.car), mapReduce (tree.cdr))));
 481 // }
 482
 483 // // Reduce all the arguments in a list
 484 // function mapReduce(tree) {
 485 //   if (tree == null) return (tree);
 486 //   if (tree.car == null) return (tree);
 487 //   return (new cons (reduce (tree.car), mapReduce(tree.cdr )));
 488 // }
 489
 490 // // If the list is of the form ((lambda var body) arg), do beta reduc.
 491 // function convert(tree) {
 492 //     if (isLet(tree)) {
 493 //       return (sub(tree.cdr.car, tree.car.cdr.car.cdr, tree.car.cdr.cdr.car));}
 494 //     else
 495 //       if (isConvertable(tree)) {
 496 //         return (sub(tree.car.cdr.cdr.car, tree.car.cdr.car.cdr, tree.cdr.car));}
 497 //       else return(tree);
 498 // }
 499
 500 // // Is of form ((let var arg) body)?
 501 // function isLet(tree) {
 502 //   if (tree == null) return (false);
 503 //   if (!(isBindingForm(tree.car))) return (false);
 504 //   if (tree.car.car.cdr != "let") return (false);
 505 //   if (tree.cdr == null) return (false);
 506 //   if (tree.cdr.car == null) return (false);
 507 //   return(true);
 508 // }
 509
 510 // // Is of form ((lambda var body) arg)?
 511 // function isConvertable(tree) {
 512 //   if (tree == null) return (false);
 513 //   if (!(isBindingForm(tree.car))) return (false);
 514 //   if (tree.car.car.cdr != "lambda") return (false);
 515 //   if (tree.cdr == null) return (false);
 516 //   if (tree.cdr.car == null) return (false);
 517 //   return(true);
 518 // }
 519
 520 // // Is of form (lambda var body)?
 521 // function isBindingForm(tree) {
 522 //   if (tree == null) return (false);
 523 //   if (tree.car == null) return (false);
 524 //   if (tree.car.car != null) return (false);
 525 //   if ((tree.car.cdr != "lambda")
 526 //       && (tree.car.cdr != "let")
 527 //       && (tree.car.cdr != "exists")
 528 //       && (tree.car.cdr != "forall")
 529 //       && (tree.car.cdr != "\u03BB")
 530 //       && (tree.car.cdr != "\u2200")
 531 //       && (tree.car.cdr != "\u2203")
 532 //      )
 533 //     return (false);
 534 //   if (tree.car.cdr == null) return (false);
 535 //   if (tree.cdr.car == null) return (false);
 536 //   if (tree.cdr.car.car != null) return (false);
 537 //   if (tree.cdr.cdr == null) return (false);
 538 //   return (true);
 539 // }
 540
 541 // function treeToString(tree) {
 542 //   if (tree == null) return ("")
 543 //   if (tree.car == null) return (tree.cdr)
 544 //   if ((tree.car).car == null)
 545 //     return (treeToString(tree.car) + " " + treeToString(tree.cdr))
 546 //   return ("(" + treeToString(tree.car) + ")" + treeToString(tree.cdr))
 547 // }
 548
 549 // // use this instead of treeToString if you want to see the full structure
 550 // function treeToStringRaw(tree) {
 551 //   if (tree == null) return ("@")
 552 //   if (typeof(tree) == "string") return (tree);
 553 //   return ("(" + treeToStringRaw(tree.car) + "." +
 554 //                 treeToStringRaw(tree.cdr) + ")")
 555 // }
 556
 557 // // Make sure each paren will count as a separate token
 558 // function stringToTree(input) {
 559 //   input = input.replace(/let/g, " ( ( let ");
 560 //   input = input.replace(/=/g, " ");
 561 //   input = input.replace(/in/g, " ) ");
 562 //   input = input.replace(/\(/g, " ( ");
 563 //   input = input.replace(/\)/g, " ) ");
 564 //   input = input.replace(/;.*\n/g," ");
 565 //   input = input.replace(/\^/g, " ^ ");
 566 //   input = input.replace(/[\\]/g, " lambda ");
 567 //   input = input.replace(/\u03BB/g, " lambda ");
 568 //   return ((parse(input.split(/[ \f\n\r\t\v]+/))).car)
 569 // }
 570
 571 // // Adjust spaces to print pretty
 572 // function formatTree(tree) {
 573 //   output = treeToStringRaw (tree);
 574 //   output = output.replace(/^[ \f\n\r\t\v]+/, "");
 575 //   output = output.replace(/[ \f\n\r\t\v]+$/, "");
 576 //   output = output.replace(/[ \f\n\r\t\v]+\)/g, ")");
 577 //   output = output.replace(/\)([^)(])/g, ") $1");
 578 //   output = output.replace(/lambda/g, "\\");
 579 // //  output = output.replace(/lambda/g, "\u03BB");
 580 // //  output = output.replace(/exists/g, "\u2203");
 581 // //  output = output.replace(/forall/g, "\u2200");
 582 //   return (output)
 583 // }
 584
 585 // function mytry(form) {
 586 //   i = 0;
 587 //   form.result.value = formatTree((stringToTree(form.input.value)));
 588 //   // form.result.value = formatTree(fixedPoint(stringToTree(form.input.value)));
 589 // }