From: Chris
Date: Thu, 12 Feb 2015 15:39:57 +0000 (0500)
Subject: move computation discussion live
XGitUrl: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=ee6a2e3f2edbc040298165943d874423d866bbc6
move computation discussion live

diff git a/topics/_week4_fixed_point_combinator.mdwn b/topics/_week4_fixed_point_combinator.mdwn
index 28e310ed..17b7b1c3 100644
 a/topics/_week4_fixed_point_combinator.mdwn
+++ b/topics/_week4_fixed_point_combinator.mdwn
@@ 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
+search for "recursion", Google asks: "Did you mean: recursion?"
+
##What is the "rec" part of "letrec" doing?##
How could we compute the length of a list? Without worrying yet about what lambdacalculus implementation we're using for the list, the basic idea would be to define this recursively:
diff git a/topics/_week3_what_is_computation.mdwn b/topics/week3_what_is_computation.mdwn
similarity index 74%
rename from topics/_week3_what_is_computation.mdwn
rename to topics/week3_what_is_computation.mdwn
index 7575abcc..79fd3999 100644
 a/topics/_week3_what_is_computation.mdwn
+++ b/topics/week3_what_is_computation.mdwn
@@ 6,13 +6,26 @@ 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
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##
@@ 84,7 +97,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 +110,16 @@ 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.
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 +142,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 wellchosen reduction system
+will characterize our intuitive notion of evaluation in most cases, or
+in some useful class of nonpathological cases.
+
These are some of the deeper issues to keep in mind as we discuss the
ins and outs of reduction strategies.

