-Lambda Evaluator
-----------------
-
-There is now a [lambda evaluator](http://lambda.jimpryor.net/lambda-let.html) available.
-It will allow you to write lambda terms and evaluate (that is, normalize) them, and inspect the results.
+This lambda evaluator will allow you to write lambda terms and evaluate (that is, normalize) them, and inspect the results.
(This won't work in Racket, because Racket doesn't even try to represent the internal structure of a function in a human-readable way.)
*Lambda terms*: lambda terms are written with a backslash, thus: `((\x (\y x)) z)`.
*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*: `true` and `false` are pre-defined to their standard values. So too are the combinators `S`, `K`, `I`, `C`, `B`, `W`, and `T`. Finally, 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`, `M` (aka <code>ω</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.
<textarea id="INPUT" style="border: 2px solid black; color: black; font-family: monospace; height: 3in; overflow: auto; padding: 0.5em; width: 100%;">
)
</textarea>
<input id="PARSE" value="Normalize" type="button">
+<input id="ETA" type="checkbox">do eta-reductions too
<noscript><p>You may not see it because you have JavaScript turned off. Uffff!</p></noscript>
-<script language=JavaScript src="code/tokens.js"></script>
-<script language=JavaScript src="code/parse.js"></script>
-<script language=JavaScript src="code/lambda.js"></script>
-<script language=JavaScript src="code/json2.js"></script>
+<script src="/code/lambda.js"></script>
+<script src="/code/tokens.js"></script>
+<script src="/code/parse.js"></script>
+<script src="/code/json2.js"></script>
<pre id="OUTPUT">
</pre>
<script>
var parse = make_parse();
function go(source) {
- var string, tree;
+ var string, tree, expr, eta;
try {
tree = parse(source);
-// string = JSON.stringify(tree, ['key', 'name', 'message', 'value', 'arity', 'first', 'second', 'third', 'fourth'], 4);
-// string = JSON.stringify(tree.handler(), ['key', 'name', 'message', 'value', 'arity', 'first', 'second', 'tag', 'variable', 'left', 'right', 'bound', 'body' ], 4);
- string = tree.handler().to_string();
+ // string = JSON.stringify(tree, ['key', 'name', 'message', 'value', 'arity', 'first', 'second', 'third', 'fourth'], 4);
+ expr = tree.handler();
+ // string = JSON.stringify(expr, ['key', 'name', 'message', 'value', 'arity', 'first', 'second', 'tag', 'variable', 'left', 'right', 'bound', 'body' ], 4);
+// string = expr.to_string() + "\n\n~~>\n\n";
+ string = '';
+ eta = document.getElementById('ETA').checked;
+ string = string + reduce(expr, eta, false).to_string();
} catch (e) {
string = JSON.stringify(e, ['name', 'message', 'from', 'to', 'key',
'value', 'arity', 'first', 'second', 'third', 'fourth'], 4);
Under the hood
---------------
-The interpreter is written in JavaScript (which is not closely related to Java), and runs inside your browser.
+The interpreter is written in JavaScript and runs inside your browser.
So if you decide to reduce a term that does not terminate (such as `((\x (x x)) (\x (x x)))`), it will be your
browser that stops responding, not the wiki server.
Improvements we hope to add soon: the ability to reduce Combinatory Logic combinators and report the result as combinators, rather than in lambda forms.
-For these assignments, you'll probably want to use a "lambda calculator" to check your work. This accepts any grammatical lambda expression and reduces it to normal form, when possible. See our [lambda-let page](/lambda-let.html),