Is it known which functions from N to N are representable in an algebraically closed ccc? (A ccc in which initial algebras for "all" endofunctors exist. "all" includes at least those definable by x and => and those arising from initial algebras like e.g. the List functor. More precisely are there functions representable in F, which aren't in an algebraically closed category? -Martin Hofmann =========================================================================
A simply typed lambda-calculus with types x, =>, and natural numbers can express functions N->N equivalently to those provably total in first order Peano arithmetic (cf. [Girard 89]). This encompass, e.g., the Ackermann function. Though I do not remember any reference, I do not think that more expressive power in terms of functions N->N is gained by adding other initial algebras, like List. You might also be interested in Tatsuya Hagino's categorical programming language CPL ([Hagino 87][Wraith 89][Dybkj{\ae}r 91]) which is based on (restricted) initial and final dialgebras (a dialgebra is an arrow f: F(A)->G(A) where F,G:C->D are functors). Dialgebras make it possible to define initial and final algebras, products, coproducts, and exponentials from scratch. ---Hans Dybkj{\ae}r Dybkj{\ae}r, Hans [1991]: "Category Theory, Types, and Programming Languages", PhD thesis, DIKU, University of Copenhagen, May 1991. Tecnical report 91/11. Girard, Jean-Yves, Yves Lafont, and Paul Taylor [1989]: "Proofs and Types", Cambridge University Press. Hagino, Tatsuya [1987]: "A Categorical Programming Language", PhD thesis, LFCS, University of Edinburgh, September 1987. Technical report CST-47-87. Wraith, Gavin C. [1989]: "A Note on Categorical Datatypes", in "Category Theory and Computer Science, Manchester UK, September 1989", Proceedings, edited by David H. Pitt et al., Springer-Verlag, LNCS 389. =========================================================================
In "Re: Algebraically Complete Categories" dybkjaer@euler.ruc.dk (Hans Dybkjaer) writes: Though I do not remember any reference, I do not think that more expressive power in terms of functions N->N is gained by adding other initial algebras , like List. If we restrict our attention to initial algebras for a *polynomial* functor this is true, but in fact if we have an initial algebra for the functor T(X)=1+X+(N=>X) (Coquand-Huet's ordinal notations) we can express the functions $F_{\epsilon_0}$ [1] and even $F_{\Gamma_0}$ [2], where F_ denotes the fast growing hierarchy. These functions are not expressible in G"odel's T. I conjecture that algebraically complete categories are at least as expressive as system F. -- Martin Hofmann References: [1] T. Coquand and C. Paulin-Mohring: "Inductively defined types" in LNCS 389 [2] J. Gallier: "What's so special about Kruskal's theorem and the ordinal $\Gamma_0$" in Annals of pure and applied logic (July 1991) =========================================================================
Martin Hofmann asks: Is it known which functions from N to N are representable in an algebraically closed ccc? (A ccc in which initial algebras for "all" endofunctors exist.) 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. Since there is something of a free structure for this theory we can not expect to get more than the recursive. To return to the original question: does someone have a counterexample to back up Hans Dybkjaer's comment: Though I do not remember any reference, I do not think that more expressive power in terms of functions N->N is gained by adding other initial algebras =========================================================================
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 ? I guess one needs a little bit more assumptions : e.g. that the category of predomains contains the reflective subcat of domains and strict maps which in turn contains the category of total strict maps (by the lift functor) which is equivalent to the category of predomains . 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 ? Thomas Streicher =========================================================================
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. =========================================================================
participants (4)
-
dybkjaer＠euler.ruc.dk -
mxh%dcs.edinburgh.ac.UK＠QUCDN.QueensU.CA -
pjf＠saul.cis.upenn.edu -
Thomas Streicher