# CCCs, computational calculi and point-surjectivity

The models of some computational calculi are in a correspondence with Cartesian Closed Categories with an object $$U$$ that has some relationship to its exponential object $$U^U$$ e.g. a retraction between $$U$$ and $$U^U$$ gives $$\lambda$$-algebra whereas those with enough points and $$U \cong U^U$$ admitting extensionality

One possible relationship between $$U$$ and $$U^U$$ is (weak) point-surjectivity which is defined as there existing a morphism $$\phi : U \rightarrow U^U$$ such that for all points $$p: 1 \rightarrow U^U$$, there exists a point $$u : 1 \rightarrow U$$ and $$\phi \circ u = p$$.

This relationship is relevant to $$\lambda$$-calculi as the $$F: D \rightarrow D^D$$ sided arrow in the retraction for lambda models and in the isomorphism can be seen to be point-surjective. Furthermore point-surjectivity appears in Lawvere's Fixed Point Theorem which can be used to derive the First-Fixed-Point theorem for the (I have written a derivation here however it has been rushed so apologies for mistakes).

A question that I have been contemplating is whether point-surjectivity corresponds to any existing class of automata or combinatorial calculi. Longo and Moggi in "A Category-Theoretic Characterization of Functional Completeness" outline the categorical models associated with combinatory algebras however it is not immediately obvious to me whether we point-surjectivity corresponds to this formulation however my intuition says otherwise. I have managed to derive several combinators in an applicative structure induced by a point-surjective $$F: U \rightarrow U^U$$ in the standard way as outlined in Chapter 5 of Barendregt's "The Lambda Calculus: It's Syntax and Semantics". These are the Mockingbird combinator $$\textbf{M} x = x x$$, the Identity combinator $$\textbf{I} x = x$$, and the combinator $$\textbf{F} x y = y$$. Derivations can be found here. I am unsure if this is an exhaustive list of the combinators that can be derived or if this set has any meaningful interpretation.

Any guidance or insights would be greatly welcomed!

• When you say "there exists a function $\phi : U \to U^U$", do you mean "there exists a morphism $\phi : U \to U^U$"? Feb 3 at 11:55
• My first instinct is that from the point-wise surjectivity you should be able to get the whole retraction. Feb 3 at 12:00
• My other question is: how do you interpret the $\lambda$-calculus, precisely, without having a retraction from $U^U \to U$? In particular, how does it work for terms with free variables? Feb 3 at 13:30
• Thank you for your explanation, I misunderstood the point about $\lambda$-calculus. Do you assume anything about $\phi$ at all, apart from point surjectivity? I would attack the question like this: figure out why/whether in $\lambda$-calculus point-surjectivity gives a retraction. If ti does, which bit of $\lambda$-calculus makes that possible, i.e., which $\lambda$-expressions appear in the proof. Then study whether you can get those in your weaker setting, expressed as combinators. Feb 3 at 19:21
• My point was that, if retraction can be obtained in $\lambda$-calculus but cannot in the general case, then by studying how the $\lambda$-calculus retraction arises, you might discover a proof that certain combinators cannot be obtained in the general case (those that would give you thre retraction). In any case, I would pay attention to combinators that require nested $\lambda$'s, as those apply transposes in non-empty contexts. Feb 4 at 7:49