X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week4_fixed_point_combinator.mdwn;h=c93a16ba2c887ff8fb64bc8c320f3e8d99fb3bff;hp=da2771a02bf88509ee37612da370d32f2d4081e1;hb=ebbcaf727cfdc7d8f183a2b6af0b77262efb691f;hpb=40a9e529a03f11246b1f6fba8e98a670c4631639 diff --git a/topics/_week4_fixed_point_combinator.mdwn b/topics/_week4_fixed_point_combinator.mdwn index da2771a0..c93a16ba 100644 --- a/topics/_week4_fixed_point_combinator.mdwn +++ b/topics/_week4_fixed_point_combinator.mdwn @@ -426,18 +426,18 @@ who knows what we'd get back? Perhaps there's some non-number-representing formu 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###