[FOM] Simple Turing machines, Universality, Encodings, etc.

[Andrej Bauer]

Richard Heck wrote:
> Could someone say a few more words about this? I find this idea very 
> interesting, but don't know anything about it and don't have easy access 
> to any of these papers.

As already mentioned by Vaughan Pratt, there are several ways of making
computability theory "more abstract". Some possible approaches I have
seen are described below. I am going to mention people's names from my
memory because I do not have all the relevant materials with me. Please
correct me and fill in the gaps. I would very much like to hear about
relevant work that was not mentioned by Vaughan Pratt or me.

If we look at different developments of the theory of computable
functions (e.g., partial recursive functions, Turing machines, and
lambda calculus) we might notice that they all use similar constructions
such as:
- pairing functions, for encoding pairs of things as single things
- partial application of functions of several arguments
- facilities for performing unbounded computation
- dove-tailing (how to interleave an unbounded number of computations)
- interpreters that simulate other computations

Instead of setting up a particluar model of computation we might
axiomatize these constructions directly, with the intention of obtaining
a more widely applicable and conceptually cleaner theory. People have
come up with many ways of doing this. Broadly, we may divide the various
approaches into "computability in the small" and "computability in the
large", altough many are a mix of both.

In "computability in the small" we want to explain what computation is,
what it means to perform computation, and what the basic properties of
computation are.

In "computability in the large" we want to capture some aspect of
computability that is not just computation, for example the effect that
computability has on other parts of mathematics (logic, topology, analysis).

Some approaches are (references are listed below):

(1) Friedman's equational theory [2] uses pairing functions, and if I am
not mistaken a universal function.

(2) Moschovakis and Fenstad [1,5] base their development on the basic
notion of _subcomputation_.

(3) Category-theoretic approach by Di Paola and Heller with their
dominical categories.

(4) Others, mentioned by Vaughan Pratt.

(5) Logical form: the computable sets and functions are those that are
definable in prescribed form, say as "Sigma 0 1" formulae or by
particular recursion schema.

(6) The theory of admissible sets, as popularized by Ershov, is another
example of "computability in logical form", with rich model theory and
study of computable structures.

(7) Richman's formulation [7] of computable functions in Bishop-style
constructive mathematics: (partial) computable functions are those that
have an enumerable graph + the axiom "partial computable functions form
an enumerable set". Richman (with Bridges in later work [0]) derive both
basic results of computability theory as well as the effects of the
axiom on constructive mathematics.

(8) Category-theoretic constructions in which a universe (a category, a
topos) is built specifically to facilitate the study of computability
and computable mathematics, such as the recursive topos by Mulry [6] and
the effective topos by Hyland [3], see also [4] and [8].

(9) As a corollary to (7) and (8) I dare mention my own contribution [9]
in which I show that very simple axioms suffice to get quite a bit of
basic computability. Some theorems, say the Recursion Theorem, do not
even require _any_ (specialized) axioms.

Best regards,

Andrej Bauer


References:

[0] Bridges, D., Richman, F., Varieties of Constructive Mathematics,
Lecture Notes Ser., 97, London Math. Soc., 1987.

[1] Fenstad, J., On axiomatizing recursion theory, in: J.E. Fenstadt et
al., editor, Generalized Recursion Theory, North Holland, 1974 pp. 385--404.

[2] Friedman, H., Axiomatic recursive function theory, in: Gandy et al.,
editor, Logic Colloquium '69 (1971), pp. 113--137.

[3] Hyland, J., The effective topos, in: A. Troelstra and D. V. Dalen,
editors, The L.E.J. Brouwer Centenary Symposium (1982), pp. 165--216.

[4] McCarty, D., "Realizability and Recursive Mathematics", D.Phil.
Thesis, University of Oxford (1984).

[5] Moschovakis, Y., Axioms for computation theories -- first draft, in:
Gandy et al., editor, Logic Colloquium '69 (1971), pp. 199--255.

[6] Mulry, P., Generalized Banach-Mazur functionals in the topos of
recursive sets, Journal of Pure and Applied Algebra 26 (1982), pp. 71--83.

[7] Richman, F., Church’s thesis without tears, The Journal of Symbolic
Logic 48 (1983), pp. 797--803.

[8] Rosolini, G., "Continuity and Effectiveness in Topoi," Ph.D. thesis,
University of Oxford (1986).

[9] http://math.andrej.com/category/synthetic-computability/, in
particular have a look at the slides for the MFPS tutorial.