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=3303e8c15d71c68c58c6eec5d6dc7c03e3d6d7bd;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 x is equivalent to *x*. For example,
+such that f x 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...