From 1dc1c72afe669382fd004e5193b1f57be4d7cef0 Mon Sep 17 00:00:00 2001
From: Jim Pryor
Date: Sun, 3 Oct 2010 13:35:50 -0400
Subject: [PATCH] week4 debugging more
Signed-off-by: Jim Pryor
---
week4.mdwn | 37 +++++++++++++++++++++++++++++++++++++
1 file changed, 37 insertions(+)
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!)
+
+
--
2.11.0