8
$\begingroup$

In the opening chapters of Hartley Rogers, Jr.'s book Theory of Recursive Functions and Effective Computability, the proofs of the unsolvability of the halting problem and related unsolvability results invoke Church's Thesis. Can Church's Thesis be avoided?

Edit added on September 7 while putting a bounty on the question:

While in no way whatsoever doubting the diagonal argument per se, I am nevertheless in doubt as to how this is meant to work in the undecidability set up as witnessed also by my probes. One $\textit{evasion-possibility}$ that I, given my befuddlements, am not able to exclude a priori is that there $\textit{is}$ a recursive function that tells us whether a given Turing machine halts, but that a diagonalisation of the Turing machine would - pace Church and Turing - provide an effective non-recursive method beyond that recursive function.

I am rather certain that the evasion-possibility does not obtain, but I want to understand precisely why it does not. Somehow, I would have thought that the answer to this were simple. (The last sentence was not meant to contradict or undermine comments that pointed towards a tediousness of carrying these matters through.)

$\endgroup$
  • 5
    $\begingroup$ It can be. The question is whether you are willing to construct a Turing machine (with possibly dozens of states) to carry out the procedure that is given in the proof. Most of the time, people choose to describe algorithms informally and invoke the Church-Turing thesis to handle the "dirty work" that is needed to be done. (Because the Church-Turing thesis is obviously true!). $\endgroup$ – Burak Aug 19 '16 at 10:27
  • 2
    $\begingroup$ The thing is about how you define "solvable". Church's thesis states that if you were to use the informal notion of "solvable", then it is exactly the same as the notion of "solvable by a Turing machine", and the proof then follows. However, if we want to prove this formally, then we need a precise notion of "solvable", and the most popular choice is then "there is a Turing machine..." one. If you adapt this definition, Church's thesis is avoided. $\endgroup$ – Wojowu Aug 19 '16 at 11:44
  • 7
    $\begingroup$ I think it should be mentioned that this light hand-waving is not unique to computability theory. Lots of areas of mathematics containing phrasing like "we leave the standard details to the reader" or "by a routine argument". Computability theory just gives it a name. $\endgroup$ – Jason Rute Aug 19 '16 at 15:25
  • 4
    $\begingroup$ (continued) Moreover, I don't think applications of Church's thesis are all that informal. While constructing the Turing machine would be a mess, in most cases proving that such a desired Turing machine exists would only involve a few lemmas showing that basic operations are doable in a Turing machine. (Unbounded search can do a lot!) Many books don't even start invoking Church's thesis until they have given lots of results convincing the reader that a number of very general computational patterns can be formalized. $\endgroup$ – Jason Rute Aug 19 '16 at 15:33
13
$\begingroup$

Let me point out that there are really a family of Church-Turing theses assertions.

On the one hand, for what is sometimes described as the weak Church-Turing thesis, one imagines an idealized human agent, not constrained by resources of time or memory (or supplies of paper and pencil), but carrying out the kind of idealized computation that Turing had described — using paper and pencil calculations according to certain kinds of formal rules — and the claim is that any such algorithm that could in principle be carried out by such an idealized human agent can in fact by carried out by a suitable Turing machine program. According to this version of the thesis, therefore, the Turing-machine account of computability has captured the correct notion of computability-in-principle for an idealized human agent.

I believe that it is the weak Church-Turing thesis that most mathematicians have in mind when speaking of the Church-Turing thesis. A convincingly large piece of evidence for at least this weak form of the Church-Turing thesis consists of the mathematical fact that all the various notions of formal computability, including Turing machines, modified and expanded Turing machines, such as multi-tape machines and expanded alphabet or instruction set Turing machines, but including also register machines, modified register machines, flowchart machines, machines based on idealized versions of the basic programming language, or C++ or whatever other computer language, and so on. All these various notions of formal computability have been proved equivalent — they can all simulate each other — and this makes us think that we have correctly captured the notion of computability-in-principle with any one of them.

And surely it is only the weak Church-Turing thesis that is used in the arguments that Rogers mentions. When one describes a computational procedure in the way that Rogers does, or anyone does in the entire field of computability theory, one is describing a computational procedure that could in principle be carried out by an idealized human agent using only paper and pencil with plenty of time and plenty of paper. So this is a use of the comparatively uncontested formulation of the Church-Turing thesis. As Andrej and the other commentators testify, there is nearly universal agreement on the accuracy of the weak Church-Turing thesis.

The point I want to emphasize, however, is that there is another stronger version of the thesis, the strong Church-Turing thesis, which asserts that not only are the idealized paper-and-pencil computational procedures all simulable by Turing machines, but also any algorithm procedure that we could in principle carry out in our physical universe, however strange, is simulable by Turing machines. This is a much stronger claim.

