Church–Turing thesis

From Wikipedia, the free encyclopedia

"Church's thesis" redirects here. See also Church's thesis (constructive mathematics).

In computability theory the Church–Turing thesis (also known as Church's thesis, Church's conjecture and Turing's thesis) is a combined hypothesis about the nature of effectively calculable (computable) functions by recursion (Church's Thesis), by mechanical device equivalent to a Turing machine (Turing's Thesis) or by use of Church's λ-calculus:

Church's Thesis: "Every effectively calculable function (effectively decidable predicate) is general[1] recursive" (Kleene 1952:300)
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." (Kleene 1952:376)

The three computational processes (recursion, λ-calculus, and Turing machine) were shown to be equivalent by Alonzo Church, Stephen Kleene and J.B. Rosser (1934-6)[2] and by Alan Turing (1936-7)[3]. Although Stephen Kleene proved the two theses equivalent, the fundamental premise behind the theses — the notion of "effectively computable" or "effectively calculable" — is "a vague intuitive one"[4] based as it is on (i) “heuristic [observational, experiential] evidence”, (ii) the “equivalence of 'diverse formulations'” (e.g. the three computational processes[5]) and (iii) on an observational analysis of a human with a pencil and paper following a set of rules (Turing's analysis[6]) and of a "worker" in boxes (Emil Post's analysis 1936[7][8]). Thus, as they stand, neither thesis can be proven.[4] The various notions for "effective calculability/computability" — the fly in the ointment — have been proposed as a "formal definition" by Church[9], Turing [10] and Rosser [11], as a "working hypothesis" leading by inductive reasoning to a "natural law" by Post[12] (an idea "sharply" criticized by Church[13]), or as an axiom or set of axioms (suggested by Kurt Gödel to Church in 1934-5[14] but discounted in Post 1936[14]).

Today the thesis has near-universal acceptance.

Informally the Church–Turing thesis states that if an algorithm (a procedure that terminates) exists then there is an equivalent Turing Machine or applicable λ-function[15] for that algorithm.

Contents

[edit] Formal statement

See also: Effectively calculable

In the following, the words "effectively[16] calculable" will mean "produced by any intuitively 'effective' means whatsoever" and "computable" will mean "produced by a Turing-machine or equivalent mechanical device".

Turing's 1939 "definitions" are virtually the same:

"†We shall use the expression "computable function" to mean a function calculable by a machine, and we let "effectively calculable" refer to the intuitive idea without particular identification with any one of these definitions." (cf the footnote † in Turing 1939 (his Ordinals paper) in Davis 1965:160).

The thesis can be stated as follows:

Every effectively calculable function is a computable function.[17]

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" († is the footnote above, ibid).

[edit] History

Main article: History of the Church-Turing thesis

[edit] 1930–1970

One of the important problems for logicians in the 1930s was David Hilbert's Entscheidungsproblem, which asked if there was a mechanical procedure for separating mathematical truths from mathematical falsehoods.

In the course of studying the problem, Alonzo 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. Church proposed to Kurt Gödel that one should define the "effectively computable" functions as the λ-definable functions. Kurt Gödel, however, was not convinced and called the proposal "thoroughly unsatisfactory"[18]. As a counter-proposal Gödel offered his (primitive) recursion, as modified by Herbrand's suggestion, that he (Gödel) had detailed in his 1934 lectures in Princeton NJ (Kleene and another student J. B. Rosser transcribed the notes.) Kleene, with help of Church and Rosser, then produced proofs to show that the two calculi are equivalent. Church modified his methods to include use of Herbrand-Gödel recursion and then proved that the Entscheidungsproblem is unsolvable: There is no generalized "effective calculation" (method, algorithm) that can determine whether or not a formula in either the recursive- or λ-calculus is "valid" (more precisely: that a well formed formula is in "normal form")[19].

Within a year, in his 1936-7 paper "On Computable Numbers, with an Application to the Entscheidungsproblem" Alan Turing asserted his notion of "effective computability" with the introduction of his a-machines (now known as the Turing machine abstract computational model). He proposed, like Church and Kleene before him, that his formal definition of mechanical computing agent was the correct one.[20]

In a proof-sketch added as an "Appendix" to his 1936-7 Turing showed that the classes of functions defined by λ-calculus and Turing machines coincided.[21] However, although Church's claim predated Turing's, it was Turing who, in the opinions of Gödel and others, finally gave a convincing argument for why these functions really contained all functions that one would be inclined to call "effectively computable". Indeed by the 1960's Gödel had become thoroughly convinced, writing about Alan Turing's machines:

"In consequence of later advances, in particular of the fact that due to A. M. Turing's work69 a precise and unquestionably adequate definition of the general notion of formal system70 can now be given ..."
"69 See Turing 1937, p. 249 [page number in original journal]
"70 In my opinion the term "formal system" or "formalism" should never be used for anything but this notion ... [of] formal systems in the proper sense of the term, whose characteristic property is that reasoning in them, in principle, can be completely replaced by mechanical devices."[22]

In a 1964 "Postscriptum" that he added to Davis's anthology The Undecidable, Gödel further expressed his opinion that recursion and the λ-calculus "are much less suitable for our purpose"[23] . Notice that in this "less suitable" category he is including his own Herbrand-Gödel recursion.[23]

Origin of the phrase "Church-Turing thesis" :

A definition describes "the meaning" of a word, word-group, or symbol; it has about it the notion of a dogmatic statement: unquestionable, decided. A thesis, on the other hand, is a proposition or proposal that one asserts and then defends by argument, or "an hypothesis" that is to be proved (or perhaps merely asserted without proof).

Both Church and Turing individually proposed their "formal systems" should be definitions of "effective calculability"[24]; neither framed their assertions as theses. Indeed Post 1936 disagreed with Church's assertion of his "definition" and insisted it should be a "working hypothesis".[25]) Rosser (1939) identified (that is: asserted the equivalence of) the three notions-as-definitions: "All three definitions are equivalent, so it does not matter which one is used."[26]

The overt expression of a "thesis" — an "hypothesis" — had to be left to Kleene. In his 1943 paper Recursive Predicates and Quantifiers Kleene proposed his "THESIS I":

"This heuristic fact [general recursive functions are effectively calculable]...led Church to state the following thesis(22). The same thesis is implicit in Turing's description of computing machines(23).
"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 ... as a definition of it..."[27]
"(22) references Church 1936
"(23) references Turing 1936-7

Kleene goes on to note that:

"...the thesis has the character of an hypothesis — a point emphasized by Post and by Church(24). 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."[27]
"(24) references Post 1936 of Post and Church's Formal definitions in the theory of ordinal numbers, Fund. Math. vol 28 (1936) pp.11-21 (see ref. #2, Davis 1965:286).

A few years later (1952) Kleene would overtly name, defend, express the two "theses" as quoted in the lead-in paragraph, and then "identify" them (show equivalence) by use of his Theorem XXX.

[edit] Later developments: Axiomatizing the notion of "effective calculation/computation"

Gōdel in correspondence with Church (ca 1934-5) proposed axiomatizing[28] "effective calculability" (Eventually Gōdel suggested to Church the use of Herbrand-Gōdel recursion as its definition; after Turing's 1936-7 he supported Turing's definition):

"...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" (Sieg 1997:160).

An attempt to understand the notion better 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", "Conway's game of life", "parallelism" and "crystalline automata" led him to propose four "principles (or constraints) ... which it is argued, any machine must satisfy."[29] 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 instaneous action at a distance."[30] 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.[31]".

In the late 1990's 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"[32]. In his 2002 he presents a series of constraints reduced to, roughly: "(B) Boundedness ... (L) Locality ... (D) Determinancy"[33].

[edit] Success of the thesis

Other formalisms (besides recursion, the lambda calculus, and the Turing machine) have been proposed for describing effective calculability/computability . Stephen Kleene (1952) adds to the list the functions " reckonable in the system S1" of Kurt Gödel 1936, and Emil Post's (1943, 1946) "canonical [also called normal] systems".[34] In the 1950's 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 is now known as the counter machine model. In the late 1960's and early 1970's researchers expanded the counter machine model into the register machine, a close cousins 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 is no way to extend the notion of computable function."[35]

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 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 S1":

"It may also be shown that a function which is computable ['reckonable'] in one of the systems Si, or even in a system of transfinite type, is already computable [reckonable] in S1. Thus the concept 'computable' ['reckonable'] 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"[36]

The success of the Church–Turing thesis prompted variations of the thesis to be proposed. For example, the Physical Church–Turing thesis (PCTT) states:

"Every function that can be physically computed can be computed by a Turing machine."

Another variation is the Strong Church–Turing Thesis (SCTT), which is not due to Church or Turing, but rather was realized gradually in the development of complexity theory. It states (cf. Bernstein, Vazirani 1997):

"Any 'reasonable' model of computation can be efficiently simulated on a probabilistic Turing machine."

The word 'efficiently' here means up to polynomial-time reductions. The Strong Church–Turing Thesis, then, posits that all 'reasonable' models of computation yield the same class of problems that can be computed in polynomial time. Assuming the conjecture that probabilistic polynomial time (BPP) equals deterministic polynomial time (P), the word 'probabilistic' is optional in the Strong Church–Turing Thesis.

If quantum computers are physically possible, they could invalidate the Strong Church–Turing Thesis, since it is also conjectured that quantum polynomial time (BQP) is larger than BPP. In other words, there are efficient quantum algorithms that perform tasks that are not known to have efficient probabilistic algorithms; for example, factoring integers. They would not however invalidate the original or Physical Church-Turing thesis, since a quantum computer can always be simulated by a Turing machine.

[edit] Philosophical implications

The Church–Turing thesis has been alleged to have some profound implications for the philosophy of mind.[37] There are also some important open questions which cover the relationship between the Church–Turing thesis and physics, and the possibility of hypercomputation. When applied to physics, the thesis has several possible meanings:

  1. The universe is equivalent to a Turing machine or is weaker; thus, computing non-recursive functions is physically impossible. This has also been termed the strong Church–Turing thesis (not to be confused with the previously mentioned SCTT) and is a foundation of digital physics.
  2. The universe is not equivalent to a Turing machine (i.e., the laws of physics are not Turing-computable), but incomputable physical events are not "harnessable" for the construction of a hypercomputer. For example, a universe in which physics involves real numbers, as opposed to computable reals, might fall into this category.
  3. The universe is a hypercomputer, and it is possible to build physical devices to harness this property and calculate non-recursive functions. For example, it is an open question whether all quantum mechanical events are Turing-computable, although it is known that rigorous models such as quantum Turing machines are equivalent to deterministic Turing machines. (They are not necessarily efficiently equivalent; see above.) John Lucas and, more famously, Roger Penrose[38] have suggested that the human mind might be the result of some kind of quantum-mechanically enhanced, "non-algorithmic" computation, although there is no scientific evidence for this proposal.

There are many other technical possibilities which fall outside or between these three categories, but these serve to illustrate the range of the concept.

[edit] Non computable functions

One can formally define functions that are not computable. For example, there are functions on natural numbers that produce values that cannot be computed. The most famous such function is the busy beaver. This function describes the largest amount of work that a Turing machine can produce with limited resources (i.e., no more than n states). For a certain model of Turing machine researchers have given exact computations for the busy beaver function for the smallest values of n: 2, 3, 4, 5, and (painfully) 6 states. For higher values, only lower bounds can be given. Finding an upper bound on the busy beaver function is equivalent to solving the halting problem, because one would have to run every possible n-state Turing machine and see which one does the most work before stopping, while ignoring the machines that never stop at all. Since these functions cannot be computed by Turing machines, the Church-Turing thesis asserts that these functions cannot be effectively computed at all, by any means.

Mark Burgin, Eugene Eberbach, Peter Kugel, and other researchers argue that super-recursive algorithms such as inductive Turing machines disprove the Church–Turing thesis. Their argument relies on a definition of algorithm broader than the ordinary one, so that non-computable functions obtained from some inductive Turing machines are called computable. This interpretation of the Church-Turing thesis differs from the interpretation commonly accepted in computability theory, discussed above. The argument that super-recursive algorithms are indeed algorithms in the sense of the Church-Turing thesis has not found broad acceptance within the computability research community.

[edit] See also

[edit] Footnotes

  1. ^ An archaic usage of Kleene et al. to distinguish Gödel's (1931) "rekursiv" (a few years later named primitive recursion by Rózsa Péter (cf Gandy 1994 in Herken 1994-5:68)) from Herbrand-Gödel's recursion of 1934 i.e. primitive recursion equipped with the additional mu operator; nowadays mu-recursion is called, simply, "recursion".
  2. ^ Church 1934:90 footnote in Davis 1952
  3. ^ Turing 1936-7 in Davis 1952:149
  4. ^ a b Kleene 1952:317
  5. ^ cf Kleene 1952:319-323
  6. ^ 1936-7 Turing 1936-7 loc cit:135ff
  7. ^ Post 1936 in Davis 1965:289
  8. ^ Kleene 152:321-2
  9. ^ Church 1934 in Davis 1965:100ff
  10. ^ Turing 1939 in Davis 1965:160
  11. ^ Rosser 1939 in Davis 1952:225-6
  12. ^ Post 1936 in Davis 1952:291
  13. ^ Sieg 1997:171 and 176-7)
  14. ^ a b Sieg 1997:160
  15. ^ Equivalently: recursively-definable function or λ-definable function. A Turing machine and a λ-function are computationally equivalent.
  16. ^ Rosser 1939 addresses this notion of "effective" as follows: "Clearly 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" (Rosser 1939 in Davis 1965:225). Thus this adverb/adjective is used in a sense of "1a: producing a decided, decisive, or desired effect", and "syn: capable of producing a result" (Merriam Webster's Ninth New Collegiate Dictionary)
  17. ^ Gandy (Gandy 1980 in Barwise 1980:123) states it this way: What is effectively calculable is computable. He calls this "Church's Thesis", a peculiar choice of moniker.
  18. ^ Dawson 1997:99
  19. ^ cf Church 1934 in Davis 1965:105ff, but also the caveat of non-constructive nature of the proof as discussed by Davis. Kleene would, in 1935 (Kleene in Davis 1965:251), present a way to construct functions not recursive. Davis then asserts a 3rd constructive undecidability argument by use of Kleene's result and Gödel's theorem X in his 1934; cf Davis 1965:108-9.
  20. ^ Turing 1939 in Davis:160
  21. ^ Turing 1936-7 in Davis 1965:263ff
  22. ^ Gödel 1963 in van Heijenoort 1967:616
  23. ^ a b Gödel 1964 in Davis 1965:72
  24. ^ cf Church 1934 in Davis 1965:100, also Turing 1939 in Davis 1965:160)
  25. ^ Post 1936 in Davis 1965:291
  26. ^ italics added, Rosser 1939 in Davis 1965:226
  27. ^ a b Kleene 1943 in Davis 1965:274
  28. ^ "Axiomatizing" is the act of producing a small collection of "self-evident" statements — the axioms — to be used as a basis for argument. These axioms are found by analysis or by experience (i.e. inductive reasoning). A properly-constructed argument will not permit dispute of the conclusion; only the axioms leading to the conclusion are debatable.
  29. ^ Gandy 1980 in Barwise 1980:123ff)
  30. ^ loc cit:135
  31. ^ loc cit:126
  32. ^ (Sieg 1998-9 in Sieg-Somner-Talcott 2002:390ff; also Sieg 1997:154ff)
  33. ^ Sieg 1998-9 in Sieg-Somner-Talcott 2002:390ff
  34. ^ Kleene 1952:320
  35. ^ Gurevich 1988:2
  36. ^ translation of Gödel (1936) by Davis in The Undecidable p. 83, differing in the use of the word 'reckonable' in the translation in Kleene (1952) p. 321
  37. ^ In particular see the numerous examples (of errors, of misappropriation of the thesis) at the entry in the Stanford Encyclopedia of Philosophy. For a good place to encounter original papers see David J. Chalmers, ed. 2002, Philosophy of Mind: Classical and Contemporary Readings, Oxford University Press, New York.
  38. ^ cf his subchapter "The Church-Turing Thesis" (p. 47-49) in his chapter "Algorithms and Turing machines" in his 1990 (2nd edition) Emperor's New Mind: Concerning Computers, Minds, and the Laws of Physics, Oxford University Press, Oxford UK. Also his a final chapter titled "Where lies the physics of mind?" where, in a subsection he asserts "The non-algorithmic nature of mathematical insight" (p. 416-8).

