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                 var s = this.name;
 127                 for (var count = 0; count < this.tag; count += 1) {
 128                         s += "'";
 129                 }
 130                 return s;
 131     };
 132     this.equal = function (other) {
 133         return (this.tag === other.tag) && (this.name === other.name);
 134     };
 135     // position of this in seq
 136     this.position = function (seq) {
 137         for (var i = 0; i < seq.length; i += 1) {
 138             if (this.equal(seq[i])) {
 139                 return new Db_index(i + 1);
 140             }
 141         }
 142         return new Db_free(this);
 143     };
 144 }
 145
 146 // if v occurs free_in term, returns Some v' where v' is the highest-tagged
 147 // variable with the same name as v occurring (free or bound) in term
 148 //
 149 function free_in(v, term) {
 150     var res = term.has_free(v);
 151     return res[0] && res[1];
 152 }
 153
 154 function subst(v, new_term, expr) {
 155     if (new_term.variable && new_term.variable.equal(v)) {
 156         return expr;
 157     } else {
 158         return expr.subst(v, new_term);
 159     }
 160 }
 161
 162 function equal(expr1, expr2) {
 163     return expr1.debruijn([]).equal(expr2.debruijn([]));
 164 }
 165
 166 function contains(expr1, expr2) {
 167     return expr1.debruijn([]).contains(expr2.debruijn([]));
 168 }
 169
 170
 171 function Lambda_var(variable) {
 172     this.variable = variable;
 173     this.debruijn = function (seq) {
 174         return this.variable.position(seq);
 175     };
 176     this.to_string = function (as_atom) {
 177         return this.variable.to_string();
 178     };
 179     this.has_free = function (v) {
 180         if (v.name !== this.variable.name) {
 181             return [false, v];
 182         } else if (v.tag === this.variable.tag) {
 183             return [true, v];
 184         } else {
 185             return [false, this.variable];
 186         }
 187     };
 188     this.subst = function (v, new_term) {
 189         if (this.variable.equal(v)) {
 190             return new_term;
 191         } else {
 192             return this;
 193         }
 194     };
 195     this.check_eta = function () {
 196         return this;
 197     };
 198     this.eval_loop = function (stack, eta) {
 199         function unwind(left, stack) {
 200 //             if (stack.length === 0) {
 201 //                 return left;
 202 //             } else {
 203 //                 var x = stack[0];
 204 //                 var xs = stack.slice(1);
 205 //                 return unwind(new Lambda_app(left, x.eval_loop([], eta)), xs);
 206 //             }
 207                         var res = left, x;
 208                         while (stack.length) {
 209                                 x = stack.shift();
 210                                 // res = new Lambda_app(res, x.eval_loop([], eta));
 211                                 res = new Lambda_app(res, reduce(x, eta, false));
 212                         }
 213                         return res;
 214         }
 215         // return unwind(this, stack);
 216                 // post-processor, trampoline to, args
 217                 return [null, null, unwind(this, stack)];
 218     };
 219     this.eval_cbv = function (aggressive) {
 220         return this;
 221     };
 222 }
 223
 224 function Lambda_app(left, right) {
 225     this.left = left;
 226     this.right = right;
 227     this.debruijn = function (seq) {
 228         return new Db_app(this.left.debruijn(seq), this.right.debruijn(seq));
 229     };
 230     this.to_string = function (as_atom) {
 231         var base;
 232         if (this.left.left) {
 233             base = this.left.to_string() + " " + this.right.to_string(true);
 234         } else {
 235             base = this.left.to_string(true) + " " + this.right.to_string(true);
 236         }
 237         if (as_atom) {
 238             return "(" + base + ")";
 239         } else {
 240             return base;
 241         }
 242     };
 243     this.has_free = function (v) {
 244         var left_res = this.left.has_free(v);
 245         var right_res = this.right.has_free(v);
 246         var left_bool = left_res[0];
 247         var right_bool = right_res[0];
 248         var left_tag = left_res[1].tag;
 249         var right_tag = right_res[1].tag;
 250         var res;
 251         if (left_tag > right_tag) {
 252             res = left_res[1];
 253         } else {
 254             res = right_res[1];
 255         }
 256         return [left_bool || right_bool, res];
 257     };
 258     this.subst = function (v, new_term) {
 259         return new Lambda_app(subst(v, new_term, this.left), subst(v, new_term, this.right));
 260     };
 261     this.check_eta = function () {
 262         return this;
 263     };
 264     this.eval_loop = function (stack, eta) {
 265         var new_stack = stack.slice(0);
 266         new_stack.unshift(this.right);
 267         // return this.left.eval_loop(new_stack, eta);
 268                 // post-processor, trampoline to, args
 269                 return [null, this.left, new_stack, eta];
 270     };
 271     this.eval_cbv = function (aggressive) {
 272         var left = this.left.eval_cbv(aggressive);
 273         var right = this.right.eval_cbv(aggressive);
 274         if (left.body) {
 275             return subst(left.bound, right, left.body).eval_cbv(aggressive);
 276         } else {
 277             return new Lambda_app(left, right);
 278         }
 279     };
 280 }
 281
 282
 283 //     (* if v occurs free_in term, returns Some v' where v' is the highest-tagged
 284 //      * variable with the same name as v occurring (free or bound) in term *)
 285
 286
 287 function Lambda_lam(variable, body) {
 288     this.bound = variable;
 289     this.body = body;
 290     this.debruijn = function (seq) {
 291         var new_seq = seq.slice(0);
 292         new_seq.unshift(this.bound);
 293         return new Db_lam(this.body.debruijn(new_seq));
 294     };
 295     this.to_string = function (as_atom) {
 296         var base = "\\" + this.to_string_funct();
 297         if (as_atom) {
 298             return "(" + base + ")";
 299         } else {
 300             return base;
 301         }
 302     };
 303     this.to_string_funct = function () {
 304         if (this.body.to_string_funct) {
 305             return this.bound.to_string() + " " + this.body.to_string_funct();
 306         } else {
 307             return this.bound.to_string() + ". " + this.body.to_string();
 308         }
 309     };
 310     this.has_free = function (v) {
 311         if (this.bound.equal(v)) {
 312             return [false, v];
 313         } else {
 314             return this.body.has_free(v);
 315         }
 316     };
 317     this.subst = function (v, new_term) {
 318         function bump_tag(v1, v2) {
 319             var max;
 320             if (v1.tag > v2.tag) {
 321                 max = v1.tag;
 322             } else {
 323                 max = v2.tag;
 324             }
 325             return new Variable(v1.name, max + 1);
 326         }
 327         function bump_tag2(v1, v2) {
 328             if (v1.name !== v2.name) {
 329                 return v1;
 330             } else {
 331                 return bump_tag(v1, v2);
 332             }
 333         }
 334         if (this.bound.equal(v)) {
 335             return this;
 336         } else {
 337             var res = free_in(this.bound, new_term);
 338             // if x is free in the inserted term new_term, a capture is possible
 339             if (res) {
 340                 // this.bound is free in new_term, need to alpha-convert
 341                 var uniq_x = bump_tag2(bump_tag(this.bound, res), v);
 342                 var res2 = free_in(uniq_x, this.body);
 343                 if (res2) {
 344                     uniq_x = bump_tag(uniq_x, res2);
 345                 }
 346                 var body2 = subst(this.bound, new Lambda_var(uniq_x), this.body);
 347                 return new Lambda_lam(uniq_x, subst(v, new_term, body2));
 348             } else {
 349                 // this.bound not free in new_term, can substitute new_term for v without any captures
 350                 return new Lambda_lam(this.bound, subst(v, new_term, this.body));
 351             }
 352         }
 353     };
 354     this.check_eta = function () {
 355         if (this.body.right && this.body.right.variable && this.bound.equal(this.body.right.variable) && !free_in(this.bound, this.body.left)) {
 356             return this.body.left;
 357         } else {
 358             return this;
 359         }
 360     };
 361     this.eval_loop = function (stack, eta) {
 362                 function post(evaluated_body) {
 363                         var term = new Lambda_lam(this.bound, evaluated_body);
 364                         if (eta) {
 365                                 return term.check_eta();
 366                         } else {
 367                                 return term;
 368                         }
 369                 }
 370         if (stack.length === 0) {
 371 //             var term = new Lambda_lam(this.bound, this.body.eval_loop([], eta));
 372 //             if (eta) {
 373 //                 return term.check_eta();
 374 //             } else {
 375 //                 return term;
 376 //             }
 377                         // post-processor, trampoline to, args
 378                         return [post, this.body, [], eta];
 379         } else {
 380             var x = stack[0];
 381             var xs = stack.slice(1);
 382             // return subst(this.bound, x, this.body).eval_loop(xs, eta);
 383                         // post-processor, trampoline to, args
 384                         return [null, subst(this.bound, x, this.body), xs, eta];
 385         }
 386     };
 387     this.eval_cbv = function (aggressive) {
 388         if (aggressive) {
 389             return new Lambda_lam(this.bound, this.body.eval_cbv(aggressive));
 390         } else {
 391             return this;
 392         }
 393     };
 394     this.to_int = function (sofar) {
 395 //         if (this.body.body && this.body.body.variable && this.body.bound.equal(this.body.body.variable)) {
 396 //             return 0 + sofar;
 397 //         } else if (this.body.variable && this.bound.equal(this.body.variable)) {
 398 //             return 1 + sofar;
 399 //         } else if (this.body.body && this.body.body.left && this.body.body.left.variable && this.bound.equal(this.body.body.left.variable)) {
 400 //             var new_int = new Lambda_lam(this.bound, new Lambda_lam(this.body.bound, this.body.body.right));
 401 //             return new_int.to_int(1 + sofar);
 402 //         } else {
 403 //             return "not a church numeral";
 404 //         }
 405                 var res = 0, s = this.bound, z, cursor;
 406                 if (this.body.variable && s.equal(this.body.variable)) {
 407                         return 1;
 408                 } else if (this.body.bound) {
 409                         z = this.body.bound;
 410                         cursor = this.body.body;
 411                         while (cursor.left && cursor.left.variable && s.equal(cursor.left.variable)) {
 412                                 res += 1;
 413                                 cursor = cursor.right;
 414                         }
 415                         if (cursor.variable && z.equal(cursor.variable)) {
 416                                 return res;
 417                         }
 418                 }
 419                 return "not a church numeral";
 420     };
 421 }
 422
 423
 424
 425 ///////////////////////////////////////////////////////////////////////////////////
 426
 427 // cbv is false: use call-by-name
 428 // cbv is 1: use call-by-value, don't descend inside lambda
 429 // cbv is 2: applicative order
 430 function reduce(expr, eta, cbv) {
 431     if (cbv) {
 432         return expr.eval_cbv(cbv > 1);
 433     } else {
 434         // return expr.eval_loop([], eta);
 435                 var post = null, to_eval = expr, res = [[], eta];
 436                 while (to_eval !== null) {
 437                         res = to_eval.eval_loop.apply(to_eval, res);
 438                         post = res.shift();
 439                         to_eval = res.shift();
 440                         if (post) {
 441                                 res = post(res);
 442                         }
 443                 }
 444                 return res[0];
 445     }
 446 }
 447
 448 function make_var(name) {
 449     return new Variable(name);
 450 }
 451 function make_app(aa, bb) {
 452     return new Lambda_app(aa, bb);
 453 }
 454 function make_lam(a, aa) {
 455     return new Lambda_lam(a, aa);
 456 }
 457
 458 try {
 459     if (console && console.debug) {
 460         function print() {
 461             console.debug.apply(this, arguments);
 462         }
 463     }
 464 } catch (e) {}
 465
 466 /*
 467 let true = K in
 468 let false = \x y. y in
 469 let and = \l r. l r false in
 470 let or = \l r. l true r in
 471 let pair = \u v f. f u v in
 472 let triple = \u v w f. f u v w in
 473 let succ = \n s z. s (n s z) in
 474 let pred = \n s z. n (\u v. v (u s)) (K z) I in
 475 let ifzero = \n. n (\u v. v (u succ)) (K 0) (\n withp whenz. withp n) in
 476 let add = \m n. n succ m in
 477 let mul = \m n. n (\z. add m z) 0 in
 478 let mul = \m n s. m (n s) in
 479 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
 480 let min = \m n. sub m (sub m n) in
 481 let max = \m n. add n (sub m n) in
 482 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
 483 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
 484 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
 485 let divmod = (\mzero msucc mtail. \n divisor.
 486                (\dhead. n (mtail dhead) (\sel. dhead (sel 0 0)))
 487               (divisor msucc mzero (\a b c. c x))
 488               (\d m a b c. pair d m) )
 489           (triple succ (K 0) I)
 490           (\d. triple I succ (K d))
 491           (\dhead d. d (\dz mz df mf drest sel. drest dhead (sel (df dz) (mf mz)))) in
 492 let div = \n d. divmod n d true in
 493 let mod = \n d. divmod n d false in
 494 let Y = \f. (\y. f(y y)) (\y. f(y y)) in
 495 let Z = (\u f. f(u u f)) (\u f. f(u u f)) in
 496 let fact = \y. y (\f n. ifzero n (\p. mul n (f p)) 1) in
 497 fact Z 3
 498 */
 499
 500
 501
 502 // // Basic data structure, essentially a LISP/Scheme-like cons
 503 // // pre-terminal nodes are expected to be of the form new cons(null, "string")
 504 // function cons(car, cdr) {
 505 //   this.car = car;
 506 //   this.cdr = cdr;
 507 // }
 508
 509 // // takes a stack of symbols, returns a pair: a tree and the remaining symbols
 510 // function parse(split) {
 511 //   if (split == null) return (new cons (null, null));
 512 //   if (split.length == 0) return (new cons (null, null));
 513 //   var token = split.shift();
 514 //   if (token == ")") return (new cons (null, split));
 515 //   var next = parse(split);
 516 //   if (token == "(") {
 517 //     var nextnext = parse(next.cdr);
 518 //     return (new cons ((new cons (next.car, nextnext.car)),
 519 //                       nextnext.cdr));
 520 //   }
 521 //   return (new cons ((new cons ((new cons (null, token)),
 522 //                                next.car)),
 523 //                     next.cdr))
 524 // }
 525
 526 // // substitute arg in for v in tree
 527 // function sub(tree, v, arg) {
 528 //   if (tree == null) return (null);
 529 //   if (tree.car == null) if (tree.cdr == v) return (arg);
 530 //   if (tree.car == null) return (tree);
 531
 532 //   // perform alpha reduction to prevent variable collision
 533 //   if (isBindingForm(tree))
 534 //     return (new cons (tree.car,
 535 //                       sub(sub(tree.cdr,         // inner sub = alpha reduc.
 536 //                               tree.cdr.car.cdr,
 537 //                               fresh(tree.cdr.car.cdr)),
 538 //                           v,
 539 //                           arg)));
 540
 541 //   return (new cons ((sub (tree.car, v, arg)),
 542 //                     (sub (tree.cdr, v, arg))))
 543 // }
 544
 545 // // Guaranteed unique for each call as long as string is not empty.
 546 // var i = 0;
 547 // function fresh(string) {
 548 //   i = i+1;
 549 //   if (typeof(string) != "string") return (string);
 550 //   return (new cons (null,
 551 //                     string.substring(0,1) + (i).toString()));
 552 // }
 553
 554 // // Keep reducing until there is no more change
 555 // function fixedPoint (tree) {
 556 //   var t2 = reduce(tree);
 557 //   if (treeToString(tree) == treeToString(t2)) return (tree);
 558 //   return (fixedPoint (t2));
 559 // }
 560
 561 // // Reduce all the arguments, then try to do beta conversion on the whole
 562 // function reduce(tree) {
 563 //   if (tree == null) return (tree);
 564 //   if (typeof(tree) == "string") return (tree);
 565 //   return (convert (new cons (reduce (tree.car), mapReduce (tree.cdr))));
 566 // }
 567
 568 // // Reduce all the arguments in a list
 569 // function mapReduce(tree) {
 570 //   if (tree == null) return (tree);
 571 //   if (tree.car == null) return (tree);
 572 //   return (new cons (reduce (tree.car), mapReduce(tree.cdr )));
 573 // }
 574
 575 // // If the list is of the form ((lambda var body) arg), do beta reduc.
 576 // function convert(tree) {
 577 //     if (isLet(tree)) {
 578 //       return (sub(tree.cdr.car, tree.car.cdr.car.cdr, tree.car.cdr.cdr.car));}
 579 //     else
 580 //       if (isConvertable(tree)) {
 581 //         return (sub(tree.car.cdr.cdr.car, tree.car.cdr.car.cdr, tree.cdr.car));}
 582 //       else return(tree);
 583 // }
 584
 585 // // Is of form ((let var arg) body)?
 586 // function isLet(tree) {
 587 //   if (tree == null) return (false);
 588 //   if (!(isBindingForm(tree.car))) return (false);
 589 //   if (tree.car.car.cdr != "let") return (false);
 590 //   if (tree.cdr == null) return (false);
 591 //   if (tree.cdr.car == null) return (false);
 592 //   return(true);
 593 // }
 594
 595 // // Is of form ((lambda var body) arg)?
 596 // function isConvertable(tree) {
 597 //   if (tree == null) return (false);
 598 //   if (!(isBindingForm(tree.car))) return (false);
 599 //   if (tree.car.car.cdr != "lambda") return (false);
 600 //   if (tree.cdr == null) return (false);
 601 //   if (tree.cdr.car == null) return (false);
 602 //   return(true);
 603 // }
 604
 605 // // Is of form (lambda var body)?
 606 // function isBindingForm(tree) {
 607 //   if (tree == null) return (false);
 608 //   if (tree.car == null) return (false);
 609 //   if (tree.car.car != null) return (false);
 610 //   if ((tree.car.cdr != "lambda")
 611 //       && (tree.car.cdr != "let")
 612 //       && (tree.car.cdr != "exists")
 613 //       && (tree.car.cdr != "forall")
 614 //       && (tree.car.cdr != "\u03BB")
 615 //       && (tree.car.cdr != "\u2200")
 616 //       && (tree.car.cdr != "\u2203")
 617 //      )
 618 //     return (false);
 619 //   if (tree.car.cdr == null) return (false);
 620 //   if (tree.cdr.car == null) return (false);
 621 //   if (tree.cdr.car.car != null) return (false);
 622 //   if (tree.cdr.cdr == null) return (false);
 623 //   return (true);
 624 // }
 625
 626 // function treeToString(tree) {
 627 //   if (tree == null) return ("")
 628 //   if (tree.car == null) return (tree.cdr)
 629 //   if ((tree.car).car == null)
 630 //     return (treeToString(tree.car) + " " + treeToString(tree.cdr))
 631 //   return ("(" + treeToString(tree.car) + ")" + treeToString(tree.cdr))
 632 // }
 633
 634 // // use this instead of treeToString if you want to see the full structure
 635 // function treeToStringRaw(tree) {
 636 //   if (tree == null) return ("@")
 637 //   if (typeof(tree) == "string") return (tree);
 638 //   return ("(" + treeToStringRaw(tree.car) + "." +
 639 //                 treeToStringRaw(tree.cdr) + ")")
 640 // }
 641
 642 // // Make sure each paren will count as a separate token
 643 // function stringToTree(input) {
 644 //   input = input.replace(/let/g, " ( ( let ");
 645 //   input = input.replace(/=/g, " ");
 646 //   input = input.replace(/in/g, " ) ");
 647 //   input = input.replace(/\(/g, " ( ");
 648 //   input = input.replace(/\)/g, " ) ");
 649 //   input = input.replace(/;.*\n/g," ");
 650 //   input = input.replace(/\^/g, " ^ ");
 651 //   input = input.replace(/[\\]/g, " lambda ");
 652 //   input = input.replace(/\u03BB/g, " lambda ");
 653 //   return ((parse(input.split(/[ \f\n\r\t\v]+/))).car)
 654 // }
 655
 656 // // Adjust spaces to print pretty
 657 // function formatTree(tree) {
 658 //   output = treeToStringRaw (tree);
 659 //   output = output.replace(/^[ \f\n\r\t\v]+/, "");
 660 //   output = output.replace(/[ \f\n\r\t\v]+$/, "");
 661 //   output = output.replace(/[ \f\n\r\t\v]+\)/g, ")");
 662 //   output = output.replace(/\)([^)(])/g, ") $1");
 663 //   output = output.replace(/lambda/g, "\\");
 664 // //  output = output.replace(/lambda/g, "\u03BB");
 665 // //  output = output.replace(/exists/g, "\u2203");
 666 // //  output = output.replace(/forall/g, "\u2200");
 667 //   return (output)
 668 // }
 669
 670 // function mytry(form) {
 671 //   i = 0;
 672 //   form.result.value = formatTree((stringToTree(form.input.value)));
 673 //   // form.result.value = formatTree(fixedPoint(stringToTree(form.input.value)));
 674 // }