author Chris Barker Sat, 2 Oct 2010 19:30:20 +0000 (15:30 -0400) committer Chris Barker Sat, 2 Oct 2010 19:30:20 +0000 (15:30 -0400)
 week4.mdwn patch | blob | history

index 8d89a5a..edf9552 100644 (file)
@@ -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...