[edit] References

  • Bernstein, E. & Vazirani, U. Quantum complexity theory, SIAM Journal on Computing 26(5) (1997) 1411?1473
  • Andreas Blass and Yuri Gurevich (2003), Algorithms: A Quest for Absolute Definitions, Bulletin of European Association for Theoretical Computer Science 81, 2003. Includes an excellent bibliography of 56 references.
  • Mark Burgin (2005), Super-recursive algorithms, Monographs in computer science, Springer. ISBN 0387955690
  • Church, A., 1932, "A set of Postulates for the Foundation of Logic", Annals of Mathematics, second series, 33, 346-366.
  • Church, A., 1936, "An Unsolvable Problem of Elementary Number Theory", American Journal of Mathematics, 58, 345-363.
  • Church, A., 1936, "A Note on the Entscheidungsproblem", Journal of Symbolic Logic, 1, 40-41.
  • Church, A., 1941, The Calculi of Lambda-Conversion, Princeton: Princeton University Press.
  • Cooper, S.B. and Odifreddi, P., "Incomputability in Nature", in "Computability and Models: Perspectives East and West" (S. B. Cooper and S. S. Goncharov, eds.), Kluwer Academic/Plenum Publishers, 2003, pp. 137-160.
  • Martin Davis editor, The Undecidable, Basic Papers on Undecidable Propositions, Unsolvable Problems And Computable Functions, Raven Press, New York, 1965. All the original papers are here including those by Gödel, Church, Turing, Rosser, Kleene, and Post mentioned in this section. Valuable commentary by Davis prefaces most papers.
  • Eberbach, E., and Wegner, P., Beyond Turing Machines, Bulletin of the European Association for Theoretical Computer Science (EATCS Bulletin), 81, Oct. 2003, 279-304
  • Robin Gandy, 1980, Church's Thesis and the Principles for Mechanisms, reprinted in H.J. Barwise, H.J. Keisler and K. Kunen, eds., (1980), The Kleene Symposium, North-Holland Publishing Company, pp. 123-148.
  • Robin Gandy 1994-5, pp. 51ff in Rolf Herken ed. 1994-5, The universal Turing Machine: A Half-Century Survey", Springer-Verlag, Wien New York, ISBN 3-211-82637-8. An extensive analysis of the history of the Church-Turing thesis.
  • Gödel, K., 1934, On Undecidable Propositions of Formal Mathematical Systems, lecture notes taken by Kleene and Rosser at the Institute for Advanced Study, reprinted in Davis, M. (ed.) 1965, The Undecidable, New York: Raven Press.
  • Gödel, K., 1936, "On The Length of Proofs", reprinted in Davis, M. (ed.) 1965, The Undecidable, New York: Raven Press (pp.82-83), "Translated by the editor from the original article in Ergenbnisse eines mathematishen Kolloquiums, Heft 7 (1936) pp. 23-24." Cited by Kleene (1952) as "Über die Lāange von Beweisen", in Ergebnisse eines math. Koll, etc.
  • Yuri Gurevich, 1988, On Kolmogorov Machines and Related Issues, Bulletin of European Assoc. for Theor. Comp. Science, Number 35, June 1988, 71-82.
  • Yuri Gurevich, Sequential Abstract State Machines Capture Sequential Algorithms, ACM Transactions on Computational Logic, Vol 1, no 1 (July 2000), pages 77-111. Includes bibliography of 33 sources.
  • Herbrand, J., 1932, "Sur la non-contradiction de l'arithmétique", Journal fur die reine und angewandte Mathematik, 166, 1-8.
  • Hofstadter, Douglas R., Gödel, Escher, Bach: an Eternal Golden Braid, Chapter 17.
  • Kleene, S.C., 1935, "A Theory of Positive Integers in Formal Logic", American Journal of Mathematics, 57, 153-173, 219-244.
  • Kleene, S.C., 1936, "Lambda-Definability and Recursiveness", Duke Mathematical Journal 2, 340-353.
  • Kleene C., Stephen (1943). "Recursive Predicates and Quantifiers". American Mathematical Society Transactions Volume 54, No. 1: 41-73.  Reprinted in The Undecidable, p. 255ff. Kleene refined his definition of "general recursion" and proceeded in his chapter "12. Algorithmic theories" to posit "Thesis I" (p. 274); he would later repeat this thesis (in Kleene 1952:300) and name it "Church's Thesis"(Kleene 1952:317) (i.e., the Church Thesis).
  • Knuth, Donald E.,The Art of Computer Programming, Second Edition, Volume 1/Fundamental Algorithms, Addison-Wesley, 1973.
  • Peter Kugel, It's time to think outside the computational box, Communications of the ACM, Volume 48, Issue 11, November 2005
  • Lewis, H.R. and Papadimitriou, C.H. Elements of the Theory of Computation, Prentice-Hall, Upper Saddle River, N.J., 1998
  • Markov, A.A., 1960, "The Theory of Algorithms", American Mathematical Society Translations, series 2, 15, 1-14. A. A. Markov (1954) Theory of algorithms. Also: [Translated by Jacques J. Schorr-Kon and PST staff] Imprint Moscow, Academy of Sciences of the USSR, 1954 [i.e. Jerusalem, Israel Program for Scientific Translations, 1961; available from the Office of Technical Services, U.S. Dept. of Commerce, Washington] Description 444 p. 28 cm. Added t.p. in Russian Translation of Works of the Mathematical Institute, Academy of Sciences of the USSR, v. 42. Original title: Teoriya algerifmov. [QA248.M2943 Dartmouth College library. U.S. Dept. of Commerce, Office of Technical Services, number OTS 60-51085.]
  • Pour-El, M.B. & Richards, J.I., 1989, Computability in Analysis and Physics, Springer Verlag.
  • J. B. Rosser 1939 An Informal Exposition of Proofs of Godel's Theorem and Church's Theorem, The Journal of Symbolic Logic, vol. 4 (1939) pp. 53-60. Reprinted in Davis 1965:223-230.
  • Robert Soare, (1995-6), Computability and Recursion, Bulletin of Symbolic Logic 2 (1996), 284–321.
  • Turing, A.M., 1936, "On Computable Numbers, with an Application to the Entscheidungsproblem", Proceedings of the London Mathematical Society, Series 2, 42 (1936-37), pp.230-265.

[edit] External links