In computability theory, the Church–Turing thesis is a thesis about the nature of computable functions. It states that a function on the natural numbers can be calculated by an effective method if and only if it is computable by a Turing machine. The thesis is named after American mathematician Alonzo Church and the British mathematician Alan Turing. Before the precise definition of computable function, mathematicians often used the informal term effectively calculable to describe functions that are computable by paper-and-pencil methods. In the 1930s, several independent attempts were made to formalize the notion of computability:
In 1933, Kurt Gödel, with Jacques Herbrand, formalized the definition of the class of general recursive functions: the smallest class of functions (with arbitrarily many arguments) that is closed under composition, recursion, and minimization, and includes zero, successor, and all projections. In 1932–33, Alonzo Church created a method for defining functions called the λ-calculus. Within λ-calculus, he defined an encoding of the natural numbers called the Church numerals. A function on the natural numbers is called λ-computable if the corresponding function on the Church numerals can be represented by a term of the λ-calculus. In 1935–36, Alonzo Church formalized the concept of effectively calculable functions by proposing that they are general recursive functions, or, equivalently, λ-definable functions. In 1936, before learning of Church's work, Alan Turing created a theoretical model for machines, now called Turing machines, that could carry out calculations from inputs by manipulating symbols on a tape. Given a suitable encoding of the natural numbers as sequences of symbols, a function on the natural numbers is called Turing computable if some Turing machine computes the corresponding function on encoded natural numbers. Turing proposed that effectively calculable functions be defined as those that are Turing computable.
Church, Kleene, and Turing proved that these three formally defined classes of computable functions coincide: a function is λ-computable if and only if it is Turing computable, and if and only if it is general recursive. This has led mathematicians and computer scientists to believe that the concept of computability is accurately characterized by these three equivalent processes. Other formal attempts to characterize computability have subsequently strengthened this belief (see below).
On the other hand, the Church–Turing thesis states that the above three formally defined classes of computable functions coincide with the informal notion of an effectively calculable function. Although the thesis has near-universal acceptance, it cannot be formally proven, as the concept of effective calculability is only informally defined.
Since its inception, variations on the original thesis have arisen, including statements about what can physically be realized by a computer in our universe (physical Church-Turing thesis) and what can be efficiently computed (Church–Turing thesis (complexity theory)). These variations are not due to Church or Turing, but arise from later work in complexity theory and digital physics. The thesis also has implications for the philosophy of mind (see below).
Statement in Church's and Turing's words
addresses the notion of "effective computability" as follows: "Clearly the existence of CC and RC [meaning Church's and Rosser's proofs of the statement that there is no effective method for deciding truth] presupposes a precise definition of 'effective'. 'Effective method' is here used in the rather special sense of a method each step of which is precisely predetermined and which is certain to produce the answer in a finite number of steps". in . Thus the adverb-adjective "effective" is used in a sense of "1a: producing a decided, decisive, or desired effect", and "capable of producing a result".See also which also gives these definitions for "effective" – the first ["producing a decided, decisive, or desired effect"] as the definition for sense "1a" of the word "effective", and the second ["capable of producing a result"] as part of the "Synonym Discussion of EFFECTIVE" there, (in the introductory part, where it summarizes the similarities between the meanings of the words "effective", "effectual", "efficient", and "efficacious").
In the following, the words "effectively calculable" will mean "produced by any intuitively 'effective' means whatsoever" and "effectively computable" will mean "produced by a Turing-machine or equivalent mechanical device". Turing's "definitions" given in a footnote in his 1938 Ph.D. thesis Systems of Logic Based on Ordinals, supervised by Church, are virtually the same:
The thesis can be stated as: Every effectively calculable function is a computable function. states it this way: "What is effectively calculable is computable." He calls this "Church's Thesis". Church wrote that the notion of an effectively calculable function of positive integers should be identified "with the notion of a recursive function of positive integers (or of a λ-definable function of positive integers)".
Turing stated it this way:
History
One of the important problems for logicians in the 1930s was the of David Hilbert and Wilhelm Ackermann, Published in English translation as Principles of Mathematical Logic (1950). Providence, Rhode Island, USA: AMS Chelsea Publishing. which asked whether there was a mechanical procedure for separating mathematical truths from mathematical falsehoods. This quest required that the notion of "algorithm" or "effective calculability" be pinned down, at least well enough for the quest to begin.Davis's commentary before in . Church uses the words "effective calculability" on page 100ff. But from the very outset Alonzo Church's attempts began with a debate that continues to this day.In his review of Church's Thesis after 70 Years edited by Adam Olszewski et al. 2006, Peter Smith's criticism of a paper by Muraswski and Wolenski suggests 4 "lines" re the status of the Church–Turing Thesis: (1) empirical hypothesis, (2) axiom or theorem, (3) definition, (4) explication. But Smith opines that (4) is indistinguishable from (3). the notion of "effective calculability" to be (i) an "axiom or axioms" in an axiomatic system, (ii) merely a definition that "identified" two or more propositions, (iii) an empirical hypothesis to be verified by observation of natural events, or (iv) just a proposal for the sake of argument (i.e. a "thesis")?
Circa 1930–1952 In the course of studying the problem, Church and his student Stephen Kleene introduced the notion of λ-definable functions, and they were able to prove that several large classes of functions frequently encountered in number theory were λ-definable.Footnote 3 in An Unsolvable Problem of Elementary Number Theory, in . The debate began when Church proposed to Gödel that one should define the "effectively computable" functions as the λ-definable functions. Gödel, however, was not convinced and called the proposal "thoroughly unsatisfactory".. Rather, in correspondence with Church (c. 1934–1935), Gödel proposed axiomatizing the notion of "effective calculability"; indeed, in a 1935 letter to Kleene, Church reported that:
But Gödel offered no further guidance. Eventually, he would suggest his recursion, modified by Herbrand's suggestion, that Gödel had detailed in his 1934 lectures in Princeton, New Jersey (Kleene and Rosser transcribed the notes). But he did not think that the two ideas could be satisfactorily identified "except heuristically"., quoting from the 1935 letter written by Church to Kleene, Footnote 3 in in .
Next, it was necessary to identify and prove the equivalence of two notions of effective calculability. Equipped with the λ-calculus and "general" recursion, Kleene with help of Church and J. Barkley Rosser produced proofs (1933, 1935) to show that the two calculi are equivalent. Church subsequently modified his methods to include use of Herbrand–Gödel recursion and then proved (1936) that the is unsolvable: there is no algorithm that can determine whether a well formed formula has a beta normal form. in
Many years later in a letter to Davis (c. 1965), Gödel said that "he was, at the time of these lectures, not at all convinced that his concept of recursion comprised all possible recursions".Davis's commentary before in . By 1963–1964 Gödel would disavow Herbrand–Gödel recursion and the λ-calculus in favor of the Turing machine as the definition of "algorithm" or "mechanical procedure" or "formal system".For a detailed discussion of Gödel's adoption of Turing's machines as models of computation, see
A hypothesis leading to a natural law?: In late 1936 Alan Turing's paper (also proving that the is unsolvable) was delivered orally, but had not yet appeared in print.. On the other hand, Emil Post's 1936 paper had appeared and was certified independent of Turing's work.Editor's footnote to Post 1936 Finite Combinatory Process. Formulation I. at . Post strongly disagreed with Church's "identification" of effective computability with the λ-calculus and recursion, stating:
Rather, he regarded the notion of "effective calculability" as merely a "working hypothesis" that might lead by inductive reasoning to a "natural law" rather than by "a definition or an axiom".Post 1936 in . This idea was "sharply" criticized by Church..
Thus, Post in his 1936 paper was also discounting Gödel's suggestion to Church in 1934–1935 that the thesis might be expressed as an axiom or set of axioms..
Turing adds another definition, Rosser equates all three: Within just a short time, Turing's 1936–1937 paper "On Computable Numbers, with an Application to the " appeared. In it he stated another notion of "effective computability" with the introduction of his a-machines (now known as the Turing machine abstract computational model). In a proof-sketch added as an appendix to his 1936–1937 paper, Turing showed that the classes of functions defined by λ-calculus and Turing machines coincided.Turing 1936–1937 in Church was quick to recognise how compelling Turing's analysis was. In his review of Turing's paper he made clear that Turing's notion made "the identification with effectiveness in the ordinary (not explicitly defined) sense evident immediately"..
In a few years (1939) Turing would propose, like Church and Kleene before him, that his formal definition of mechanical computing agent was the correct one.Turing 1939 in Davis:160. Thus, by 1939, both Church (1934) and Turing (1939) had individually proposed that their "formal systems" should be definitions of "effective calculability";Church 1934 in , also Turing 1939 in . neither framed their statements as theses.
Rosser (1939) formally identified the three notions-as-definitions:
Kleene proposes Thesis I: This left the overt expression of a "thesis" to Kleene. In 1943 Kleene proposed his "Thesis I": in (footnotes omitted).
The Church–Turing Thesis: Stephen Kleene, in Introduction to Metamathematics, finally goes on to formally name "Church's Thesis" and "Turing's Thesis", using his theory of recursive realizability, having switched from presenting his work in the terminology of Church–Kleene lambda definability to that of Gödel–Kleene recursiveness (partial recursive functions). In this transition, Kleene modified Gödel's general recursive functions to allow for proofs of the unsolvability of problems in the intuitionism of E. J. Brouwer. In his graduate textbook on logic, "Church's thesis" is introduced and basic mathematical results are demonstrated to be unrealizable. Next, Kleene proceeds to present "Turing's thesis", where results are shown to be uncomputable, using his simplified derivation of a Turing machine based on the work of Emil Post. Both theses are proven equivalent by use of "Theorem XXX".