Turing machines vs. other models of computation

Posted on October 30, 2014 by Tommy McGuire
Labels: theory, math

Every once in a while, I hear someone complain about the fascination with Turing Machines, in comparison with other models of computation such as lambda calculus, general recursive functions (well, ok, maybe not that one), etc.

The following is Philip Wadler's answer, from "Propositions as Types", an otherwise equally good paper:

Turing’s most significant difference from Church was not in logic or mathematics but in philosophy. Whereas Church merely presented the definition of λ-definability and baldly claimed that it corresponded to effective calculability, Turing undertook an analysis of the capabilities of a “computer”—at this time, the term referred to a human performing a computation assisted by paper and pencil. Turing argued that the number of symbols must be finite (for if infinite, some symbols would be arbitrarily close to each other and undistinguishable), that the number of states of mind must be finite (for the same reason), and that the number of symbols under consideration at one moment must be bounded (“We cannot tell at a glance whether 9999999999999999 and 999999999999999 are the same”). Later, Gandy [16] would point out that Turing’s argument amounts to a theorem asserting that any computation a human with paper and pencil can perform can also be performed by a Turing Machine. It was Turing’s argument that finally convinced Gödel; since λ-definability, recursive functions, and Turing machines had been proved equivalent, he now accepted that all three defined “effectively calculable”.

In other words, a Turing Machine is built for an argument based on the capabilities of a human being, making the argument that it encodes effective calculation stronger. As in Gödel's case, it is not clear that lambda calculus does encode effective calculation.

Further, the Turing Machine formalism has a number of immediately-obvious extensions, such as multiple tapes, that are easily proven to be equivalent to the original machine. As a result, the subsequent, loose, argument that it is closed in power above further strengthens its argument.

active directory applied formal logic ashurbanipal authentication books c c++ comics conference continuations coq data structure digital humanities Dijkstra eclipse virgo electronics emacs goodreads haskell http java job Knuth ldap link linux lisp math naming nimrod notation OpenAM osgi parsing pony programming language protocols python quote R random REST ruby rust SAML scala scheme shell software development system administration theory tip toy problems unix vmware yeti
Member of The Internet Defense League
Site proudly generated by Hakyll.