tweak combinatory
[lambda.git] / topics / _week4_fixed_point_combinator.mdwn
1 [[!toc]]
2
3 #Recursion: fixed points in the lambda calculus##
4
5 Sometimes when you type in a web search, Google will suggest
6 alternatives.  For instance, if you type in "Lingusitics", it will ask
7 you "Did you mean Linguistics?".  But the engineers at Google have
8 added some playfulness to the system.  For instance, if you search for
9 "anagram", Google asks you "Did you mean: nag a ram?"  And if you
10 search for "recursion", Google asks: "Did you mean: recursion?"
11
12 ##What is the "rec" part of "letrec" doing?##
13
14 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:
15
16 >       the empty list has length 0
17
18 >       any non-empty list has length 1 + (the length of its tail)
19
20 In OCaml, you'd define that like this:
21
22         let rec get_length = fun lst ->
23                 if lst == [] then 0 else 1 + get_length (tail lst)
24         in ... (* here you go on to use the function "get_length" *)
25
26 In Scheme you'd define it like this:
27
28         (letrec [(get_length
29                                 (lambda (lst) (if (null? lst) 0 [+ 1 (get_length (cdr lst))] )) )]
30                 ... ; here you go on to use the function "get_length"
31         )
32
33 Some comments on this:
34
35 1. `null?` is Scheme's way of saying `isempty`. That is, `(null? lst)` returns true (which Scheme writes as `#t`) iff `lst` is the empty list (which Scheme writes as `'()` or `(list)`).
36
37 2. `cdr` is function that gets the tail of a Scheme list. (By definition, it's the function for getting the second member of an ordered pair. It just turns out to return the tail of a list because of the particular way Scheme implements lists.)
38
39 3.      I use `get_length` instead of the convention we've been following so far of hyphenated names, as in `make-list`, because we're discussing OCaml code here, too, and OCaml doesn't permit the hyphenated variable names. OCaml requires variables to always start with a lower-case letter (or `_`), and then continue with only letters, numbers, `_` or `'`. Most other programming languages are similar. Scheme is very relaxed, and permits you to use `-`, `?`, `/`, and all sorts of other crazy characters in your variable names.
40
41 4.      I alternate between `[ ]`s and `( )`s in the Scheme code just to make it more readable. These have no syntactic difference.
42
43
44 The main question for us to dwell on here is: What are the `let rec` in the OCaml code and the `letrec` in the Scheme code?
45
46 Answer: These work like the `let` expressions we've already seen, except that they let you use the variable `get_length` *inside* the body of the function being bound to it---with the understanding that it will there refer to the same function that you're then in the process of binding to `get_length`. So our recursively-defined function works the way we'd expect it to. In OCaml:
47
48         let rec get_length = fun lst ->
49                 if lst == [] then 0 else 1 + get_length (tail lst)
50         in get_length [20; 30]
51         (* this evaluates to 2 *)
52
53 In Scheme:
54
55         (letrec [(get_length
56                                 (lambda (lst) (if (null? lst) 0 [+ 1 (get_length (cdr lst))] )) )]
57                         (get_length (list 20 30)))
58         ; this evaluates to 2
59
60 If you instead use an ordinary `let` (or `let*`), here's what would happen, in OCaml:
61
62         let get_length = fun lst ->
63                 if lst == [] then 0 else 1 + get_length (tail lst)
64         in get_length [20; 30]
65         (* fails with error "Unbound value length" *)
66
67 Here's Scheme:
68
69         (let* [(get_length
70                                 (lambda (lst) (if (null? lst) 0 [+ 1 (get_length (cdr lst))] )) )]
71                         (get_length (list 20 30)))
72         ; fails with error "reference to undefined identifier: get_length"
73
74 Why? Because we said that constructions of this form:
75
76         let get_length = A
77                 in B
78
79 really were just another way of saying:
80
81         (\get_length. B) A
82
83 and so the occurrences of `get_length` in A *aren't bound by the `\get_length` that wraps B*. Those occurrences are free.
84
85 We can verify this by wrapping the whole expression in a more outer binding of `get_length` to some other function, say the constant function from any list to the integer 99:
86
87         let get_length = fun lst -> 99
88         in let get_length = fun lst ->
89                         if lst == [] then 0 else 1 + get_length (tail lst)
90         in get_length [20; 30]
91         (* evaluates to 1 + 99 *)
92
93 Here the use of `get_length` in `1 + get_length (tail lst)` can clearly be seen to be bound by the outermost `let`.
94
95 And indeed, if you tried to define `get_length` in the lambda calculus, how would you do it?
96
97         \lst. (isempty lst) zero (add one (get_length (extract-tail lst)))
98
99 We've defined all of `isempty`, `zero`, `add`, `one`, and `extract-tail` in earlier discussion. But what about `get_length`? That's not yet defined! In fact, that's the very formula we're trying here to specify.
100
101 What we really want to do is something like this:
102
103         \lst. (isempty lst) zero (add one (... (extract-tail lst)))
104
105 where this very same formula occupies the `...` position:
106
107         \lst. (isempty lst) zero (add one (
108                 \lst. (isempty lst) zero (add one (... (extract-tail lst)))
109                         (extract-tail lst)))
110
111 but as you can see, we'd still have to plug the formula back into itself again, and again, and again... No dice.
112
113 So how could we do it? And how do OCaml and Scheme manage to do it, with their `let rec` and `letrec`?
114
115 1.      OCaml and Scheme do it using a trick. Well, not a trick. Actually an impressive, conceptually deep technique, which we haven't yet developed. Since we want to build up all the techniques we're using by hand, then, we shouldn't permit ourselves to rely on `let rec` or `letrec` until we thoroughly understand what's going on under the hood.
116
117 2.      If you tried this in Scheme:
118
119                 (define get_length
120                                 (lambda (lst) (if (null? lst) 0 [+ 1 (get_length (cdr lst))] )) )
121
122                 (get_length (list 20 30))
123
124         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.
125
126 3.      In fact, it *is* possible to define the `get_length` function in the lambda calculus despite these obstacles. This depends on using the "version 3" implementation of lists, and exploiting its internal structure: that it takes a function and a base value and returns the result of folding that function over the list, with that base value. So we could use this as a definition of `get_length`:
127
128                 \lst. lst (\x sofar. successor sofar) zero
129
130         What's happening here? We start with the value zero, then we apply the function `\x sofar. successor sofar` to the two arguments <code>x<sub>n</sub></code> and `zero`, where <code>x<sub>n</sub></code> is the last element of the list. This gives us `successor zero`, or `one`. That's the value we've accumuluted "so far." Then we go apply the function `\x sofar. successor sofar` to the two arguments <code>x<sub>n-1</sub></code> and the value `one` that we've accumulated "so far." This gives us `two`. We continue until we get to the start of the list. The value we've then built up "so far" will be the length of the list.
131
132 We can use similar techniques to define many recursive operations on
133 lists and numbers. The reason we can do this is that our "version 3,"
134 fold-based implementation of lists, and Church's implementations of
135 numbers, have a internal structure that *mirrors* the common recursive
136 operations we'd use lists and numbers for.  In a sense, the recursive
137 structure of the `get_length` operation is built into the data
138 structure we are using to represent the list.  The non-recursive
139 version of get_length exploits this embedding of the recursion into
140 the data type.
141
142 This is one of the themes of the course: using data structures to
143 encode the state of some recursive operation.  See discussions of the
144 [[zipper]] technique, and [[defunctionalization]].
145
146 As we said before, it does take some ingenuity to define functions like `extract-tail` or `predecessor` for these implementations. However it can be done. (And it's not *that* difficult.) Given those functions, we can go on to define other functions like numeric equality, subtraction, and so on, just by exploiting the structure already present in our implementations of lists and numbers.
147
148 With sufficient ingenuity, a great many functions can be defined in the same way. For example, the factorial function is straightforward. The function which returns the nth term in the Fibonacci series is a bit more difficult, but also achievable.
149
150 ##Some functions require full-fledged recursive definitions##
151
152 However, some computable functions are just not definable in this
153 way. We can't, for example, define a function that tells us, for
154 whatever function `f` we supply it, what is the smallest integer `x`
155 where `f x` is `true`.  (You may be thinking: but that
156 smallest-integer function is not a proper algorithm, since it is not
157 guaranteed to halt in any finite amount of time for every argument.
158 This is the famous [[!wikipedia Halting problem]].  But the fact that
159 an implementation may not terminate doesn't mean that such a function
160 isn't well-defined.  The point of interest here is that its definition
161 requires recursion in the function definition.)
162
163 Neither do the resources we've so far developed suffice to define the
164 [[!wikipedia Ackermann function]]:
165
166         A(m,n) =
167                 | when m == 0 -> n + 1
168                 | else when n == 0 -> A(m-1,1)
169                 | else -> A(m-1, A(m,n-1))
170
171         A(0,y) = y+1
172         A(1,y) = 2+(y+3) - 3
173         A(2,y) = 2(y+3) - 3
174         A(3,y) = 2^(y+3) - 3
175         A(4,y) = 2^(2^(2^...2)) [where there are y+3 2s] - 3
176         ...
177
178 Many simpler functions always *could* be defined using the resources we've so far developed, although those definitions won't always be very efficient or easily intelligible.
179
180 But functions like the Ackermann function require us to develop a more general technique for doing recursion---and having developed it, it will often be easier to use it even in the cases where, in principle, we didn't have to.
181
182 ##Using fixed-point combinators to define recursive functions##
183
184 ###Fixed points###
185
186 In general, we call a **fixed point** of a function f any value *x*
187 such that f <em>x</em> is equivalent to *x*. For example,
188 consider the squaring function `sqare` that maps natural numbers to their squares.
189 `square 2 = 4`, so `2` is not a fixed point.  But `square 1 = 1`, so `1` is a
190 fixed point of the squaring function.
191
192 There are many beautiful theorems guaranteeing the existence of a
193 fixed point for various classes of interesting functions.  For
194 instance, imainge that you are looking at a map of Manhattan, and you
195 are standing somewhere in Manhattan.  The the [[!wikipedia Brouwer
196 fixed point]] guarantees that there is a spot on the map that is
197 directly above the corresponding spot in Manhattan.  It's the spot
198 where the blue you-are-here dot should be.
199
200 Whether a function has a fixed point depends on the set of arguments
201 it is defined for.  For instance, consider the successor function `succ`
202 that maps each natural number to its successor.  If we limit our
203 attention to the natural numbers, then this function has no fixed
204 point.  (See the discussion below concerning a way of understanding
205 the successor function on which it does have a fixed point.)
206
207 In the lambda calculus, we say a fixed point of an expression `f` is any formula `X` such that:
208
209         X <~~> f X
210
211 You should be able to immediately provide a fixed point of the
212 identity combinator I.  In fact, you should be able to provide a whole
213 bunch of distinct fixed points.
214
215 With a little thought, you should be able to provide a fixed point of
216 the false combinator, KI.  Here's how to find it: recall that KI
217 throws away its first argument, and always returns I.  Therefore, if
218 we give it I as an argument, it will throw away the argument, and
219 return I.  So KII ~~> I, which is all it takes for I to qualify as a
220 fixed point of KI.
221
222 What about K?  Does it have a fixed point?  You might not think so,
223 after trying on paper for a while.
224
225 However, it's a theorem of the lambda calculus that every formula has
226 a fixed point. In fact, it will have infinitely many, non-equivalent
227 fixed points. And we don't just know that they exist: for any given
228 formula, we can explicit define many of them.
229
230 Yes, even the formula that you're using the define the successor
231 function will have a fixed point. Isn't that weird? Think about how it
232 might be true.  We'll return to this point below.
233
234 ###How fixed points help definie recursive functions###
235
236 Recall our initial, abortive attempt above to define the `get_length` function in the lambda calculus. We said "What we really want to do is something like this:
237
238         \list. if empty list then zero else add one (... (tail lst))
239
240 where this very same formula occupies the `...` position."
241
242 Imagine replacing the `...` with some function that computes the
243 length function.  Call that function `length`.  Then we have
244
245         \list. if empty list then zero else add one (length (tail lst))
246
247 At this point, we have a definition of the length function, though
248 it's not complete, since we don't know what value to use for the
249 symbol `length`.  Technically, it has the status of an unbound
250 variable.
251
252 Imagine now binding the mysterious variable:
253
254         h := \length \list . if empty list then zero else add one (length (tail list))
255
256 Now we have no unbound variables, and we have complete non-recursive
257 definitions of each of the other symbols.
258
259 Let's call this function `h`.  Then `h` takes an argument, and returns
260 a function that accurately computes the length of a list---as long as
261 the argument we supply is already the length function we are trying to
262 define.  (Dehydrated water: to reconstitute, just add water!)
263
264 But this is just another way of saying that we are looking for a fixed point.
265 Assume that `h` has a fixed point, call it `LEN`.  To say that `LEN`
266 is a fixed point means that
267
268     h LEN <~~> LEN
269
270 But this means that
271
272     (\list . if empty list then zero else add one (LEN (tail list))) <~~> LEN
273
274 So at this point, we are going to search for fixed point.
275 The strategy we will present will turn out to be a general way of
276 finding a fixed point for any lambda term.
277
278 ##Deriving Y, a fixed point combinator##
279
280 How shall we begin?  Well, we need to find an argument to supply to
281 `h`.  The argument has to be a function that computes the length of a
282 list.  The function `h` is *almost* a function that computes the
283 length of a list.  Let's try applying `h` to itself.  It won't quite
284 work, but examining the way in which it fails will lead to a solution.
285
286     h h <~~> \list . if empty list then zero else 1 + h (tail list)
287
288 There's a problem.  The diagnosis is that in the subexpression `h
289 (tail list)`, we've applied `h` to a list, but `h` expects as its
290 first argument the length function.
291
292 So let's adjust h, calling the adjusted function H:
293
294     H = \h \list . if empty list then zero else one plus ((h h) (tail list))
295
296 This is the key creative step.  Since `h` is expecting a
297 length-computing function as its first argument, the adjustment
298 tries supplying the closest candidate avaiable, namely, `h` itself.
299
300 We now reason about `H`.  What exactly is H expecting as its first
301 argument?  Based on the excerpt `(h h) (tail l)`, it appears that `H`'s
302 argument, `h`, should be a function that is ready to take itself as an
303 argument, and that returns a function that takes a list as an
304 argument.  `H` itself fits the bill:
305
306     H H <~~> (\h \list . if empty list then zero else 1 + ((h h) (tail list))) H
307         <~~> \list . if empty list then zero else 1 + ((H H) (tail list))
308         == \list . if empty list then zero else 1 + ((\list . if empty list then zero else 1 + ((H H) (tail list))) (tail list))
309         <~~> \list . if empty list then zero
310                     else 1 + (if empty (tail list) then zero else 1 + ((H H) (tail (tail list))))
311
312 We're in business!
313
314 How does the recursion work?
315 We've defined `H` in such a way that `H H` turns out to be the length function.
316 In order to evaluate `H H`, we substitute `H` into the body of the
317 lambda term.  Inside the lambda term, once the substitution has
318 occurred, we are once again faced with evaluating `H H`.  And so on.
319
320 We've got the infinite regress we desired, defined in terms of a
321 finite lambda term with no undefined symbols.
322
323 Since `H H` turns out to be the length function, we can think of `H`
324 by itself as half of the length function (which is why we called it
325 `H`, of course).  Given the implementation of addition as function
326 application for Church numerals, this (H H) is quite literally H + H.
327 Can you think up a recursion strategy that involves "dividing" the
328 recursive function into equal thirds `T`, such that the length
329 function <~~> T T T?
330
331 We've starting with a particular recursive definition, and arrived at
332 a fixed point for that definition.
333 What's the general recipe?
334
335 1.   Start with any recursive definition `h` that takes itself as an arg: `h := \fn ... fn ...`
336 2.   Next, define `H := \f . h (f f)` 
337 3.   Then compute `H H = ((\f . h (f f)) (\f . h (f f)))`
338 4.   That's the fixed point, the recursive function we're trying to define
339
340 So here is a general method for taking an arbitrary h-style recursive function
341 and returning a fixed point for that function:
342
343      Y := \h. ((\f.h(ff))(\f.h(ff)))
344
345 Test:
346
347     Yh == ((\f.h(ff))(\f.h(ff)))
348        <~~> h((\f.h(ff))(\f.h(ff)))
349        == h(Yh)
350
351 That is, Yh is a fixed point for h.
352
353 Works!
354
355
356 ##What is a fixed point for the successor function?##
357
358 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:
359
360         successor make-pair
361
362 who knows what we'd get back? Perhaps there's some non-number-representing formula such that when we feed it to `successor` as an argument, we get the same formula back.
363
364 Yes! That's exactly right. And which formula this is will depend on the particular way you've implemented the successor function.
365
366 Moreover, the recipes that enable us to name fixed points for any
367 given formula aren't *guaranteed* to give us *terminating* fixed
368 points. They might give us formulas X such that neither `X` nor `f X`
369 have normal forms. (Indeed, what they give us for the square function
370 isn't any of the Church numerals, but is rather an expression with no
371 normal form.) However, if we take care we can ensure that we *do* get
372 terminating fixed points. And this gives us a principled, fully
373 general strategy for doing recursion. It lets us define even functions
374 like the Ackermann function, which were until now out of our reach. It
375 would also let us define arithmetic and list functions on the "version
376 1" and "version 2" implementations, where it wasn't always clear how
377 to force the computation to "keep going."
378
379 OK, so how do we make use of this?
380
381 Many fixed-point combinators have been discovered. (And some
382 fixed-point combinators give us models for building infinitely many
383 more, non-equivalent fixed-point combinators.)
384
385 Two of the simplest:
386
387 <pre><code>&Theta;&prime; &equiv; (\u f. f (\n. u u f n)) (\u f. f (\n. u u f n))
388 Y&prime; &equiv; \f. (\u. f (\n. u u n)) (\u. f (\n. u u n))</code></pre>
389
390 <code>&Theta;&prime;</code> has the advantage that <code>f (&Theta;&prime; f)</code> really *reduces to* <code>&Theta;&prime; f</code>. Whereas <code>f (Y&prime; f)</code> is only *convertible with* <code>Y&prime; f</code>; that is, there's a common formula they both reduce to. For most purposes, though, either will do.
391
392 You may notice that both of these formulas have eta-redexes inside them: why can't we simplify the two `\n. u u f n` inside <code>&Theta;&prime;</code> to just `u u f`? And similarly for <code>Y&prime;</code>?
393
394 Indeed you can, getting the simpler:
395
396 <pre><code>&Theta; &equiv; (\u f. f (u u f)) (\u f. f (u u f))
397 Y &equiv; \f. (\u. f (u u)) (\u. f (u u))</code></pre>
398
399 I stated the more complex formulas for the following reason: in a language whose evaluation order is *call-by-value*, the evaluation of <code>&Theta; (\self. BODY)</code> and `Y (\self. BODY)` will in general not terminate. But evaluation of the eta-unreduced primed versions will.
400
401 Of course, if you define your `\self. BODY` stupidly, your formula will never terminate. For example, it doesn't matter what fixed point combinator you use for <code>&Psi;</code> in:
402
403 <pre><code>&Psi; (\self. \n. self n)</code></pre>
404
405 When you try to evaluate the application of that to some argument `M`, it's going to try to give you back:
406
407         (\n. self n) M
408
409 where `self` is equivalent to the very formula `\n. self n` that contains it. So the evaluation will proceed:
410
411         (\n. self n) M ~~>
412         self M ~~>
413         (\n. self n) M ~~>
414         self M ~~>
415         ...
416
417 You've written an infinite loop!
418
419 However, when we evaluate the application of our:
420
421 <pre><code>&Psi; (\self (\lst. (isempty lst) zero (add one (self (extract-tail lst))) ))</code></pre>
422
423 to some list `L`, we're not going to go into an infinite evaluation loop of that sort. At each cycle, we're going to be evaluating the application of:
424
425         \lst. (isempty lst) zero (add one (self (extract-tail lst)))
426
427 to *the tail* of the list we were evaluating its application to at the previous stage. Assuming our lists are finite (and the implementations we're using don't permit otherwise), at some point one will get a list whose tail is empty, and then the evaluation of that formula to that tail will return `zero`. So the recursion eventually bottoms out in a base value.
428
429 ##Fixed-point Combinators Are a Bit Intoxicating##
430
431 ![tatoo](/y-combinator-fixed.jpg)
432
433 There's a tendency for people to say "Y-combinator" to refer to fixed-point combinators generally. We'll probably fall into that usage ourselves. Speaking correctly, though, the Y-combinator is only one of many fixed-point combinators.
434
435 I used <code>&Psi;</code> above to stand in for an arbitrary fixed-point combinator. I don't know of any broad conventions for this. But this seems a useful one.
436
437 As we said, there are many other fixed-point combinators as well. For example, Jan Willem Klop pointed out that if we define `L` to be:
438
439         \a b c d e f g h i j k l m n o p q s t u v w x y z r. (r (t h i s i s a f i x e d p o i n t c o m b i n a t o r))
440
441 then this is a fixed-point combinator:
442
443         L L L L L L L L L L L L L L L L L L L L L L L L L L
444
445
446 ##Watching Y in action##
447
448 For those of you who like to watch ultra slow-mo movies of bullets
449 piercing apples, here's a stepwise computation of the application of a
450 recursive function.  We'll use a function `sink`, which takes one
451 argument.  If the argument is boolean true (i.e., `\x y.x`), it
452 returns itself (a copy of `sink`); if the argument is boolean false
453 (`\x y. y`), it returns `I`.  That is, we want the following behavior:
454
455     sink false ~~> I
456     sink true false ~~> I
457     sink true true false ~~> I
458     sink true true true false ~~> I
459
460 So we make `sink = Y (\f b. b f I)`:
461
462     1. sink false
463     2. Y (\fb.bfI) false
464     3. (\f. (\h. f (h h)) (\h. f (h h))) (\fb.bfI) false
465     4. (\h. [\fb.bfI] (h h)) (\h. [\fb.bfI] (h h)) false
466     5. [\fb.bfI] ((\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))) false
467     6. (\b.b[(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))]I)  false
468     7. false [(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))] I
469              --------------------------------------------
470     8. I
471
472 So far so good.  The crucial thing to note is that as long as we
473 always reduce the outermost redex first, we never have to get around
474 to computing the underlined redex: because `false` ignores its first
475 argument, we can throw it away unreduced.
476
477 Now we try the next most complex example:
478
479     1. sink true false
480     2. Y (\fb.bfI) true false
481     3. (\f. (\h. f (h h)) (\h. f (h h))) (\fb.bfI) true false
482     4. (\h. [\fb.bfI] (h h)) (\h. [\fb.bfI] (h h)) true false
483     5. [\fb.bfI] ((\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))) true false
484     6. (\b.b[(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))]I)  true false
485     7. true [(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))] I false
486     8. [(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))] false
487
488 We've now arrived at line (4) of the first computation, so the result
489 is again I.
490
491 You should be able to see that `sink` will consume as many `true`s as
492 we throw at it, then turn into the identity function after it
493 encounters the first `false`.
494
495 The key to the recursion is that, thanks to Y, the definition of
496 `sink` contains within it the ability to fully regenerate itself as
497 many times as is necessary.  The key to *ending* the recursion is that
498 the behavior of `sink` is sensitive to the nature of the input: if the
499 input is the magic function `false`, the self-regeneration machinery
500 will be discarded, and the recursion will stop.
501
502 That's about as simple as recursion gets.
503
504 ##Application to the truth teller/liar paradoxes##
505
506 ###Base cases, and their lack###
507
508 As any functional programmer quickly learns, writing a recursive
509 function divides into two tasks: figuring out how to handle the
510 recursive case, and remembering to insert a base case.  The
511 interesting and enjoyable part is figuring out the recursive pattern,
512 but the base case cannot be ignored, since leaving out the base case
513 creates a program that runs forever.  For instance, consider computing
514 a factorial: `n!` is `n * (n-1) * (n-2) * ... * 1`.  The recursive
515 case says that the factorial of a number `n` is `n` times the
516 factorial of `n-1`.  But if we leave out the base case, we get
517
518     3! = 3 * 2! = 3 * 2 * 1! = 3 * 2 * 1 * 0! = 3 * 2 * 1 * 0 * -1! ...
519
520 That's why it's crucial to declare that 0! = 1, in which case the
521 recursive rule does not apply.  In our terms,
522
523     fac = Y (\fac n. iszero n 1 (fac (predecessor n)))
524
525 If `n` is 0, `fac` reduces to 1, without computing the recursive case.
526
527 Curry originally called `Y` the paradoxical combinator, and discussed
528 it in connection with certain well-known paradoxes from the philosophy
529 literature.  The truth teller paradox has the flavor of a recursive
530 function without a base case: the truth-teller paradox (and related
531 paradoxes).
532
533 (1)    This sentence is true.
534
535 If we assume that the complex demonstrative "this sentence" can refer
536 to (1), then the proposition expressed by (1) will be true just in
537 case the thing referred to by *this sentence* is true.  Thus (1) will
538 be true just in case (1) is true, and (1) is true just in case (1) is
539 true, and so on.  If (1) is true, then (1) is true; but if (1) is not
540 true, then (1) is not true.
541
542 Without pretending to give a serious analysis of the paradox, let's
543 assume that sentences can have for their meaning boolean functions
544 like the ones we have been working with here.  Then the sentence *John
545 is John* might denote the function `\x y. x`, our `true`.
546
547 Then (1) denotes a function from whatever the referent of *this
548 sentence* is to a boolean.  So (1) denotes `\f. f true false`, where
549 the argument `f` is the referent of *this sentence*.  Of course, if
550 `f` is a boolean, `f true false <~~> f`, so for our purposes, we can
551 assume that (1) denotes the identity function `I`.
552
553 If we use (1) in a context in which *this sentence* refers to the
554 sentence in which the demonstrative occurs, then we must find a
555 meaning `m` such that `I m = I`.  But since in this context `m` is the
556 same as the meaning `I`, so we have `m = I m`.  In other words, `m` is
557 a fixed point for the denotation of the sentence (when used in the
558 appropriate context).
559
560 That means that in a context in which *this sentence* refers to the
561 sentence in which it occurs, the sentence denotes a fixed point for
562 the identity function.  Here's a fixed point for the identity
563 function:
564
565 <pre><code>Y I
566 (\f. (\h. f (h h)) (\h. f (h h))) I
567 (\h. I (h h)) (\h. I (h h)))
568 (\h. (h h)) (\h. (h h)))
569 &omega; &omega;
570 &Omega
571 </code></pre>
572
573 Oh.  Well!  That feels right.  The meaning of *This sentence is true*
574 in a context in which *this sentence* refers to the sentence in which
575 it occurs is <code>&Omega;</code>, our prototypical infinite loop...
576
577 What about the liar paradox?
578
579 (2)  This sentence is false.
580
581 Used in a context in which *this sentence* refers to the utterance of
582 (2) in which it occurs, (2) will denote a fixed point for `\f.neg f`,
583 or `\f l r. f r l`, which is the `C` combinator.  So in such a
584 context, (2) might denote
585
586      Y C
587      (\f. (\h. f (h h)) (\h. f (h h))) I
588      (\h. C (h h)) (\h. C (h h)))
589      C ((\h. C (h h)) (\h. C (h h)))
590      C (C ((\h. C (h h))(\h. C (h h))))
591      C (C (C ((\h. C (h h))(\h. C (h h)))))
592      ...
593
594 And infinite sequence of `C`s, each one negating the remainder of the
595 sequence.  Yep, that feels like a reasonable representation of the
596 liar paradox.
597
598 See Barwise and Etchemendy's 1987 OUP book, [The Liar: an essay on
599 truth and circularity](http://tinyurl.com/2db62bk) for an approach
600 that is similar, but expressed in terms of non-well-founded sets
601 rather than recursive functions.
602
603 ##However...##
604
605 You should be cautious about feeling too comfortable with
606 these results.  Thinking again of the truth-teller paradox, yes,
607 <code>&Omega;</code> is *a* fixed point for `I`, and perhaps it has
608 some a privileged status among all the fixed points for `I`, being the
609 one delivered by Y and all (though it is not obvious why Y should have
610 any special status).
611
612 But one could ask: look, literally every formula is a fixed point for
613 `I`, since
614
615     X <~~> I X
616
617 for any choice of X whatsoever.
618
619 So the Y combinator is only guaranteed to give us one fixed point out
620 of infinitely many---and not always the intuitively most useful
621 one. (For instance, the squaring function has zero as a fixed point,
622 since 0 * 0 = 0, and 1 as a fixed point, since 1 * 1 = 1, but `Y
623 (\x. mul x x)` doesn't give us 0 or 1.) So with respect to the
624 truth-teller paradox, why in the reasoning we've
625 just gone through should we be reaching for just this fixed point at
626 just this juncture?
627
628 One obstacle to thinking this through is the fact that a sentence
629 normally has only two truth values.  We might consider instead a noun
630 phrase such as
631
632 (3)  the entity that this noun phrase refers to
633
634 The reference of (3) depends on the reference of the embedded noun
635 phrase *this noun phrase*.  It's easy to see that any object is a
636 fixed point for this referential function: if this pen cap is the
637 referent of *this noun phrase*, then it is the referent of (3), and so
638 for any object.
639
640 The chameleon nature of (3), by the way (a description that is equally
641 good at describing any object), makes it particularly well suited as a
642 gloss on pronouns such as *it*.  In the system of
643 [Jacobson 1999](http://www.springerlink.com/content/j706674r4w217jj5/),
644 pronouns denote (you guessed it!) identity functions...
645
646 Ultimately, in the context of this course, these paradoxes are more
647 useful as a way of gaining leverage on the concepts of fixed points
648 and recursion, rather than the other way around.