The n-Category Café

Last time we proved that every lambda-term in the untyped lambda calculus has a fixed point, but the proof looked like magic: we pulled a rabbit out of a hat. This time, following Tom Payne’s comments, we explained where such rabbits come from. In fact, Curry’s construction of a fixed point for any lambda-term is based on the same ideas as Cantor’s diagonal argument!

For more along these lines, try these:

• F. William Lawvere, Diagonal arguments and cartesian closed categories, with author commentary, Reprints in Theory and Applications of Categories 15. Originally published in Category Theory, Homology Theory, and their Applications II, eds. Dold and Eckmann, Springer Lecture Notes in Mathematics 92, 1969, pp. 134–145.
• Noson Yanofsky, A universal approach to self-referential paradoxes, incompleteness and fixed points.

Lawvere’s paper begins:

The similarity between the famous arguments of Cantor, Russell, Gödel and Tarski is well-known, and suggests that these arguments should all be special cases of a single theorem about a suitable kind of abstract structure. We offer here a fixed-point theorem in cartesian closed categories which seems to play this role.

Yanofsky’s paper is expository and lots of fun. Now he’s writing a book on quantum computation for computer scientists. One of my grad students, Alex Hoffnung, previously studied with him.

We also gave a preview of coming attractions: more on quantum computation, and categorifying our work so far to see the process of computation as a 2-morphism in a 2-category.

This is my last class this quarter, since next Thursday I’ll be giving a talk at Stanford. In my absence, Tom Payne will speak about the Myhill-Shepherdson Theorem. We’ll continue in January!