The topos of recursive sets, or, for short, the recursive topos , is a Grothendieck topos that provides a cartesian closed context to do higher order recursion theory in. It can be viewed as a discrete analogue to the topological topos.
Let be the monoid of all total recursive functions under concatenation viewed as a category with one object . Consider the coverage whose covers consist of finite families of maps such that .
The recursive topos is defined as .
is a local topos i.e. the global section functor has a right adjoint: .
This appears as prop.1.5 in Mulry (1982). maps a set to the sheaf of sequences of elements in .
The object of Dedekind real numbers corresponds to the sheaf of sequences of real numbers satisfying:
For all there exists a finite recursive cover such that for all in , .
This is prop.4.1 in Mulry (1982).
The recursive topos was introduced in
A comparison with the effective topos is in chapter 6 of
See also
Peter Johnstone, Sketches of an Elephant vol. I, Oxford UP 2002. (example A2.1.11(k), p.81)
F. William Lawvere, Diagonal arguments and cartesian closed categories , pp.134-145 in LNM 92 Springer Heidelberg 1969. (Reprinted with author’s commentary as TAC Reprint 15 (2006))
P. S. Mulry, Adjointness in recursion ,
APAL 32 (1986), pp.281–289.
P. S. Mulry, A categorical approach to the theory of computation ,
APAL 43 (1989), pp.293–305.
P. S. Mulry, Partial map classifiers and partial cartesian closed categories , Theor. Comp. Sci. 136 (1994) pp.109–123.
Last revised on November 2, 2016 at 18:22:54. See the history of this page for a list of all contributions to it.