add Q comparing our exposition to The Little Schemer's
[lambda.git] / topics / week2_encodings.mdwn
index 8b760e2..85d4d77 100644 (file)
@@ -5,7 +5,7 @@ The Lambda Calculus can represent any computable function?
 We need to do some work to show how to represent some of the functions
 we've become acquainted with.
 
-
+<a id=booleans></a>
 ## Booleans ##
 
 We'll start with the `if ... then ... else ...` construction we saw last week:
@@ -135,6 +135,7 @@ There's also a (slow, bare-bones, but perfectly adequate) version of Scheme avai
 You should also be experimenting with this site's [[lambda evaluator|code/lambda evaluator]].
 
 
+<a id=tuples></a>
 ## Tuples ##
 
 In class, we also showed you how to encode a tuple in the Lambda Calculus. 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.)
@@ -207,6 +208,7 @@ That is, `g` is a function expecting one argument (here `x`), that evaluates to
 In some cases you can't do this, because you'll be partaking of some general pattern that only makes room for a single argument --- like the "starting value" `z` in the `fold_right` function discussed below; yet you're performing some task that really requires you to stuff a couple of values into that position. Tuples are ideal for that purpose. But in for run-of-the-mill functions you're defining in the Lambda Calculus, if multiple arguments need to be passed to a function, and it's up to you whether to pass them in curried or uncurried/tuple style, you should default to the curried style (as in, `g x y z`). That's the more idiomatic, native style for passing arguments in the Lambda Calculus.
 
 
+<a id=lists></a>
 ## Lists ##
 
 There are multiple ways to encode lists, and also multiple ways to encode numbers. We are going to start with what we think are the most natural and elegant encodings. Historically these were the first encodings of numbers but not of lists.
@@ -274,7 +276,7 @@ Now, what should the `SOMETHING` be? Well, when we supply an `f` and a `z` we sh
 
     \f z. f a (f b (f c z))
 
-Here we work with curried functions, because as we explained at the end of the section on Tuples, that's the idiomatic and native style for passing multiple arguments in the Lambda Calculus.
+Here we assume `f` to be a curried function, taking its arguments in the form `f c z` rather that `f (c, z)` (that is, `f (\h. h c z)`), because as we explained at the end of the section on Tuples, the curried form is the idiomatic and native style for passing multiple arguments in the Lambda Calculus.
 
 So if `[a, b, c]` should be the displayed higher-order function above, what should `[c]` be? Evidently:
 
@@ -354,6 +356,7 @@ That will evaluate to:
 which looks like what we want, a higher-order function that will take an `f` and a `z` as arguments and then return the right fold of those arguments over `[g a, g b, g c]`, which is `map g [a, b, c]`.
 
 
+<a id=numbers></a>
 ## Numbers ##
 
 Armed with the encoding we developed for lists above, Church's method for encoding numbers in the Lambda Calculus is very natural. But this is not the order that these ideas were historically developed.
@@ -394,6 +397,8 @@ In fact, there's a way of looking at this that makes it look incredibly natural.
 
     \x. f (g x)
 
+For example, the operation that maps a number `n` to <code>n<sup>2</sup>+1</code> is the composition of the successor function and the squaring function (first we square, then we take the successor).
+
 The composition of a function `f` with itself, namely:
 
     \x. f (f x)
@@ -412,13 +417,13 @@ we are proposing to encode it as:
 
 And indeed this is the Church encoding of the numbers:
 
-<code>0 &equiv; \f z. I z &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;;  or \f z. f<sup>0</sup> z</code>  
-<code>1 &equiv; \f z. f z &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;;  or \f z. f<sup>1</sup> z</code>  
-<code>2 &equiv; \f z. f (f z) &nbsp;&nbsp;&nbsp;&nbsp;;  or \f z. f<sup>2</sup> z</code>  
-<code>3 &equiv; \f z. f (f (f z)) ;  or \f z. f<sup>3</sup> z</code>  
+<code>0 &equiv; \f z. z &nbsp;&nbsp;;  <~~> \f z. I z, or \f z. f<sup>0</sup> z</code>  
+<code>1 &equiv; \f z. f z &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;;  or \f z. f<sup>1</sup> z</code>  
+<code>2 &equiv; \f z. f (f z) &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;;  or \f z. f<sup>2</sup> z</code>  
+<code>3 &equiv; \f z. f (f (f z)) &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;;  or \f z. f<sup>3</sup> z</code>  
 <code>...</code>
 
-The encoding for `0` is equivalent to `\f z. z`, which we've also proposed as the encoding for `[]` and for `false`. Don't read too much into this.
+The encoding for `0` is what we also proposed as the encoding for `[]` and for `false`. Don't read too much into this.
 
 Given the above, can you figure out how to define the `succ` function? We already worked through the definition of `cons`, and this is just a simplification of that, so you should be able to do it. We'll make it a homework.