From: Chris
Date: Wed, 18 Feb 2015 19:54:30 +0000 (0500)
Subject: moved fixed point for succ to exercises
XGitUrl: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=ebbcaf727cfdc7d8f183a2b6af0b77262efb691f
moved fixed point for succ to exercises

diff git a/topics/_week4_fixed_point_combinator.mdwn b/topics/_week4_fixed_point_combinator.mdwn
index eca5fc99..c93a16ba 100644
 a/topics/_week4_fixed_point_combinator.mdwn
+++ b/topics/_week4_fixed_point_combinator.mdwn
@@ 426,61 +426,6 @@ who knows what we'd get back? Perhaps there's some nonnumberrepresenting formu
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?

Let's run the recipe:

 H := \f . succ (ff)
 == \f . (\nfz.f(nfz)) (ff)
 ~~> \h . (\nfz.f(nfz)) (hh)
 ~~> \hfz.f(hhfz)

 H H == (\hfz.f(hhfz)) (\hfz.f(hhfz))
 ~~> \fz.f((\hfz.f(hhfz))(\hfz.f(hhfz))fz)
 ~~> \fz.f(f((\hfz.f(hhfz))(\hfz.f(hhfz))fz))
 ~~> \fz.f(f(f((\hfz.f(hhfz))(\hfz.f(hhfz))fz))

We can see that the fixed point generates an endless series of `f`'s.
In terms of Church numbers, this is a way of representing infinity:
if the size of a Church number is the number `f`'s it contains, and
this Church number contains an unbounded number of `f`'s, then its
size is unbounded.

We can also see how this candidate for infinity behaves with respect
to our other arithmetic operators.

 add 2 (HH) == (\mnfz.mf(nfz)) (\fz.f(fz)) (H H)
 ~~> \fz.(\fz.f(fz)) f ((HH)fz)
 ~~> \fz.\z.f(fz) ((HH)fz)
 ~~> \fz.f(f((HH)fz))
 == \fz.f(f(((\hfz.f(hhfz)) (\hfz.f(hhfz)))fz))
 ~~> \fz.f(f((\fz.f((\hfz.f(hhfz)) (\hfz.f(hhfz))))fz))
 ~~> \fz.f(f(f((\hfz.f(hhfz)) (\hfz.f(hhfz)))))

So `2 + (HH) <~~> (HH)`. This is what we expect from arithmetic infinity.
You can check to see if `2 * (HH) <~~> (HH)`.

So our fixed point recipe has delivere a reasonable candidate for
arithmetic infinity.

One (by now obvious) upshot is that the recipes that enable us to name
fixed points for any given formula aren't *guaranteed* to give us
*terminating* fixed points. They might give us formulas X such that