Frankly, the evidence for this stronger version of the Church-Turing thesis is considerably weaker, in light of the fact that we already know that the fundamental nature of physical reality, including various bizarre quantum effects as well as relativistic effects, such as time dilation, are quite bizarre. We don't actually have much reason to think that it should not be possible in principle to take advantage of them for computational effect.

The quantum Turing machines may be a familiar example. Although we already know a lot about quantum Turing machines, in fact these will not violate the strong Church-Turing thesis, since they are in principle simulable by ordinary Turing machines (although the simulation takes much longer time, so the new quantum machines may give rise to a new complexity theory, even though they give rise to the same computability theory). So there seems to be no hidden violation of the strong Church-Turing thesis arising there.

But meanwhile, there are other strange computational procedures such as black hole computation and others, which seem possibly to offer a way to violate the Church-Turing thesis, by taking advantage of the relativistic effects such as time dilation that occur in our actual physical world. See Philip Welch's article, The extent of computation in Malament-Hogarth spacetimes, for a great summary and mathematical analysis of this kind of thing.

Jack Copeland has particularly emphasized the distinction between the weak and the strong Church-Turing theses.

$\endgroup$
  • $\begingroup$ Many thanks! I like the comprehensive nature of your answer and its fine distinction between the weak and the strong CTT. I will accept it, though that is not intended as a detriment to other answers. Some of this on CTT that you mention I remember from ages ago in connection with literature I read on AI. As you know, László Kalmár, expressed skepticism concerning CTT, as did a Polish philosopher Leon Gumański; Jan Woleński expressed in conversation many years ago that it was a scandal that Gumanski did not understand the diagonal argument. $\endgroup$ – Frode Bjørdal Sep 8 '16 at 15:05
  • $\begingroup$ Regarding your remark that "We don't actually have much reason to think that it should not be possible in principle to take advantage of them for computational effect," I believe that we do have good reasons to refuse to use the word "computation" to refer to such "hypercomputational" proposals whose results cannot be confirmed by any kind of finitary procedure, even in principle. I've discussed this on the Foundations of Mathematics mailing list at some length. $\endgroup$ – Timothy Chow Sep 8 '16 at 15:56
  • $\begingroup$ If it is just a question of terminology, then one can of course use another word. But I would say that the point of the discussion is the possibility, true or not, that there may be these other physical computation-like procedures that we cannot verify in the Turing manner by a finitary procedure. I would find it inadequate to say that the strong CTT is true simply by the definition of the term, "computation." Meanwhile, I would add that we do use the word more generally, as in oracle computations, BSS computations, ITTM computations and in higher recursion theory. It is a metaphorical use. $\endgroup$ – Joel David Hamkins Sep 8 '16 at 18:07
  • $\begingroup$ I wouldn't argue that the strong CTT is true by definition, but I would argue that to deserve the name "computation" (as used in the CTT, strong or weak) there needs to be some kind of finiteness condition (not necessarily "in the Turing manner" though), which every hypercomputation proposal I have seen blatantly violates. But this is not the place to spell out the argument in detail. $\endgroup$ – Timothy Chow Sep 8 '16 at 20:22
  • $\begingroup$ Well, let's call it scomputation then. The question is whether our physical universe allows for these scomputational procedures or not, and the strong CTT says that it does not. And it is that for which I am claiming we have only weak evidence. It seems to me that the question is one of physics, rather than mathematics or philosophy. The issue of whether they are sufficiently finitary for you or not seems beside the point. $\endgroup$ – Joel David Hamkins Sep 8 '16 at 20:34
19
$\begingroup$

The invocation of Church's thesis is not a religuous move but rather a warning to the reader that the author is describing informally an effective procedure which could be translated into a construction of a Turing machine (if one enjoyed such a thing). This is completely standard in computability theory. (And other branches of mathematics have a similar level of rigour, as pointed out by Jason Rute in the comments.)

We could ask whether we have to worry about the informal level of proof or Church's thesis itself. The answer is that Church's thesis has been tested billions of times in practice: every time anyone thinks of an algorithm and then actually codes it up, that is a confirmation that they did not violate Chuch's thesis and that their sense of what makes an algorithm did not lead them astray. In any case, for the paranoid there is always the formalization of Halting problem.

