The Church-Turing Thesis lies at the junction between computer science, mathematics, physics and philosophy. The Thesis essentially states that everything computable in the “real world” is exactly what is computable within our accepted mathematical abstractions of computation, such as Turing machines. This is a strong statement, and, of course, if one had tried to say the same thing about natural laws and Newtonian physics, one would have a respectable thesis that turned out to be false. (There is even a theoretical research area, hypercomputation, that attempts to show how “super-Turing” computers could be built in real life by taking advantage on non-Newtonian physics.)
When I learned the Church-Turing Thesis in school, I was told that it was a thesis, not a theorem, precisely because it was not formally provable. The notion of “computable” was intuitive, not mathematically precise, so it was impossible to say whether a particular mathematical abstraction was the ULTIMATELY CORRECT one. Nevertheless, in 2008, two respected researchers — Nachum Dershowitz of Tel Aviv University, and Yuri Gurevich of Microsoft Research – did indeed publish a proof of the Church-Turing Thesis in the Bulletin of Symbolic Logic. How is this possible? They constructed an axiomatization of computation based on abstract state machines, a theoretical notion developed by Gurevich that Microsoft has used to perform practical software tests, and then proved that the Church-Turing Thesis held for that axiomatization of computation. In other words, they managed to formalize the notoriously unformalizable “computation in the real world.”
This impressed me quite a bit — so much so, that when a user named Avinash asked on the theoretical computer science question and answer site, “What would it mean to disprove Church-Turing Thesis?” I answered that the Thesis had been proved for all practical purposes. Not my finest hour, as we will see. Fortunately, Avinash, in a feat of crowdsourcing genius, accepted my answer as correct, in order to encourage discussion. Since then, some of the top theorists in the world have contributed their opinion of the Dershowitz/Gurevich paper, and their philosophy about the thesis overall. I will cover some of the main points in the rest of this blog entry.
First off, the Wikipedia definition of the Church-Turing Thesis is:
Every effectively calculable function is a computable function.
Here, “effectively calculable” means intuitively computable, by rote, in real life; and “computable” means formally computable according to some mathematically defined notion of computation. The history leading up to the formulation of the Thesis is fascinating, and not without controversy. Dershowitz and Gurevich believe, in fact, that Church and Turing put forth two separate Theses, while the computability theorist Robert Soare believes the Thesis should be named simply, “Turing’s Thesis.” I won’t go into any of this here, but for further information, you can look at a video of a presentation Gurevich gave in 2009, or read Computability and Recursion by Soare.
The informal axiomatization of computation provided by Dershowitz and Gurevich is as follows.
I. An algorithm determines a sequence of “computational” states for each input.
II. The states of a computational sequence are structures. And everything is invariant under isomorphism.
III. The transitions from state to state in computational sequences are governable by some fixed, finite description.
IV. Only undeniably computable operations are available in initial states.
Dershowitz and Gurevich formalize these axioms using abstract state machines, and proceed to derive from those axioms the statements they call Church’s Thesis and Turing’s Thesis. Pretty cool. But… what is wrong with this picture? I will quote from the comments and answers generated by Avinash’s question, and my own answer to it.
As normally understood, the Church-Turing thesis is not a formal proposition that can be proved. It is a scientific hypothesis, so it can be “disproved” in the sense that it is falsifiable. Any “proof” must provide a definition of computability with it, and the proof is only as good as that definition. I’m sure Dershowitz-Gurevich have a fine proof, but the real issue is whether the definition really covers everything computable. Answering “can it be disproved?” by saying “it’s been proved” is misleading. It has been proved under a reasonable (falsifiable!) definition of computability. — Ryan Williams
The Dershowitz-Gurevich paper says nothing about probabilistic or quantum computation. It does write down a set of axioms about computation, and prove the Church-Turing thesis assuming those axioms. However, we’re left with justifying these axioms. Neither probabilistic nor quantum computation is covered by these axioms (they admit this for probabilistic computation, and do not mention quantum computation at all), so it’s quite clear to me these axioms are actually false in the real world, even though the Church-Turing thesis is probably true. — Peter Shor
Peter Shor is, of course, a Godel Prize winner for designing the “quantum factoring algorithm” among many other impressive accomplishments; Ryan Williams is on the short list for a future Godel Prize, because of a major breakthrough he recently achieved in the field of circuit complexity.
Other heavy hitters weighed in on the subject as well. Gil Kalai provided several pointers to papers discussing variants of the Church-Turing Thesis, and some thoughts of his own. Andrej Bauer said he thought it was impossible to prove the thesis, but it might be disproved by designing a real-world computational device that was able to compute a function that Turing machines provably could not compute. Timothy Chow responded to that by saying it brought up a philosophical problem: how could we know that the real-world device was actually performing that super-Turing computation? It’s a fascinating conversation, that is still ongoing. I doubt the Dershowitz/Gurevich paper is the last word.
Nachum Dershowitz, & Yuri Gurevich (2008). A Natural Axiomatization of Computability and Proof of Church’s Thesis The Bulletin of Symbolic Logic DOI: 10.2178/bsl/1231081370