2
$\begingroup$

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?

$\endgroup$
2
$\begingroup$

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

$\endgroup$

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.