A popular model for doing Computable Analysis are Turing machines. The tape configuration and interpretation of mathematical structures are described as follows.
A Type 2 Turing Machine is a Turing machine with three tapes: An input tape which is read-only; a working tape which can be written to and read from; and, notably, an output tape which is "append-only".
Real numbers
In this context, real numbers are represented as arbitrary infinite sequences of symbols. These sequences could for instance represent the digits of a real number. Such sequences need not be computable. On the other hand, the programs that act on these sequences doneed to be computable in a reasonable sense.
Computable functions
Computable functions are represented as programs on a Type 2 Turing Machine. A program is considered total if it takes finite time to write any number of symbols on the output tape regardless of the input. The programs run forever, generating increasingly more digits of the output.
Names
Results about computability associated with infinite sets often involve namings, which are maps between those sets and recursive representations of subsets thereof.
Discussion
The issue of Type 1 versus Type 2 computability
Type 1 computability is the naive form of computable analysis in which one restricts the inputs to a machine to be computable numbers instead of arbitrary real numbers. The difference between the two models lies in the fact that a function which is well-behaved over computable numbers is not necessarily well-behaved over arbitrary real numbers. For instance, there are continuous and computable functions over the computable real numbers which are total, but which map some closed intervals to unbounded open intervals. These functions clearly cannot be extended to arbitrary real numbers without making them partial, as doing so would violate the Extreme value theorem. Since that sort of behaviour could be considered pathological, it is natural to insist that a function should only be considered total if it is total over all real numbers, not just the computable ones.
Realisability
In the event that one is unhappy with using Turing Machines, there is a realisability topos called the Kleene-Vesley topos in which one can reduce computable analysis to constructive analysis. This constructive analysis includes everything that is valid in the Brouwer school, and not just the Bishop school.
One of the basic results of computable analysis is that every computable function from to is continuous. Taking this further, this suggests that there is an analogy between basic notions in topology and basic notions in computability:
Computable functions are analogous to continuous functions.
Co-semideciable sets are analogous to closed sets.
There is a computable analogue of topological compactness. Namely, a subset of is computably compact if it there is a semi-decision procedure "" that, given a semidecidable predicate as input, semi-decides whether every point in the set satisfies the predicate.
The above notion of computable compactness satisfies an analogue of the Heine-Borel theorem. In particular, the unit interval is computably compact.
Discrete sets in topology are analogous to sets in computability where equality between elements is semi-decidable.
Hausdorff sets in topology are analogous to sets in computability where inequality between elements is semi-decidable.
The analogy suggests that general topology and computability are nearly mirror images of each other. The analogy can be explained by using the fact that computability theory and general topology can both be performed using constructive logic.
