There are mainly two frameworks to carry out computability investigations over general spaces. The one is domain theory, the other is representation theory. The first one (see [Eda97] for instance) uses order theory and has nice categorical properties, but does not handle mathematical objects from the classical point of view. The second one (see [Wei00]) applies to topological spaces but uses a rather heavy language, everything being expressed in terms of Turing machines and symbols (representations are ways to encode objects into symbolic sequences).

Our goal is to develop a language which is closer to the classical mathematical one, in order to take advantage of the mathematical intuitions one has when starting to work in computability theory. Of course, our framework is much inspired by the two frameworks mentioned above which are rich in ideas and results. We are guided by the following principle: a mathematical space shall be handled from the first or the second point of view, depending on the natural structure which comes with it (an order or a topology). We introduce the rather elementary structure of enumerative lattice from which all constructivity notions on general spaces can be derived. It enables one to express computability proofs in a more algebraic fashion, freeing oneself from coding questions. The structure of enumerative lattice enables one to carry out important constructions in a straightforward way:
1. construction of effective enumerations. Effective enumerations are recurrent in computer science (the first one being the enumeration of Turing machines) and can be reduced to a general abstract result,
2. conversion of algorithms into extensional algorithms,
3. extension of partial functions to total functions,
4. constructivity relative to non-constructive objects can be easily expressed.

We assume that the reader is familiar with recursion theory on the natural numbers. We recall some basic concepts that will be intensively used along this thesis. For more details, we refer the reader to a standard text [Rog87]. On the set of natural numbers, recursion theory provides a robust notion of recursive function i.e. possibly partial functions which can be ”effectively computed”. There are bijective functions hi: N k → N which are effective in the sense that the projections π k i : N → N defined by π k i (hn1, . . . , nki) = ni are recursive. An essential property of recursive functions is their effective enumerability: there is an enumeration {φe : e ∈ N} of this set such that not only φe is recursive, but the function f : he, ni 7→ φe(n) is recursive. In other words, there is a universal recursive function φu which simulates all recursive functions. We will say that φe is recursive uniformly in e: there is a single recursive function which computes φe when it is provided with e. One of the most important notions of recursion theory is the notion of recursively enumerable (r.e.) subset of N. E ⊆ N is recursively enumerable if there is a recursive function φ such that E = imφ = {φ(n) : n ∈ N}. The effective enumeration of all the recursive functions induces an effective enumeration: Ee = imϕe. We recall some well-known facts which prove to be very useful:

1. If E = imφ it is possible to construct, in a uniform way, a recursive function ψ such that E = domψ. In other words, there is a total recursive function f such that imφe = domφf(e) . We say that φf(e) semi-decides E: it can be thought of as an algorithm which tests if an element belongs to E and stops exactly when it is true.
2. The conversion is also possible in the other direction: there is a total recursive function g such that domφe = imφg(e) .
3. There is a total recursive function h such that imφe = imφh(e) and φh(e) is total when Ee is non-empty.

The existence of a universal recursive function φu induces the existence of a r.e. set E which is universal in the sense that Ee = {n : hn, ei ∈ E} for all e. Indeed, let E = imf where f is the recursive function defined by f(he, ni) = hn, ϕe(n)i.

Among the historical models of effective procedures, some work on the natural numbers (recursive functions), some work on finite symbolic sequences (Turing machines). Modulo effective encoding, these two classes of mathematical objects are equivalent. Godel ¨ initiated this by encoding logical formulas into integers in order for encoding and decoding to be effective (he modeled effectivity by primitive recursion). This is now a very common principle, intensively used by programmers: expressive programming languages internally represent discrete objects as graphs, trees, formulas by binary strings.