XGitUrl: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek2_encodings.mdwn;h=091fb4c5e19d8069a851375db8dc7d28fdfa794a;hp=386236495906721a51b701f9f192ae8406c95f50;hb=629e27a98dad2c0c1bb4dbcc246c2d03693ef7c6;hpb=0ac2d90aac898f1e1d5f90c502d52845c68b5b2a
diff git a/topics/week2_encodings.mdwn b/topics/week2_encodings.mdwn
index 38623649..091fb4c5 100644
 a/topics/week2_encodings.mdwn
+++ b/topics/week2_encodings.mdwn
@@ 1,15 +1,14 @@
# 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.

+
## Booleans ##
We'll start with the `if ... then
... else...` construction we saw last week:
+We'll start with the `if ... then ... else ...` construction we saw last week:
if M then N else L
@@ 55,7 +54,7 @@ Sucess! In the same spirit, `'false` could be **K I**, which reduces to `(\y x.
~~> ((\x x) L)
~~> L
So have seen our first major encoding in the lambda calculus:
+So we 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
@@ 136,21 +135,22 @@ There's also a (slow, barebones, but perfectly adequate) version of Scheme avai
You should also be experimenting with this site's [[lambda evaluatorcode/lambda evaluator]].
+
## 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:
 \f. f a b c
+ \h. h a b c
To extract the first element of this, you'd write:
 (\f. f a b c) fst_of_three
+ (\h. h a b c) fst_of_three
where `fst_of_three` is the function `\x y z. x`:
 (\f. f a b c) (\x y z. x) ~~>
+ (\h. h a b c) (\x y z. x) ~~>
(\x y z. x) a b c ~~>
(\y z. a) b c ~~>
(\z. a) c ~~>
@@ 159,7 +159,7 @@ where `fst_of_three` is the function `\x y z. x`:
Here are the corresponding definitions in Scheme (Racket):
(define maketriple (lambda (a) (lambda (b) (lambda (c)
 (lambda (f) (((f a) b) c))))))
+ (lambda (h) (((h a) b) c))))))
(define fst_of_three (lambda (x) (lambda (y) (lambda (z) x))))
(define snd_of_three (lambda (x) (lambda (y) (lambda (z) y))))
@@ 177,21 +177,38 @@ If you're puzzled by having the triple to the left and the function that "uses"
If you really want to, you can disguise what's going on like this:
 (define liftedfst_of_three (lambda (p) (p fst_of_three)))
+ (define liftedfst_of_three (lambda (trip) (trip fst_of_three)))
Then you could say:
 (liftedfst_of_three p)
+ (liftedfst_of_three t)
instead of:
 (p fst_of_three)
+ (t fst_of_three)
Of course, the last is still what's happening under the hood.
(Remark: `(liftedf (((maketriple 10) 20) 30))` stands to `((((maketriple 10) 20) 30) f)` as
`((((maketriple 10) 20) 30) f)` stands to `(((f 10) 20) 30)`.)
+
+### Curried and Uncurried functions in the Lambda Calculus ###
+
+As we've explained before, an *uncurried* function is one that takes multiple arguments in a single bundle, as a tuple, like this:
+
+ f (x, y, z)
+
+Whereas a *curried* function is one that takes multiple arguments in sequence, like this:
+
+ g x y z
+
+That is, `g` is a function expecting one argument (here `x`), that evaluates to a second function, that itself expects another argument (here `y`), and so on. (So `g` is a *higherorder function*: the result of applying it to argument `x` returns another function.) In discussing Kapulet and Scheme and OCaml and Haskell, we sometimes worked with uncurried functions, and other times with curried ones. Now that you've seen how to build and work with tuples in the Lambda Calculus, you can write uncurried functions there too. That is, you can write functions `f` that will expect arguments of the form `\h. h x y z`. But in the end, `f` is going to have to apply that argument to some auxiliary handler function `g` anyway, where `g` takes *its* arguments in curried form. So if you can, in the Lambda Calculus it's easiest to just work with curried functions like `g` in the first place, rather than uncurried, tupleexpecting arguments like `f`.
+
+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 runofthemill 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.
+
+
+
## 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.
@@ 214,6 +231,7 @@ That will evaluate to whatever this does:
f (f (f (z, 10), 20), 30)
+
With a commutative operator like `(+)`, it makes no difference whether you say `fold_right ((+), z) xs` or `fold_left ((+), z) xs`. But with other operators it will make a difference. We can't say `fold_left ((&), []) [10, 20, 30]`, since that would start by trying to evaluate `[] & 10`, which would crash. But we could do this:
let
@@ 236,12 +254,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
 [] then zs;
