From ddafcdc11f354d8ce4be628b006316c57083d1ec Mon Sep 17 00:00:00 2001 From: Jim Date: Sat, 7 Feb 2015 15:17:56 -0500 Subject: [PATCH 1/1] tweaks, thanks Kyle for feedback --- topics/_lambda_encodings.mdwn | 19 +++++++++++-------- topics/week2_lambda_intro.mdwn | 7 ++++++- 2 files changed, 17 insertions(+), 9 deletions(-) diff --git a/topics/_lambda_encodings.mdwn b/topics/_lambda_encodings.mdwn index 2e4c58c0..90fea0cc 100644 --- a/topics/_lambda_encodings.mdwn +++ b/topics/_lambda_encodings.mdwn @@ -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: # @@ -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: diff --git a/topics/week2_lambda_intro.mdwn b/topics/week2_lambda_intro.mdwn index 091e1234..d002abf8 100644 --- a/topics/week2_lambda_intro.mdwn +++ b/topics/week2_lambda_intro.mdwn @@ -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: -- 2.11.0