author Chris Thu, 12 Feb 2015 15:50:55 +0000 (10:50 -0500) committer Chris Thu, 12 Feb 2015 15:50:55 +0000 (10:50 -0500)
 topics/_week4_fixed_point_combinator.mdwn patch | blob | history topics/week3_what_is_computation.mdwn [moved from topics/_week3_what_is_computation.mdwn with 74% similarity] patch | blob | history

index 253fd97..bc714f3 100644 (file)
@@ -1,5 +1,14 @@
[[!toc]]

+#Recursion: fixed points in the lambda calculus##
+
+Sometimes when you type in a web search, Google will suggest
+alternatives.  For instance, if you type in "Lingusitics", it will ask
+you "Did you mean Linguistics?".  But the engineers at Google have
+added some playfulness to the system.  For instance, if you search for
+"anagram", Google asks you "Did you mean: nag a ram?"  And if you
+
##What is the "rec" part of "letrec" doing?##

How could we compute the length of a list? Without worrying yet about what lambda-calculus implementation we're using for the list, the basic idea would be to define this recursively:
similarity index 74%
rename from topics/_week3_what_is_computation.mdwn
rename to topics/week3_what_is_computation.mdwn
index 47748a1..32a4572 100644 (file)
@@ -6,6 +6,7 @@ expression and replacing it with an equivalent simpler expression.
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
@@ -13,6 +14,28 @@ 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.
+>>>>>>> working:topics/week3_what_is_computation.mdwn

##Church arithmetic##

@@ -84,7 +107,7 @@ 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
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
@@ -97,16 +120,22 @@ that reduce to that term.
(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.
+>>>>>>> working:topics/week3_what_is_computation.mdwn

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
@@ -129,7 +158,9 @@ is no simplification at all.
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.
-
-