$\endgroup$
  • $\begingroup$ I also associate myself to no church on the matter, although I had Church as a teacher; in the spring of 1989 - as he turned 86 - I took his last graduate seminary in logic at UCLA, with an oral exam at the end. It seemed to me that Rogers' account inaccurately assigns Curch's Thesis a more prominent role than necessary in the proof of Theorem VII. But at this point I am confused, and I wonder about how to unconfuse myself. $\endgroup$ – Frode Bjørdal Aug 27 '16 at 21:37
  • 4
    $\begingroup$ Read Roger's reference to Church's thesis as a phrase whose meaning is "we could do the following in terms of Turing machines but it would be very painful, so let's be a bit informal". It's not a real reference to the real Church's thesis. That's how I understand it. I envy a bit that you took classes from Church himself. I am his academic grandson but I never met him. $\endgroup$ – Andrej Bauer Aug 28 '16 at 11:25
  • $\begingroup$ Thanks! On p. 25 with the \textit{More formal proof}, it is the step summed up with the sentence \quote{By Church's Thesis, \psi is partial recursive} which worried me; as in the informal version, the premise is that there is an algorithm for \psi. Is it that a Turing machine may show that the function \psi would be partial recursive, where $\psi(z,x)=(1 \ if \ \phi_z(x,x)=0; divergent \ if \ \phi_z(x,x)\neq 0 \ or \ divergent)$ and \phi is partial recursive? $\endgroup$ – Frode Bjørdal Aug 28 '16 at 14:23
6
$\begingroup$

I would say that Church's thesis is more of a physical principle that formalizes the notion of "computable in finite time". One cannot rule out new scientific discoveries that would falsify Church's thesis.

$\endgroup$
  • 2
    $\begingroup$ Indeed, we can even formalize such discoveries with the theory of hypercomputation. $\endgroup$ – Kevin Aug 19 '16 at 14:40
  • $\begingroup$ But see the caveat that I give here: cstheory.stackexchange.com/q/4838 $\endgroup$ – Timothy Chow Aug 21 '16 at 2:15
4
+50
$\begingroup$

To address your "evasion-possibility" directly: Let's look again at the overall structure of the proof of the unsolvability of the halting problem. If there were a Turing machine $M$ that could solve the halting problem, then we could construct another Turing machine $M'$ that uses $M$ as a subroutine in a certain way, etc., contradiction. We can explicitly write down the additional instructions that are needed to convert $M$ into $M'$, since this is a fixed piece of code that is independent of $M$, and so in particular there is no reason (other than laziness) to invoke the Church–Turing thesis to establish the existence of this piece of code. So if $M$ is a Turing machine then $M'$ must also be a Turing machine. That's all that we need to prove that there is no Turing machine to solve the halting problem.

This proof doesn't exclude the possibility that there is an effective but non-recursive procedure to solve the halting problem; for that conclusion, we would need to invoke the Church–Turing thesis. But the proof does exclude the possibility that there is a Turing machine to solve the halting problem for Turing machines, and that is all that we would expect to be able to prove mathematically anyway.

$\endgroup$
  • $\begingroup$ My original question was predicated precisely upon the belief that "if there were a Turing machine $M$ that could solve the halting problem, then we could constuct another Turing machine $M'$ that uses $M$ as a subroutine etc., contradiction." as you have it, and that the CTT was solely needed in a final step connected with decidability. But Rogers' wording and wordings in the exchanges here have left me confused. Is it a lemma that if $f(x,y)$ is a partial p.r.f. onto 2 then also a $g$ s.t. $g(x)=1$ if $f(x,x)=0$ and divergent if $f(x,x) =1$ is a partial p.r.f.? $\endgroup$ – Frode Bjørdal Sep 9 '16 at 22:49
  • 1
    $\begingroup$ @FrodeBjørdal : If I understand your question correctly, yes. From a Turing machine point of view, the proof is simple, since to compute g(x) you just have to compute f(x,x), which you can do by assumption. What is the sticking point for you? $\endgroup$ – Timothy Chow Sep 9 '16 at 23:14
  • $\begingroup$ @Tmothy Chow The sticking point was Rogers' presentation. $\endgroup$ – Frode Bjørdal Sep 10 '16 at 1:36
  • $\begingroup$ I will believe such a lemme if I understand a proof for it. $\endgroup$ – Frode Bjørdal Sep 10 '16 at 3:56
  • 1
    $\begingroup$ @FrodeBjørdal : Proofs of claims of this type are usually most easily done using Turing machines. In that context, these sorts of claims essentially become exercises in computer programming. In my view, what Rogers is getting at is that once one reaches a certain level of proficiency in computer programming, then one can "see immediately" that certain functions can be computed by a computer program. Admittedly, this kind of claim can seem confusing and even mystical to someone who is not so proficient, but I would argue that developing such proficiency really is the right way to go. $\endgroup$ – Timothy Chow Sep 11 '16 at 18:37

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.