Lawere's Theorem for Lambda Calculus (& Combinatory Logic)

November 3, 2020

In lieu of ever writing this all up properly I thought I would write some of the work I did in my master’s thesis and beyond properly. I’m hoping that this will serve as a jumping off point for when I take a break from being a traitor and doing statistics. Most of this work was done with my Master’s thesis supervisor Nicolas Wu. I claim no originality to this work.

Being not-very-well-read in categorical logic (and everything really) I am sure that there is some unifying way to understand all this that makes my work derivative or naive. However, this was the first research endeavour I ever undertook and it arose quite organically out of genuine interest so I still think it’s neat.

I’m going to skip the explanation of Category theory here, primarily to save time but also to save the embarassment of trying to give good explanations. If anyone is reading this and cares I think (Awodey 2010) is a good overview of the basics for logicians and theoretical computer scientists.

Lawvere’s Theorem

Lawvere’s theorem is a statement in the context of Cartesian Closed Categories. We begin with some definitions

Definition: Point Surjective Morphism A point-surjective morphism is some $\phi: A \rightarrow B$ such that, for all points $p : 1 \rightarrow B$, there exists a point $q : 1 \rightarrow A$ such that

\begin{equation} \label{eq:point-surjection} \phi \circ q = p \end{equation}

Definition: Fixed Point An endomorphism $g: A \rightarrow A$ has a fixed point if there exists a point $p : 1 \rightarrow A$ such that

\begin{equation} \label{eq:fixed-point-property} g \circ p = p \end{equation}

Theorem: Lawvere’s Fixed Point Theorem In some CCC $C$, if there exists a point-surjective morphism $\phi: A \rightarrow B^A$ then all endomorphisms $g : B \rightarrow B$ have a fixed point. The proof can be found on nLab or in Lawvere’s original paper (Lawvere 1969) as this is already too long.

Applications

Lambda Calculus & Lawvere

It seems intuitive that there must be an application of the Lawvere’s theorem within the Lambda calculus. I discussed some uninteresting background about the claim on nLab that Lawvere’s implies the existence of a fixed point combinator in the Lambda calculus. I have yet to find a demonstration of this claim and have myself only derived the first fixed point theorem in the $λ$-calculus.

Introduction

The intuition that Lawvere’s theorem has an application in the lambda calculus stems from the observation that $\lambda$ terms are intended to be functions between $\lambda$ terms. Any domain $D$ of $\lambda$ terms therefore is isomorphic to $D \rightarrow D$ which with squinting can be seen to induce a size problem, something Lawvere’s theorem witnesses. We will borrow definitions and results from (Barendregt 1991).

We will demonstrate the first fixed point theorem in the lambda calculus for this result i.e. that every lambda term has a fixed point.

We specifically want to relate Lawvere’s theorem to the $\lambda$ -calculus itself which in this context means a statement that holds true in the equational theory $\lambda$. The way will do this is using some basic model theory, using Theorem 5.2.18 from (Barendregt 1991) which states:

Theorem 5.2.18i) (Barendregt 1991) Let $M, N \in \Lambda$

\begin{align*} \lambda \vdash M = N \Leftrightarrow M=N \textrm{ is true in all models of the } \lambda\textrm{-calculus} \end{align*}

This fact will be used using the reverse implication and a connection between CCCs and models of the $\lambda$ calculus.

Prerequisites

For each equational theory of the $\lambda$ calculus there are two ways that models can be specified: as syntactic models where there is an interpretation function which maps $\lambda$ terms to the objects of the model in which the equational theories are preserved, and non-syntactic models where there are distinguished objects corresponding to complete sets of combinators. For the equational theory $\lambda\beta$ these are known as syntactic $\lambda$ algebras and, uh, $\lambda$ algebras.

