From 1dc1c72afe669382fd004e5193b1f57be4d7cef0 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Sun, 3 Oct 2010 13:35:50 -0400 Subject: [PATCH 1/1] 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