Lawvere's fixed point theorem states that that in a cartesian closed category, if there is a morphism $ϕ: A \to B^A$ which is point-surjective (i.e., for every point $q : 1 \to B^A$ there exists a point $p : 1 \to A$ such that $ϕp = q$), then every endomorphism $f : B \to B$ has a fixed point.

The fixed point of $f$ is obtained as $ϕ(p)(p)$ where $p : 1 \to A$ is the point of $A$ such that $ϕp = q$ for $q : 1 \to B^A$ defined in lambda calculus notation as $q = λa:A.fϕ(a)(a)$.

I've seen it remarked several times that the existence of Y combinator in lambda calculus, i.e., $Y = λf.(λx.f(xx))(λx.f(xx))$, is an application of Lawvere's fixed point theorem, but the remark has always been made only in passing and I haven't been able to figure out precisely how to get from the one to the other.

Can someone help me out by making the application explicit?


What Scott did with domain theory was construct a cartesian closed category with $\varphi:D\cong D^D$. More generally, we have an retraction, i.e. split epimorphism, $D\to D^D$. Isomorphisms/split-epimorphisms are clearly point-surjective: simply set $p = \varphi^{-1}\circ q$.

We can actually arrange for $\varphi=id_D$ for some models of the untyped lambda calculus. Then the fixed point of $f$ by the above statement would be $(p\,p)$ where $p=q=\lambda x.f(x\,x)$, i.e. $$\mathsf{fix}\,f = (\lambda x.f(x\,x))(\lambda x.f(x\,x))$$ which we, of course, lambda abstract to get $$\mathsf{fix}=\lambda f.(\lambda x.f(x\,x))(\lambda x.f(x\,x))$$ Not assuming $\varphi=id_D$ adds some noise but just as easily leads to the appropriate expression. For example, in Haskell if you wanted to model the untyped lambda calculus, you could use:

newtype D = D {unD :: D -> D}

The data constructor D corresponds to $\varphi^{-1}$ with unD corresponding to $\varphi$ witnessing D ≅ (D -> D). It's an easy enough exercise to insert the uses of D and unD, more or less guided by the types, into the expression for the $Y$ combinator to get a type checking version in Haskell. In practice, you'd probably want some kind of "base type" so you can actually observe something from these values. This would produce a type like:

data D b = Base b | Fun (D b -> D b)

Here Fun plays the role of $\varphi^{-1}$ and unFun (Fun f) = f plays the role of $\varphi$ and we only have a retraction. (To make unFun total you can make unFun send Base b to any value of D -> D, though bottom is a value and not so dismissable anyway given the context of the problem.)


Lawvere's Fixed Point Theorem:

$X\times X\xrightarrow{f} Y\\ \Delta\uparrow\qquad\;\;\downarrow\alpha\\ \;\;\;X\;\; \xrightarrow[g]\;\; Y$

For sets $X, Y$, functions $f: X\times X\to Y$, $\alpha: Y\to Y$, let $g := \alpha\circ f\circ\Delta$. If $g$ is representable by $f(-,\ulcorner g\urcorner)$, then $\alpha$ has a fixed point: $\alpha\big(f\left(\ulcorner g\urcorner,\ulcorner g\urcorner\right)\big)=g\left(\ulcorner g\urcorner\right)=f\left(\ulcorner g\urcorner,\ulcorner g\urcorner\right)$.

Now let's fit Curry's $Y$ combinator into Lawvere's schema.

$\Lambda\times \Lambda \xrightarrow{f} \Lambda \\ \Delta\uparrow\qquad\;\;\downarrow\alpha_y\\ \;\;\;\Lambda\;\; \xrightarrow[g]\;\; \Lambda$

where $\Lambda$ is the class of lambda terms, and $f:(x,y)\mapsto yx$, and $\alpha_y: x\mapsto yx$.

then $g=\lambda x.y(xx)$ is a fixed point of $\alpha_y$:


Curry's $Y$ combinator is

$Y := \lambda y.gg=\lambda y.(\lambda x.y(xx))(\lambda x.y(xx))$

If we let $f:(x,y)\mapsto \lambda v.yxv$, and $\alpha_y: x\mapsto yx$, then

$g=\lambda x.y(\lambda v.xxv)$

and $gg=\alpha_y(gg)$.

Now we get the call-by-value version of $Y$ combinator:

$\lambda y.gg=\lambda y.(\lambda x.y(\lambda v.xxv))(\lambda x.y(\lambda v.xxv))$

If we let $f:(x,y)\mapsto yx$, and $\alpha: x\mapsto\lambda y.y(xy)$, then

$g=\lambda xy.y(xxy)$


Now we get Turing's $\Theta$ combinator:

$\Theta := gg=(\lambda xy.y(xxy))(\lambda xy.y(xxy))$

The call-by-value version of $\Theta$ combinator is similar.

Let $f:(x,y)\mapsto yx$, and $\alpha: x\mapsto\lambda y.y(\lambda z.xyz)$.

$g=\lambda xy.y(\lambda z.xxyz)$


$gg=(\lambda xy.y(\lambda z.xxyz))(\lambda xy.y(\lambda z.xxyz))$

  • $\begingroup$ The question is asking about Lawvere's fixed point theorem, which you haven't addressed. $\endgroup$
    – Zhen Lin
    Apr 11 at 13:55
  • $\begingroup$ @Zhen Lin Sorry, I forgot to address Lawvere's fixed point theorem. $\endgroup$
    – Xi Li
    Apr 11 at 14:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.