X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=9bfa3ee70cf3a259103510eafa8fdb4b492017be;hp=bd3d8e5c6e0deac02d0954379f67b4d393ab2bc8;hb=1dc1c72afe669382fd004e5193b1f57be4d7cef0;hpb=ee659ed0921805be0db5de5658290b6dc1222eee

diff --git a/week4.mdwn b/week4.mdwn
index bd3d8e5c..9bfa3ee7 100644
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -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!)
+
+