X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek4_fixed_point_combinators.mdwn;h=41a5273751c7fc6ca4fcf5c5e01d8f23f176f6e8;hp=a16d7c5962d74d236cadef5ff3344037ab58ffb0;hb=7d5f235b46a5fb4ac8d6aaeffa65d0244522bdd0;hpb=12b94057358619fd5ae7a48f685fedba8ce4d082 diff --git a/topics/week4_fixed_point_combinators.mdwn b/topics/week4_fixed_point_combinators.mdwn index a16d7c59..41a52737 100644 --- a/topics/week4_fixed_point_combinators.mdwn +++ b/topics/week4_fixed_point_combinators.mdwn @@ -281,7 +281,7 @@ saying that we are looking for a fixed point for `h`: h LENGTH <~~> LENGTH -Replacing `h` with its definition, we have +Replacing `h` with its definition, we have: (\xs. (empty? xs) 0 (succ (LENGTH (tail xs)))) <~~> LENGTH @@ -289,10 +289,21 @@ If we can find a value for `LENGTH` that satisfies this constraint, we'll have a function we can use to compute the length of an arbitrary list. All we have to do is find a fixed point for `h`. -The strategy we will present will turn out to be a general way of +Let's reinforce this. The left-hand side has the form: + + (\body. Î¦[...body...]) LENGTH + +which beta-reduces to: + + Î¦[...LENGTH...] + +where that whole formula is convertible with the term `LENGTH` itself. In other words, the term `Î¦[...LENGTH...]` contains (a term that convertible with) itself --- despite being only finitely long. (If it had to contain a term *syntactically identical to* itself, this could not be achieved.) + +The key to achieving all this is finding a fixed point for `h`. The strategy we will present will turn out to be a general way of finding a fixed point for any lambda term. + ## Deriving Y, a fixed point combinator ## How shall we begin? Well, we need to find an argument to supply to @@ -303,7 +314,7 @@ work, but examining the way in which it fails will lead to a solution. h h <~~> \xs. (empty? xs) 0 (succ (h (tail xs))) -The problem is that in the subexpression `h (tail list)`, we've +The problem is that in the subexpression `h (tail xs)`, we've applied `h` to a list, but `h` expects as its first argument the length function. @@ -318,7 +329,7 @@ to discuss generalizations of this strategy.) Shifting to `H` is the key creative step. Instead of applying `u` to a list, as happened when we self-applied `h`, `H` applies its argument `u` first to *itself*: `u u`. -After `u` gets an argument, the *result* is ready to apply to a list, so we've solved the problem noted above with `h (tail list)`. +After `u` gets an argument, the *result* is ready to apply to a list, so we've solved the problem noted above with `h (tail xs)`. We're not done yet, of course; we don't yet know what argument `u` to give to `H` that will behave in the desired way. @@ -562,7 +573,7 @@ returns itself (a copy of `sink`); if the argument is boolean false sink true true false <~~> I sink true true true false <~~> I -Evidently, then, `sink true <~~> sink`. So we want `sink` to be the fixed point +To get this behavior, we want `sink` to be the fixed point of `\sink. \b. b sink I`. That is, `sink â¡ Y (\sb.bsI)`: 1. sink false