1
$\begingroup$

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?

Improve this question
$\endgroup$
8
  • 2
    $\begingroup$ 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? $\endgroup$
    – David Richerby
    Commented Jun 1, 2018 at 16:55
  • $\begingroup$ @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 $\endgroup$
    – user56834
    Commented Jun 1, 2018 at 17:44
  • $\begingroup$ 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... $\endgroup$
    – user56834
    Commented Jun 1, 2018 at 17:46
  • 1
    $\begingroup$ 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. $\endgroup$
    – David Richerby
    Commented Jun 1, 2018 at 17:51
  • $\begingroup$ @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. $\endgroup$
    – user56834
    Commented Jun 1, 2018 at 17:55

1 Answer 1

Reset to default
4
$\begingroup$

The question "what is a computational model" is quite open ended and is difficult to answer definitely. It's a bit like asking "what is geometry". But people have given some answers.

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.

One should never just "collect models of computation" but also ask how to relate them, so we should think about transformations between PCAs. John Longley gave a very good account of these, namely the applicative morphisms. Speaking a bit vaguely, an applicative morphism is an interpretr of one PCA implemented in another PCA.

If you are interested in this topic you can consul Jaap van Oosten's book on realizability.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.