From: Chris Barker <barker@kappa.linguistics.fas.nyu.edu>
Date: Sat, 2 Oct 2010 19:30:20 +0000 (-0400)
Subject: edits
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=1f5422bb82c42ac01506c66e21faea79e4872af3

edits
---

diff --git a/week4.mdwn b/week4.mdwn
index 8d89a5a6..edf9552d 100644
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -18,7 +18,7 @@ X = WW = (\x.T(xx))W = T(WW) = TX
 Please slow down and make sure that you understand what justified each
 of the equalities in the last line.
 
-Q: How do you know that for any term T, YT is a fixed point of T?
+Q: How do you know that for any term `T`, `YT` is a fixed point of `T`?
 
 A: Note that in the proof given in the previous answer, we chose `T`
 and then set `X = WW = (\x.T(xx))(\x.T(xx))`.  If we abstract over
@@ -26,7 +26,7 @@ and then set `X = WW = (\x.T(xx))(\x.T(xx))`.  If we abstract over
 what argument `T` we feed Y, it returns some `X` that is a fixed point
 of `T`, by the reasoning in the previous answer.
 
-Q: So if every term has a fixed point, even Y has fixed point.
+Q: So if every term has a fixed point, even `Y` has fixed point.
 
 A: Right:
 
@@ -42,7 +42,7 @@ Q: Ouch!  Stop hurting my brain.
 A: Let's come at it from the direction of arithmetic.  Recall that we
 claimed that even `succ`---the function that added one to any
 number---had a fixed point.  How could there be an X such that X = X+1?
-Then
+That would imply that
 
     X = succ X = succ (succ X) = succ (succ (succ (X))) = succ (... (succ X)...)
 
@@ -58,7 +58,7 @@ successor.  Let's just check that `X = succ X`:
 
 You should see the close similarity with YY here.
 
-Q. So `Y` applied to `succ` returns infinity!
+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:
@@ -82,8 +82,10 @@ succ)(Y succ)`?  What would you expect infinity minus infinity to be?
 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:
+represents arithmetic infinity.  
+
+It's important to bear in mind the simplest term in question is not
+infinite:
 
      Y succ = (\f.(\x.f(xx))(\x.f(xx)))(\n s z. s (n s z))
 
@@ -122,12 +124,13 @@ endless reduction:
 
 The crucial step is the third from the last.  We have our choice of
 either evaluating the test `isZero 0 1 ...`, which evaluates to `1`,
+no matter what the ... contains;
 or we can evaluate the `Y` pump, `(\x.prefac(xx))(\x.prefac(xx))`, to
 produce another copy of `prefac`.  If we postpone evaluting the
 `isZero` test, we'll pump out copy after copy of `prefac`, and never
 realize that we've bottomed out in the recursion.  But if we adopt a
-leftmost/call by name/normal order evaluation strategy, we'll always
-start with the isZero predicate, and only produce a fresh copy of
+leftmost/call-by-name/normal-order evaluation strategy, we'll always
+start with the `isZero` predicate, and only produce a fresh copy of
 `prefac` if we are forced to. 
 
 Q.  You claimed that the Ackerman function couldn't be implemented
@@ -160,5 +163,5 @@ For instance,
 A 1 x is to A 0 x as addition is to the successor function;
 A 2 x is to A 1 x as multiplication is to addition;
 A 3 x is to A 2 x as exponentiation is to multiplication---
-so A 4 x is to A 3 x as super-exponentiation is to exponentiation...
+so A 4 x is to A 3 x as hyper-exponentiation is to exponentiation...