Yes! That's exactly right. And which formula this is will depend on the particular way you've implemented the successor function.
-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."
+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
+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."
###Varieties of fixed-point combinators###