Church-Turing Thesis

computation

Definition

Church-Turing Thesis (Function)

If a function is computable in any concrete sense, then it is already computable on a Turing machine.

Church-Turing Thesis (Language)

If there exists a finitely describable procedure for the exact specification of a formal language $L$, then there exists a Turing machine that accepts $L$.

Church-Turing Thesis (Register Machine, Shepherdson & Sturgis)

If an arithmetic function is informally computable, then it is also computable on a register machine.

Church-Turing Thesis ( Church)

If an arithmetic function is informally computable, then it is representable as lambda abstraction and computable in lambda calculus (lambda definable).

Origins

From Functions to Formal Languages

Formal languages and functions can be translated into each other:

• Language ($u\subseteq {\Sigma }^{\ast }$) $\to$ characteristic function ${\Sigma }^{\ast }\to \{0,1\}$
• Functions ${\mathbb{N}}^k\to {\mathbb{N}}^m$ or $({\Sigma }^{\ast }{)}^k\to ({\Sigma }^{\ast }{)}^m$ are sets of tuples, therefore representable as sets of words - that is, as languages.

The restriction to $\mathbb{N}$ or to strings from $\{0,1{\}}^{\ast }$ is irrelevant for the fundamental computability or decidability.

Church and Turing were motivated to find a negative solution to Hilbert’s problems.

An informal model for computability is enough to find a positive instance for a problem. To prove an existence-algorithm, one just exhibit one (give clear step). Any reasonable model of computation will implement it, so an informal description is enough.

However, finding a negative solution is equivalent to “there is no procedure”, which is an all-statement (proof of incomputability). To prove that an all-algorithm fails, one must say what counts as an algorithm in the first place. Otherwise, someone could claim a different, not-yet-described “procedure” works. Hence, they needed a precise model (Turing machines, Lambda abstractions) and then prove within that model no machine can solve it (e.g. Halting Problem).

They wanted negative answers (no decision method for certain problems). A precise model lets you quantify over all procedures and close loopholes. For positive answers, giving one concrete algorithm settles it.

• Church proposed Lambda calculus in 1936.
• Turing proposed the Turing machine in 1936.