Point-Surjectivity and Combinators

February 2, 2021

Some models of computational calculi have categorical analogues that are CCCs with some distinguished object $D$ with some relationship to its function space $D^{D}$.

Models of the equational theory $\lambda\beta$ are CCCs with a reflexive object (morphisms $F: D \rightarrow D^D$ and $G: D^D \rightarrow D$ such that $F \circ G = id_{D^{D}}$). We have weak extensionality if we have enough points and extensionality ($\eta$ rule) if we have enough points and there is an isomorphism $D \cong D^{D}$ (Propositions: 5.2.8 - 5.2.10 (Barendregt 1991))

The story for models of $CL is slightly more complicated (see (Longo and Moggi 1990))

For the differing equational theories of the Lambda Calculus, the correspondence between CCCs is witnessed by an isomorphism where the model is generated by setting the underlying set of the lambda algebra to be the set of points to $D$ with the binary operation, $\star$, being defined as follows: $\forall x, y : 1 \rightarrow D$

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

Further to this a semantic valuation function is defined to intepret lambda terms in the applicative structure.

For the details see Chapter 5 of (Barendregt 1991)

Question

One possible relationship between $D$ and $D^D$ is that of point-surjectivity. This is strictly weaker than reflexivity of $D$. A morphism $\phi: A \rightarrow B^{A}$ in some CCC is point-surjective if, for all points, $f$, to $B^A$ there exists a point, $u$, to $A$ such that

\begin{align*} \phi \circ u = f \end{align*}

It can be seen that the $F$ of a reflexive object is point surjective. This fact can be used to derive the first fixed point theorem for the lambda calculus see here. A natural question may arise - are the class of models that correspond to CCCs with a point-surjective $\phi : D \rightarrow D^{D}$ interesting computationally? We do not answer this question here however we provide some of the combinators (perhaps all!) that can be derived from an applicative structure generated from a CCC with a reflexive object.

We begin with the observation that we can recover any endomorphism on $D$ through the fact that $a \star b$ can be reduced to $\overline{\text{uncurry}(\phi \circ a)} \circ b$ where the overline is the appropriate direction of the isomorphism between $1 \times D \rightarrow D$ and $D \rightarrow D$ . Therefore, for any endomorphism $f: D \rightarrow D$ let $f’ = \text{curry}(\underline{f})$ where the underline is the other direction of the aformentioned isomorphism. The type of $f’$ is $1 \rightarrow D^{D}$ and therefore a point, $u : 1 \rightarrow D$, to $D$ can be found that $\phi$ lifts to be $f’$ i.e. $\phi \circ u = f’$. Now examining $u$ under $\star$, for all $b : 1 \rightarrow D$

\begin{align*} u \star b &= \overline{\text{uncurry}(\phi \circ u)} \circ b \\\
&= \overline{\text{uncurry}(f’)} \circ b \\\
&= \overline{\text{uncurry}(\text{curry}(\underline{f}))} \circ b \\\
&= f \circ b \end{align*}

From this we will make some combinators. Coonsider the identity combinator $\textbf{I} x = x$ can be found by selecting $f$ to be $\text{id}_{D}$ and calculating the appropriate $u$ which will be your identity combinator.

The Mockingbird combinator $\textbf{M} x = x x$ can be derived by letting $f = \text{eval} \circ \langle \phi \times \text{id} \rangle \circ \delta$ which is of type $D \rightarrow D$. Calculating the appropriate $u$ we obtain the Mockingbird $M$.

The final combinator is the combinator $\textbf{F} x y = y$ which we will make as follows. Let $y = \text{curry}(\underline{\text{id}_{D}}) : 1 \rightarrow D^{D}$ and let $z = 1 \rightarrow D$ s.t. $\phi \circ z= y$. Let $f = z \circ !_{D} : D \rightarrow D$ and, recovering $u$ and calling it $\textbf{F}$

\begin{align*} \textbf{F} \star a \star b &= (z \circ !_D) \star b \\\
&= \text{eval} \circ \langle \phi \times id \rangle \circ \langle z \circ !_D \circ a , b \rangle \\\
&= \text{eval} \circ \langle \phi \times id \rangle \circ \langle z , b \rangle \\\
&= \overline{\text{uncurry}(\phi \circ z)} \circ b \\\
&= id \circ b \\\
&= b \end{align*}

A point of note here is that with these three combinators we don’t have any dangling fixed points so there are no added combinators that are warranted by logic. M has I as a fixed point I has everything as a fixed point and F has I as a fixed point

Update: 09/02/21

Before drifting off to my peaceful sleep I thought back to the first problem in (Smullyan 1990). This problem shows that the fixed point property for a combinatory calculi can be derived from two properties:

Combinator Composition: For all Combinators $A$ and $B$ there exists a combinator $C$ such that for all combinators $X$

\begin{align*} C \cdot X = A \cdot (B \cdot X) \end{align*}

Mockingbird: There exists a mockingbird $M$

The second of these two conditions is fulfilled by the applicative structure induced by a point surjective arrow.

The first of these conditions is given by any arrow $f : D \rightarrow D^{D}$ in a CCC

Proof

For given points to $D$, $A$ and $B$ for given point $X$

\begin{align*} A \star (B \star X) &= \text{eval } \circ \langle \varphi \times \text{id } \rangle \circ \langle A , (\text{eval } \circ \langle \varphi \times id \rangle \circ \langle B , X \rangle) \rangle \\\
&= \overline{\text{uncurry}(\varphi \circ A)} \circ \overline{\text{uncurry}(\varphi \circ B)} \circ X \end{align*}

Now towards constructing our $C$, let (now regretting my overline / underline option )

\begin{align*} C’ = \text{curry}(\underline{\overline{\text{uncurry}(\varphi \circ A)} \circ \overline{\text{uncurry}(\varphi \circ B)}}) \end{align*}

which is a point to $D^{D}$, lifting $C’$ through $\varphi$ giving a point to $D$, name this point $C$. This can easily be seen to be equal to $A \star (B \star X)$

From this we can see that point surjectivty isn’t minimal for the fixed point theorem in the lambda calculus - therefore the next step is to see if $F$ disappears with weak point surjectivity - (Identity is a natural consequence of the first fixed point theorem and the mockingbird as the first fixed point of the mockinbird is $I$). Weakly point surjective then is the mockingbird core.

Future Topics

Check what combinators you get out of weakly point surjective
See if I can prove / disprove point surjectivity gives reflexivity
See if Longo and Moggi’s condition gives point surjectivty.
Check to mock a mockingbird for other interesting properties that can be derived.

Are these everything? What does this mean? Is there life after death?

Bibliography

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

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.

Smullyan, Raymond. 1990. To Mock a Mockingbird : and Other Logic Puzzles Including an Amazing Adventure in Combinatory Logic. Oxford: Oxford University Press.