author Jim Pryor Sun, 3 Oct 2010 17:35:50 +0000 (13:35 -0400) committer Jim Pryor Sun, 3 Oct 2010 17:35:50 +0000 (13:35 -0400)
Signed-off-by: Jim Pryor <profjim@jimpryor.net>
 week4.mdwn patch | blob | history

index bd3d8e5..9bfa3ee 100644 (file)
@@ -59,3 +59,40 @@ succ X
You should see the close similarity with `Y Y` here.

+#Q. So `Y` applied to `succ` returns a number that is not finite!#
+
+A. Yes!  Let's see why it makes sense to think of `Y succ` as a Church
+numeral:
+
+       [same definitions]
+       succ X
+       = (\n s z. s (n s z)) X
+       = \s z. s (X s z)
+       = succ (\s z. s (X s z)) ; using fixed-point reasoning
+       = \s z. s ([succ (\s z. s (X s z))] s z)
+       = \s z. s ([\s z. s ([succ (\s z. s (X s z))] s z)] s z)
+       = \s z. s (s (succ (\s z. s (X s z))))
+
+So `succ X` looks like a numeral: it takes two arguments, `s` and `z`,
+and returns a sequence of nested applications of `s`...
+
+You should be able to prove that `add 2 (Y succ) <~~> Y succ`,
+likewise for `mult`, `minus`, `pow`.  What happens if we try `minus (Y
+succ)(Y succ)`?  What would you expect infinity minus infinity to be?
+(Hint: choose your evaluation strategy so that you add two `s`s to the
+first number for every `s` that you add to the second number.)
+
+This is amazing, by the way: we're proving things about a term that
+represents arithmetic infinity.
+
+It's important to bear in mind the simplest term in question is not
+infinite:
+
+       Y succ = (\f. (\x. f (x x)) (\x. f (x x))) (\n s z. s (n s z))
+
+The way that infinity enters into the picture is that this term has
+no normal form: no matter how many times we perform beta reduction,
+there will always be an opportunity for more beta reduction.  (Lather,
+rinse, repeat!)
+
+