We saw before what a `make-triple` function would look like. What about a `make-list` 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 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`.
Formally:
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
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 right-folding 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 right-folding 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.
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
\f z. f (g a) (f (g b) (f (g c) z))
-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 values over `[g a, g b, g c]`, which is `map g [a, b, c]`.
+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]`.
## 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.
-*More coming...*
+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 zero-length 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 <code>f ○ g</code>, or in Kapulet as `f comp g`. This is defined to be:
+
+ \x. f (g x)
+
+The composition of a function `f` with itself, namely:
+
+ \x. f (f x)
+
+is sometimes abbreviated as <code>f<sup>2</sup></code>. Similarly, <code>f ○ f ○ 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:
+
+ \f z. f (f (f z))
+
+we are proposing to encode it as:
+
+<code>\f z. f<sup>3</sup> z</code>
+
+(The <code>f<sup><em>n</em></sup></code> 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:
+
+<code>0 ≡ \f z. I z ; or \f z. f<sup>0</sup> z</code>
+<code>1 ≡ \f z. f z ; or \f z. f<sup>1</sup> z</code>
+<code>2 ≡ \f z. f (f z) ; or \f z. f<sup>2</sup> z</code>
+<code>3 ≡ \f z. f (f (f z)) ; or \f z. f<sup>3</sup> z</code>
+<code>...</code>
+
+The encoding for `0` can also be written as `\f z. z`, which we've 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'll look at other encodings of lists and numbers later.