From: Chris Date: Thu, 12 Feb 2015 15:50:55 +0000 (-0500) Subject: added discussion of computation X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=31cebc8050836005ee17dd1d20ae81b2ab9afa3c;hp=ee79965dbd07b39cd3ab7d489ba87b8cc5e2b68b added discussion of computation --- diff --git a/topics/_week4_fixed_point_combinator.mdwn b/topics/_week4_fixed_point_combinator.mdwn index 253fd975..bc714f37 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 lambda-calculus 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 47748a16..32a4572d 100644 --- a/topics/_week3_what_is_computation.mdwn +++ b/topics/week3_what_is_computation.mdwn @@ -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 +<<<<<<< HEAD:topics/_week3_what_is_computation.mdwn 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. +<<<<<<< HEAD:topics/_week3_what_is_computation.mdwn 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. - -