index 7575abc..47748a1 100644 (file)
@@ -9,10 +9,10 @@ This equation can be interpreted as expressing the thought that the
complex expression `3 + 4` evaluates to `7`.  The evaluation of the
expression computing a sum.  There is a clear sense in which the
expression `7` is simpler than the expression `3 + 4`: `7` is
complex expression `3 + 4` evaluates to `7`.  The evaluation of the
expression computing a sum.  There is a clear sense in which the
expression `7` is simpler than the expression `3 + 4`: `7` is
-syntactically simple, and `3 + 4` is syntactically complex.
+syntactically simple, and `3 + 4` is syntactically complex.

Now let's take this folk notion of computation, and put some pressure

Now let's take this folk notion of computation, and put some pressure
-on it.
+on it.

##Church arithmetic##

##Church arithmetic##

@@ -64,14 +64,14 @@ But now consider multiplication:
Is the final result simpler?  This time, the answer is not so straightfoward.
Compare the starting expression with the final expression:

Is the final result simpler?  This time, the answer is not so straightfoward.
Compare the starting expression with the final expression:

-        *           3             4
+        *           3             4
(\lrf.l(rf))(\fz.f(f(fz)))(\fz.f(f(f(fz))))
~~> 12
(\fz.f(f(f(f(f(f(f(f(f(f(f(fz))))))))))))

And if we choose different numbers, the result is even less clear:

(\lrf.l(rf))(\fz.f(f(fz)))(\fz.f(f(f(fz))))
~~> 12
(\fz.f(f(f(f(f(f(f(f(f(f(f(fz))))))))))))

And if we choose different numbers, the result is even less clear:

-        *           3             6
+        *           3             6
(\lrf.l(rf))(\fz.f(f(fz)))(\fz.f(f(f(f(f(fz))))))
~~> 18
(\fz.f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(fz))))))))))))))))))
(\lrf.l(rf))(\fz.f(f(fz)))(\fz.f(f(f(f(f(fz))))))
~~> 18
(\fz.f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(fz))))))))))))))))))
@@ -99,7 +99,7 @@ that reduce to that term.

In the arithmetic example, there is only one number that corresponds
to the sum of 3 and 4 (namely, 7).  But there are many sums that add

In the arithmetic example, there is only one number that corresponds
to the sum of 3 and 4 (namely, 7).  But there are many sums that add
-up to 7: 3+4, 4+3, 5+2, 2+5, 6+1, 1+6, etc.
+up to 7: 3+4, 4+3, 5+2, 2+5, 6+1, 1+6, etc.

So the unevaluated expression contains information that is missing
from the evaluated value: information about *how* that value was

So the unevaluated expression contains information that is missing
from the evaluated value: information about *how* that value was
@@ -124,7 +124,7 @@ pathological examples where the results do not align so well:
In this example, reduction returns the exact same lambda term.  There
is no simplification at all.

In this example, reduction returns the exact same lambda term.  There
is no simplification at all.

-    (\x.xxx)(\x.xxx) ~~> ((\x.xxxx)(\x.xxxx)(\x.xxxx))
+    (\x.xxx)(\x.xxx) ~~> ((\x.xxxx)(\x.xxxx)(\x.xxxx))

Even worse, in this case, the "reduced" form is longer and more
complex by any measure.

Even worse, in this case, the "reduced" form is longer and more
complex by any measure.