It can be demonstrated that these models are equivalent (the categories of each structure are isomorphic to each other) and therefore we will introduce syntactic lambda algebras and refer to them as lambda algebras (exploiting univalence to preserve proofs on lambda algebras over to syntactic ones). To observe a precise definition of lambda algebras, syntactic lambda algebras and a proof of equivalence see Theorem 5.2.2 and Definition 5.3.1 (Barendregt 1991) in Theorem 5.3.6 (Barendregt 1991) respectively

To do this we have to build them incrementally from syntactic applicative structures.

Definition: Applicative Structure An applicative structure is a set $A$ along with a binary operation $\cdot : A \times A \rightarrow A$ (yes that is it).

These are the basic units of models of $\lambda$ calculus-like things. Syntactic algebras are applicative structures alongside syntactical interpretation functions which map from $\lambda$ terms to the underlying set of the applicative structure. A syntactic interpretation function is somewhat non-trivial and I am too lazy to outline it. Definition 5.3.1 contains a description of the conditions of the syntatic interpretation function. We will use semantic brackets to refer to syntactic interpretation functions $[[\cdot]]$

The syntactic version of models of $\lambda\beta$ is called syntactic lambda-algebras.

Definition: Syntactic Lambda Algebras A Syntactic Lambda Algebra is a Syntactic Applicative Structure $(A, \cdot, [[\cdot]])$ where

\begin{align*} \lambda\beta \vdash M = N \implies [[M]] = [[N]] \end{align*}

We will connect the above definitions to category theory through the observation that syntactic Lambda Algebras are in correspondence with a class of CCCs, namely those with a reflexive object.

Definition: Reflexive Object A reflexive object, $D$ in a category $C$ retracts into $D^{D}$ in the sense that there exists morphisms $F: D \rightarrow D^{D}$ and $G: D^D \rightarrow D$ such that

\begin{align*} F \circ G = \text{id}_{U^{U}} \end{align*}

This definition relates to Lawvere’s through $F$ being a point surjection where the point associated with some point $u : D^D$ is given by $G \circ u$. Therefore every endomorphism on $D$ has a fixed point. This property, when understood in light of the isomorphism between CCCs with a reflexive object and syntactic lambda algebras yields the first fixed point theorem.

Correspondence - Categorical Models of the lambda calculus - Lambda models

To get from $λ$-algebras to CCCs with a reflexive object the Karoubi Envelope is used (see Definition 5.5.11 (Barendregt 1991)). This direction of the isomorphism provides no information as to how to recover the first fixed point theorem

To get from CCCs w/ reflexive object to a syntactic lambda algebra we take as the underlying set of the algebra the set of points to $D$ i.e. the morphisms of type $1 \rightarrow D$. The syntactic interpretation function is verbose but can be found in Definition 5.5.3 (Barendregt 1991) . The evaluation function $\star$ takes two points to a third point and is defined as:

\begin{align*} x \star y = eval \circ \langle F \times \text{id} \rangle \circ \langle x , y \rangle \end{align*}

We can obtain the first fixed point theorem in the syntax of the lambda calculus by considering Theorem 5.2.18 part i) in (Barendregt 1991) and result below

Lemma The first fixed point property can be obtained in all lambda algebras by considering CCCs with a reflexive object.

We will use $\text{curry}$ and $\text{uncurry}$ to refer to the tensor-hom adjunctions hom-set isomorphisms and overline and underline respectively to indicate extending and collapsing the target of a morphism to the terminal object.

Proof

As acknowledged earlier, the $F$ in the retraction s a point surjective function. Therefore, for any point $x: 1 \rightarrow D$ a fixed point under $\star$ can be found as follows.

Let $t = F \circ x : 1 \rightarrow D^{D}$

We obtain an endomorphism on $D$ by uncurrying and then collapsing the terminal object $\underline{\text{uncurry}(t)} : D \rightarrow D$

We now use the consequence of Lawvere’s fixed point theorem to obtain a fixed point $u : 1 \rightarrow D$ of $\underline{\text{uncurry}(t)}$. We claim that $u$ is a fixed point for $x$ under $\star$. Now demonstrating this:

