From c755fb35412150c91b5dc7ec2efdc2a28aa6cac3 Mon Sep 17 00:00:00 2001 From: Chris Date: Tue, 17 Feb 2015 18:23:34 -0500 Subject: [PATCH 1/1] the succ fixed point as arithmetic infinity --- topics/_week4_fixed_point_combinator.mdwn | 79 ++++++++++++++++++++++++++----- 1 file changed, 67 insertions(+), 12 deletions(-) diff --git a/topics/_week4_fixed_point_combinator.mdwn b/topics/_week4_fixed_point_combinator.mdwn index da2771a0..01185c40 100644 --- a/topics/_week4_fixed_point_combinator.mdwn +++ b/topics/_week4_fixed_point_combinator.mdwn @@ -426,18 +426,73 @@ 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." +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 +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### -- 2.11.0