12
$\begingroup$

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.

Thanks in advance.

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

Improve this question
$\endgroup$
3
  • $\begingroup$ I would appreciate a definition if you don't mind too much. Thanks for offering it. $\endgroup$
    – Harry Gindi
    Commented Apr 18, 2010 at 14:25
  • $\begingroup$ Ok. Give me a while. $\endgroup$
    – Doctor Gibarian
    Commented Apr 18, 2010 at 14:26
  • 1
    $\begingroup$ 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? $\endgroup$
    – Andrej Bauer
    Commented Apr 19, 2010 at 13:37

3 Answers 3

Reset to default
13
$\begingroup$

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 :-)

Improve this answer
$\endgroup$
1
  • $\begingroup$ 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? $\endgroup$
    – Doctor Gibarian
    Commented Apr 20, 2010 at 14:45
8
$\begingroup$

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.

Improve this answer
$\endgroup$
2
$\begingroup$

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/

Improve this answer
$\endgroup$
0

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .