Misplaced Pages

#495504

66-516: In computability theory , the Church–Turing thesis (also known as computability thesis , the Turing–Church thesis , the Church–Turing conjecture , Church's thesis , Church's conjecture , and Turing's 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

132-591: 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 : Church, Kleene , and Turing proved that these three formally defined classes of computable functions coincide:

198-431: A " natural law " rather than by "a definition or an axiom". This idea was "sharply" criticized by Church. Thus Post in his 1936 paper was also discounting Kurt 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

264-574: A (multi-tape) universal Turing machine only suffers a logarithmic slowdown factor in simulating any Turing machine. Computability theory (computation) Too Many Requests If you report this error to the Wikimedia System Administrators, please include the details below. Request from 172.68.168.133 via cp1102 cp1102, Varnish XID 545615740 Upstream caches: cp1102 int Error: 429, Too Many Requests at Thu, 28 Nov 2024 05:40:55 GMT Entscheidungsproblem By

330-409: A Turing Machine". Turing stated it this way: It was stated ... that "a function is effectively calculable if its values can be found by some purely mechanical process". We may take this literally, understanding that by a purely mechanical process one which could be carried out by a machine. The development ... leads to ... an identification of computability with effective calculability. [

396-494: A Turing machine based on the work of Emil Post. Both theses are proven equivalent by use of "Theorem XXX". Thesis I. Every effectively calculable function (effectively decidable predicate) is general recursive . 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 ... Turing's thesis: Turing's thesis that every function which would naturally be regarded as computable

462-448: 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 ). J. B. Rosser  ( 1939 ) addresses the notion of "effective computability" as follows: "Clearly

528-689: A finite set of Aristotelean logic formulas, it is NLOGSPACE -complete to decide its S a t {\displaystyle {\rm {Sat}}} . It is also NLOGSPACE-complete to decide S a t {\displaystyle {\rm {Sat}}} for a slight extension (Theorem 2.7): ∀ x , ± p ( x ) → ± q ( x ) , ∃ x , ± p ( x ) ∧ ± q ( x ) {\displaystyle \forall x,\pm p(x)\to \pm q(x),\quad \exists x,\pm p(x)\wedge \pm q(x)} Relational logic extends Aristotelean logic by allowing

594-405: 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,

660-1463: A relational predicate. For example, "Everybody loves somebody" can be written as ∀ x , b o d y ( x ) , ∃ y , b o d y ( y ) ∧ l o v e ( x , y ) {\textstyle \forall x,{\rm {{body}(x),\exists y,{\rm {{body}(y)\wedge {\rm {{love}(x,y)}}}}}}} . Generally, we have 8 kinds of sentences: ∀ x , p ( x ) → ( ∀ y , q ( x ) → ± r ( x , y ) ) , ∀ x , p ( x ) → ( ∃ y , q ( x ) ∧ ± r ( x , y ) ) ∃ x , p ( x ) ∧ ( ∀ y , q ( x ) → ± r ( x , y ) ) , ∃ x , p ( x ) ∧ ( ∃ y , q ( x ) ∧ ± r ( x , y ) ) {\displaystyle {\begin{aligned}\forall x,p(x)\to (\forall y,q(x)\to \pm r(x,y)),&\quad \forall x,p(x)\to (\exists y,q(x)\wedge \pm r(x,y))\\\exists x,p(x)\wedge (\forall y,q(x)\to \pm r(x,y)),&\quad \exists x,p(x)\wedge (\exists y,q(x)\wedge \pm r(x,y))\end{aligned}}} It

726-407: A result". 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: We shall use

SECTION 10

#1732772455496

792-485: A rigorous, formal proof. To establish that a function is computable by Turing machine, it is usually considered sufficient to give an informal English description of how the function can be effectively computed, and then conclude "by the Church–Turing thesis" that the function is Turing computable (equivalently, partial recursive). Dirk van Dalen gives the following example for the sake of illustrating this informal use of

