We're continuing to assume Church's encodings of the numbers:

`0`

≡ `\f z. z`

, which is (convertible with) `\f z. f`

^{0} z

`1`

≡ `\f z. f z`

, which is (syntactically identical to) `\f z. f`

^{1} z

`2`

≡ `\f z. f (f z)`

, which is `\f z. f`

^{2} z

`3`

≡ `\f z. f (f (f z))`

, which is `\f z. f`

^{3} z

One of your homework problems for last week was to define `succ`

for this encoding. Here is how we do it:

```
\n. \f z. f (n f z)
```

Now how shall we define more advanced arithmetic functions, such as addition?

Let's recall the structural similarity between this encoding of the numbers and our right-fold encoding of lists. If we feed the number `3`

the `succ`

function and `0`

as its arguments, we get:

```
3 succ 0 ~~>
succ (succ (succ 0))
```

and that will reduce to `\f z. f (f (f z))`

, the same number with which we began. This parallels the fact that if we feed the `cons`

function and `[]`

as arguments to our encoded list `[a, b, c]`

, we get:

```
[a, b, c] cons [] ~~>
cons a (cons b (cons c []))
```

and that will reduce to `\f z. f a (f b (f c z))`

, the same list with which we began. You may recall that if you supply `cons`

plus a *non*-empty list as arguments to a right-fold operation, the result is

```
[a, b, c] cons [d, e] ~~>
cons a (cons b (cons c [d, e]))
```

which will reduce to `[a, b, c] && [d, e]`

, that is `[a, b, c, d, e]`

or `\f z. f a (f b (f c (f d (f e z))))`

. What if we did the analogous thing to our Church number? That is, what do we get if instead of `3 succ 0`

we evaluate `3 succ 2`

?

```
3 succ 2 ~~>
succ (succ (succ 2))
```

which we abbreviate as `succ`

. That will reduce to our encoding for ^{3} 2`5`

.

In general, this can be our strategy for performing the addition `add 2 3`

. We can define **add** as:

```
\l r. r succ l
```

That lambda term cannot be further reduced, but
we can prove inductively that when that abstract is applied to any Church-encoded numbers `l`

and `r`

, the result will always be convertible with
`\f z. r f (l f z)`

. So we can alternatively define **add** as:

```
\l r. \f z. r f (l f z)
```

This corresponds to the natural extension of our "exponential" metalanguage abbreviation:

`f`

^{l+r} z ≡ f^{r} (f^{l} z)

(If you wonder why the `l`

s and `r`

s are in the specific orders they are here, the answer is that with `add`

their order doesn't matter, but the pattern begun here coheres better with the orders needed for some other arithmetic functions to be described below.)

If we knew how to encode `pred`

, then we could define subtraction in a similar way: `sub l r`

would just be `pred`

, or ^{r} l`r pred l`

. We'd have to decide what `pred 0`

should reduce to. Perhaps some special error formula, or a free variable `err`

, or perhaps just to `0`

--- in the same spirit that it can be natural to make `tail []`

just be `[]`

. A more pressing issue is that we don't know yet how to define `pred`

. And in fact, with Church's encoding of the numbers, this is not trivial. We discuss the issue and give you some guidance about how to do it in this week's homework. (With some other encodings of the numbers, it is more straightforward to define `pred`

; but then those other encodings have other compensating disadvantages.)

What about multiplication? Well, in general, `mul l r`

should be the result of applying the (curried, partially applied) function `(add l)`

to `0`

, and then applying `(add l)`

again to the result, and again, ... `r`

times. In other words, it should be `(add l)`

. But given how we encode ^{r} 0`r`

, that will just be `r (add l) 0`

. And so we can define **mul** as:

```
\l r. r (add l) 0
```

As with `add`

,
we can prove inductively that when that abstract is applied to any Church-encoded numbers `l`

and `r`

, the result will always be convertible with
`\f z. r (l f) z`

. So we can alternatively define **mul** as:

```
\l r. \f z. r (l f) z
```

This corresponds to the natural extension of our "exponential" metalanguage abbreviation:

`f`

^{l*r} z ≡ (f^{l})^{r} z

Interestingly, `mul l r`

defined in that second way eta-reduces to `\f. r (l f)`

, which we also know as the *composition* `r ○ l`

of `r`

with `l`

.

If we continue in this direction, we end up defining `l^r`

(where `2^5`

is `32`

) either as `r (mul l) one`

or as the *application* `r l`

of `r`

to `l`

.

Not all of the arithmetic encodings are so neat and elegant, however. As we mentioned, `pred`

takes some ingenuity. We'll also have you define `zero?`

and `≤`

for homework.

Here is an example of some programmers having fun with Church numbers. A tiny glossary: FORTRAN is a very old imperatival language that Scheme hoped to replace; SML is a sister language to OCaml; Chez is one Scheme implementation (like Racket and Chicken); and you will learn about "Y" next week. You should be able to figure out what the refrain means.