Thomas Streicher wrote:
Peter Freyd claims that any partial recursive function arises as Hom(1,f) for some endomorphism from N to N .
From his comment I could not see why. If one assumes the solution
D = N + [N->N]
then one may define the recursor Y in the usual lambda calculus style.
BUT how can one transform the exponentiation functor in the ambient ccc to a functor on the reflective cat of strict maps ?
Actually, I did not make that claim since Hom(1,f) can't be recursive if Hom(1,N) is, for example, an uncountably infinite set. What I said was: I don't know about algebraically closed ccc's but I should have answered this question in my Durham paper for the algebraically compact case. (Algebraically compact means every endofunctor has both an initial algebra and a final coalgebra and they are canonically isomorphic.) The only algebraically compact ccc is the degenerated category, so we ask for it not to be a ccc but to be a reflective subcategory of an ambient ccc. To get off the ground for a (flat) natural numbers object, N, we ask that the algebraically compact category have finite coproducts. Then the answer is, essentially, that every recursive function appears as an endomorphism of N. To make this precise, define a "point" of N to be a map thereto from the terminator, a "standard point" to be either the 0-point or one of its successors. Any endomorphism on N induces a partial endomorphism on the standard points. The result is that every recursive partial function is induced by an endomorphism on N. There is a missing word, I'm afraid, in that paragraph. The assumption should be that the algebraically compact category is a reflective _lluf_ subcategory of a ccc (that is, the two categories have the same objects). If that word is left out, we are stuck with the fact that the full subcategory of the terminator is always a reflective algebraically compact subcategory (of any category with a terminator). Let S be the reflection of the terminator (I denoted it with sigma in the Como and Durham papers). Let N be the initial algebra for the functor \X. S+X ( "\" for lambda, + for the coproduct in the algebraically compact subcategory, denoted as "wedge" in the Como/Durham papers). The result stands as now stated, where 0:1 -> N is the composition 1 -> S -> S+N -> N (the first arrow is the reflector, the second is from the coproduct structure and the third is the algebra structure on N) and the successor map N -> N is N -> S+N -> N (the first arrow is from the coproduct structure, and the second is the algebra structure on N). The proof requires the existence a fixed-point operator, that is, a dinatural transformation from \X.(X=>X) to \X.X. A proof is in the Durham paper, which paper contains, I submit, a positive answer to Streicher's question:
Can one axiomatize this situation in a sufficiently strong way, e.g. that one can transfer the exponentiation functor from the category of predomains to the category of domains and strict maps ?
The answer is the theory of algebraically compact categories with finite coproducts which appear as reflective lluf subcategories of ccc's. =========================================================================