The folk notion of computation involves taking a complicated
expression and replacing it with an equivalent simpler expression.
- 3 + 4 == 7
+ 4 + 3 == 7
This equation can be interpreted as expressing the thought that the
-complex expression `3 + 4` evaluates to `7`. In this case, the
+complex expression `4 + 3` 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
+`4 + 3`: `7` is syntactically simple, and `4 + 3` 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`
+complex expression like `4 + 3` with a simpler 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`?
+`2^9`, or `512`? Likewise, in the realm of logic, why should we ever
+prefer `B` to the conjunction of `A` with <code>A ⊃ B</code>?
The question to ask here is whether our intuitions about what counts
as more evaluated always tracks simplicity of expression, or whether
In our system of computing with Church encodings, we have the
following representations:
- 3 := \f z . f (f (f z))
- 4 := \f z . f (f (f (f z)))
- 7 := \f z . f (f (f (f (f (f (f z))))))
+ 3 ≡ \f z. f (f (f z))
+ 4 ≡ \f z. f (f (f (f z)))
+ 7 ≡ \f z. f (f (f (f (f (f (f z))))))
-[By the way, those of you who did the extra credit problem on homework
-2, solving the reverse function with Oleg's holes---do you see the
-resemblance?]
+<!--
+By the way, those of you who solved the `reverse` function in homework 2 using the "holes" idea: do you see the resemblance?
+-->
-The addition of 3 and 4, then, clearly needs to just tack 4's string
-of f's onto the end of 3's string of f's. This suggests the following
-implementation of the arithmetic addition:
+The addition of `4` and `3`, then, clearly needs to just insert `3`'s string
+of `f`s in front of `4`'s string of `f`s. That guides our
+implementation of addition:
- + := \lrfz.lf(rfz)
+ add ≡ \l r. \f z. r f (l f z)
- + 3 4 == (\lrfz.lf(rfz)) 3 4
- ~~> \fz.3f(4fz)
- == \fz.(\fz.f(f(fz))) f (4fz)
- ~~> \fz.f(f(f(4fz)))
- == \fz.f(f(f((\fz.f(f(f(fz))) f z))))
- ~~> \fz.f(f(f(f(f(f(fz))))))
- == 7
+ add 4 3 ≡ (\l r. \f z. r f (l f z)) 4 3
+ ~~> \f z. 3 f (4 f z)
+ ≡ \f z. (\f z. f (f (f z))) f (4 f z)
+ ~~> \f z. f (f (f (4 f z)))
+ ≡ \f z. f (f (f ((\f z. f (f (f (f z))) f z))))
+ ~~> \f z. f (f (f (f (f (f (f z))))))
+ ≡ 7
-as desired. Is there still a sense in which the encoded version of `3
-+ 4` is simpler than the encoded version of `7`? Well, yes: once the
-numerals `3` and `4` have been replaced with their encodings, the
-encoding of `3 + 4` contains more symbols than the encoding of `7`.
+as desired. Is there still a sense in which the encoded version of `add 4 3`
+is simpler than the encoded version of `7`? Well, yes: once the
+numerals `4` and `3` have been replaced with their encodings, the
+encoding of `add 4 3` contains more symbols than the encoding of `7`.
But now consider multiplication:
- * := \lrf.l(rf)
- * 3 4 := (\lrf.l(rf)) 3 4
- ~~> (\rf.3(rf)) 4
- ~~> \f.3(4f)
- == \f.(\fz.f(f(fz)))(4f)
- ~~> \fz.(4f)((4f)((4f)z))
- == \fz.((\fz.f(f(f(fz))))f) (((\fz.f(f(f(fz))))f) (((\fz.f(f(f(fz))))f) z))
- ~~> \fz.((\z.f(f(f(fz)))) ((\z.f(f(f(fz)))) ((\z.f(f(f(fz))))z)))
- ~~> \fz.((\z.f(f(f(fz)))) ((\z.f(f(f(fz)))) (f(f(f(fz))))))
- ~~> \fz.((\z.f(f(f(fz)))) (f(f(f(f(f(f(f(fz)))))))))
- ~~> \fz.f(f(f(f(f(f(f(f(f(f(f(fz)))))))))))
- == 12
-
-Is the final result simpler? This time, the answer is not so straightfoward.
+ mul ≡ \l r. \f z. r (l f) z
+
+ mul 4 3 ≡ (\l r. \f z. r (l f) z) 4 3
+ ~~> \f z. 3 (4 f) z
+ ≡ \f z. (\f z. f (f (f z))) (4 f) z
+ ~~> \f z. (4 f) ((4 f) (4 f z))
+ ≡ \f z. ((\f z. f (f (f (f z)))) f) (((\f z. f (f (f (f z)))) f) ((\f z. f (f (f (f z)))) f z))
+ ~~> \f z. (\z. f (f (f (f z)))) ((\z. f (f (f (f z)))) (f (f (f (f z)))))
+ ~~> \f z. (\z. f (f (f (f z)))) (f (f (f (f (f (f (f (f z))))))))
+ ~~> \f z. f (f (f (f (f (f (f (f (f (f (f (f z)))))))))))
+ ≡ 12
+
+Is the final result simpler? This time, the answer is not so straightforward.
Compare the starting expression with the final expression:
- * 3 4
- (\lrf.l(rf))(\fz.f(f(fz)))(\fz.f(f(f(fz))))
+ mul 4 3
+ (\l r. \f z. r (l f) z) (\f z. f (f (f (f z)))) (\f z. f (f (f z))))
~~> 12
- (\fz.f(f(f(f(f(f(f(f(f(f(f(fz))))))))))))
+ (\f z. f (f (f (f (f (f (f (f (f (f (f (f z))))))))))))
And if we choose different numbers, the result is even less clear:
- * 3 6
- (\lrf.l(rf))(\fz.f(f(fz)))(\fz.f(f(f(f(f(fz))))))
+ mul 6 3
+ (\l r. \f z. r (l f) z) (\f z. f ( f (f (f (f (f z)))))) (\f z. f (f (f z))))
~~> 18
- (\fz.f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(fz))))))))))))))))))
+ (\f z. f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f z))))))))))))))))))
On the on hand, there are more symbols in the encoding of `18` than in
-the encoding of `* 3 6`. On the other hand, there is more complexity
-(speaking pre-theoretically) in the encoding of `* 3 6`, since the
-encoding of `18` is just a uniform sequence of nested `f`'s.
+the encoding of `mul 6 3`. On the other hand, there is more complexity
+(speaking pre-theoretically) in the encoding of `mul 6 3`, since the
+encoding of `18` is just a uniform sequence of nested `f`s.
This example shows that computation can't be just simplicity as
measured by the number of symbols in the representation. There is
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
+reduction rules of the lambda calculus define an non-symmetric relation
over terms: for any given redex, there is a unique reduced term (up to
-alphabetic variance). But for any given term, there are many redexes
+alphabetic variance). But for any given term, there will be many redexes
that reduce to that term.
- ((\x.xx)y) ~~> yy
- ((\xx)yy) ~~> yy
- (y((\xx)y)) ~~> yy
+ ((\x. x x) y) ~~> y y
+ ((\x x) y y) ~~> y y
+ (y ((\x x) y)) ~~> y y
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.
+corresponds to the sum of `4` and `3` (namely, `7`). But there are many
+ways to add numbers to get `7`: `4+3`, `3+4`, `5+2`, `2+5`, `6+1`, `1+6`, `7+0` and `0+7`.
+And that's only looking at sums.
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 reduces to the other,
- the more evaluated one is the one that contains less information.
+> 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
of information using, say, [[!wikipedia Komolgorov complexity]].
up well with our intuitive sense of simplification, there are
pathological examples where the results do not align so well:
- (\x.xx)(\x.xx) ~~> (\x.xx)(\x.xx) ~~> (\x.xx)(\x.xx)
+ (\x. x x) (\x. x x) ~~> (\x. x x) (\x. x x) ~~> (\x. x x) (\x. x x) ~~> ...
In this example, reduction returns the exact same lambda term. There
-is no simplification at all.
+is no simplification at all. (As we mentioned in class, the term `(\x. x x)` is often referred to in these discussions as (little) <b>ω</b> or "omega", or sometimes **M**; and its self-application <code>ω ω</code>, displayed above, is called (big) <b>Ω</b> or "Omega".)
+
+Even worse, consider this term:
- (\x.xxx)(\x.xxx) ~~> ((\x.xxxx)(\x.xxxx)(\x.xxxx))
+ (\x. x x x) (\x. x x x) ~~> (\x. x x x) (\x. x x x) (\x. x x x) ~~> ...
-Even worse, in this case, the "reduced" form is longer and more
-complex by any measure.
+Here, the "reduced" form is longer and more
+complex by any reasonable 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