X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=lambda_evaluator.mdwn;h=d46fc78577d3884c031e3f8446185283ddb3568a;hp=4cf073616c23eca99b37672019949d79b5b93dfc;hb=eb2a14f6c7111e6c308b72dd0e8567e4296fcfe0;hpb=08e5cbb580b637a3e4c92fbb4fbb9f7891b81103
diff --git a/lambda_evaluator.mdwn b/lambda_evaluator.mdwn
index 4cf07361..d46fc785 100644
--- a/lambda_evaluator.mdwn
+++ b/lambda_evaluator.mdwn
@@ -1,19 +1,125 @@
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 them, with full ability to 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)`.
-If you click "Reduce", the system will produce a lambda term that is guaranteed to be reduction equivalent (`<~~>`) with the original term.
-*Let*: in order to make building a more elaborate system easier, it is possible to define values using `let`.
+If you click "Normalize", the system will try to produce a normal-form lambda expression that your original term reduces to (~~>). So `((\x (\y x)) z)` reduces to `(\y z)`.
+
+*Let*: in order to make building a more elaborate set of terms easier, it is possible to define values using `let`.
In this toy system, `let`s should only be used at the beginning of a file. If we have, for intance,
let true = (\x (\y x)) in
let false = (\x (\y y)) in
+ ((true yes) no)
+
+the result is `yes`.
+
+*Comments*: anything following a semicolon to the end of the line is ignored.
+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.
+
+*Constants*: The combinators `S`, `K`, `I`, `C`, `B`, `W`, and `T` 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.)
+
+
+
+

+let true = \x y. x in
+let false = \x y. y in
+let and = \l r. l r false in
+(
+ (and true true yes no)
+ (and true false yes no)
+ (and false true yes no)
+ (and false false yes no)
+)
+

+
+

You may not see it because you have JavaScript turned off. Uffff!

+
+
+
+
+

+

+
+
+
+
+Under the hood
+---------------
+
+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.
+
+The main code is [here](http://lambda.jimpryor.net/code/lambda.js). Suggestions for improvements welcome.
+
+The code is based on:
+
+* Chris Barker's JavaScript lambda calculator
+* [Oleg Kiselyov's Haskell lambda calculator](http://okmij.org/ftp/Computation/lambda-calc.html#lambda-calculator-haskell).
+* The top-down JavaScript lexer and parser at .
+
+Improvements we hope to add soon: the ability to reduce Combinatory Logic combinators and report the result as combinators, rather than in lambda forms.
-*Comments*:
-[more soon]