author Jim Sat, 7 Feb 2015 20:17:56 +0000 (15:17 -0500) committer Jim Sat, 7 Feb 2015 20:17:56 +0000 (15:17 -0500)

index 2e4c58c..90fea0c 100644 (file)
@@ -14,7 +14,7 @@ We'll start with the `if ... then
if M then N else L

For a boolean-valued expression `M`, the displayed expression should evaluate to whatever `N` does
-if `M` evaluates to `'true`, and to whatever `L` does if `M` evaluates to `'false.
+if `M` evaluates to `'true`, and to whatever `L` does if `M` evaluates to `'false`.
In order to encode or simulate such an `if` clause in the Lambda Calculus, we
need to settle on a way to represent `'true` and `'false`.

@@ -48,7 +48,7 @@ Let's test:

((K N) L) == (((\x y. x) N) L) ~~> ((\y. N) L) ~~> N

-Sucess! In the same spirit, `'false` could be **K I**, which reduces to `(\y x. x)`:
+Sucess! In the same spirit, `'false` could be **K I**, which reduces to `(\y x. x)` (also written as `(\y. (\x x))`):

(((K I) N) L) == ((((\x y. x) (\x x)) N) L)
~~> (((\y. (\x x)) N) L)
@@ -85,9 +85,12 @@ all your other decisions about how to encode other functions. In this case, we c
because we're assuming that the `p` only gets bound to arguments that are either `\x y. x` or `\y x. x`. We don't make any
promises about what will happen if our encodings are abused, that is, supplied with arguments they weren't designed to accept.
If `p` is bound to `\x y. x`, then the result of both of the above displayed expressions will be whatever `q` is bound to.
-If on the other hand, `p` is bound to `\y x. x`, then the two dislayed expressions will be the same. Despite this, they are
-two different lambda expressions, and are not convertible. It's only within the frame of our assumptions about the restricted
-arguments we're thinking of supplying them that they behave exactly the same.
+If on the other hand, `p` is bound to `\y x. x`, then the two displayed expressions will return the same result, namely that function.
+
+Despite this, the two displayed expressions are two different lambda terms, and
+are not convertible. It's only within the frame of our assumptions about the
+restricted arguments we're thinking of supplying them that they behave exactly
+alike.

You can try out these expressions in the [[lambda evaluator|code/lambda evaluator]]:

@@ -96,7 +99,7 @@ You can try out these expressions in the [[lambda evaluator|code/lambda evaluato
let and = \p q. p q p in
and true false

-will reduce or "normalize" to `\y x. x`, or false, just as you'd predict. The `let true =` stuff isn't officially part of the Lambda Calculus language. It's just a convenient shorthand that lets you use the lambda evaluator more efficiently. Behind the scenes, the displayed expression above gets translated to:
+will reduce or "normalize" to `\y x. x`, or false, just as you'd predict. The `let true =` stuff isn't officially part of the Lambda Calculus language. It's just a convenient shorthand that lets you use the lambda evaluator more easily. Behind the scenes, the displayed expression above gets translated to:

(\true.
(\false.
@@ -117,7 +120,7 @@ and then used like this:

((lambda-and true) false)

-which will evaluate to a function, that happens to be the true function. Most Scheme interpreters like Racket will helpfully display the function with the name, if any, that was first defined to be bound to it. So we'll see the result as:
+which will evaluate to a function, that happens to be the same function `false` is bound to. Most Scheme interpreters like Racket will helpfully display the function with the name, if any, that was first defined to be bound to it. So we'll see the result as:

#<procedure:false>

@@ -135,7 +138,7 @@ You should also be experimenting with this site's [[lambda evaluator|code/lambda

## Tuples ##

-In class, we also showed you how to encode a tuple in the Lambda Calculator. We did it with an ordered triple, but the strategy generalizes in a straightforward way. (Some authors just use this strategy to define pairs, then define triples as pairs whose second member is another pair, and so on. Yech. If you keep a firm grip on your wits, that can also be made to work, but it's extremely likely that people who code in that way are going to lose their grip at some point and get themselves in a corner where they'll regret having made that decision about how to encode triples. The strategy presented here is elegant and will help you program more hygienically even when your attention lapses.)
+In class, we also showed you how to encode a tuple in the Lambda Calculator. We did it with an ordered triple, but the strategy generalizes in a straightforward way. (Some authors just use this strategy to define *pairs*, then define triples as pairs whose second member is another pair, and so on. Yech. If you keep a firm grip on your wits, that can also be made to work, but it's extremely likely that people who code in that way are going to lose their grip at some point and get themselves in a corner where they'll regret having made that decision about how to encode triples. And they will be forced to add further complexities at later points, that they're probably not anticipating now. The strategy presented here is as elegant as it first looks, and will help you program more hygienically even when your attention lapses.)

Our proposal was to define the triple `(a, b, c)` as:

index 091e123..d002abf 100644 (file)
@@ -228,7 +228,12 @@ abbreviates:

((\x (\y (x y))) x)

-We didn't have to insert any parentheses around the inner body of `\y. (x y)` because they were already there.
+The outermost parentheses were added because we have an application. `(\x. \y.
+...)` became `(\x (\y. ...))` because of the rule for dots. We didn't have to
+insert any parentheses around the inner body of `\y. (x y)` because they were
+already there. That is, in expressions of the form `\y. (...)`, the dot abbreviates
+nothing. It's harmless to write such a dot, though, and it can be conceptually
+helpful especially in light of the next convention...

**Merging lambdas** An expression of the form `(\x (\y M))`, or equivalently, `(\x. \y. M)`, can be abbreviated as: