Editing Church–Turing thesis (section)

==History==
{{Main|History of the Church–Turing thesis}}

One of the important problems for logicians in the 1930s was the {{lang|de|[[Entscheidungsproblem]]}} of [[David Hilbert]] and [[Wilhelm Ackermann]],<ref>{{cite book |first1=David |last1=Hilbert |first2=Wilhelm |last2=Ackermann |title=Grundzüge der theoretischen Logik |trans-title=Fundamentals of Theoretical Logic |language=de |location=Berlin, Germany |publisher=Springer |orig-year=1st ed. 1928 |edition=6th |year=1972 |isbn=3-540-05843-5}} Published in English translation as ''Principles of Mathematical Logic'' (1950). Providence, Rhode Island, USA: AMS Chelsea Publishing.</ref> 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.<ref>Davis's commentary before {{harvnb|Church|1936}}{{ambiguous|date=March 2025}} in {{harvcolnb|Davis|1965|p=88}}. Church uses the words "effective calculability" on page 100ff.</ref> But from the very outset [[Alonzo Church]]'s attempts began with a debate that continues to this day.<ref>In his review of ''Church's Thesis after 70 Years'' edited by Adam Olszewski et al. 2006, [[Peter Smith (computer scientist)|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). {{cite web |last=Smith |first=Peter |date=2007-07-11 |title=Church's Thesis after 70 Years |url=http://www.logicmatters.net/resources/pdfs/CTT.pdf |work=Logic Matters}}<!--SPS exception as subject-matter expert--></ref> {{clarify span|Was|reason=It should be made clear who asked the question (Peter Smith, mentioned in the previous footnote?).  (revised March 2024)|date=March 2019}} 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 Cole Kleene|Stephen Kleene]] introduced the notion of [[Lambda calculus|λ-definable functions]], and they were able to prove that several large classes of functions frequently encountered in number theory were λ-definable.<ref>Footnote 3 in {{harvnb|Church|1936a}} ''An Unsolvable Problem of Elementary Number Theory'', in {{harvcolnb|Davis|1965|page=89}}.</ref> 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".<ref>{{harvcolnb|Dawson|1997|page=99}}.</ref> 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:

{{Blockquote|His [Gödel's] only idea at the time was that it might be possible, in terms of effective calculability as an undefined notion, to state a set of axioms which would embody the generally accepted properties of this notion, and to do something on that basis.<ref name="sieg160"/>}}

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 [[J. B. Rosser|Rosser]] transcribed the notes). But he did not think that the two ideas could be satisfactorily identified "except heuristically".<ref>{{harvcolnb|Sieg|1997|p=160}},{{missing long citation|date=March 2025}} quoting from the 1935 letter written by Church to Kleene, Footnote 3 in {{harvnb|Gödel|1934}} in {{harvcolnb|Davis|1965|page=44}}.</ref>

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 {{lang|de|[[Entscheidungsproblem]]}} is unsolvable: there is no algorithm that can determine whether a [[well formed formula]] has a [[beta normal form]].<ref>{{harvnb|Church|1936}}{{ambiguous|date=March 2025}} in {{harvcolnb|Davis|1965|pages=105ff.}}</ref>

Many years later in a letter to Davis (c. 1965), Gödel said that "he was, at the time of these [1934] lectures, not at all convinced that his concept of recursion comprised all possible recursions".<ref>Davis's commentary before {{harvnb|Gödel|1934}} in {{harvcolnb|Davis|1965|page=40}}.</ref> 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".<ref>For a detailed discussion of Gödel's adoption of Turing's machines as models of computation, see {{cite book |last=Shagrir |first=Oron |author-link=Oron Shagrir | title=Church's Thesis After 70 Years |chapter=Gödel on Turing on Computability |publisher=De Gruyter | date=2006-06-15 |pages=393–419 |isbn=978-3-11-032494-5 | doi=10.1515/9783110325461.393 |chapter-url=http://moon.cc.huji.ac.il/oron-shagrir/papers/Goedel_on_Turing_on_Computability.pdf |access-date=2016-02-08 |url-status=dead |archive-url=https://web.archive.org/web/20151217145831/http://moon.cc.huji.ac.il/oron-shagrir/papers/Goedel_on_Turing_on_Computability.pdf |archive-date=2015-12-17}}</ref>

'''A hypothesis leading to a natural law?''': In late 1936 [[Alan Turing]]'s paper (also proving that the {{lang|de|[[Entscheidungsproblem]]}} is unsolvable) was delivered orally, but had not yet appeared in print.<ref name="On Computable">{{Harvnb|Turing|1937a}}.</ref> On the other hand, [[Emil Post]]'s 1936 paper had appeared and was certified independent of Turing's work.<ref>Editor's footnote to Post 1936 ''Finite Combinatory Process. Formulation I.'' at {{harvcolnb|Davis|1965|page=289}}.</ref> Post strongly disagreed with Church's "identification" of effective computability with the λ-calculus and recursion, stating:

{{quote|Actually the work already done by Church and others carries this identification considerably beyond the working hypothesis stage. But to mask this identification under a definition&nbsp;... blinds us to the need of its continual verification.<ref>Post 1936 in {{harvcolnb|Davis|1965|page=291}}, footnote 8.</ref>}}

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".<ref>Post 1936 in {{harvcolnb|Davis|1952|p=291}}.</ref> This idea was "sharply" criticized by Church.<ref>{{harvcolnb|Sieg|1997|pp=171 and 176–177}}.{{missing long citation|date=March 2025}}</ref>

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.<ref name="sieg160">{{harvcolnb|Sieg|1997|p=160}}.{{missing long citation|date=March 2025}}</ref>

'''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 {{lang|la|italic=no|Entscheidungsproblem}}"<ref name="On Computable"/> 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.<ref>Turing 1936–1937 in {{harvcolnb|Davis|1965|pages=263ff.}}</ref> 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".<ref>{{harvnb|Church|1937}}.</ref>

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.<ref>Turing 1939 in Davis:160.{{year needed|date=March 2025}}</ref> Thus, by 1939, both Church (1934) and Turing (1939) had individually proposed that their "formal systems" should be ''definitions'' of "effective calculability";<ref>Church 1934 in {{harvcolnb|Davis|1965|page=100}}, also Turing 1939 in {{harvcolnb|Davis|1965|page=160}}.</ref> neither framed their statements as ''theses''.

Rosser (1939) formally identified the three notions-as-definitions:

{{quote|All three ''definitions'' are equivalent, so it does not matter which one is used.<ref>Italics added, {{harvnb|Rosser|1939}} in {{harvcolnb|Davis|1965|page=226}}.</ref>}}

'''Kleene proposes ''Thesis I''''': This left the overt expression of a "thesis" to Kleene. In 1943 Kleene proposed his "Thesis I":<ref name="Davis274">{{harvnb|Kleene|1943|page=60}} in {{harvcolnb|Davis|1965|page=274}}. Footnotes omitted.</ref>

{{quote|This heuristic fact [general recursive functions are effectively calculable]&nbsp;... led Church to state the following thesis. The same thesis is implicit in Turing's description of computing machines.
{{quote|style=font-size:inherit;quotes:none;|Thesis I. ''Every effectively calculable function (effectively decidable predicate) is general recursive'' [Kleene's italics]}}
Since a precise mathematical definition of the term effectively calculable (effectively decidable) has been wanting, we can take this thesis&nbsp;... as a definition of it&nbsp;...}}
{{quote|...the thesis has the character of an hypothesis—a point emphasized by Post and by Church. If we consider the thesis and its converse as definition, then the hypothesis is an hypothesis about the application of the mathematical theory developed from the definition. For the acceptance of the hypothesis, there are, as we have suggested, quite compelling grounds.}}

'''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".

{{quote|style=font-size:inherit;quotes:none|Thesis I. ''Every effectively calculable function (effectively decidable predicate) is general recursive''.<ref>{{harvcolnb|Kleene|1952|page=300}}.</ref>}}

{{quote|style=font-size:inherit;quotes:none|Theorem XXX: The following classes of partial functions are coextensive, i.e. have the same members: (a) the partial recursive functions, (b) the computable functions&nbsp;...<ref name="Kleene_1952_p376">{{harvcolnb|Kleene|1952|page=376}}.</ref>}}

{{quote|style=font-size:inherit;quotes:none|Turing's thesis: Turing's thesis that every function which would naturally be regarded as computable is computable under his definition, i.e. by one of his machines, is equivalent to Church's thesis by Theorem XXX.<ref name="Kleene_1952_p376"/>}}

Kleene, finally, uses for the first time the term the "Church-Turing thesis" in a section in which he helps to give clarifications to concepts in Alan Turing's paper "The Word Problem in Semi-Groups with Cancellation", as demanded in a critique from William Boone.<ref>{{harvcolnb|Kleene|1952|pages=382, 536}}</ref>

=== Later developments ===
An attempt to better understand the notion of "effective computability" led [[Robin Gandy]] (Turing's student and friend) in 1980 to analyze ''machine'' computation (as opposed to human-computation acted out by a Turing machine). Gandy's curiosity about, and analysis of, [[cellular automata]] (including [[Conway's game of life]]), parallelism, and crystalline automata, led him to propose four "principles (or constraints)&nbsp;... which it is argued, any machine must satisfy".<ref>{{harvcolnb|Gandy|1980|pages=123ff.}}</ref> His most-important fourth, "the principle of causality" is based on the "finite velocity of propagation of effects and signals; contemporary physics rejects the possibility of instantaneous action at a distance".<ref>{{harvcolnb|Gandy|1980|page=135}}</ref> From these principles and some additional constraints—(1a) a lower bound on the linear dimensions of any of the parts, (1b) an upper bound on speed of propagation (the velocity of light), (2) discrete progress of the machine, and (3) deterministic behavior—he produces a theorem that "What can be calculated by a device satisfying principles I–IV is computable."<ref>{{harvcolnb|Gandy|1980|page=126}}</ref>

In the late 1990s [[Wilfried Sieg]] analyzed Turing's and Gandy's notions of "effective calculability" with the intent of "sharpening the informal notion, formulating its general features axiomatically, and investigating the axiomatic framework".<ref>Sieg 1998–1999 in {{harvcolnb|Sieg|Sommer|Talcott|2002|pages=390ff.}}; also {{harvcolnb|Sieg|1997|pp=154ff.}}</ref> In his 1997 and 2002 work Sieg presents a series of constraints on the behavior of a ''computor''—"a human computing agent who proceeds mechanically". These constraints reduce to:

*"(B.1) (Boundedness) There is a fixed bound on the number of symbolic configurations a computor can immediately recognize.
*"(B.2) (Boundedness) There is a fixed bound on the number of internal states a computor can be in.
*"(L.1) (Locality) A computor can change only elements of an observed symbolic configuration.
*"(L.2) (Locality) A computor can shift attention from one symbolic configuration to another one, but the new observed configurations must be within a bounded distance of the immediately previously observed configuration.
*"(D) (Determinacy) The immediately recognizable (sub-)configuration determines uniquely the next computation step (and id [instantaneous description])"; stated another way: "A computor's internal state together with the observed configuration fixes uniquely the next computation step and the next internal state."<ref>In a footnote Sieg breaks Post's 1936 (B) into (B.1) and (B.2) and (L) into (L.1) and (L.2) and describes (D) differently. With respect to his proposed [[Gandy machine]] he later adds LC.1, LC.2, GA.1 and GA.2. These are complicated; see Sieg 1998–1999 in {{harvcolnb|Sieg|Sommer|Talcott|2002|pages=390ff.}}</ref>

The matter remains in active discussion within the academic community.<ref>A collection of papers can be found in {{harvtxt|Olszewski|Woleński|Janusz|2006}}. Also a review of this collection: {{cite web |author-first=Peter |author-last=Smith |date=2007-07-11 |title=Church's Thesis after 70 Years |url=http://www.logicmatters.net/resources/pdfs/CTT.pdf}}</ref><ref>See also {{cite web |url=http://www.turing.org.uk/publications/ct70.pdf |title=Did Church and Turing Have a Thesis about Machines? |last=Hodges |first=Andrew |date=2005 |access-date=2014-07-27 |archive-url=https://web.archive.org/web/20160304032827/http://www.turing.org.uk/publications/ct70.pdf |archive-date=2016-03-04 |url-status=dead}}</ref>

=== The thesis as a definition ===
The thesis can be viewed as nothing but an ordinary mathematical definition. Comments by Gödel on the subject suggest this view, e.g. "the correct definition of mechanical computability was established beyond any doubt by Turing".<ref>{{cite book |last=Gödel |first=Kurt |author-link=Kurt Gödel |orig-date=193? |section=Undecidable Diophantine Propositions |section-url={{google books|gDzbuUwma5MC|page=164|plainurl=yes}} |title=Collected Works |url={{google books|gDzbuUwma5MC|plainurl=yes}} |volume=3 |page=[{{google books|gDzbuUwma5MC|page=168|plainurl=yes}} 168] |editor-last=Feferman |editor-first=Solomon |editor-link=Solomon Feferman |date=1995 |publisher=[[Oxford University Press]] |location=New York |isbn=978-0-19-507255-6 |oclc=928791907}}</ref> The case for viewing the thesis as nothing more than a definition is made explicitly by [[Robert I. Soare]],<ref name="Soare">{{cite journal |first=Robert I. |last=Soare |author-link=Robert I. Soare |date=September 1996 |title=Computability and Recursion |journal=Bulletin of Symbolic Logic |volume=2 |issue=3 |pages=284–321 |doi=10.2307/420992 |jstor=420992 |citeseerx=10.1.1.35.5803|s2cid=5894394 }}</ref> where it is also argued that Turing's definition of computability is no less likely to be correct than the epsilon-delta definition of a [[continuous function]].