<p>The models of some computational calculi are in a correspondence with Cartesian Closed Categories with an object <span class="math-container">$U$</span> that has some relationship to its exponential object <span class="math-container">$U^U$</span> e.g. a retraction between <span class="math-container">$U$</span> and <span class="math-container">$U^U$</span> gives <span class="math-container">$\lambda$</span>-algebra whereas those with enough points and <span class="math-container">$U \cong U^U$</span> admitting extensionality</p>
<p>One possible relationship between <span class="math-container">$U$</span> and <span class="math-container">$U^U$</span> is (weak) point-surjectivity which is defined as there existing a morphism <span class="math-container">$\phi : U \rightarrow U^U$</span> such that for all points <span class="math-container">$p: 1 \rightarrow U^U$</span>, there exists a point <span class="math-container">$u : 1 \rightarrow U$</span> and <span class="math-container">$\phi \circ u = p$</span>.</p>
<p>This relationship is relevant to <span class="math-container">$\lambda$</span>-calculi as the <span class="math-container">$F: D \rightarrow D^D$</span> sided arrow in the retraction for lambda models and in the isomorphism can be seen to be point-surjective. Furthermore point-surjectivity appears in <a href="https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem" rel="nofollow noreferrer">Lawvere's Fixed Point Theorem</a> which can be used to derive the First-Fixed-Point theorem for the (I have written a derivation <a href="https://alessio-b-zak.github.io/posts/lambda-cal/" rel="nofollow noreferrer">here</a> however it has been rushed so apologies for mistakes).</p>
<p>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 &quot;A Category-Theoretic Characterization of Functional Completeness&quot; 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 <span class="math-container">$F: U \rightarrow U^U$</span> in the standard way as outlined in Chapter 5 of Barendregt's &quot;The Lambda Calculus: It's Syntax and Semantics&quot;. These are the Mockingbird combinator <span class="math-container">$\textbf{M} x = x x$</span>, the Identity combinator <span class="math-container">$\textbf{I} x = x$</span>, and the combinator <span class="math-container">$\textbf{F} x y = y$</span>. Derivations can be found <a href="https://alessio-b-zak.github.io/posts/combin/" rel="nofollow noreferrer">here</a>. I am unsure if this is an exhaustive list of the combinators that can be derived or if this set has any meaningful interpretation.</p>
<p>Any guidance or insights would be greatly welcomed!</p>

CC BY-SA 4.0
2021-02-03T11:55:45.677Z
When you say "there exists a function $\phi : U \to U^U$", do you mean "there exists a **morphism** $\phi : U \to U^U$"?
Andrej Bauer
CC BY-SA 4.0
2021-02-03T12:00:02.253Z
My first instinct is that from the point-wise surjectivity you should be able to get the whole retraction.
Andrej Bauer
CC BY-SA 4.0
2021-02-03T13:30:54.443Z
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?
Andrej Bauer
CC BY-SA 4.0
2021-02-03T16:46:57.473Z
@AndrejBauer I did mean morphism (late night question asking makes me sloppy). I am not necessarily thinking that it will have a interpretation in some lambda calculus, perhaps something more combinatorial. This is why I have attempted to derive combinators as I was attempting to get S and K which would at least give some equivalence to Longo and Moggis formulation. I would need to think before I can give my thoughts on whether it is equivalent to the retraction. Thank you for the responses!
alessio-b-zak
CC BY-SA 4.0
2021-02-03T19:21:03.257Z
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.
Andrej Bauer
CC BY-SA 4.0
2021-02-03T20:59:12.397Z
@AndrejBauer I'm hoping to work with just point-surjectivity as I think it would be interesting in light of Lawvere's theorem. My intuition tells me that point-surjectivity won't give me a retraction (otherwise I think it would be easier to find other combinators in the induced applicative structure - I think i've found them all). However, it is clear to me now that this must be the next step. I think playing with the terms induced by the normal isomorphism between CCCs with a retraction and Lambda algebras is also a very helpful piece of advice. Thanks!
alessio-b-zak
CC BY-SA 4.0
2021-02-04T07:49:51.923Z
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.
Andrej Bauer
<lambda-calculus><ct.category-theory>
CCCs, computational calculi and point-surjectivity
alessio-b-zak
# CCCs, computational calculi and point-surjectivity

(Asked by: username_0 on 2021-02-03)

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](https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem) which can be used to derive the First-Fixed-Point theorem for the (I have written a derivation [here](https://username_0.github.io/posts/lambda-cal/) 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](https://username_0.github.io/posts/combin/). 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!

**Tags:** lambda-calculus, ct.category-theory

> **Comments:**
> **username_1**: When you say "there exists a function $\phi : U \to U^U$", do you mean "there exists a **morphism** $\phi : U \to U^U$"?  
> **username_1**: My first instinct is that from the point-wise surjectivity you should be able to get the whole retraction.  
> **username_1**: 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?  
> **username_0**: @AndrejBauer I did mean morphism (late night question asking makes me sloppy). I am not necessarily thinking that it will have a interpretation in some lambda calculus, perhaps something more combinatorial. This is why I have attempted to derive combinators as I was attempting to get S and K which would at least give some equivalence to Longo and Moggis formulation. I would need to think before I can give my thoughts on whether it is equivalent to the retraction. Thank you for the responses!  
> **username_1**: 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.  
> **username_0**: @AndrejBauer I'm hoping to work with just point-surjectivity as I think it would be interesting in light of Lawvere's theorem. My intuition tells me that point-surjectivity won't give me a retraction (otherwise I think it would be easier to find other combinators in the induced applicative structure - I think i've found them all). However, it is clear to me now that this must be the next step. I think playing with the terms induced by the normal isomorphism between CCCs with a retraction and Lambda algebras is also a very helpful piece of advice. Thanks!  
> **username_1**: 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.  

---

## 0 answers