+ [] then z;
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 rightfolds or leftfolds. Either is viable. Some things are more natural if you use rightfolds, though, so let's do that.
@@ 259,7 +277,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 that's how the Lambda Calculus does things. You wouldn't want to build up a tuple using the mechanisms described above, and then supply `f` as an argument to that tuple, and so on. That would be a lot of red tape for no benefit. In the Lambda Calculus, it's simpler to just work with curried functions as our natural idiom.
+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 higherorder function above, what should `[c]` be? Evidently:
@@ 273,19 +291,21 @@ I hope it was this one: `\f z. z`. Because when we fold a function `f` and a sta
We saw before what a `maketriple` function would look like. What about a `makelist` function, or as we've been calling it, "cons" (`&` in Kapulet)? Well, we've already seen what the representation of `[]` and `[c]` are. In that simplest case, the `cons` function should take us from the encoding of `[]`, namely `\f z. z` to the encoding of `[c]`, namely `\f z. f c z`, as a result. Here is how we can define this:
 let cons = \c cs. \f z. f c (cs f z)
+ 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 `c` gets bound to our `c`, and its `cs` 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 wuld 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 been given an `f` and a `z`, supplied by the consumer or user of the sequence `[c]` that we're building. So let's just give them to `\f z. z` as its arguments, and it gives us `z`. In other words, we make `SOMETHING` be `cs 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 []
is:
 (\c cs. \f z. f c (cs f z)) c (\f z. z) ~~>
 (\cs. \f z. f c (cs f z)) (\f z. z) ~~>
+ (\d ds. \f z. f d (ds f z)) c (\f z. z) ~~>
+ (\ds. \f z. f c (ds f z)) (\f z. z) ~~>
\f z. f c ((\f z. z) f z) ~~>
\f z. f c ((\z. z) z) ~~>
\f z. f c z
@@ 298,13 +318,13 @@ Will this work when more complex values are supplied as the second argument to `
is:
 (\c cs. \f z. f c (cs f z)) b (\f z. f c z) ~~>
 (\cs. \f z. f b (cs f z)) (\f z. f c z) ~~>
+ (\d ds. \f z. f d (ds f z)) b (\f z. f c z) ~~>
+ (\ds. \f z. f b (ds f z)) (\f z. f c z) ~~>
\f z. f b ((\f z. f c z) f z) ~~>
\f z. f b ((\z. f c z) z) ~~>
\f z. f b (f c z)
which looks right. Persuade yourself that the `cons` we've defined here, together with the representation `\f z. z` for the empty list, always give us the correct encoding for complex lists, in terms of a function that takes an `f` and a `z` as arguments, and then returns the result of rightfolding those values over the list elements in the appropriate order.
+which looks right. Persuade yourself that the `cons` we've defined here, together with the representation `\f z. z` for the empty list, always give us the correct encoding for complex lists, in terms of a function that takes an `f` and a `z` as arguments, and then returns the result of rightfolding those arguments over the list elements in the appropriate order.
You may notice that the encoding we're proposing for `[]` is the same encoding we proposed above for `false`. There's nothing deep to this. If we had adopted other conventions, we could easily have made it instead be `true` and `[]` that had the same encoding.
@@ 314,18 +334,18 @@ Now we saw above how to define `map` in terms of `fold_right`. In Kapulet syntax
In our Lambda Calculus encoding, `fold_right (f, z) xs` gets translated to `xs f z`. That is, the list itself is the operator, just as we saw triples being. So we just need to know how to represent `lambda (x, zs). g x & zs`, on the one hand, and `[]` on the other, into the Lambda Calculus, and then we can also express `map`. Well, in the Lambda Calculus we're working with curried functions, and there's no infix syntax, so we'll replace the first by `lambda x zs. cons (g x) zs`. But we just defined `cons`, and the lambda is straightforward. And we also just defined `[]`. So we already have all the pieces to do this. Namely:
 map (g, z) xs
