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!

  • 1
    $\begingroup$ When you say "there exists a function $\phi : U \to U^U$", do you mean "there exists a morphism $\phi : U \to U^U$"? $\endgroup$ Feb 3, 2021 at 11:55
  • 1
    $\begingroup$ My first instinct is that from the point-wise surjectivity you should be able to get the whole retraction. $\endgroup$ Feb 3, 2021 at 12:00
  • 1
    $\begingroup$ 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? $\endgroup$ Feb 3, 2021 at 13:30
  • 1
    $\begingroup$ 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. $\endgroup$ Feb 3, 2021 at 19:21
  • 1
    $\begingroup$ 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. $\endgroup$ Feb 4, 2021 at 7:49


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.