# An axiomatic theory of computational models?

There are many different computational models, e.g. Turing machines, register machines, lambda calculus, etc.

I am wondering if there exists an axiomatization of computation, that abstracts away from the specifically constructed computational model.

I.e. is there a more general theory about computation that deals with computational machines that are not perfectly specified, but that still captures their common characteristic as computation machines?

• I'm not really sure what you mean. What's the difference between an "axiomatization of computation" and a "computational model"? Surely, any axiomatization would be a model of computation? – David Richerby Jun 1 '18 at 16:55
• @DavidRicherby, I'm not sure what there is to explain about this. Obviously I can't tell you exactly what I'm looking for, because then I would have already invented it. But I am wondering if there is a theory of which the specific computational models (turing machines, lambda calculus, etc), are examples. Clearly, there is a difference between an (axiomatic) theory and a constructed model. A model is not an axiomatization, wouldn't you agree? In the same way that the structure arithmetic is not the same thing as Peano arithmetic, which is not a structure but a set of axioms in FOL – user56834 Jun 1 '18 at 17:44
• For example, a specific group, (let's say the integers with addition), is not the same as the theory of groups, which is an incomplete set of axioms (incomplete in the sense that there are sentences not implied by the axioms, nor their negation is implied). This is what it means for a theory to apply to multiple models... – user56834 Jun 1 '18 at 17:46
• Well, in the sense that the definition of "computable" is "there's a Turing machine that does it", a (Turing-complete) model of computation is essentially an axiomatization of computation; indeed, that's what Turing invented his model for. I suppose it's possible that, in the converse direction (which is what you're asking) there could be axiomatizations that aren't models but it's not really clear to me what they would mean. – David Richerby Jun 1 '18 at 17:51
• @DavidRicherby, So your answer is "I don't that anything like that exists". it's not really clear to me what it looks like either, otherwise I wouldn't need to ask this question. – user56834 Jun 1 '18 at 17:55

As far as I can understand you, you are looking for a general theory of computation (so, not a model that "contains other, for what's that supposed to mean, nor an "axiomatization" of a specific thing). One such theory is offered by partial combinatory algebras (PCA), which are very simple structures that subsume many models of computation, including: Turing machines (with and without oracles), $\lambda$-calculus (with many of its extensions), enumeration operators, and even topological models of computation. There are further variants of PCAs: ordered PCAs, typed PCAs, etc.