-Well, you might think, only some of the formulas that we might give to the `successor` as arguments would really represent numbers. If we said something like:
-
- successor make-pair
-
-who knows what we'd get back? Perhaps there's some non-number-representing formula such that when we feed it to `successor` as an argument, we get the same formula back.
-
-Yes! That's exactly right. And which formula this is will depend on the particular way you've implemented the successor function.
-
-Let's pick a way of defining the successor function and reason about it.
-Here is one way that is compatible with the constraints given in
-homework 2: `succ := \nfz.f(nfz)`. This takes a Church
-number, and returns the next Church number. For instance,
-
- succ 2 == succ (\fz.f(fz))
- == (\nfz.f(nfz)) (\fz.f(fz))
- ~~> \fz.f((\fz.f(fz))fz)
- ~~> \fz.f(f(fz))
- == 3
-
-Using logic similar to the discussion above of the fixed point for K,
-we can say that for any Church number argument to the successor
-function, the result will be the next Church number. Assume that
-there is some Church number `n` that is a fixed point. Then
-`succ n <~~> n` (because `n` is a fixed point) and `succ n <~~> n + 1`
-(since that's what the successor function does). By the Church Rosser
-theorem, `n <~~> n + 1`. What kind of `n` could satisfy that
-requirement?