X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week4_fixed_point_combinator.mdwn;h=bc714f374dd84d884accdff0c06c604180aa39a0;hp=17b7b1c368d8eb52c2cdf51715a27d31b3c010e0;hb=31cebc8050836005ee17dd1d20ae81b2ab9afa3c;hpb=ee6a2e3f2edbc040298165943d874423d866bbc6

diff --git a/topics/_week4_fixed_point_combinator.mdwn b/topics/_week4_fixed_point_combinator.mdwn
index 17b7b1c3..bc714f37 100644
--- a/topics/_week4_fixed_point_combinator.mdwn
+++ b/topics/_week4_fixed_point_combinator.mdwn
@@ -52,11 +52,11 @@ Answer: These work like the `let` expressions we've already seen, except that th
 
 In Scheme:
 
-	(letrec [(get_length 
+	(letrec [(get_length
 				(lambda (lst) (if (null? lst) 0 [+ 1 (get_length (cdr lst))] )) )]
 			(get_length (list 20 30)))
 	; this evaluates to 2
-	
+
 If you instead use an ordinary `let` (or `let*`), here's what would happen, in OCaml:
 
 	let get_length = fun lst ->
@@ -66,7 +66,7 @@ If you instead use an ordinary `let` (or `let*`), here's what would happen, in O
 
 Here's Scheme:
 
-	(let* [(get_length 
+	(let* [(get_length
 				(lambda (lst) (if (null? lst) 0 [+ 1 (get_length (cdr lst))] )) )]
 			(get_length (list 20 30)))
 	; fails with error "reference to undefined identifier: get_length"
@@ -116,9 +116,9 @@ So how could we do it? And how do OCaml and Scheme manage to do it, with their `
 
 2.	If you tried this in Scheme:
 
-		(define get_length 
+		(define get_length
 				(lambda (lst) (if (null? lst) 0 [+ 1 (get_length (cdr lst))] )) )
-		
+
 		(get_length (list 20 30))
 
 	You'd find that it works! This is because `define` in Scheme is really shorthand for `letrec`, not for plain `let` or `let*`. So we should regard this as cheating, too.
@@ -160,7 +160,7 @@ an implementation may not terminate doesn't mean that such a function
 isn't well-defined.  The point of interest here is that its definition
 requires recursion in the function definition.)
 
-Neither do the resources we've so far developed suffice to define the 
+Neither do the resources we've so far developed suffice to define the
 [[!wikipedia Ackermann function]]:
 
 	A(m,n) =
@@ -184,10 +184,10 @@ But functions like the Ackermann function require us to develop a more general t
 ###Fixed points###
 
 In general, we call a **fixed point** of a function f any value *x*
-such that f <em>x</em> is equivalent to *x*. For example, 
+such that f <em>x</em> is equivalent to *x*. For example,
 consider the squaring function `sqare` that maps natural numbers to their squares.
 `square 2 = 4`, so `2` is not a fixed point.  But `square 1 = 1`, so `1` is a
-fixed point of the squaring function.  
+fixed point of the squaring function.
 
 There are many beautiful theorems guaranteeing the existence of a
 fixed point for various classes of interesting functions.  For
@@ -210,7 +210,7 @@ In the lambda calculus, we say a fixed point of an expression `f` is any formula
 
 You should be able to immediately provide a fixed point of the
 identity combinator I.  In fact, you should be able to provide a whole
-bunch of distinct fixed points.  
+bunch of distinct fixed points.
 
 With a little thought, you should be able to provide a fixed point of
 the false combinator, KI.  Here's how to find it: recall that KI
@@ -247,7 +247,7 @@ length function.  Call that function `length`.  Then we have
 At this point, we have a definition of the length function, though
 it's not complete, since we don't know what value to use for the
 symbol `length`.  Technically, it has the status of an unbound
-variable.  
+variable.
 
 Imagine now binding the mysterious variable:
 
@@ -261,13 +261,13 @@ a function that accurately computes the length of a list---as long as
 the argument we supply is already the length function we are trying to
 define.  (Dehydrated water: to reconstitute, just add water!)
 
-But this is just another way of saying that we are looking for a fixed point.  
+But this is just another way of saying that we are looking for a fixed point.
 Assume that `h` has a fixed point, call it `LEN`.  To say that `LEN`
 is a fixed point means that
 
     h LEN <~~> LEN
 
-But this means that 
+But this means that
 
     (\list . if empty list then zero else add one (LEN (tail list))) <~~> LEN
 
@@ -275,7 +275,7 @@ So at this point, we are going to search for fixed point.
 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## 
+##Deriving Y, a fixed point combinator##
 
 How shall we begin?  Well, we need to find an argument to supply to
 `h`.  The argument has to be a function that computes the length of a
@@ -283,11 +283,11 @@ list.  The function `h` is *almost* a function that computes the
 length of a list.  Let's try applying `h` to itself.  It won't quite
 work, but examining the way in which it fails will lead to a solution.
 
-    h h <~~> \list . if empty list then zero else 1 + h (tail list) 
+    h h <~~> \list . if empty list then zero else 1 + h (tail list)
 
 There's a problem.  The diagnosis is that in the subexpression `h
 (tail list)`, we've applied `h` to a list, but `h` expects as its
-first argument the length function.  
+first argument the length function.
 
 So let's adjust h, calling the adjusted function H:
 
@@ -306,12 +306,12 @@ argument.  `H` itself fits the bill:
     H H <~~> (\h \list . if empty list then zero else 1 + ((h h) (tail list))) H
         <~~> \list . if empty list then zero else 1 + ((H H) (tail list))
         == \list . if empty list then zero else 1 + ((\list . if empty list then zero else 1 + ((H H) (tail list))) (tail list))
-        <~~> \list . if empty list then zero 
+        <~~> \list . if empty list then zero
                     else 1 + (if empty (tail list) then zero else 1 + ((H H) (tail (tail list))))
-   
+
 We're in business!
 
-How does the recursion work?  
+How does the recursion work?
 We've defined `H` in such a way that `H H` turns out to be the length function.
 In order to evaluate `H H`, we substitute `H` into the body of the
 lambda term.  Inside the lambda term, once the substitution has
@@ -353,7 +353,7 @@ That is, Yh is a fixed point for h.
 Works!
 
 
-##What is a fixed point for the successor function?## 
+##What is a fixed point for the successor function?##
 
 Well, you might think, only some of the formulas that we might give to the `successor` as arguments would really represent numbers. If we said something like:
 
@@ -457,9 +457,9 @@ returns itself (a copy of `sink`); if the argument is boolean false
     sink true true false ~~> I
     sink true true true false ~~> I
 
-So we make `sink = Y (\f b. b f I)`: 
+So we make `sink = Y (\f b. b f I)`:
 
-    1. sink false 
+    1. sink false
     2. Y (\fb.bfI) false
     3. (\f. (\h. f (h h)) (\h. f (h h))) (\fb.bfI) false
     4. (\h. [\fb.bfI] (h h)) (\h. [\fb.bfI] (h h)) false
@@ -476,7 +476,7 @@ argument, we can throw it away unreduced.
 
 Now we try the next most complex example:
 
-    1. sink true false 
+    1. sink true false
     2. Y (\fb.bfI) true false
     3. (\f. (\h. f (h h)) (\h. f (h h))) (\fb.bfI) true false
     4. (\h. [\fb.bfI] (h h)) (\h. [\fb.bfI] (h h)) true false
@@ -490,7 +490,7 @@ is again I.
 
 You should be able to see that `sink` will consume as many `true`s as
 we throw at it, then turn into the identity function after it
-encounters the first `false`. 
+encounters the first `false`.
 
 The key to the recursion is that, thanks to Y, the definition of
 `sink` contains within it the ability to fully regenerate itself as
@@ -542,7 +542,7 @@ true, then (1) is not true.
 Without pretending to give a serious analysis of the paradox, let's
 assume that sentences can have for their meaning boolean functions
 like the ones we have been working with here.  Then the sentence *John
-is John* might denote the function `\x y. x`, our `true`.  
+is John* might denote the function `\x y. x`, our `true`.
 
 Then (1) denotes a function from whatever the referent of *this
 sentence* is to a boolean.  So (1) denotes `\f. f true false`, where
@@ -585,7 +585,7 @@ context, (2) might denote
 
      Y C
      (\f. (\h. f (h h)) (\h. f (h h))) I
-     (\h. C (h h)) (\h. C (h h))) 
+     (\h. C (h h)) (\h. C (h h)))
      C ((\h. C (h h)) (\h. C (h h)))
      C (C ((\h. C (h h))(\h. C (h h))))
      C (C (C ((\h. C (h h))(\h. C (h h)))))
@@ -627,7 +627,7 @@ just this juncture?
 
 One obstacle to thinking this through is the fact that a sentence
 normally has only two truth values.  We might consider instead a noun
-phrase such as 
+phrase such as
 
 (3)  the entity that this noun phrase refers to
 
@@ -639,7 +639,7 @@ for any object.
 
 The chameleon nature of (3), by the way (a description that is equally
 good at describing any object), makes it particularly well suited as a
-gloss on pronouns such as *it*.  In the system of 
+gloss on pronouns such as *it*.  In the system of
 [Jacobson 1999](http://www.springerlink.com/content/j706674r4w217jj5/),
 pronouns denote (you guessed it!) identity functions...