-Moreover, 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 neither `X` nor `f X`
-have normal forms. (Indeed, what they give us for the square function
-isn't any of the Church numerals, but is rather an expression with no
-normal form.) However, if we take care we can ensure that we *do* get
-terminating fixed points. And this gives us a principled, fully
-general strategy for doing recursion. It lets us define even functions
-like the Ackermann function, which were until now out of our reach. It
-would also let us define arithmetic and list functions on the "version
-1" and "version 2" implementations, where it wasn't always clear how
-to force the computation to "keep going."
+ K(H H) ≡ (\xy.x)((\uy.uu)(\uy.uu)
+ ~~> \y.(\uy.uu)(\uy.uu)
+
+Yep, `H H` and `K(H H)` both reduce to the same term.
+
+To see what this fixed point does, let's reduce it a bit more:
+
+ H H ≡ (\uy.uu)(\uy.uu)
+ ~~> \y.(\uy.uu)(\uy.uu)
+ ~~> \yy.(\uy.uu)(\uy.uu)
+ ~~> \yyy.(\uy.uu)(\uy.uu)
+
+Sure enough, this fixed point ignores an endless, infinite series of
+arguments. It's a write-only memory, a black hole.
+
+Now that we have one fixed point, we can find others, for instance,
+
+ (\uy.uuu)(\uy.uuu)
+ ~~> \y.(\uy.uuu)(\uy.uuu)(\uy.uuu)
+ ~~> \yy.(\uy.uuu)(\uy.uuu)(\uy.uuu)(\uy.uuu)
+ ~~> \yyy.(\uy.uuu)(\uy.uuu)(\uy.uuu)(\uy.uuu)(\uy.uuu)
+
+Continuing in this way, you can now find an infinite number of fixed
+points, all of which have the crucial property of ignoring an infinite
+series of arguments.
+
+##What is a fixed point for the successor function?##
+
+As we've seen, the recipe just given for finding a fixed point worked
+great for our `h`, which we wrote as a definition for the length
+function. But the recipe doesn't make any assumptions about the
+internal structure of the function it works with. That means it can
+find a fixed point for literally any function whatsoever.
+
+In particular, what could the fixed point for the
+successor function possibly be like?
+
+Well, you might think, only some of the formulas that we might give to the `succ` as arguments would really represent numbers. If we said something like:
+
+ succ pair
+
+who knows what we'd get back? Perhaps there's some non-number-representing formula such that when we feed it to `succ` 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 succ function.
+
+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 `ξ` such that
+neither `ξ` nor `f ξ` have normal forms. (Indeed, what they give us
+for the `square` function isn't any of the Church numerals, but is
+rather an expression with no normal form.) However, if we take care we
+can ensure that we *do* get terminating fixed points. And this gives
+us a principled, fully general strategy for doing recursion. It lets
+us define even functions like the Ackermann function, which were until
+now out of our reach. It would also let us define list
+functions on [[the encodings we discussed last week|week3_lists#other-lists]], where it
+wasn't always clear how to force the computation to "keep going."
+
+###Varieties of fixed-point combinators###