Applications of Lawvere's fixed point theorem

Question

Lawvere's fixed point theorem states that in a cartesian closed category, if there is a morphism $A \to X^A$ which is point-surjective (meaning that $\hom(1,A) \to \hom(1,X^A)$ is surjective), then every endomorphism of $X$ has a fixed point (meaning a morphism $1 \to X$ which is fixed by the endomorphism). It unifies several (all?) diagonal arguments appearing in mathematical logic (Cantor's theorem, Russel's paradox, Tarski's non-definability of truth, the Recursion theorem, Gödel's first incompleteness theorem). See Yanovsky's paper for an expository account. Somehow it reminds me of the Yoneda Lemma because the proof is so short and simple, but the theorem unifies several theorems which are often regarded to be nontrivial. I wonder why it doesn't have a Wikipedia or at least an nlab entry yet (only Cantor's theorem alludes to it). Edit. Since March '14 there is an nlab entry.

The applications mentioned above all take place within the category of sets (or similar categories). But since the theorem applies to arbitrary cartesian closed categories, I wonder:

Question. Are there any interesting applications of Lawvere's fixed point theorem outside of mathematical logic by applying it to cartesian closed categories which are substantially different from the category of sets?

Qiaochu recently asked if the theorem implies Brouwer's fixed point theorem. But this seems to be a little bit too optimistic. Anyway, it would be nice to see at least some applications. Interesting examples of cartesian closed categories include the category $G\mathsf{-Set}$ for a group $G$ (here, a point of a $G$-set is already fixed by the $G$-action), the category $\mathrm{Sh}(X)$ of sheaves on a space $X$ (here a point is a global section), or the category of compactly generated (weak) Hausdorff spaces $\mathsf{CGHaus}$. What are interesting choices for the object $A$, and how can we use the resulting fixed point theorem?

Answer 1

It follows from Lawvere's theorem that for most spaces $X$ there is no space-filling curve for its path space, $\alpha: I \to X^I$, working here in the category of $k$-spaces. (Yes, that would also follow where one knows $X^I$ is not compact, but one point is that a similar result holds replacing $I$ by $\mathbb{R}$).

The category of Polish spaces is not cartesian closed, because every Polish space $X$ admits a continuous surjection $B\to X$ from Baire space $B$ (the space of irrationals), so that in particular there is no Polish function space $X^B$ for most Polish spaces $X$.

Answer 2

A lot of programming languages (PHP,C++0x,Java...) were just added lambda expression facilities recently.

However their lambda expression definitions usually does not allow direct recursion. But we can always do this:

1. Define a type WRAP that can

   a) Be constructed from a function closure receives a WRAP and returns an generic type. this is equivalent to the surjective condition.

   b) Be executed with another WRAP object and evaluate the function used to construct the object at this point. This is equivlent to a morphism $WRAP \to X^{WRAP}$

2. Now apply the trick garanteed by Lawvere's fixed point theorem, which says every function X -> X have a fixed point (of type X). Since we don't even know whether X have an accessable constructor, the only way we can construct such an X is by recursion. Implement a function that receive such a function and return the fixed point, now we obtained the Y combinator for the programming language.

See this code review post for an instance of how the above trick applies to C++1x.