858-464: A series of constraints on the behavior of a computor —"a human computing agent who proceeds mechanically". These constraints reduce to: The matter remains in active discussion within the academic community. 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". The case for viewing

924-515: A set of axioms which would embody the generally accepted properties of this notion, and to do something on that basis. 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 NJ (Kleene and Rosser transcribed the notes). But he did not think that the two ideas could be satisfactorily identified "except heuristically". Next, it

990-516: A successful mechanical calculating machine , dreamt of building a machine that could manipulate symbols in order to determine the truth values of mathematical statements. He realized that the first step would have to be a clean formal language , and much of his subsequent work was directed toward that goal. In 1928, David Hilbert and Wilhelm Ackermann posed the question in the form outlined above. In continuation of his "program", Hilbert posed three questions at an international conference in 1928,

1056-412: Is NEXPTIME -complete (Theorem 3.18). With x , y , z {\displaystyle x,y,z} , it is RE -complete to decide its S a t {\displaystyle {\rm {Sat}}} , and co-RE-complete to decide F i n S a t {\displaystyle {\rm {FinSat}}} (Theorem 3.15), thus undecidable. The monadic predicate calculus

1122-464: Is NLOGSPACE -complete to decide its S a t {\displaystyle {\rm {Sat}}} (Theorem 2.15). Relational logic can be extended to 32 kinds of sentences by allowing ± p , ± q {\displaystyle \pm p,\pm q} , but this extension is EXPTIME -complete (Theorem 2.24). The first-order logic fragment where the only variable names are x , y {\displaystyle x,y}

1188-424: Is a general method for determining whether 'Un(it)' is provable, then there is a general method for determining whether 'it' ever prints 0". The work of both Church and Turing was heavily influenced by Kurt Gödel 's earlier work on his incompleteness theorem , especially by the method of assigning numbers (a Gödel numbering ) to logical formulas in order to reduce logic to arithmetic. The Entscheidungsproblem

1254-903: Is a hierarchy of decidabilities. On the top are the undecidable problems. Below it are the decidable problems. Furthermore, the decidable problems can be divided into a complexity hierarchy. Aristotelian logic considers 4 kinds of sentences: "All p are q", "All p are not q", "Some p is q", "Some p is not q". We can formalize these kinds of sentences as a fragment of first-order logic: ∀ x , p ( x ) → ± q ( x ) , ∃ x , p ( x ) ∧ ± q ( x ) {\displaystyle \forall x,p(x)\to \pm q(x),\quad \exists x,p(x)\wedge \pm q(x)} where p , q {\displaystyle p,q} are atomic predicates, and + q := q , − q := ¬ q {\displaystyle +q:=q,\;-q:=\neg q} . Given

1320-418: Is also undecidable. Some notations: S a t ( Φ ) {\displaystyle {\rm {{Sat}(\Phi )}}} means the problem of deciding whether there exists a model for a set of logical formulas Φ {\displaystyle \Phi } . F i n S a t ( Φ ) {\displaystyle {\rm {{FinSat}(\Phi )}}}

1386-463: Is argued, any machine must satisfy". 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". 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

SECTION 20

#1732772455496

1452-533: Is computable under his definition, i.e. by one of his machines, is equivalent to Church's thesis by Theorem XXX. 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. An attempt to better understand

1518-401: Is correct. In fact, Gödel (1936) proposed something stronger than this; he observed that there was something "absolute" about the concept of "reckonable in S 1 ": It may also be shown that a function which is computable ['reckonable'] in one of the systems S i , or even in a system of transfinite type, is already computable [reckonable] in S 1 . Thus the concept 'computable' ['reckonable']

1584-416: 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 ... as a definition of it ... ...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

1650-417: Is in a certain definite sense 'absolute', while practically all other familiar metamathematical concepts (e.g. provable, definable, etc.) depend quite essentially on the system to which they are defined ... Proofs in computability theory often invoke the Church–Turing thesis in an informal way to establish the computability of functions while avoiding the (often very long) details which would be involved in

1716-522: Is no computable function which decides, for two given λ-calculus expressions, whether they are equivalent or not. He relied heavily on earlier work by Stephen Kleene . Turing reduced the question of the existence of an 'algorithm' or 'general method' able to solve the Entscheidungsproblem to the question of the existence of a 'general method' which decides whether any given Turing machine halts or not (the halting problem ). If 'algorithm'

1782-463: Is no way to extend the notion of computable function." All these contributions involve proofs that the models are computationally equivalent to the Turing machine; such models are said to be Turing complete . Because all these different attempts at formalizing the concept of "effective calculability/computability" have yielded equivalent results, it is now generally assumed that the Church–Turing thesis

1848-428: Is now known as the counter machine model. In the late 1960s and early 1970s researchers expanded the counter machine model into the register machine , a close cousin to the modern notion of the computer . Other models include combinatory logic and Markov algorithms . Gurevich adds the pointer machine model of Kolmogorov and Uspensky (1953, 1958): "... they just wanted to ... convince themselves that there

1914-614: Is of considerable interest for program verification and circuit verification. Pure Boolean logical formulas are usually decided using SAT-solving techniques based on the DPLL algorithm . For more general decision problems of first-order theories, conjunctive formulas over linear real or rational arithmetic can be decided using the simplex algorithm , formulas in linear integer arithmetic ( Presburger arithmetic ) can be decided using Cooper's algorithm or William Pugh 's Omega test . Formulas with negations, conjunctions and disjunctions combine

1980-534: Is related to Hilbert's tenth problem , which asks for an algorithm to decide whether Diophantine equations have a solution. The non-existence of such an algorithm, established by the work of Yuri Matiyasevich , Julia Robinson , Martin Davis , and Hilary Putnam , with the final piece of the proof in 1970, also implies a negative answer to the Entscheidungsproblem . Using the deduction theorem ,

2046-575: Is the class of first-order formulas with quantifier prefix ∃ ⋯ ∃ ∀ ⋯ ∀ {\displaystyle \exists \cdots \exists \forall \cdots \forall } , equality symbols, and no function symbols . For example, Turing's 1936 paper (p. 263) observed that since the halting problem for each Turing machine is equivalent to a first-order logical formula of form ∀ ∃ ∀ ∃ 6 {\displaystyle \forall \exists \forall \exists ^{6}} ,

Church–Turing thesis - Misplaced Pages Continue

2112-402: Is the footnote quoted above.] One of the important problems for logicians in the 1930s was the Entscheidungsproblem of David Hilbert and Wilhelm Ackermann , 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

2178-631: Is the fragment where each formula contains only 1-ary predicates and no function symbols. Its S a t {\displaystyle {\rm {Sat}}} is NEXPTIME-complete (Theorem 3.22). Any first-order formula has a prenex normal form. For each possible quantifier prefix to the prenex normal form, we have a fragment of first-order logic. For example, the Bernays–Schönfinkel class , [ ∃ ∗ ∀ ∗ ] = {\displaystyle [\exists ^{*}\forall ^{*}]_{=}} ,

2244-466: Is the same problem, but for finite models. The S a t {\displaystyle {\rm {Sat}}} -problem for a logical fragment is called decidable if there exists a program that can decide, for each Φ {\displaystyle \Phi } finite set of logical formulas in the fragment, whether S a t ( Φ ) {\displaystyle {\rm {{Sat}(\Phi )}}} or not. There

2310-400: Is understood as meaning a method that can be represented as a Turing machine, and with the answer to the latter question negative (in general), the question about the existence of an algorithm for the Entscheidungsproblem also must be negative (in general). In his 1936 paper, Turing says: "Corresponding to each computing machine 'it' we construct a formula 'Un(it)' and we show that, if there

2376-403: Is unsolvable: there is no algorithm that can determine whether a well formed formula has a beta normal form . 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". By 1963–1964 Gödel would disavow Herbrand–Gödel recursion and the λ-calculus in favor of

2442-504: The Entscheidungsproblem is impossible, assuming that the intuitive notion of " effectively calculable " is captured by the functions computable by a Turing machine (or equivalently, by those expressible in the lambda calculus ). This assumption is now known as the Church–Turing thesis . The origin of the Entscheidungsproblem goes back to Gottfried Leibniz , who in the seventeenth century, after having constructed

2508-459: 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

2574-499: The Church–Turing thesis: Example: Each infinite recursively enumerable (RE) set contains an infinite recursive set . Proof: Let A be infinite RE. We list the elements of A effectively, n 0 , n 1 , n 2 , n 3 , ... From this list we extract an increasing sublist: put m 0  = n 0 , after finitely many steps we find an n k such that n k > m 0 , put m 1  = n k . We repeat this procedure to find m 2 > m 1 , etc. this yields an effective listing of

2640-607: The Entscheidungsproblem encompasses the more general problem of deciding whether a given first-order sentence is entailed by a given finite set of sentences, but validity in first-order theories with infinitely many axioms cannot be directly reduced to the Entscheidungsproblem. Such more general decision problems are of practical interest. Some first-order theories are algorithmically decidable ; examples of this include Presburger arithmetic , real closed fields , and static type systems of many programming languages . On

2706-601: The Entscheidungsproblem" 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). And 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. 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

Church–Turing thesis - Misplaced Pages Continue

2772-486: The Turing machine as the definition of "algorithm" or "mechanical procedure" or "formal system". A hypothesis leading to a natural law? : In late 1936 Alan Turing 's paper (also proving that the Entscheidungsproblem 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. Post strongly disagreed with Church's "identification" of effective computability with

2838-473: The above example completely rigorous, one would have to carefully construct a Turing machine, or λ-function, or carefully invoke recursion axioms, or at best, cleverly invoke various theorems of computability theory. But because the computability theorist believes that Turing computability correctly captures what can be computed effectively, and because an effective procedure is spelled out in English for deciding

2904-509: 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. Kleene having switched from presenting his work in

2970-412: The completeness theorem of first-order logic , a statement is universally valid if and only if it can be deduced using logical rules and axioms, so the Entscheidungsproblem can also be viewed as asking for an algorithm to decide whether a given statement is provable using the rules of logic . In 1936, Alonzo Church and Alan Turing published independent papers showing that a general solution to

3036-486: The difficulties of satisfiability testing with that of decision of conjunctions; they are generally decided nowadays using SMT-solving techniques, which combine SAT-solving with decision procedures for conjunctions and propagation techniques. Real polynomial arithmetic, also known as the theory of real closed fields , is decidable; this is the Tarski–Seidenberg theorem , which has been implemented in computers by using

3102-439: The existence of CC and RC (Church's and Rosser's proofs) 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". Thus the adverb-adjective "effective" is used in a sense of "1a: producing a decided, decisive, or desired effect", and "capable of producing

3168-425: The expression "computable function" to mean a function calculable by a machine, and let "effectively calculable" refer to the intuitive idea without particular identification with any one of these definitions. The thesis can be stated as: Every effectively calculable function is a computable function . Church also stated that "No computational procedure will be considered as an algorithm unless it can be represented as

3234-503: The list the functions " reckonable in the system S 1 " of Kurt Gödel 1936, and Emil Post 's (1943, 1946) " canonical [also called normal ] systems ". In the 1950s Hao Wang and Martin Davis greatly simplified the one-tape Turing-machine model (see Post–Turing machine ). Marvin Minsky expanded the model to two or more tapes and greatly simplified the tapes into "up-down counters", which Melzak and Lambek further evolved into what

3300-436: The machine, and (3) deterministic behavior—he produces a theorem that "What can be calculated by a device satisfying principles I–IV is computable." 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". In his 1997 and 2002 work Sieg presents

3366-454: 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) ... which it

SECTION 50

#1732772455496

3432-467: 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. Thus, by 1939, both Church (1934) and Turing (1939) had individually proposed that their "formal systems" should be definitions of "effective calculability"; neither framed their statements as theses . Rosser (1939) formally identified

3498-460: The other hand, the first-order theory of the natural numbers with addition and multiplication expressed by Peano's axioms cannot be decided with an algorithm. By default, the citations in the section are from Pratt-Hartmann (2023). The classical Entscheidungsproblem asks that, given a first-order formula, whether it is true in all models. The finitary problem asks whether it is true in all finite models. Trakhtenbrot's theorem shows that this

3564-551: The problem S a t ( ∀ ∃ ∀ ∃ 6 ) {\displaystyle {\rm {{Sat}(\forall \exists \forall \exists ^{6})}}} is undecidable. The precise boundaries are known, sharply: Börger et al. (2001) describes the level of computational complexity for every possible fragment with every possible combination of quantifier prefix, functional arity, predicate arity, and equality/no-equality. Having practical decision procedures for classes of logical formulas

3630-402: The quest to begin. But from the very outset Alonzo Church 's attempts began with a debate that continues to this day. Was 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

3696-408: The sake of argument (i.e. a "thesis")? 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. The debate began when Church proposed to Gödel that one should define the "effectively computable" functions as

3762-460: The set B, the computability theorist accepts this as proof that the set is indeed recursive. The success of the Church–Turing thesis prompted variations of the thesis to be proposed. For example, the physical Church–Turing thesis states: "All physically computable functions are Turing-computable." The Church–Turing thesis says nothing about the efficiency with which one model of computation can simulate another. It has been proved for instance that

3828-459: The subset B={m 0 , m 1 , m 2 ,...} of A, with the property m i < m i+1 . Claim . B is decidable. For, in order to test k in B we must check if k = m i for some i. Since the sequence of m i 's is increasing we have to produce at most k+1 elements of the list and compare them with k. If none of them is equal to k, then k not in B. Since this test is effective, B is decidable and, by Church's thesis , recursive. In order to make

3894-612: 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

3960-423: The thesis as nothing more than a definition is made explicitly by Robert I. Soare , 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 . Other formalisms (besides recursion, the λ-calculus , and the Turing machine ) have been proposed for describing effective calculability/computability. Kleene (1952) adds to

4026-400: The third of which became known as "Hilbert's Entscheidungsproblem ". In 1929, Moses Schönfinkel published one paper on special cases of the decision problem, that was prepared by Paul Bernays . As late as 1930, Hilbert believed that there would be no such thing as an unsolvable problem. Before the question could be answered, the notion of "algorithm" had to be formally defined. This

SECTION 60

#1732772455496

4092-535: The three notions-as-definitions: All three definitions are equivalent, so it does not matter which one is used. Kleene proposes Thesis I : This left the overt expression of a "thesis" to Kleene. In 1943 Kleene proposed his "Thesis I": This heuristic fact [general recursive functions are effectively calculable] ... led Church to state the following thesis. The same thesis is implicit in Turing's description of computing machines. Thesis I. Every effectively calculable function (effectively decidable predicate)

4158-413: The λ-calculus and recursion, stating: 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… blinds us to the need of its continual verification. Rather, he regarded the notion of "effective calculability" as merely a "working hypothesis" that might lead by inductive reasoning to

4224-434: 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: 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

4290-483: Was done by Alonzo Church in 1935 with the concept of "effective calculability" based on his λ-calculus , and by Alan Turing the next year with his concept of Turing machines . Turing immediately recognized that these are equivalent models of computation . A negative answer to the Entscheidungsproblem was then given by Alonzo Church in 1935–36 ( Church's theorem ) and independently shortly thereafter by Alan Turing in 1936 ( Turing's proof ). Church proved that there

4356-411: 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 Entscheidungsproblem

#495504