\begin{align*} x \star u &= \text{eval} \circ \langle F \times \text{id} \rangle \circ \langle x , u \rangle \\\
&= \text{eval} \circ \langle F \circ x \times \text{id} \rangle \circ \langle \text{id} , u \rangle \\\
&= \text{eval} \circ \langle \text{curry}(\text{uncurry}(F \circ x)) \times \text{id} \rangle \circ \langle \text{id} , u \rangle \\\
&= \text{uncurry}(F \circ x) \circ \langle \text{id} \times u \rangle \\\
&= \underline{\text{uncurry}(F \circ x)} \circ u \\\
&= u \end{align*}

Combinatory Logic & Lawvere

An alternate version of Lawvere’s fixed point theorem is valid in cartesian categories by considering the proof pushed through Yoneda’s lemma stating the theorem without proof from (Lawvere 1969)

Theorem 2.2. (Lawvere 1969)

Let $A$, $Y$ be objects in a category with finite products and a terminal object then the following statements cannot both be true

a) there exists $\overline{g} : A \times A \rightarrow Y$ such that for all $f : A \rightarrow Y$ there exists $X : 1 \rightarrow A$ such that for all $a : 1 \rightarrow A$

\begin{align*} f \circ a = \overline{g} \circ \langle a, x \rangle \end{align*}

b) There exists $t : Y \rightarrow Y$ such that for all $y : 1 \rightarrow Y$

\begin{align*} t \circ y \neq y \end{align*}

This formulation of Lawvere’s theorem has a nice correspondence to categorical models of Combinatory Logic that are present in (Longo and Moggi 1990). First introducing some definitions

Defintion: Retraction A retraction from $U$ to $U \times U$ are pairs of arrows $j : U \rightarrow U \times U$ and $i : U \times U \rightarrow U$ such that $i \circ j = \text{id}_{U\times U}$.

Definition; K-Universal Arrow In some Cartesian category a morphism $u : X \times Y \rightarrow Z$ is K-universal if for all $f : X \times Y \rightarrow Z$ there exists an $s : X \rightarrow X$ such that

\begin{align*} f = u \circ \langle s \times \text{id} \rangle \end{align*}

Definition: Applicative Structure generated from Cartesian Category For some Cartesian category with a terminal object, some object $U$ such that there is a retraction from $U$ to $1$, the applicative structure associated with a morphism $u: U\times U \rightarrow U$ is given by the set of points to $U$ as the underlying set and, as the binary operation $\star$ is given by

\begin{align*} a \star b = u \circ \langle a , b \rangle \end{align*}

Longo and Moggi find that models of Combinatory Logic, Combinatory Algebras, are in a correspondence with Cartesian categories with a retraction from $U$ to $T$ and from $U$ to $U\times U$ in which there exists a K-Universal arrow $u : U \times U \rightarrow U$ This is demonstrated in Theorems 2.11 and 2.12. The associated combinatory algebra is the applicative structure is by the process outlined above. We forgo proofs of the above results for brevity.

We wish to show that Theorem 2.2 from (Lawvere 1969) can be used to derive that all combinators in $CL$ have a fixed point. To do this we need to use Theorem 2.2 to derive a fixed point theorem in Categorical models of $CL$ and then we need to show that this induces a fixed point theorem in the resultant combinatory algebras. We then use that it is true of all models of $CL$ to bring it back to $CL$ itself. See Definition 5.1.7 (Barendregt 1991) for a definition of combinatory algebras

The first theorem first

Theorem For a cartesian category with an object U that has a retraction to $1$ and a retraction to $U\times U$ and a K-universal arrow $u: U\times U \rightarrow U$ every $t: U \rightarrow U$ has a fixed point.

Proof

Aiming to satisfy the conditions 2a) of Theorem 2.2 in (Lawvere 1969)

Let $\overline{g}$ be the K-Universal arrow $U$, forall $f: U \rightarrow U$ by K-universality there exists an $s : U \rightarrow U$ such that

