how to formalize the class(?) of computational models and their equivalence

Question

Introductory books to theoretical computer science usually introduce a the Turing machine and some of its variants, as well as the Random Access machine as computational models. Sometimes more specialized or even exotic systems (such as quantum computers) can be found briefly sketched.

The equivalence of these models ( say two models A and B ) is usually proven by mimicing the mechanics of A with the "gears" of B and then providing "cheap" conversion functions which convert input of A to input B and output of B back to output A - the same is then done for A and B reversed.

Whereas proofs provide valid statements about well-defined mathematical objects, I don't think they prove what is ought to be proved, namely the equivalance of two computational models, because that question is non mathematically defined. I doubt that this can be done.

First of all, the conversion functions between the different input/output formats cannot necessarily be formalized as computations, because they act in "both worlds" (say binary strings and a cell setting in the game of life), and thus require a new computational model for themselves. Hence at least two further computational models are introduced. The triviality of the conversion functions doesn't seem be formalized. - One might argue that the conversions are the most vital part of the proof, because the "mimicry" of one model A within another model B has no mathematicly well-defined relation with the model A.

Second, I wonder whether the "class" of computational models can be formalized. I don't think it is a set, because, for example, you could build several Turing machines with 0 and 1 represented by arbitrary inequal sets. - One might define a category of computational models, with the arrows, say from object A to object B, present when A can be simulated by B. This raises the question what we would want the objects to be. I do not know.

I regard these points, (i) non having a formal definition for the conversion functions to be trivial, (ii) having no definition of a (Turing-equivalent) model of computation as unsatisfying.

Does anybody know whether and how this has been treated in literature so far? I am aware this touches what to understand the question of what to call "computation", but so do the usual practices in computer science anyway, in my opinion.

Answer 1

I recommend that you look at realizability theory. In realizability computational models are known as partial combinatory algebras (PCA). They cover a wide range of computational models. There is a 2-category of PCAs in which we can speak not only of equivlence, but also about general morphisms from one computational model to another.

Some references:

1. Jaap van Oosten's book on realizability.
2. John Longley's Ph.D. thesis.

John's Ph.D. is probably the best source to read about comparison of PCAs. An abridged version can be found in my Ph.D. thesis.

I should point out that realizability theory is just one way of organizing and structuring the world of computational models in a mathematically precise way. Nevertheless, it is a very sophisticated machinery which shows what can be done.

Answer 2

We have to first decide about the domain of inputs and outputs, and how they are represented by what is given to the machine and what machine outputs.

AFAIU, your questions is essentially about what is considered a reasonable representations of elements of a structure using inputs and outputs of the machines in the model (strings in TM case, natural numbers in RAM case, ...).

There is considerable amount of literature on this, search for "naming systems", "representations", etc.

After we agree on what is a reasonable way of coding/representing the objects in a structure using the input and output objects of the machine model the rest can be done complete mathematical rigor.

As an example, consider partial functions from natural numbers to natural numbers, and TM and RAM model. RAM model gets its inputs as integer variables, TM model gets them as strings over $\{0,1,b \}$. We have to first agree on how we are encoding the natural numbers in each model. For RAM let's take the trivial encoding, for TM the binary encoding of the natural numbers. After we agree on the encodings the rest is completely formal, any partial function over natural numbers computable in the RAM model is computable in the TM model using the above encodings.

All of this can be state clearly but many think that getting into these encoding stuff will distract and take unnecessary time from the main topics of an undergrad course in computability/complexity, when students intuition about these is good enough to deal with the main topics of the course there is not a need to complicate things by mentioning encodings, numberings, representations, naming systems, etc.