tweaks

diff --git a/topics/week2_encodings.mdwn b/topics/week2_encodings.mdwn
index 6df8291..eca1514 100644 (file)
--- a/topics/week2_encodings.mdwn
+++ b/topics/week2_encodings.mdwn
@@ -1,6 +1,6 @@
 # Encoding Booleans, Tuples, Lists, and Numbers #
 
 # Encoding Booleans, Tuples, Lists, and Numbers #
 

-The lambda calculus can represent any computable function?
+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.
 
 We need to do some work to show how to represent some of the functions
 we've become acquainted with.


@@ -55,7 +55,7 @@ Sucess! In the same spirit, `'false` could be **K I**, which reduces to `(\y x.
                      ~~> ((\x x) L)
                      ~~> L
 
                      ~~> ((\x x) L)
                      ~~> L
 

-So have seen our first major encoding in the lambda calculus:
+So have seen our first major encoding in the Lambda Calculus:

 "true" is represented by **K**, and "false" is represented by **K I**.
 We'll be building up a lot of representations in the weeks to come,
 and they will all maintain the discipline that if a expression is
 "true" is represented by **K**, and "false" is represented by **K I**.
 We'll be building up a lot of representations in the weeks to come,
 and they will all maintain the discipline that if a expression is


@@ -138,7 +138,7 @@ You should also be experimenting with this site's [[lambda evaluator|code/lambda
 
 ## Tuples ##
 
 
 ## 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. 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.)
+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.)

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


@@ -236,12 +236,12 @@ We also saw in seminar how to define `fold_right`. We could do this in Kapulet l
 
     letrec
       fold_right (f, z) xs = case xs of
 
     letrec
       fold_right (f, z) xs = case xs of

-                               [] then zs;
+                               [] then z;

                                y & ys then f (y, fold_right (f, z) ys)
                              end
     in fold_right
 
                                y & ys then f (y, fold_right (f, z) ys)
                              end
     in fold_right
 

-(In some presentations you may see this expecting `f` to be a curried function `lambda x z. ...` rather than the uncurried `lambda (x, z). ...` that I'm expecting here. We will be shifting to the curried form ourselves momentarily.)
+(In some presentations you may see this expecting `f` to be a curried function `lambda y z. ...` rather than the uncurried `lambda (y, z). ...` that I'm expecting here. We will be shifting to the curried form ourselves momentarily.)

 
 We suggested in class that these functions were very powerful, and could be deployed to do most everything you might want to do with a list. Given how our strategy for encoding booleans turned out, this ought to suggest to you the idea that *folding is what we fundamentally do* with lists, just as *conditional branching is what we fundamentally do* with booleans. So we can try to encode lists in terms of lambda expressions that will let us perform folds on them. We could try to do this with either right-folds or left-folds. Either is viable. Some things are more natural if you use right-folds, though, so let's do that.
 
 
 We suggested in class that these functions were very powerful, and could be deployed to do most everything you might want to do with a list. Given how our strategy for encoding booleans turned out, this ought to suggest to you the idea that *folding is what we fundamentally do* with lists, just as *conditional branching is what we fundamentally do* with booleans. So we can try to encode lists in terms of lambda expressions that will let us perform folds on them. We could try to do this with either right-folds or left-folds. Either is viable. Some things are more natural if you use right-folds, though, so let's do that.
 


@@ -276,9 +276,11 @@ We saw before what a `make-triple` function would look like. What about a `make-
     let cons = \d ds. \f z. f d (ds f z)
     in ...
 
     let cons = \d ds. \f z. f d (ds f z)
     in ...
 