+ map g xs
in Kapulet syntax, turns into this in our lambda evaluator:
let empty = \f z. z in
 let cons = \c cs. \f z. f c (cs f z) in
+ let cons = \d ds. \f z. f d (ds f z) in
xs (\x zs. cons (g x) zs) empty
Try out this:
let empty = \f z. z in
 let cons = \c cs. \f z. f c (cs f z) in
+ let cons = \d ds. \f z. f d (ds f z) in
let map = \g xs. xs (\x zs. cons (g x) zs) empty in
let abc = \f z. f a (f b (f c z)) in
map g abc
@@ 334,11 +354,95 @@ That will evaluate to:
\f z. f (g a) (f (g b) (f (g c) z))
which looks like what we want, a higherorder function that will take an `f` and a `z` as arguments and then return the right fold of those values over `[g a, g b, g c]`, which is `map g [a, b, c]`.
+which looks like what we want, a higherorder 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]`.
+
## Numbers ##
It's noteworthy that when he was developing the lambda calculus, Church had not predicted it would be possible to encode the numbers. It came as a welcome surprise.
+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.
+
+It's noteworthy that when he was developing the Lambda Calculus, Church had not predicted it would be possible to encode the numbers. It came as a welcome surprise.
+
+The idea here is that a number is something like a list, only without any slot for an interesting, possibly varying head element at each level. Whereas in a list like:
+
+ [a, b, c]
+
+we have:
+
+ head=a, sublist=(head=b, sublist=(head=c, sublist=[]))
+
+with the number `3` we instead only have:
+
+ head=(), subnumber=(head=(), subnumber=(head=(), subnumber=zero))
+
+where `()` is the zerolength tuple, the one and only member of its type. That is, the head here is a type of thing that cannot interestingly vary. Or we could just eliminate the head, and have:
+
+ subnumber=(subnumber=(subnumber=zero))
+
+probably more familiar to you as:
+
+ succ (succ (succ zero))
+
+In other words, where a list is inductively built up out of some interesting new datum and its "sublist" or tail, a number is inductively built up out of no interesting new datum and its "subnumber" or predecessor. In this light, a number can be seen as a kind of stunted or undernourished list.
+
+Now, we had a strategy for encoding the list `[a, b, c]` as:
+
+ \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:
+
+ \f z. f (f (f z))
+
+In fact, there's a way of looking at this that makes it look incredibly natural. You may have encountered the idea of a composition of two functions `f` and `g`, written as f ○ g
, or in Kapulet as `f comp g`. This is defined to be:
+
+ \x. f (g x)
+
+For example, the operation that maps a number `n` to n^{2}+1
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)
+
+is sometimes abbreviated as f^{2}
. Similarly, f ○ f ○ f
or `\x. f (f (f x))` is sometimes abbreviated as f^{3}
. f^{1}
is understood to be just `f` itself, and f^{0}
is understood to be the identity function.
+
+So in proposing to encode the number `3` as:
+
+ \f z. f (f (f z))
+
+we are proposing to encode it as:
+
+\f z. f^{3} z
+
+(The f^{n}
isn't some bit of new Lambda Calculus syntax. It's just our metalanguage abbreviation for the same expressions we had before. It does help focus our attention on what we're essentially doing here.)
+
+And indeed this is the Church encoding of the numbers:
+
+0 ≡ \f z. z ; <~~> \f z. I z, or \f z. f^{0} z
+1 ≡ \f z. f z ; or \f z. f^{1} z
+2 ≡ \f z. f (f z) ; or \f z. f^{2} z
+3 ≡ \f z. f (f (f z)) ; or \f z. f^{3} z
+...
+
+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.
+
+We saw that using the `cons` operation (Kapulet's `&`) and `[]` as arguments to `fold_right` over a list give us back that very same list. In the Lambda Calculus, that comes to the following:
+
+ [a, b, c] cons []
+
+with the appropriate lambda terms substituted throughout, just reduces to the same lambda term we used to encode `[a, b, c]`.
+
+In the same spirit, what do you expect this will reduce to:
+
+ 3 succ 0
+
+Since `3` is `\f z. f (f (f z))`, it should reduce to whatever:
+
+ succ (succ (succ 0))
+
+does. And if we define `succ` properly, we should expect that to give us the same lambda term that we used to encode `3` in the first place.
+
*More coming...*
+We'll look at other encodings of lists and numbers later.