3 + 4 == 7
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
-syntactically simple, and `3 + 4` is syntactically complex.
-
-Now let's take this folk notion of computation, and put some pressure
-on it.
+complex expression `3 + 4` evaluates to `7`. In this case, the
+evaluation of the expression involves 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.
+
+It's worth pausing a moment and wondering why we feel that replacing a
+complex expression like `3 + 4` with a simplex expression like `7`
+feels like we've accomplished something. If they really are
+equivalent, why shouldn't we consider them to be equally valuable, or
+even to prefer the longer expression? For instance, should we prefer
+2^9, or 512? Likewise, in the realm of logic, why shold we ever
+prefer `B` to the conjunction of `A` with `A --> B`?
+
+The question to ask here is whether our intuitions about what counts
+as more evaluated always tracks simplicity of expression, or whether
+it tracks what is more useful to us in a given larger situation.
+
+But even deciding which expression ought to count as simpler is not
+always so clear.
##Church arithmetic##
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:
- * 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))))))))))))))))))
This example shows that computation can't be just simplicity as
measured by the number of symbols in the representation. There is
still some sense in which the evaluated expression is simpler, but the
-right way to characterize simpler is elusive.
+right way to characterize "simpler" is elusive.
One possibility is to define simpler in terms of irreversability. The
reduction rules of the lambda calculus define an asymmetric relation
(y((\xx)y)) ~~> yy
etc.
-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.
+Likewise, 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.
So the unevaluated expression contains information that is missing
from the evaluated value: information about *how* that value was
arrived at. So this suggests the following way of thinking about what
counts as evaluated:
- Given two expressions such that one reduced to the other,
+ Given two expressions such that one reduces to the other,
the more evaluated one is the one that contains less information.
This definition is problematic, though, if we try to define the amount
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.
+We may have to settle for the idea that a well-chosen reduction system
+will characterize our intuitive notion of evaluation in most cases, or
+in some useful class of non-pathological cases.
+
These are some of the deeper issues to keep in mind as we discuss the
ins and outs of reduction strategies.
-
-