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 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 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 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 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 at 7:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.