-Let's walk through this. We supply this function with our `c` and `[]` as arguments. So its `d` gets bound to our `c`, and its `ds` gets bound to our `[]`, namely `\f z. z`. Then our result is a higher order function of the form `\f z. f c SOMETHING`. That looks good, what we're after is just this, except the `SOMETHING` should be `z`. If we just simply said `z` here, then our `cons` function would always be giving us back a singleton list of the form `\f z. f x z` for some `x`. That's what we want in this case, but not in the general case. What we'd like is to use the second argument we fed to `cons`, here `[]` or `\f z. z`, and have it reduce to `z`, with the hope that the same strategy would make more complex second arguments reduce to other appropriate values. Well, `\f z. z` expects an `f` and a `z` as arguments, and hey we happen to have an `f` and a `z` handy, since we're inside something of the form `\f z. f c SOMETHING`. The `f` and `z` will be supplied by the consumer or user of the sequence `[c]` that we're building. So let's just give *those* `f` and `z` to `\f z. z` as *its* arguments, and we end up with simply `z`. In other words, where `ds` is the second argument we fed to `cons`, we make `SOMETHING` be `ds f z`.
+Let's walk through this. We supply this function with our `c` and `[]` as arguments. So its `d` gets bound to our `c`, and its `ds` gets bound to our `[]`, namely `\f z. z`. Then our result is a higher order function of the form `\f z. f c SOMETHING`. That looks good, what we're after is just this, except the `SOMETHING` should end up as `z`. If we just simply *substituted* `z` for `SOMETHING`, then our `cons` function would *always* end up giving us back a singleton list of the form `\f z. f X z` for some `X`. That is the form we want in the present case, computing `cons c []`, but not in the general case. What we'd like instead is to *do something to* the second argument we fed to `cons`, here `[]` or `\f z. z`, and have *it* reduce to `z`, with the hope that the same operation would make *more complex* second arguments reduce to *other* appropriate values. Well, `\f z. z` expects an `f` and a `z` as arguments, and hey we happen to have an `f` and a `z` handy, since we're inside something of the form `\f z. f c SOMETHING`. The `f` and `z` will be supplied by the consumer or user of the sequence `[c]` that we're building. So let's just give *those* `f` and `z` to `\f z. z` as *its* arguments, and we end up with simply `z`. In other words, where `ds` is the second argument we fed to `cons`, we make `SOMETHING` in `\f z. f c SOMETHING` be `ds f z`. That is why we make `cons` be:

 
 

-Formally:
+    \d ds. \f z. f d (ds f z)
+
+Let's step through it formally. Given our definitions:

 
     cons c []
 
 
     cons c []
 


@@ -351,7 +353,7 @@ we have:
 
     head=a, sublist=(head=b, sublist=(head=c, sublist=[]))
 
 
     head=a, sublist=(head=b, sublist=(head=c, sublist=[]))
 

-with the number 3 we instead only have:
+with the number `3` we instead only have:

 
     head=(), subnumber=(head=(), subnumber=(head=(), subnumber=zero))
 
 
     head=(), subnumber=(head=(), subnumber=(head=(), subnumber=zero))
 


@@ -369,7 +371,7 @@ Now, we had a strategy for encoding the list `[a, b, c]` as:
 
     \f z. f a (f b (f c z))
 
 
     \f z. f a (f b (f c z))
 

-So perhaps we can apply the same kind of idea to the number 3, and encode it as:
+So perhaps we can apply the same kind of idea to the number `3`, and encode it as:

 
     \f z. f   (f   (f   z))
 
 
     \f z. f   (f   (f   z))
 


@@ -383,7 +385,7 @@ The composition of a function `f` with itself, namely:
 
 is sometimes abbreviated as <code>f<sup>2</sup></code>. Similarly, <code>f &cir; f &cir; f</code> or `\x. f (f (f x))` is sometimes abbreviated as <code>f<sup>3</sup></code>. <code>f<sup>1</sup></code> is understood to be just `f` itself, and <code>f<sup>0</sup></code> is understood to be the identity function.
 
 
 is sometimes abbreviated as <code>f<sup>2</sup></code>. Similarly, <code>f &cir; f &cir; f</code> or `\x. f (f (f x))` is sometimes abbreviated as <code>f<sup>3</sup></code>. <code>f<sup>1</sup></code> is understood to be just `f` itself, and <code>f<sup>0</sup></code> is understood to be the identity function.
 

-So in proposing to encode the number 3 as:
+So in proposing to encode the number `3` as:

 
     \f z. f   (f   (f   z))
 
 
     \f z. f   (f   (f   z))
 


@@ -415,7 +417,7 @@ In the same spirit, what do you expect this will reduce to:
 
     3 succ 0
 
 
     3 succ 0
 

-Since 3 is `\f z. f (f (f z))`, it should reduce to whatever:
+Since `3` is `\f z. f (f (f z))`, it should reduce to whatever:

 
     succ (succ (succ 0))
 
 
     succ (succ (succ 0))