From ebbcaf727cfdc7d8f183a2b6af0b77262efb691f Mon Sep 17 00:00:00 2001 From: Chris Date: Wed, 18 Feb 2015 14:54:30 -0500 Subject: [PATCH] moved fixed point for succ to exercises --- topics/_week4_fixed_point_combinator.mdwn | 55 ------------------------------- 1 file changed, 55 deletions(-) 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 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. -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 -- 2.11.0