Y combinator as an application of Lawvere's fixed point theorem

Question

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?

Answer 1

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.)

Answer 2

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$: $$ gg=\alpha_y(gg) $$

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)\\ gg=\alpha(gg) $$

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=\alpha(gg)\\ gg=(\lambda xy.y(\lambda z.xxyz))(\lambda xy.y(\lambda z.xxyz)) $$