The difference between the Recursive and the Effective topos.

I would like to know which is the real difference between the Recursive topos (in the sense of Mulry) and the Effective topos (in the sense of Hyland). Especially what is related to recursive functions. Do they have the same semantic power? I will be gratefull with some hints about texts related to this.

PS: I don't give definitions because of their big extension, but I could give them if anybody wants.

-
I would appreciate a definition if you don't mind too much. Thanks for offering it. – Harry Gindi Apr 18 '10 at 14:25
Ok. Give me a while. – Doctor Gibarian Apr 18 '10 at 14:26
The toposes are not equivalent. Can you be a bit more specific about whatsort of difference you would like to hear about? In terms of their categorical properties? In terms of their internal language? What do you want to use these toposes for? – Andrej Bauer Apr 19 '10 at 13:37

Your question is a bit unclear, but an obvious difference between these two toposes is that the Recursive Topos is a topos of sheaves, hence cocomplete, wherease the Effective topos only has finite (non-trivial) coproducts. For example, the natural numbers object in the Effective topos is not a countable coproduct of 1's.

If you are looking for a deeper explanation, then perhaps it is fair to say that the Recursive Topos models computability a la Banach-Mazur (a map is computable if it takes computable sequences to computable sequences) and the Effective topos models computability a la Kleene (a map is computable if it is realized by a Turing machine). In many respects Kleene's notion of computability is better, but you'll have to ask another question to find out why :-)

-
What I know is that in both topos recursive functions can be represented. The problem for me is: though in Eff is quite easy to see how is it done (because recursive realizability is a quite easy concept) in Rec everything is harder. One reason is that Mulry's papers are more difficult to find than Hyland's. This is why I ask for (open, free) references. At the same time I would like to join Krishnaswami question here:mathoverflow.net/questions/21947/… made after mine. Thank you, A. Bauer, and...have you Mulry's key papers? – Doctor Gibarian Apr 20 '10 at 14:45

I am aware that I am answering an old question, but for completeness of MathOverflow, I'd like to point out that G. Rosolini's 1986 thesis "Continuity and effectiveness in topoi" contains (chapter 6) a description of both the effective and the recursive topoi, and a comparison of them by constructing a functor from the effective to the recursive (preserving limits, finite coproducts, images and the natural number object, faithful on the full subcategory of countable objects and full and faithful on the full subcategory of countable separated objects). According to the author, "the major difference between the effective topos and the recursive topos is that the [natural number object] in [the effective topos] does not generate the topos", and the functor takes an object of the effective topos to the set of maps from the natural numbers object to it, which can be viewed as an object of the recursive topos.

-

As far as I now (correct me if I'm wrong, please):

1 The recursive topos was introduced in "The topos of recursive sets", Thesis, Buffalo, 1980. It is $Rec=Sh_{J}(Set^{M^{op}})$ where:

-M is the monoid of total recursive functions in $\mathbb{N}$

-Sh relates to sheaves

-J is the canonical Grothendieck topology

One has to take some concrete ideals and pullbacks to have a representation of partial recursive functions through Rec.

2 For the Effective topos (introduced by Hyland in "The Effective Topos", Cambridge, 1982) I could suggest "An introduction to fibrations, the effective topos and modest sets" by W. Phoa and a shorter explanation in: http://xorshammer.com/2008/10/13/what-would-the-world-look-like-if-everything-was-computable-an-introduction-to-hylands-effective-topos/

-