typo in untyped_evaluator
[lambda.git] / 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                 // trampoline to, args
217                 return [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                 // trampoline to, args
269                 return [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_dotted();
297         if (as_atom) {
298             return "(" + base + ")";
299         } else {
300             return base;
301         }
302     };
303     this.to_dotted = function () {
304         if (this.body.to_dotted) {
305             return this.bound.to_string() + " " + this.body.to_dotted();
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         if (stack.length === 0) {
363                         // var term = new Lambda_lam(this.bound, this.body.eval_loop([], eta));
364                         var term = new Lambda_lam(this.bound, reduce(this.body, eta, false));
365                         if (eta) {
366                                 return [null, term.check_eta()];
367                         } else {
368                                 return [null, term];
369                         }
370         } else {
371             var x = stack[0];
372             var xs = stack.slice(1);
373             // return subst(this.bound, x, this.body).eval_loop(xs, eta);
374                         // trampoline to, args
375                         return [subst(this.bound, x, this.body), xs, eta];
376         }
377     };
378     this.eval_cbv = function (aggressive) {
379         if (aggressive) {
380             return new Lambda_lam(this.bound, this.body.eval_cbv(aggressive));
381         } else {
382             return this;
383         }
384     };
385     this.to_int = function (sofar) {
386 //         if (this.body.body && this.body.body.variable && this.body.bound.equal(this.body.body.variable)) {
387 //             return 0 + sofar;
388 //         } else if (this.body.variable && this.bound.equal(this.body.variable)) {
389 //             return 1 + sofar;
390 //         } else if (this.body.body && this.body.body.left && this.body.body.left.variable && this.bound.equal(this.body.body.left.variable)) {
391 //             var new_int = new Lambda_lam(this.bound, new Lambda_lam(this.body.bound, this.body.body.right));
392 //             return new_int.to_int(1 + sofar);
393 //         } else {
394 //             return "not a church numeral";
395 //         }
396                 var res = 0, s = this.bound, z, cursor;
397                 if (this.body.variable && s.equal(this.body.variable)) {
398                         return 1;
399                 } else if (this.body.bound) {
400                         z = this.body.bound;
401                         cursor = this.body.body;
402                         while (cursor.left && cursor.left.variable && s.equal(cursor.left.variable)) {
403                                 res += 1;
404                                 cursor = cursor.right;
405                         }
406                         if (cursor.variable && z.equal(cursor.variable)) {
407                                 return res;
408                         }
409                 }
410                 return "not a church numeral";
411     };
412 }
413
414
415
416 ///////////////////////////////////////////////////////////////////////////////////
417
418 // cbv is false: use call-by-name
419 // cbv is 1: use call-by-value, don't descend inside lambda
420 // cbv is 2: applicative order
421 function reduce(expr, eta, cbv) {
422     if (cbv) {
423         return expr.eval_cbv(cbv > 1);
424     } else {
425         // return expr.eval_loop([], eta);
426                 // using trampoline to reduce call stack overflows
427                 var to_eval = expr, res = [[], eta];
428                 while (to_eval !== null) {
429                         res = to_eval.eval_loop.apply(to_eval, res);
430                         to_eval = res.shift();
431                 }
432                 return res[0];
433     }
434 }
435
436 function make_var(name) {
437     return new Variable(name);
438 }
439 function make_app(aa, bb) {
440     return new Lambda_app(aa, bb);
441 }
442 function make_lam(a, aa) {
443     return new Lambda_lam(a, aa);
444 }
445
446 try {
447     if (console && console.debug) {
448         function print() {
449             console.debug.apply(this, arguments);
450         }
451     }
452 } catch (e) {}
453
454
455
456
457 /* Chris's original
458
459 // Basic data structure, essentially a LISP/Scheme-like cons
460 // pre-terminal nodes are expected to be of the form new cons(null, "string")
461 function cons(car, cdr) {
462   this.car = car;
463   this.cdr = cdr;
464 }
465
466 // takes a stack of symbols, returns a pair: a tree and the remaining symbols
467 function parse(split) {
468   if (split == null) return (new cons (null, null));
469   if (split.length == 0) return (new cons (null, null));
470   var token = split.shift();
471   if (token == ")") return (new cons (null, split));
472   var next = parse(split);
473   if (token == "(") {
474         var nextnext = parse(next.cdr);
475         return (new cons ((new cons (next.car, nextnext.car)),
476                                           nextnext.cdr));
477   }
478   return (new cons ((new cons ((new cons (null, token)),
479                                                            next.car)),
480                                         next.cdr))
481 }
482
483 // substitute arg in for v in tree
484 function sub(tree, v, arg) {
485   if (tree == null) return (null);
486   if (tree.car == null) if (tree.cdr == v) return (arg);
487   if (tree.car == null) return (tree);
488
489   // perform alpha reduction to prevent variable collision
490   if (isBindingForm(tree))
491         return (new cons (tree.car,
492                                           sub(sub(tree.cdr,         // inner sub = alpha reduc.
493                                                           tree.cdr.car.cdr,
494                                                           fresh(tree.cdr.car.cdr)),
495                                                   v,
496                                                   arg)));
497
498   return (new cons ((sub (tree.car, v, arg)),
499                                         (sub (tree.cdr, v, arg))))
500 }
501
502 // Guaranteed unique for each call as long as string is not empty.
503 var i = 0;
504 function fresh(string) {
505   i = i+1;
506   if (typeof(string) != "string") return (string);
507   return (new cons (null,
508                                         string.substring(0,1) + (i).toString()));
509 }
510
511 // Keep reducing until there is no more change
512 function fixedPoint (tree) {
513   var t2 = reduce(tree);
514   if (treeToString(tree) == treeToString(t2)) return (tree);
515   return (fixedPoint (t2));
516 }
517
518 // Reduce all the arguments, then try to do beta conversion on the whole
519 function reduce(tree) {
520   if (tree == null) return (tree);
521   if (typeof(tree) == "string") return (tree);
522   return (convert (new cons (reduce (tree.car), mapReduce (tree.cdr))));
523 }
524
525 // Reduce all the arguments in a list
526 function mapReduce(tree) {
527   if (tree == null) return (tree);
528   if (tree.car == null) return (tree);
529   return (new cons (reduce (tree.car), mapReduce(tree.cdr )));
530 }
531
532 // If the list is of the form ((lambda var body) arg), do beta reduc.
533 function convert(tree) {
534         if (isLet(tree)) {
535           return (sub(tree.cdr.car, tree.car.cdr.car.cdr, tree.car.cdr.cdr.car));}
536         else
537           if (isConvertable(tree)) {
538                 return (sub(tree.car.cdr.cdr.car, tree.car.cdr.car.cdr, tree.cdr.car));}
539           else return(tree);
540 }
541
542 // Is of form ((let var arg) body)?
543 function isLet(tree) {
544   if (tree == null) return (false);
545   if (!(isBindingForm(tree.car))) return (false);
546   if (tree.car.car.cdr != "let") 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) arg)?
553 function isConvertable(tree) {
554   if (tree == null) return (false);
555   if (!(isBindingForm(tree.car))) return (false);
556   if (tree.car.car.cdr != "lambda") return (false);
557   if (tree.cdr == null) return (false);
558   if (tree.cdr.car == null) return (false);
559   return(true);
560 }
561
562 // Is of form (lambda var body)?
563 function isBindingForm(tree) {
564   if (tree == null) return (false);
565   if (tree.car == null) return (false);
566   if (tree.car.car != null) return (false);
567   if ((tree.car.cdr != "lambda")
568           && (tree.car.cdr != "let")
569           && (tree.car.cdr != "exists")
570           && (tree.car.cdr != "forall")
571           && (tree.car.cdr != "\u03BB")
572           && (tree.car.cdr != "\u2200")
573           && (tree.car.cdr != "\u2203")
574          )
575         return (false);
576   if (tree.car.cdr == null) return (false);
577   if (tree.cdr.car == null) return (false);
578   if (tree.cdr.car.car != null) return (false);
579   if (tree.cdr.cdr == null) return (false);
580   return (true);
581 }
582
583 function treeToString(tree) {
584   if (tree == null) return ("")
585   if (tree.car == null) return (tree.cdr)
586   if ((tree.car).car == null)
587         return (treeToString(tree.car) + " " + treeToString(tree.cdr))
588   return ("(" + treeToString(tree.car) + ")" + treeToString(tree.cdr))
589 }
590
591 // use this instead of treeToString if you want to see the full structure
592 function treeToStringRaw(tree) {
593   if (tree == null) return ("@")
594   if (typeof(tree) == "string") return (tree);
595   return ("(" + treeToStringRaw(tree.car) + "." +
596                                 treeToStringRaw(tree.cdr) + ")")
597 }
598
599 // Make sure each paren will count as a separate token
600 function stringToTree(input) {
601   input = input.replace(/let/g, " ( ( let ");
602   input = input.replace(/=/g, " ");
603   input = input.replace(/in/g, " ) ");
604   input = input.replace(/\(/g, " ( ");
605   input = input.replace(/\)/g, " ) ");
606   input = input.replace(/;.*\n/g," ");
607   input = input.replace(/\^/g, " ^ ");
608   input = input.replace(/[\\]/g, " lambda ");
609   input = input.replace(/\u03BB/g, " lambda ");
610   return ((parse(input.split(/[ \f\n\r\t\v]+/))).car)
611 }
612
613 // Adjust spaces to print pretty
614 function formatTree(tree) {
615   output = treeToStringRaw (tree);
616   output = output.replace(/^[ \f\n\r\t\v]+/, "");
617   output = output.replace(/[ \f\n\r\t\v]+$/, "");
618   output = output.replace(/[ \f\n\r\t\v]+\)/g, ")");
619   output = output.replace(/\)([^)(])/g, ") $1");
620   output = output.replace(/lambda/g, "\\");
621 //  output = output.replace(/lambda/g, "\u03BB");
622 //  output = output.replace(/exists/g, "\u2203");
623 //  output = output.replace(/forall/g, "\u2200");
624   return (output)
625 }
626
627 function mytry(form) {
628   i = 0;
629   form.result.value = formatTree((stringToTree(form.input.value)));
630   // form.result.value = formatTree(fixedPoint(stringToTree(form.input.value)));
631 }
632
633 */
634