add V combinator to lambda_evaluator
authorJim <jim.pryor@nyu.edu>
Mon, 23 Mar 2015 17:46:21 +0000 (13:46 -0400)
committerJim <jim.pryor@nyu.edu>
Mon, 23 Mar 2015 17:46:21 +0000 (13:46 -0400)
code/lambda_evaluator.mdwn
code/parse.js

index 2231951..220f613 100644 (file)
@@ -19,7 +19,7 @@ Blank lines are fine.
 
 *Abbreviations*: In an earlier version, you couldn't use abbreviations. `\x y. y x x` had to be written `(\x (\y ((y x) x)))`. We've upgraded the parser though, so now it should be able to understand any lambda term that you can.
 
 
 *Abbreviations*: In an earlier version, you couldn't use abbreviations. `\x y. y x x` had to be written `(\x (\y ((y x) x)))`. We've upgraded the parser though, so now it should be able to understand any lambda term that you can.
 
-*Constants*: The combinators `S`, `K`, `I`, `C`, `B`, `W`, `T`, `M` (aka <code>&omega;</code>) and `L` are pre-defined to their standard values. Also, integers will automatically be converted to Church numerals. (`0` is `\s z. z`, `1` is `\s z. s z`, and so on.)
+*Constants*: The combinators `S`, `K`, `I`, `C`, `B`, `W`, `T`, `V`, `M` (aka <code>&omega;</code>) and `L` are pre-defined to their standard values. Also, integers will automatically be converted to Church numerals. (`0` is `\s z. z`, `1` is `\s z. s z`, and so on.)
 
 *Variables*: Variables must start with a letter and can continue with any sequence of letters, numbers, `_`, `-`, or `/`. They may optionally end with `?` or `!`. When the evaluator does alpha-conversion, it may change `x` into `x'` or `x''` and so on. But you should not attempt to use primed variable names yourself.
 
 
 *Variables*: Variables must start with a letter and can continue with any sequence of letters, numbers, `_`, `-`, or `/`. They may optionally end with `?` or `!`. When the evaluator does alpha-conversion, it may change `x` into `x'` or `x''` and so on. But you should not attempt to use primed variable names yourself.
 
index ddc6199..9712809 100644 (file)
@@ -212,12 +212,14 @@ var make_parse = function () {
                constant("B", make_lam3(u, v, x, make_app(uu, make_app(vv, xx))));
                constant("C", make_lam3(u, v, x, make_app3(uu, xx, vv)));
 
                constant("B", make_lam3(u, v, x, make_app(uu, make_app(vv, xx))));
                constant("C", make_lam3(u, v, x, make_app3(uu, xx, vv)));
 
-               // trush \uv.vu = CI
+               // trush \uv.vu = CI = box
                constant("T", make_lam2(u, v, make_app(vv, uu)));
                constant("T", make_lam2(u, v, make_app(vv, uu)));
-               // mockingbird \u.uu = SII
-               constant("M", make_lam(u, make_app(uu, uu)));
+               // vireo \uvw.wuv = pair
+               constant("V", make_lam3(u, v, x, make_app3(xx, uu, vv)));
                // warbler \uv.uvv = C(BM(BBT) = C(BS(C(BBI)I))I
                constant("W", make_lam2(u, v, make_app3(uu, vv, vv)));
                // warbler \uv.uvv = C(BM(BBT) = C(BS(C(BBI)I))I
                constant("W", make_lam2(u, v, make_app3(uu, vv, vv)));
+               // mockingbird \u.uu = SII = omega
+               constant("M", make_lam(u, make_app(uu, uu)));
                // lark \uv.u(vv) = CBM = BWB
                constant("L", make_lam2(u, v, make_app(uu, make_app(vv, vv))));
                // Y is SLL
                // lark \uv.u(vv) = CBM = BWB
                constant("L", make_lam2(u, v, make_app(uu, make_app(vv, vv))));
                // Y is SLL