## 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 2010 at 14:25
Ok. Give me a while. – Doctor Gibarian Apr 18 2010 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 2010 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 2010 at 14:45

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/

-