1 [[!toc]]
3 ##What is the "rec" part of "letrec" doing?##
5 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:
7 >       the empty list has length 0
9 >       any non-empty list has length 1 + (the length of its tail)
11 In OCaml, you'd define that like this:
13         let rec get_length = fun lst ->
14                 if lst == [] then 0 else 1 + get_length (tail lst)
15         in ... (* here you go on to use the function "get_length" *)
17 In Scheme you'd define it like this:
19         (letrec [(get_length
20                                 (lambda (lst) (if (null? lst) 0 [+ 1 (get_length (cdr lst))] )) )]
21                 ... ; here you go on to use the function "get_length"
22         )
26 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)`).
28 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.)
30 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.
32 4.      I alternate between `[ ]`s and `( )`s in the Scheme code just to make it more readable. These have no syntactic difference.
35 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?
37 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:
39         let rec get_length = fun lst ->
40                 if lst == [] then 0 else 1 + get_length (tail lst)
41         in get_length [20; 30]
42         (* this evaluates to 2 *)
44 In Scheme:
46         (letrec [(get_length
47                                 (lambda (lst) (if (null? lst) 0 [+ 1 (get_length (cdr lst))] )) )]
48                         (get_length (list 20 30)))
49         ; this evaluates to 2
51 If you instead use an ordinary `let` (or `let*`), here's what would happen, in OCaml:
53         let get_length = fun lst ->
54                 if lst == [] then 0 else 1 + get_length (tail lst)
55         in get_length [20; 30]
56         (* fails with error "Unbound value length" *)
58 Here's Scheme:
60         (let* [(get_length
61                                 (lambda (lst) (if (null? lst) 0 [+ 1 (get_length (cdr lst))] )) )]
62                         (get_length (list 20 30)))
63         ; fails with error "reference to undefined identifier: get_length"
65 Why? Because we said that constructions of this form:
67         let get_length = A
68                 in B
70 really were just another way of saying:
72         (\get_length. B) A
74 and so the occurrences of `get_length` in A *aren't bound by the `\get_length` that wraps B*. Those occurrences are free.
76 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:
78         let get_length = fun lst -> 99
79         in let get_length = fun lst ->
80                         if lst == [] then 0 else 1 + get_length (tail lst)
81         in get_length [20; 30]
82         (* evaluates to 1 + 99 *)
84 Here the use of `get_length` in `1 + get_length (tail lst)` can clearly be seen to be bound by the outermost `let`.
86 And indeed, if you tried to define `get_length` in the lambda calculus, how would you do it?
88         \lst. (isempty lst) zero (add one (get_length (extract-tail lst)))
90 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.
92 What we really want to do is something like this:
94         \lst. (isempty lst) zero (add one (... (extract-tail lst)))
96 where this very same formula occupies the `...` position:
98         \lst. (isempty lst) zero (add one (
99                 \lst. (isempty lst) zero (add one (... (extract-tail lst)))
100                         (extract-tail lst)))
102 but as you can see, we'd still have to plug the formula back into itself again, and again, and again... No dice.
104 So how could we do it? And how do OCaml and Scheme manage to do it, with their `let rec` and `letrec`?
106 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.
108 2.      If you tried this in Scheme:
110                 (define get_length
111                                 (lambda (lst) (if (null? lst) 0 [+ 1 (get_length (cdr lst))] )) )
113                 (get_length (list 20 30))
115         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.
117 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`:
119                 \lst. lst (\x sofar. successor sofar) zero
121         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.
123 We can use similar techniques to define many recursive operations on
124 lists and numbers. The reason we can do this is that our "version 3,"
125 fold-based implementation of lists, and Church's implementations of
126 numbers, have a internal structure that *mirrors* the common recursive
127 operations we'd use lists and numbers for.  In a sense, the recursive
128 structure of the `get_length` operation is built into the data
129 structure we are using to represent the list.  The non-recursive
130 version of get_length exploits this embedding of the recursion into
131 the data type.
133 This is one of the themes of the course: using data structures to
134 encode the state of some recursive operation.  See discussions of the
135 [[zipper]] technique, and [[defunctionalization]].
137 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.
139 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.
141 ##Some functions require full-fledged recursive definitions##
143 However, some computable functions are just not definable in this
144 way. We can't, for example, define a function that tells us, for
145 whatever function `f` we supply it, what is the smallest integer `x`
146 where `f x` is `true`.  (You may be thinking: but that
147 smallest-integer function is not a proper algorithm, since it is not
148 guaranteed to halt in any finite amount of time for every argument.
149 This is the famous [[!wikipedia Halting problem]].  But the fact that
150 an implementation may not terminate doesn't mean that such a function
151 isn't well-defined.  The point of interest here is that its definition
152 requires recursion in the function definition.)
154 Neither do the resources we've so far developed suffice to define the
155 [[!wikipedia Ackermann function]]:
157         A(m,n) =
158                 | when m == 0 -> n + 1
159                 | else when n == 0 -> A(m-1,1)
160                 | else -> A(m-1, A(m,n-1))
162         A(0,y) = y+1
163         A(1,y) = 2+(y+3) - 3
164         A(2,y) = 2(y+3) - 3
165         A(3,y) = 2^(y+3) - 3
166         A(4,y) = 2^(2^(2^...2)) [where there are y+3 2s] - 3
167         ...
169 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.
171 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.
173 ##Using fixed-point combinators to define recursive functions##
175 ###Fixed points###
177 In general, we call a **fixed point** of a function f any value *x*
178 such that f <em>x</em> is equivalent to *x*. For example,
179 consider the squaring function `sqare` that maps natural numbers to their squares.
180 `square 2 = 4`, so `2` is not a fixed point.  But `square 1 = 1`, so `1` is a
181 fixed point of the squaring function.
183 There are many beautiful theorems guaranteeing the existence of a
184 fixed point for various classes of interesting functions.  For
185 instance, imainge that you are looking at a map of Manhattan, and you
186 are standing somewhere in Manhattan.  The the [[!wikipedia Brouwer
187 fixed point]] guarantees that there is a spot on the map that is
188 directly above the corresponding spot in Manhattan.  It's the spot
189 where the blue you-are-here dot should be.
191 Whether a function has a fixed point depends on the set of arguments
192 it is defined for.  For instance, consider the successor function `succ`
193 that maps each natural number to its successor.  If we limit our
194 attention to the natural numbers, then this function has no fixed
195 point.  (See the discussion below concerning a way of understanding
196 the successor function on which it does have a fixed point.)
198 In the lambda calculus, we say a fixed point of an expression `f` is any formula `X` such that:
200         X <~~> f X
202 You should be able to immediately provide a fixed point of the
203 identity combinator I.  In fact, you should be able to provide a whole
204 bunch of distinct fixed points.
206 With a little thought, you should be able to provide a fixed point of
207 the false combinator, KI.  Here's how to find it: recall that KI
208 throws away its first argument, and always returns I.  Therefore, if
209 we give it I as an argument, it will throw away the argument, and
210 return I.  So KII ~~> I, which is all it takes for I to qualify as a
211 fixed point of KI.
213 What about K?  Does it have a fixed point?  You might not think so,
214 after trying on paper for a while.
216 However, it's a theorem of the lambda calculus that every formula has
217 a fixed point. In fact, it will have infinitely many, non-equivalent
218 fixed points. And we don't just know that they exist: for any given
219 formula, we can explicit define many of them.
221 Yes, even the formula that you're using the define the successor
222 function will have a fixed point. Isn't that weird? Think about how it
223 might be true.  We'll return to this point below.
225 ###How fixed points help definie recursive functions###
227 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:
229         \list. if empty list then zero else add one (... (tail lst))
231 where this very same formula occupies the `...` position."
233 Imagine replacing the `...` with some function that computes the
234 length function.  Call that function `length`.  Then we have
236         \list. if empty list then zero else add one (length (tail lst))
238 At this point, we have a definition of the length function, though
239 it's not complete, since we don't know what value to use for the
240 symbol `length`.  Technically, it has the status of an unbound
241 variable.
243 Imagine now binding the mysterious variable:
245         h := \length \list . if empty list then zero else add one (length (tail list))
247 Now we have no unbound variables, and we have complete non-recursive
248 definitions of each of the other symbols.
250 Let's call this function `h`.  Then `h` takes an argument, and returns
251 a function that accurately computes the length of a list---as long as
252 the argument we supply is already the length function we are trying to
253 define.  (Dehydrated water: to reconstitute, just add water!)
255 But this is just another way of saying that we are looking for a fixed point.
256 Assume that `h` has a fixed point, call it `LEN`.  To say that `LEN`
257 is a fixed point means that
259     h LEN <~~> LEN
261 But this means that
263     (\list . if empty list then zero else add one (LEN (tail list))) <~~> LEN
265 So at this point, we are going to search for fixed point.
266 The strategy we will present will turn out to be a general way of
267 finding a fixed point for any lambda term.
269 ##Deriving Y, a fixed point combinator##
271 How shall we begin?  Well, we need to find an argument to supply to
272 `h`.  The argument has to be a function that computes the length of a
273 list.  The function `h` is *almost* a function that computes the
274 length of a list.  Let's try applying `h` to itself.  It won't quite
275 work, but examining the way in which it fails will lead to a solution.
277     h h <~~> \list . if empty list then zero else 1 + h (tail list)
279 There's a problem.  The diagnosis is that in the subexpression `h
280 (tail list)`, we've applied `h` to a list, but `h` expects as its
281 first argument the length function.
285     H = \h \list . if empty list then zero else one plus ((h h) (tail list))
287 This is the key creative step.  Since `h` is expecting a
288 length-computing function as its first argument, the adjustment
289 tries supplying the closest candidate avaiable, namely, `h` itself.
291 We now reason about `H`.  What exactly is H expecting as its first
292 argument?  Based on the excerpt `(h h) (tail l)`, it appears that `H`'s
293 argument, `h`, should be a function that is ready to take itself as an
294 argument, and that returns a function that takes a list as an
295 argument.  `H` itself fits the bill:
297     H H <~~> (\h \list . if empty list then zero else 1 + ((h h) (tail list))) H
298         <~~> \list . if empty list then zero else 1 + ((H H) (tail list))
299         == \list . if empty list then zero else 1 + ((\list . if empty list then zero else 1 + ((H H) (tail list))) (tail list))
300         <~~> \list . if empty list then zero
301                     else 1 + (if empty (tail list) then zero else 1 + ((H H) (tail (tail list))))
305 How does the recursion work?
306 We've defined `H` in such a way that `H H` turns out to be the length function.
307 In order to evaluate `H H`, we substitute `H` into the body of the
308 lambda term.  Inside the lambda term, once the substitution has
309 occurred, we are once again faced with evaluating `H H`.  And so on.
311 We've got the infinite regress we desired, defined in terms of a
312 finite lambda term with no undefined symbols.
314 Since `H H` turns out to be the length function, we can think of `H`
315 by itself as half of the length function (which is why we called it
316 `H`, of course).  Given the implementation of addition as function
317 application for Church numerals, this (H H) is quite literally H + H.
318 Can you think up a recursion strategy that involves "dividing" the
319 recursive function into equal thirds `T`, such that the length
320 function <~~> T T T?
322 We've starting with a particular recursive definition, and arrived at
323 a fixed point for that definition.
324 What's the general recipe?
326 1.   Start with any recursive definition `h` that takes itself as an arg: `h := \fn ... fn ...`
327 2.   Next, define `H := \f . h (f f)`
328 3.   Then compute `H H = ((\f . h (f f)) (\f . h (f f)))`
329 4.   That's the fixed point, the recursive function we're trying to define
331 So here is a general method for taking an arbitrary h-style recursive function
332 and returning a fixed point for that function:
334      Y := \h. ((\f.h(ff))(\f.h(ff)))
336 Test:
338     Yh == ((\f.h(ff))(\f.h(ff)))
339        <~~> h((\f.h(ff))(\f.h(ff)))
340        == h(Yh)
342 That is, Yh is a fixed point for h.
344 Works!
347 ##What is a fixed point for the successor function?##
349 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:
351         successor make-pair
353 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.
355 Yes! That's exactly right. And which formula this is will depend on the particular way you've implemented the successor function.
357 Moreover, the recipes that enable us to name fixed points for any
358 given formula aren't *guaranteed* to give us *terminating* fixed
359 points. They might give us formulas X such that neither `X` nor `f X`
360 have normal forms. (Indeed, what they give us for the square function
361 isn't any of the Church numerals, but is rather an expression with no
362 normal form.) However, if we take care we can ensure that we *do* get
363 terminating fixed points. And this gives us a principled, fully
364 general strategy for doing recursion. It lets us define even functions
365 like the Ackermann function, which were until now out of our reach. It
366 would also let us define arithmetic and list functions on the "version
367 1" and "version 2" implementations, where it wasn't always clear how
368 to force the computation to "keep going."
370 OK, so how do we make use of this?
372 Many fixed-point combinators have been discovered. (And some
373 fixed-point combinators give us models for building infinitely many
374 more, non-equivalent fixed-point combinators.)
376 Two of the simplest:
378 <pre><code>&Theta;&prime; &equiv; (\u f. f (\n. u u f n)) (\u f. f (\n. u u f n))
379 Y&prime; &equiv; \f. (\u. f (\n. u u n)) (\u. f (\n. u u n))</code></pre>
381 <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.
383 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>?
385 Indeed you can, getting the simpler:
387 <pre><code>&Theta; &equiv; (\u f. f (u u f)) (\u f. f (u u f))
388 Y &equiv; \f. (\u. f (u u)) (\u. f (u u))</code></pre>
390 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.
392 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:
394 <pre><code>&Psi; (\self. \n. self n)</code></pre>
396 When you try to evaluate the application of that to some argument `M`, it's going to try to give you back:
398         (\n. self n) M
400 where `self` is equivalent to the very formula `\n. self n` that contains it. So the evaluation will proceed:
402         (\n. self n) M ~~>
403         self M ~~>
404         (\n. self n) M ~~>
405         self M ~~>
406         ...
408 You've written an infinite loop!
410 However, when we evaluate the application of our:
412 <pre><code>&Psi; (\self (\lst. (isempty lst) zero (add one (self (extract-tail lst))) ))</code></pre>
414 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:
416         \lst. (isempty lst) zero (add one (self (extract-tail lst)))
418 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.
420 ##Fixed-point Combinators Are a Bit Intoxicating##
422 ![tatoo](/y-combinator-fixed.jpg)
424 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.
426 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.
428 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:
430         \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))
432 then this is a fixed-point combinator:
434         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
437 ##Watching Y in action##
439 For those of you who like to watch ultra slow-mo movies of bullets
440 piercing apples, here's a stepwise computation of the application of a
441 recursive function.  We'll use a function `sink`, which takes one
442 argument.  If the argument is boolean true (i.e., `\x y.x`), it
443 returns itself (a copy of `sink`); if the argument is boolean false
444 (`\x y. y`), it returns `I`.  That is, we want the following behavior:
446     sink false ~~> I
447     sink true false ~~> I
448     sink true true false ~~> I
449     sink true true true false ~~> I
451 So we make `sink = Y (\f b. b f I)`:
453     1. sink false
454     2. Y (\fb.bfI) false
455     3. (\f. (\h. f (h h)) (\h. f (h h))) (\fb.bfI) false
456     4. (\h. [\fb.bfI] (h h)) (\h. [\fb.bfI] (h h)) false
457     5. [\fb.bfI] ((\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))) false
458     6. (\b.b[(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))]I)  false
459     7. false [(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))] I
460              --------------------------------------------
461     8. I
463 So far so good.  The crucial thing to note is that as long as we
464 always reduce the outermost redex first, we never have to get around
465 to computing the underlined redex: because `false` ignores its first
466 argument, we can throw it away unreduced.
468 Now we try the next most complex example:
470     1. sink true false
471     2. Y (\fb.bfI) true false
472     3. (\f. (\h. f (h h)) (\h. f (h h))) (\fb.bfI) true false
473     4. (\h. [\fb.bfI] (h h)) (\h. [\fb.bfI] (h h)) true false
474     5. [\fb.bfI] ((\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))) true false
475     6. (\b.b[(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))]I)  true false
476     7. true [(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))] I false
477     8. [(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))] false
479 We've now arrived at line (4) of the first computation, so the result
480 is again I.
482 You should be able to see that `sink` will consume as many `true`s as
483 we throw at it, then turn into the identity function after it
484 encounters the first `false`.
486 The key to the recursion is that, thanks to Y, the definition of
487 `sink` contains within it the ability to fully regenerate itself as
488 many times as is necessary.  The key to *ending* the recursion is that
489 the behavior of `sink` is sensitive to the nature of the input: if the
490 input is the magic function `false`, the self-regeneration machinery
491 will be discarded, and the recursion will stop.
493 That's about as simple as recursion gets.
495 ##Application to the truth teller/liar paradoxes##
497 ###Base cases, and their lack###
499 As any functional programmer quickly learns, writing a recursive
500 function divides into two tasks: figuring out how to handle the
501 recursive case, and remembering to insert a base case.  The
502 interesting and enjoyable part is figuring out the recursive pattern,
503 but the base case cannot be ignored, since leaving out the base case
504 creates a program that runs forever.  For instance, consider computing
505 a factorial: `n!` is `n * (n-1) * (n-2) * ... * 1`.  The recursive
506 case says that the factorial of a number `n` is `n` times the
507 factorial of `n-1`.  But if we leave out the base case, we get
509     3! = 3 * 2! = 3 * 2 * 1! = 3 * 2 * 1 * 0! = 3 * 2 * 1 * 0 * -1! ...
511 That's why it's crucial to declare that 0! = 1, in which case the
512 recursive rule does not apply.  In our terms,
514     fac = Y (\fac n. iszero n 1 (fac (predecessor n)))
516 If `n` is 0, `fac` reduces to 1, without computing the recursive case.
518 Curry originally called `Y` the paradoxical combinator, and discussed
519 it in connection with certain well-known paradoxes from the philosophy
520 literature.  The truth teller paradox has the flavor of a recursive
521 function without a base case: the truth-teller paradox (and related
524 (1)    This sentence is true.
526 If we assume that the complex demonstrative "this sentence" can refer
527 to (1), then the proposition expressed by (1) will be true just in
528 case the thing referred to by *this sentence* is true.  Thus (1) will
529 be true just in case (1) is true, and (1) is true just in case (1) is
530 true, and so on.  If (1) is true, then (1) is true; but if (1) is not
531 true, then (1) is not true.
533 Without pretending to give a serious analysis of the paradox, let's
534 assume that sentences can have for their meaning boolean functions
535 like the ones we have been working with here.  Then the sentence *John
536 is John* might denote the function `\x y. x`, our `true`.
538 Then (1) denotes a function from whatever the referent of *this
539 sentence* is to a boolean.  So (1) denotes `\f. f true false`, where
540 the argument `f` is the referent of *this sentence*.  Of course, if
541 `f` is a boolean, `f true false <~~> f`, so for our purposes, we can
542 assume that (1) denotes the identity function `I`.
544 If we use (1) in a context in which *this sentence* refers to the
545 sentence in which the demonstrative occurs, then we must find a
546 meaning `m` such that `I m = I`.  But since in this context `m` is the
547 same as the meaning `I`, so we have `m = I m`.  In other words, `m` is
548 a fixed point for the denotation of the sentence (when used in the
549 appropriate context).
551 That means that in a context in which *this sentence* refers to the
552 sentence in which it occurs, the sentence denotes a fixed point for
553 the identity function.  Here's a fixed point for the identity
554 function:
556 <pre><code>Y I
557 (\f. (\h. f (h h)) (\h. f (h h))) I
558 (\h. I (h h)) (\h. I (h h)))
559 (\h. (h h)) (\h. (h h)))
560 &omega; &omega;
561 &Omega
562 </code></pre>
564 Oh.  Well!  That feels right.  The meaning of *This sentence is true*
565 in a context in which *this sentence* refers to the sentence in which
566 it occurs is <code>&Omega;</code>, our prototypical infinite loop...
570 (2)  This sentence is false.
572 Used in a context in which *this sentence* refers to the utterance of
573 (2) in which it occurs, (2) will denote a fixed point for `\f.neg f`,
574 or `\f l r. f r l`, which is the `C` combinator.  So in such a
575 context, (2) might denote
577      Y C
578      (\f. (\h. f (h h)) (\h. f (h h))) I
579      (\h. C (h h)) (\h. C (h h)))
580      C ((\h. C (h h)) (\h. C (h h)))
581      C (C ((\h. C (h h))(\h. C (h h))))
582      C (C (C ((\h. C (h h))(\h. C (h h)))))
583      ...
585 And infinite sequence of `C`s, each one negating the remainder of the
586 sequence.  Yep, that feels like a reasonable representation of the
589 See Barwise and Etchemendy's 1987 OUP book, [The Liar: an essay on
590 truth and circularity](http://tinyurl.com/2db62bk) for an approach
591 that is similar, but expressed in terms of non-well-founded sets
592 rather than recursive functions.
594 ##However...##
596 You should be cautious about feeling too comfortable with
597 these results.  Thinking again of the truth-teller paradox, yes,
598 <code>&Omega;</code> is *a* fixed point for `I`, and perhaps it has
599 some a privileged status among all the fixed points for `I`, being the
600 one delivered by Y and all (though it is not obvious why Y should have
601 any special status).
603 But one could ask: look, literally every formula is a fixed point for
604 `I`, since
606     X <~~> I X
608 for any choice of X whatsoever.
610 So the Y combinator is only guaranteed to give us one fixed point out
611 of infinitely many---and not always the intuitively most useful
612 one. (For instance, the squaring function has zero as a fixed point,
613 since 0 * 0 = 0, and 1 as a fixed point, since 1 * 1 = 1, but `Y
614 (\x. mul x x)` doesn't give us 0 or 1.) So with respect to the
615 truth-teller paradox, why in the reasoning we've
616 just gone through should we be reaching for just this fixed point at
617 just this juncture?
619 One obstacle to thinking this through is the fact that a sentence
620 normally has only two truth values.  We might consider instead a noun
621 phrase such as
623 (3)  the entity that this noun phrase refers to
625 The reference of (3) depends on the reference of the embedded noun
626 phrase *this noun phrase*.  It's easy to see that any object is a
627 fixed point for this referential function: if this pen cap is the
628 referent of *this noun phrase*, then it is the referent of (3), and so
629 for any object.
631 The chameleon nature of (3), by the way (a description that is equally
632 good at describing any object), makes it particularly well suited as a
633 gloss on pronouns such as *it*.  In the system of