Can we formalize the operational/denotational semantics of a Turing Machine? Is there any formalization in literature?

  • 2
    $\begingroup$ Isn't a universal Turing machine exactly that - a formalisation of the operational semantics of a Turing machine - since it can reproduce the behaviour of any Turing machine given any input ? $\endgroup$
    – gandalf61
    May 6, 2020 at 11:27
  • $\begingroup$ yes but it's a little confusing. Consider a While language (if, assignments, lops, concatenation). Can a universal program written in While language be the semantics? I'm not about this. $\endgroup$ May 6, 2020 at 15:44
  • $\begingroup$ @gandalf61: No, a universal Turing machine is not a formalization of Turing machines. That would establish a vicious circle, as you would still have to formalize the universal Turing machine, but you cannot state its properties without having first formalized Turing machines. $\endgroup$ Oct 18, 2020 at 9:24

1 Answer 1


The usual definitions of Turing machines are given in terms of formal semantics. For instance, the Wikipedia definition describes Turing machines in precise mathematical formalism. If you are looking for something even more formal, have a look at this Coq formalization of Turing machines.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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