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

0\f z. z, which is (convertible with) \f z. f0 z
1\f z. f z, which is (syntactically identical to) \f z. f1 z
2\f z. f (f z), which is \f z. f2 z
3\f z. f (f (f z)), which is \f z. f3 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 succ3 2. That will reduce to our encoding for 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:

fl+r z ≡ fr (fl z)

(If you wonder why the ls and rs 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 predr l, or 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)r 0. But given how we encode 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:

fl*r z ≡ (fl)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.