\begin{align*} f \circ \pi_2 = u \circ \langle s \times id \rangle \end{align*}

For all $a : 1 \rightarrow U$

\begin{align*} u \circ \langle s , a \rangle &= u \circ \langle s \times \text{id} \rangle \circ \langle id , a \rangle \\\
&= f \circ \pi_2 \circ \langle \text{id} , a \rangle \\\
&= f \circ a \end{align*}

Giving us that all endos on $U$ have a fixed point

Moving onto the second theorem now

Theorem Every combinator in the induced combinatory algebra from a Cartesian category has a fixed point.

Proof

We begin by reformulating the application operation somewhat

\begin{align*} u \circ \langle a , b \rangle &= u \circ \langle a \times \text{id} \rangle \circ \langle \text{id} , b \rangle \\\
&= u \circ \langle a \times \text{id} \rangle \circ \text{id} \circ \langle \text{id} , b \rangle \\\
&= (u \circ \langle a \times \text{id} \rangle \circ \langle ! , \text{id} \rangle) \circ (\pi_2 \circ \langle \text{id} , b \rangle) \\\
&= (u \circ \langle a \times \text{id} \rangle \circ \langle ! , \text{id} \rangle) \circ b \\\
&= (u \circ \langle a \circ ! , \text{id} \rangle) \circ b \end{align*}

$U \circ \langle a \circ ! , \text{id} \rangle : U \rightarrow U$ so by the previous it has a fixed point therefore for a given $a$ pick $b$ to be a fixed point of the previous expression then $a \star b = b$

Conclusion and Discussion

To my mind there is clearly something going on here. Obviously since $CL$ is a sub-theory(?) of $\lambda\beta$ so the first proof gives us the second abitrarily - however - the correspondence between the cartesian version of Lawvere and the categorical models of combinatory algebras in addition to the original proof seems too good to be true (this may just be that the proof is somehow the original proof “shoved through” Yoneda if that is possible). The proofs are both largely isolated to formal rewrite systems derived from CCCs. This raises a question to me:

What is the rewrite system that corresponds to point-surjectivity? Is it functionally complete? If not then is point surjectivity a necessary condition of functional completeness and what are the other necessary conditions? Point-surjectivity seems so important and integral to the notion of computation that the above seems like an interesting question, perhaps grasping more of the core of “computation”. See here for some more stuff on this question.

Further Work

The stronger equational theories here come from granting more power to the points of the category, I’d like to investigate points more and try to look at Deligne’s completeness theorem and derive an appropriate analogue in rewrite systems. This point comes down to the fact that the background interest that I have in these topics is that I’m really intrigued by what computation actually is and what the relationship is between the interplay of attributes that a formal system can have. These are reasonably life long goals - hopefuly I’ll get some time to read everything to understand this.

I also have an inkling that we have a categorical computational interpretation of Reproducing Kernel Hilbert Spaces, a space that is explored a lot in statistics. The reproducing kernel property looks a lot like a self-reproducing combinator perhaps indicating some rewrite system interpratation. This also has parsimony with my intuition that RKHSs are as flexible as they are due to some underlying interesting property. There is a lot of work done on the categorical intepretation of Hilbert Spaces but this seems to be a blind spot in the literature - potentially a future project????

Real spacy stuff: paradox of predictability

Bibliography

Awodey, Steve. 2010. Category Theory. Oxford University Press.

Barendregt, HP. 1991. “The Lambda Calculus. Number 103 in Studies in Logic and the Foundations of Mathematics.” North-Holland, Amsterdam, revised edition.

Lawvere, F William. 1969. “Diagonal Arguments and Cartesian Closed Categories.” In Category Theory, Homology Theory and Their Applications II, 134–45. Springer.

Longo, Giuseppe, and Eugenio Moggi. 1990. “A Category-Theoretic Characterization of Functional Completeness.” Theoretical Computer Science 70 (2):193–211. http://www.sciencedirect.com/science/article/pii/030439759090122X.