It's interesting indeed that Turing's machines as he defined them can never halt:
> he does not discuss the halting of his machines at all,
and makes no provision for the computational processes undertaken by his machines
ever to stop; in particular, he has no convention as in contemporary accounts of
a halt state for the machines
So instead of asking whether they halt, Turing asked whether they ever print a particular symbol. Of course one could call that symbol the halting symbol, and adopt the convention that printing the halting symbol amounts to halting. So while Turing did not name it the "Halting Problem" he proved an obviously equivalent result.
I think Rice's theorem implies that proving the undecidability of the halting problem is equivalent to proving the undecidability of any other non-trivial semantic property of a program (*). So this discussion is basically just splitting hairs as you said.
(*) > Rice's theorem states that all non-trivial semantic properties of programs are undecidable. A semantic property is one about the program's behavior (for instance, "does the program terminate for all inputs?"), unlike a syntactic property (for instance, "does the program contain an if-then-else statement?"). A non-trivial property is one which is neither true for every program, nor false for every program.
It’s worth noting that the undecidability of the halting problem doesn’t prevent computing scientists from proving that a program halts or has some other nontrivial property.
In general, it absolutely does. I'm not sure what you're trying to say.
(1) Yes, there are classes of programs for which you can say whether it halts
(2) Yes, there are programs who do not fall into those classes who can be shown to halt
But the point remains... there's no 'general' way to show that any program halts.
Part of the point of good PL design is to produce a language that is amenable to analysis, including halting analysis. Some languages do this better than others. Others are okay so long as you make particular assumptions. The halting problem tells us that the languages that are perfectly analyzable are categorically less powerful than the ones that are not. However, this may be 'enough' for us.
> In general, it absolutely does. I'm not sure what you're trying to say.
I can see that you don't so I'll try to be clearer. For any given program one might choose there is no reason in principle why a competent computing scientist can't perform a semantic analysis for every statement and then deduce from that whether it is totally or partially correct. Obviously most programs in the set of all programs are too long for a computing scientist to read in a human life time, but that's another issue entirely.
As a matter of practicality though, the working computing scientist is far more likely to first decide on the properties he wants his program to have and then derive a program that has them. This is yet another case of construction being considerably easier than verification.
This points to (but doesn't prove) the possibility that the human computing scientist isn't using a decision procedure to analyze (or construct) the program.
About here is where I expect to see some misinterpretation of Church-Turing as somehow proving that everything, including computing scientists, is a Turing machine brought up. Oddly, rarely is the far more interesting Curry-Howard correspondence mentioned.
I'm sure you know this, but even very simple/short programs can have complex behaviours that put them out of reach of computer scientists with present-day knowledge. For example, short programs can encode things like the Goldbach conjecture, the Collatz conjecture, or the Riemann Hypothesis. For example, does this program (written in Python, but translate to your computational system) halt?
def isprime(n): return n > 1 and all(n % d for d in range(2, n))
def goldbach(n): return any(isprime(p) and isprime(n - p) for p in range(2, n))
n = 4
while goldbach(n): n += 2
(See also the recent https://www.quantamagazine.org/amateur-mathematicians-find-f... which describes how hard it was to prove things even about puny 5-state Turing machines, and that already with just 6 states there is one "antihydra" that encodes Collatz-like behaviour and will probably be hard to prove anything about.)
Absolutely. And frankly I think that’s very exciting. If I had to lay a wager I reckon if those problems will be solved by a human intelligence, the most likely method will be through taking advantage of that correspondence and proving some tractable representation of the appropriate program halts.
Like many people I had a casual go at it for Collatz. It was a humbling experience of course, but it did nothing to convince me some more capable person can’t eventually manage it.
If you fix a particular axiom system for deriving your termination proofs (e.g. because you write them all down in Coq), then for Gödelian reasons, there are programs that don't terminate but for which a nontermination proof doesn't exist (and thus can never be found). If Coq is consistent, then the program that enumerates all possible Coq proofs and stops as soon as it finds a contradiction, is one such program.
> I can see that you don't so I'll try to be clearer. For any given program one might choose there is no reason in principle why a competent computing scientist can't perform a semantic analysis for every statement and then deduce from that whether it is totally or partially correct.
'Correct'? In what sense? 'Correctness' and halting have little to do with each other. For example:
def f(p):
p()
return 2
is 'correct' if the definition of f is to evaluate to two. But it's not clear it's ever going to halt (depends on haltingness of p).
But that being said, actually no, there are many reasons in principle why a competent computer scientist would not be able to perform a semantic analysis for every statement and deduce from that whether the program will halt.
> Obviously most programs in the set of all programs are too long for a computing scientist to read in a human life time, but that's another issue entirely.
Irrelevant because even an immortal computer scientist would be unable to determine if the program halts.
> This points to (but doesn't prove) the possibility that the human computing scientist isn't using a decision procedure to analyze (or construct) the program.
The difference between a computer and a person (and I'm going to ignore all the various philosophies of consciousness) is that a human will 'arbitrarily' determine under what system he/she wants to operate, and thus can change axioms on the fly. of course, one could write a computer system that does this as well. It's really not obvious what you're saying here
> About here is where I expect to see some misinterpretation of Church-Turing as somehow proving that everything, including computing scientists, is a Turing machine brought up. Oddly, rarely is the far more interesting Curry-Howard correspondence mentioned.
Computer scientists may or may not be turing machines, but any deterministic procedure they follow can be encoded as a turing machine so your distinction is irrelevant.
I'm not sure what Curry-Howard really has to do with this, but in general, for a theorem checker, you should make sure your proofs are total.
> ‘Correct'? In what sense? 'Correctness' and halting have little to do with each other.
Confident ignorance isn’t a good look. To help you out, here you go from the wiki[1]:
Within the latter notion, partial correctness, requiring that if an answer is returned it will be correct, is distinguished from total correctness, which additionally requires that an answer is eventually returned, i.e. the algorithm terminates.
To be fair to your time and mine—I stopped reading your reply there based on the principle that nonsense follows nonsense, so you needn’t elaborate further.
This is a non-productive comment. You said 'correctness', not 'total correctness'. Totality absolutely relates to halting. 'correctness' itself doesn't imply totality.
But regardless, it's pretty clear from your ramblings that you're not well-versed in this stuff. As for my part, I implement theorem provers and programming languages, so what do I know
But do we need general ways to show that any program halts? We don't write general programs
In particular, our programs have a limited size and use a limited amount of memory (or else the OS will make sure they will halt..). And for this specific class of programs, the halting problem is actually decidable!
Theoretical impossibility results like this one are often interesting because they tell you there is no "smart" way even in practice beyond just brute forcing it.
While it's true that the class of programs that terminate in time at most T is decidable for trivial reasons (just run the program for at most time T), that trivial decider is of course not gonna run in time T (but at least T+1). So if you set T=time until the heat death of the universe, you haven't gained any practical ability to solve the halting problem either.
It's a little more impactful than that. Have a look at Z3, Boogie, Dafny, and similar technologies to see practical application of what I mean. It boils down to there being "non-general" algorithms that still work for virtually every input you're ever going to give them. A hypothetical algorithm that decides the halting problem for 99.9999999% of programs would not violate the impossibility proof.
The limit case is maybe interesting. What about the algorithm that decides the halting problem for every program except for one? Does the impossibility proof prohibit such an algorithm? Does it make a difference if the identity of the unique program is known or unknown?
And then of course there is classic pen and paper hand derivation like the old guard (Knuth and his peers) did. The claim that that is following an algorithm is yet to be proved or disproved.
You are right in that there is a class of algorithms for which it is possible to do that. It is just not possible to decide if any algorithm is in that specific class of algorithms or not. There is an even smaller class of algorithms that can be constructed bottom up from halting sub algorithms. But these are not as powerful.
I kinda hate that people dress up this analysis as a theorem. We have lots of formally verified programs that show useful work can be done here. And even if we can't prove most of it, high assurance methods are very useful for preventing fuckery. I can't mathematically prove any lock is unpickable. But I can use a lock advanced enough that the cost of picking it becomes absurd.
Also, theoretical quantum computers can solve whether a problem halts 100% of the time. So Rice's Theorem is theoretically meaningless.
Man I feel like I'm missing something. Figuring out whether a single given program halts is decidable, it's figuring out an arbitrary unknown problem (or all of them rather) that is undecidable. So you can formally verify programs but you can't formally verify all programs with the same algorithm.
Secondly, what do you mean by the idea that quantum computation makes the problem decidable? This isn't a complexity class issue, and my understanding is that quantum computation can't compute anything that turing machines can't, they just are able to compute certain algorithms faster. Am i wrong? Among other things we can simulate quantum computers on turing machines, just without the complexity advantages.
Like think about what you're saying: of course we can prove that "exit(0)" halts, it'd be absurd to say otherwise. So we're clearly referring to a harder problem—proving whether arbitrary programs halt with a single algorithm in finite time.
If it helps, Roger Penrose misunderstood the halting problem and basically said "humans aren't practically constrained by godel's incompleteness theorems (equivalent to the halting problem I believe) so consciousness is quantum". This might yet be true but human computers are still bound by the same computational constraints computer's are.
It's been a bit since my computer theory courses so apologies for any botched terminology or understanding.
I would like to add that even deciding if a particular single program halts can be undecidable. At least in PA or ZFC, and I don't think there is a better math framework.
There was a pretty cool Bachelor's thesis (I think? Can't recall) that that used this fact to show that busy beavers beyond some point cannot be determined.
And even without any trickery, deciding single program halting can be extremely hard. For instance, the 3x+1 problem is as trivial to write as fizzbuzz but noone can figure out if it halts.
Probably! This paper is a year or two newer but used the exact same principle. It also has a much better constant than I recall. Perhaps I was reading a precursor article. I really enjoy this approach, it is a lovely idea.
It is never undecidable to determine whether a single particular program halts or not.
For any single program, one of these two functions will correctly output whether it halts or not.
bool always_true(TuringMachine M) {
return true;
}
bool always_false(TuringMachine M) {
return false;
}
It won't work for every Turing Machine, but it will work for a specific one.
This is why it's not very meaningful to talk about the decidability of particular Turing Machines and also why the halting problem is not, and never was about specific Turing Machines.
As to your point about being decidable within ZFC or PA, that is true but it's also not really significant. Neither ZFC or PA are a kind of master authority when it comes to decidability and in fact the vast majority of mathematics is fairly agnostic with respect to the use of ZFC.
The choice of a particular set theory tends to only come up in very explicit circumstances, and even in those circumstances you'll find mathematicians using theories that are more powerful than ZFC such as by making use of large cardinal axioms.
I suspect what GP means is that for certain programs, (assuming a fixed set of axioms) there exists neither a proof of its termination nor of its non-termination (not just that we can't find it; it doesn't exist).
Of course, if the program did eventually terminate, then a termination proof would exist (just enumerate all the state transitions, there's only a finite number of them). So what it means is that some programs never halt, but it's impossible to prove this fact.
This ties in with Gödel's theorems, e.g. (if we use ZFC and assume ZFC is consistent) a program that enumerates all possible valid proofs from axioms in ZFC and halts whenever it finds a contradiction, would never halt, but we can't prove this (at least not in ZFC) because that would contradict Gödel's second incompleteness theorem.
> For any single program, one of these two functions will correctly output whether it halts or not.
Saying "one of these functions is correct" is not a decision procedure. You actually need to decide which one of them is correct.
> This is why it's not very meaningful to talk about the decidability of particular Turing Machines
I disagree. There are particular Turing machines whose decidability is extremely meaningful. For example, there are specific Turing machines which encode mathematical problems of interest such as the Goldbach conjecture. Deciding whether they halt is equivalent to solving those mathematical problems, which is definitely meaningful.
>Saying "one of these functions is correct" is not a decision procedure. You actually need to decide which one of them is correct.
That's precisely what a decision procedure is, it's an algorithm that takes as input the description of a Turing machine, and an input, and returns true if and only if the Turing machine halts when given the input. You are using the term "decide" as if there were some kind of agency involved, like you have to actually "choose" what is correct or incorrect, but no such agency is involved, it is a purely mechanical process.
>There are particular Turing machines whose decidability is extremely meaningful.
You are mixing up the notion of decidability with the notion of halting, and there is a subtle difference. The Turing machine that encodes the Goldbach conjecture proves the conjecture if it halts, and disproves the conjecture if it doesn't halt. That is an interesting and meaningful property of such a Turing machine. What is not meaningful or interesting is whether that particular Turing machine is decidable.
As I said, there is a subtle difference between whether a Turing machine halts or not, and whether it's decidable whether it halts or not. The former is interesting, the latter is not particularly insightful.
> You are using the term "decide" as if there were some kind of agency involved, like you have to actually "choose" what is correct or incorrect
Isn't this literally what a decision procedure is? It's an algorithm that always outputs the correct answer, not one which tells you "the correct answer is either true or false". I'm not talking about agency or consciousness.
One of the two algorithms I posted tells you the correct answer for any specific Turing machine, so for any given Turing machine one of them is a decision procedure for it.
Exactly, so then we agree, there is nothing useful about an algorithm that can decide whether one specific Turing machine halts. Utility only emerges from an algorithm that can decide whether entire classes of other Turing machines halt, not from whether a particular machine does.
> there is nothing useful about an algorithm that can decide whether one specific Turing machine halts.
Yes there is. If someone gives me a working algorithm (this means one algorithm, not two algorithms either of which may work or not as you've been doing) which can provably decide whether the machine encoding the Goldbach conjecture halts or not, that is a very useful algorithm.
I must insist that giving two algorithms and saying "one of them works" without telling me which one works is is not a valid answer, since that is strictly different from giving a working algorithm which I can run in finite time in order to find out one correct answer.
You said this yourself earlier:
> The Turing machine that encodes the Goldbach conjecture proves the conjecture if it halts, and disproves the conjecture if it doesn't halt. That is an interesting and meaningful property of such a Turing machine.
I just think you're making a very subtle mistake here by mixing up the question of whether Fermat's Last Theorem (or Goldbach's Conjecture) is true with whether there is an algorithm that tells you that that specific theorem is true.
In my opinion, it's useful to know whether Fermat's Last Theorem is true, and that requires a proof. An algorithm that can only tell you whether a particular theorem is true is entirely useless.
For example, Sir Andrew Wiles proved that Fermat's Last Theorem is true, so would you reject an algorithm that simply returned true for any input as somehow being wrong? Would you only be happy if the algorithm wasted some energy doing some "computation", messing around with some variables and producing copious amounts of heat before telling you that Fermat's Last Theorem were true? Of course not. It doesn't matter what the algorithm does as an implementation detail, what matters is that the output is correct, not the heat it generates in the process.
Knowing a theorem is true is valuable. Having an algorithm that simply returns the correct answer about whether a particular theorem is true is entirely useless.
In general, an algorithm is only useful when it can be used for some arbitrarily large set of inputs. An algorithm that only works for one single instance is hardly an algorithm at all, it's nothing more than a lookup table. To be something more than a lookup table, it needs to work for an entire class of inputs, it needs to take an infinite number of possibilities and compress them down into the finite description of a process.
We know that no such algorithm can decide the halting problem for every single Turing Machine, but we can construct algorithms that can decide the halting problem for subsets of Turing machines, infinitely large subsets in fact.
Having an algorithm that just works for one single Turing machine... pretty meaningless.
Also worth noting that, from a practical perspective, even very simple programs/TMs can exhibit very complex behaviours that make it difficult to work out whether they will actually halt or not.
At the time of writing there are 2833 5 state binary TMs that haven't been decided yet:
That is a much lower complexity grade than I thought we would struggle with. Especially since we have decades of experience in solvers for rather large Boolean Satisfiability Problems, which seems like it could be adapted here.
A few months back I spent a couple of hours writing a binary TM simulator (yes I know you can download them - I wanted to write one) and then spent a couple of weeks running various TMs for days on end...
They exhibit quite bizarre amounts of complexity for what are really simple structures - indeed some TMs have apparently been observed employing Collatz conjecture type behaviour.
Penrose's entire thesis seems to boil down that AGI is impossible because brains use Quantum Oogly-Boogly and that since Quantum Oogly-Boogly isn't computable, no computer can do it. The Emperor's New Mind is a tour de force of a book, but its central premise feels thoroughly unconvincing, or at least poorly communicated.
It's been a long time since I've read TENM but I don't think Penrose argued that AGI was impossible, just that consciousness was not computable by a Turing machine. Presumably you could create AGI by utilising these quantum effects if it turns out that Penrose is correct and they do something.
I wouldn't particularly bet on Penrose being correct but until someone figures out how consciousness actually works or proves that it's somehow a big self-convincing illusion I don't think we can completely discount the idea that there's some kind of physics involved.
> I wouldn't particularly bet on Penrose being correct but until someone figures out how consciousness actually works or proves that it's somehow a big self-convincing illusion I don't think we can completely discount the idea that there's some kind of physics involved.
Despite my flippant rejection of Penrose I very much agree. I just thought the computational approach was misguided and his colleagues did him dirty.
> "Figuring out whether a single given program halts is decidable"
What does "decidable" mean in this context? Simply running the program may not be sufficient to know whether or not it halts. One could have a program that loops infinitely but never repeats the same state. So it will never halt, nor will its looping be obvious. So does it count as "decidable" if we cannot yet prove whether or not it's looping?
Not knowing the configuration of a TM at time t without running it (or similarly involved computation) doesn't mean that we cannot divide the space of TMs into classes.
One class has to each TM an associated mathematical function mapping inputs to nonnegative integers that tells you the exact integral time at which the TM transitions to the halting state. This is the class of decidable TMs.
The other class contains every TM not in the first class. For this class, any choice of such a function is provably wrong for some input. This is the class of undecicdable TMs.
Both classes are nonempty, and their existence is just about as well-defined as many other common mathematical objects. It is just not possible to provide a "nice" alternative characterization which TMs fall under which class.
> Figuring out whether a single given program halts is decidable
It's maybe nitpicky, but by definition "decidable" applies to a language, i.e. a set of programs, not a single program. Of course, there is a trivial TM (either the one that always accepts or the one that always rejects) that, for any given single program, gives the correct answer for exactly that program, but that is rather uninteresting. So this framing doesn't make a lot of sense.
What is actually decidable is the language consisting of pairs of a TM (+ input) and a valid proof of its termination, and that's why we can prove (some) programs to be terminating (or any other more interesting property).
I spent a long time thinking about this same dillema as Penrose: if solving maths is undecidable, how can humans do math? It seemed like a great paradox and maybe revealing a super ability of humans.
I think the truth is both more boring and more wondrous. We of course can't "solve math". For any given mathematical problem, humans are not guaranteed to find a solution given enough time. Indeed there are many problems that have been proven very difficult for a long time and there's no certainty they will be solved any time soon. As Conway put it (paraphrasing) "It's not because we don't have a big enough brain or something ... it's because there's no way to know [without just looking]". That is, we effectively do increasingly sophisticated forms of search, the same search you can do with an algorithm.
For example, you can simply try running the algorithm for a long time and see if it does halt. If it does, there's your proof. If it doesn't, you either declare you don't know, or declare they halt and accept it may be a mistake. As T->inf, you can cover all programs that halt, and the unknown/mistakes (depending on how you measure[1], because there are infinitely many programs) you'd make go to 0 in a particular sense ([1]).
You can also try to be more clever. You can start enumerating all proofs that (A) a given program halts, and (B) a given program does not halt, (C) it cannot be proven either way (assuming the proofs are verifiable). This allows potentially (depending on your axiomatic system) proving your program halts much faster than waiting T(p) (its halting time), in particular in the case p is part of a class of programs that has superexponential halting time as a function of size (e.g. it halts in 2^2^(N), where N is its size -- those programs should be fairly easy to construct). But you'd still be waiting a long time. Note however, it still can be the case that no proof exists in your axiomatic system either of A, B or C. So you still have to declare either you don't know, or mistakenly assume it doesn't halt/no proof exists. As your proof search time T->inf you get the same coverage property, but faster (in the sense that it eventually overcomes the previous method).
I said both boring and wondrous because there is some magic here (just not magic outside of the rules of the cosmos :) ): you can (always?) do better in some sense. You can build more and more clever methods of deciding whether programs halt; I think of them as "bags of heuristics" or "bags of tricks": from simple observations e.g. that an empty loop does not halt, to more complex properties.
Those heuristics eventually are also meta-heuristics (or just proof-heuristics): not only heuristics to tell whether P halts, but heuristics in a search for proofs that P halts (allowing a faster proof search). (Of course, there are also meta-heuristics in the sense of thinking about better ways to solve the problem in general). In the case of humans, the interesting distinction is that we are "messy extremely large minds", and we, through experience, "learn", or accumulate those various heuristics in a generalizing way -- that's what intuition is. Our learning is still limited in the same fundamental way any algorithm would be, we just turn out to be a very special (maybe you can call it magical in a sense) learning, intuitive and sentient, system (although likely the particular architecture of our brains/minds is specially relevant to how we operate and how it "feels to be a human", consciousness, etc.).
Not only is our brain special, but in a sense we're "lucky" to be initialized or to have fallen into a more or less "universalizing environment". Of course, if you put a children in an empty room, or even in a forest (even provided with unlimited food), he is unlikely to learn much, least of all the secrets of the universe. Our society, our environment is such that we teach ourselves language and we particularly put value on discovery, such that we have set in motion an environment where we can, and we do, discover asymptotically more. And this discovery has a great purpose. As we learn more, we not only learn more about the Cosmos (which we're part of), we learn about our own nature, what it means to have a good existence, and all the things we can do to have a better (more complete, more fulfilling, more full of love, more meaningful) amazing existence[2]. That's our real "magic bean"[3] that must be guarded with utmost care.
[1] Measuring the performance here is tricky, again because there are infinitely many cases. In a strict sense, the fraction of programs you prove that halts is 0 for any T. But that seems like a poor model: we're usually much more interested in small cases. If you weight them with some decaying weights, for example exponentially decaying 1/2^N, then this weighted fraction converges.
[2] I think that should be the general objective of rationality, or reason, and science/reason is the general system of conducting, refining and making this process reliable.
[3] Gold mine, Golden goose, Jewel, Delicate flower, etc.. :)
---
On quantum behavior, essentially none of those conclusions are affected at all, or even require quantum behavior. Quantum computing might accelerate some operations, but that's all. (And quantum computation has been shown so far to require extremely delicate conditions that would be hard to happen in our brains)
> We have lots of formally verified programs that show useful work can be done here.
Yes, by restricting things to a non-Turing Complete subset.
> Also, theoretical quantum computers can solve whether a problem halts 100% of the time.
That is absolutely not true. Quantum computers are proven to be entirely equivalent to classical computers in terms of what problems they can solve. The only difference is that they seem to show an exponential speed advantage for a certain very limited subset of problems, mostly related to quantum transforms.
> Yes, by restricting things to a non-Turing Complete subset.
No, not necessarily. There are procedures that _can_ verify properties against Turing-complete and even infinite-state systems. It's just that no _general_ (as in, sound and complete) procedure can exist.
If it's not sound, than the result is meaningless. If it is not complete, then it only works on a subset of problems, which is equivalent to what I said.
Agree that soundness is desirable, but "it only works on a subset of instances" and "you are restricted to a non-Turing complete subset" are not equivalent in the slightest.
huh, is that true? Is that class of computable function with a halting guarantee strictly smaller than the class of computable function without one? <citation missing>
I'm not sure what you're asking about. It is well known that certain computations can be determinstically proven to halt - there's even a prigramming language that only accepts programs that do so, Idris.
Of course, not any computation can be written in such a way. But it's clearly possible to write certain programs in such a way that they must halt by construction. You can even do it in C: don't use goto, only use loops with a known bound (e.g. while (x > 0) is not ok, but for(i = 0; i < 100; i++) is ok, as long as i is not modified in the body), don't use in-line ASM, don't use recursion, don't use stdlib functions (definitely no string functions). These rules can be verified syntactically (+- problems with UB), and the resulting program is guaranteed to halt. But there are problems for which you can't write such a program.
As to the relative size of these sets, I think that's a meaningless question - they are both infinite sets.
> there's even a prigramming language that only accepts programs that do so, Idris.
If you declare every function total. Idris still allows partial functions, and you can even cheat the whole system with "assert_total". Of course, with some sort of linter, you could still make sure that everything is actually total (although technically, in Idris "total" doesn't necessarily mean "halts" - programs which generate infinite input are also total in Idris).
> We have lots of formally verified programs that show useful work can be done here
Yes, if you start writing your program with the explicit intent of making such proofs possible, then it can be done. What Rice's theorem says is that you can't expect to be able to do so when given an arbitrary program, not that it's always impossible.
Formal verification (i.e., automated theorem proving) relies on only admitting 'total' programs, which usually requires that any potential sources of 'bottom' (i.e., non-termination) come equipped with a proof that that never happens (usually based on well ordering of some structural decomposition in the recursion).
Thus, most theorem provers are not turing complete and explicitly ban any turing complete structures.
So, the various things they show and prove cannot be said to encompass all programs.
> Many papers and textbooks refer the definition and proof of undecidability of the halting problem to Turing's 1936 paper. However, this is not correct.[19][24] Turing did not use the terms "halt" or "halting" in any of his published works, including his 1936 paper.[25] A search of the academic literature from 1936 to 1958 showed that the first published material using the term “halting problem” was Rogers (1957). However, Rogers says he had a draft of Davis (1958) available to him,[19] and Martin Davis states in the introduction that "the expert will perhaps find some novelty in the arrangement and treatment of topics",[26] so the terminology must be attributed to Davis.[
https://en.wikipedia.org/wiki/Halting_problem#Origin_of_the_...
The paper in the OP discusses this claim in section 3, and mentions that Kleene came even before that:
> We would note that Kleene seems, however, to have already had the self-referential argument earlier in his classic book from 1952, Introduction to Metamathematics
They also bring up the "symbol-printing problem" present in Turing's 1936 paper, which is trivially equivalent to the halting problem with today's hindsight. That paper has a well nuanced take with a lot of interesting information.
This version makes more sense to me. When the halting problem was first explained to me in school the professor didn't get into what it actually meant in terms of computability, just that we couldn't tell if a program halted or not then we just moved on.
I actually like the symbol phrasing, it's more general than halting. You can't prove that any arbitrary program that can be in state X will ever actually reach state X. Besides, I feel like https://xkcd.com/1266/ is relevant :)
While it is an interesting quirk of history that we mainly think about computability hand-in-hand with the "halting" problem instead of Turing's symbol-printing, there are so many more interesting nuggets in the 1936 paper (like computational universality, the first ever programming bugs, etc). I do think the paper linked gets the nuances of attribution here correct.
I wrote up a little guide to Turing's paper a while back [0] if anyone is interested in reading it but needs help like I did.
This is ridiculous academic click-bait. Here is a quote from Turing's 1936 paper:
"If a computing machine never writes down more than a finite number of symbols of the first kind [i.e. 0 or 1], it will be called circular. Otherwise it is said to be circle-free."
He then goes on to prove that "circularity" as he has defined it is undecidable.
So no, he never defines "halting", he just talks about whether or not a machine ever prints a finite number of 1's and 0's. Showing that these questions are equivalent is an elementary exercise.
He also proves that "there can be no machine £ which, when supplied with the S.D of an arbitrary machine AV, will determine vhether AV ever prints a given symbol (0 say)." Which, again, is trivially equivalent to the question of whether or not the machine ever enters a particular privileged state.
Saying that Turing's paper was not about the halting problem because it doesn't use the word "halt" is like saying that the EPR paper was not about entanglement because it doesn't use the word "entangled".
> So no, he never defines "halting", he just talks about whether or not a machine ever prints a finite number of 1's and 0's. Showing that these questions are equivalent is an elementary exercise.
I think it's subtler than that. Circular programs in Turing's language are those that return to some exact earlier state and thus go into an infinite loop. So circular programs by definition do not halt. But circle-free programs can either halt or not halt!
> Circular programs in Turing's language are those that return to some exact earlier state
No, they aren't. They are programs that print a finite number of "symbols of the first kind" i.e. 0s and 1s. They can print an infinite number of other symbols.
You might want to check out this branch of the discussion:
> Showing that these questions are equivalent is an elementary exercise.
Do you mean that there's a simple computable mapping f from TMs as Turing defined them to TMs which can halt such that machine m prints finitely many 0s/1s iff f(m) halts?
I think you'd want the reverse, which is indeed elementary: if f halts then you get a circle-free TM, but if f does not halt then you get a non-circle-free TM. This can be done by
f(); while(1) output_digit(0);
or any number of other simple constructions. This is because a circle-free TM always reaches a certain pre-defined event (output_digit), much like a halting TM. But a non-circle-free TM might forever fail to make progress, in a way that you can't necessarily tell if it's stuck or will eventually output another digit, much like a non-halting TM.
Edited to add: also Turing proved that the symbol-printing problem is undecidable, as the authors of this paper describe: will a Turing machine ever print a certain symbol? If you name the symbol in question "HALT" then this is almost identical to the halting problem, and easily reducible in either direction.
No. In fact, my guess is that you can prove there is no such function. But (and I confess I have not thought this all the way through so I might be wrong) while producing such a mapping would be sufficient to carry out the equivalence proof (if it were possible, which I suspect it is not) it is not necessary. All that is necessary (I think) is to show that if a machine is non-circular, then it is possible to produce an equivalent machine by using a halting state which is entered after the machine prints its final "symbol of the first kind". And that seems like it should not be hard, though I concede I may have overstated my case by calling it trivial.
(You also have to prove the opposite, that a machine with a halting state can be converted into a Turing-style TM, but that really is obviously trivial.)
That point is discussed in the paper: circle-freeness is Pi^0_2 in the arithmetic hierarchy, so there isn't a reduction to halting (Sigma^0_1) in the usual sense of a mapping between inputs. And in fact, Turing's paper does do a construction like you describe to show that yet another problem ("symbol-printing") is undecidable, and that one is much more similar to halting than circle-freeness. Again, this subtlety is discussed in the paper.
I think you were a bit quick in dismissing the OP paper based only on its title.
Yes, I think you might be right about that. FWIW, it's 4AM here and I am not firing on all cylinders. I live in the U.S. and politics is weighing heavily on my mind tonight.
> to show that if a machine is non-circular, then it is possible to produce an equivalent machine by using a halting state which is entered after the machine prints its final "symbol of the first kind".
The key is the assumption that the machine is non-circular. So there must be a state in which it prints its last symbol (can we agree to drop the "of the first kind" qualification?). After that, it never prints another symbol, so you can just replace whatever it does after that with a halting state.
But I see the problem with this now that I've written it out. The future behavior of the machine also depends on the state of the tape so you can't "just replace" all the future behavior because you don't know which entry into the state that prints the last symbol will be the one that actually prints the last symbol. So that doesn't work.
Still, going meta, there are only two possibilities here: either the undecidability of the HP is equivalent to the undecidability of circularity (i.e. that either result follows from the other) or it isn't. If it isn't then that would be Big News, and if it is, then it's just a question of how easy or hard it is to prove this. If it's hard, then someone should get the credit for being the first, and since I've never heard anyone get the credit I conclude that it's probably easy notwithstanding that my intuition about how to do it turns out to be wrong.
Chaitin has pointed out an important difference between such questions [1] :
> In our approach to incompleteness, we shall ask whether or not
a program produces an infinite amount of output rather than asking
whether it produces any; this is equivalent to asking whether or not
a diophantine equation has infinitely many solutions instead of asking
whether or not it is solvable.
If one asks whether or not a diophantine equation has a solution
for N different values of a parameter, the N different answers to this
question are not independent; in fact, they are only log2 N bits of information. But if one asks whether or not there are infinitely many
solutions for N different values of a parameter, then there are indeed
cases in which the N different answers to these questions are independent mathematical facts, so that knowing one answer is no help in
knowing any of the others
It turns out I was not as wrong as I thought. From the opening of the paper:
"...the term halting problem, the modern formulation of the problem, as well as the common self-referential proof of its undecidability, are all, strictly speaking, absent from Turing’s work. However, Turing does introduce the concept of an undecidable decision problem, proving that what he calls the circle-free problem is undecidable and subsequently also that what we call the symbol-printing problem, to decide if a given program will ever print a given symbol, is undecidable. This latter problem is easily seen to be computably equivalent to the halting problem and can arguably serve in diverse contexts and applications in place of the halting problem—they are easily translated to one another."
So I was basically correct, just wrong about a detail: it is the symbol-printing problem that is easily translated to the halting problem, not the circle-free problem. So I am going back to standing by my initial assessment: saying that Turing's paper was not about the halting problem because it doesn't actually use that exact phrase is like saying that the EPR paper was not about entanglement because it doesn't use that exact word.
BTW, hats off to you for the subtlety of your pedantry. You made me realize that I was wrong by asking just the right question. Socrates would be proud.
When I read Turing's paper some years ago, this really confused me. The best sense I could make was that "circle-free" means "halts". But in popular explanations, writers often equate "halts" with "gives a result" and "doesn't halt" with "has a bug", i.e. an infinite loop. And Turing seems to connote just the opposite. The point is to print a real number, so if the program stops printing digits, something went wrong. (I guess many numbers would end in 0s forever.) From today's paper:
> a program is circular, when it produces only finitely many digits of the output digit sequence, and circle-free, when it has succeeded in giving us an infinite digit sequence for the output real number.
But I could never really believe my interpretation. It was just the best I could come up with, as an amateur reading the paper alone for fun. Later I read Petzold's book, and I'm not sure that really solved the trouble for me either.
I've only read a few pages so far, but I'm gathering it's not as simple as I wanted: "circle-free" is not merely equivalent to "halts" after all. I'm looking forward to seeing their more nuanced take.
EDIT: Btw, this reminds me of the best riddle I've ever invented myself. Q: What do you call a fully autonomous self-driving car that can operate with as much understanding as a person? A: N Gheavat Znpuvar. (I didn't say it was a good riddle.)
I don't think the examples are meant as actual real world things, but rather abstractions to help reason about the problem.
The most important thing about the halting problem, is that Turing gave an example of a computational problem that is unsolvable, thereby proofing that from all possible computational problems, some of them are be unsolvable.
I think you can use a Turing-like argument to argue against the existence of a finite set of moral rules that covers every situation too. The argument goes: suppose you have some set of rules. Now engineer a situation where, if the rules are followed, you cause something bad to happen. That’s similar to the step where turing says, “now create a program that asks if p halts, and if so runs an infinite loop”.
Which means, no sacred text or set of commandments could possibly cover every situation.
My grad school mate Ron Maimon one day told me in a bar about the problem of computable numbers in a way that made him sound like a serious crackpot. I thought about it enough to conclude that the “real” numbers were “phony” numbers because unlike the integers or rationals most of them don’t have a name and can’t be referred to specifically.
I found out later that Turing had introduced the computable numbers idea and that was the work he had really done as opposed to the modern formulation of the halting problem.
As for Ron he really descended into conspiracy theory insanity and got kicked off Quora because he was saying the Boston bombing was an inside job. I still wish Steve Wolfram would grow some balls, take his constructivist program seriously, and reject the axiom of choice.
I found his Physics Stack Exchange answers to be immensely valuable. Although, I did have to read everything he wrote with a little bit of a critical eye, due to some of the rants he went on.
I'm glad to see he bought into the abiotic generation of oil; it's my favorite fringe theory I just can't shake.
I think it's one of the more unfortunate thing in mathematics that the real numbers are as popular as they are. I'm with your roommate. I don't believe they exist. I don't think every set of rational numbers has a least upper bound
If only those things existed that have a name, the world would be a pretty small and boring place. Also, that would be a world entirely defined by humans, and that just doesn't make sense.
Sorry, to be clear, it's irrelevant whether humans are doing it or someone else. They're not identifiable, and there's no example of such a thing. There are noncomputable reals which we can identify. I'm willing to say those exist. There are non-computable reals that we cannot identify (basic countability argument), that must exist as part of the reals if defined as they are.
But we've no example of them. They're just kind of there. They don't exist.
Either way, you don't need to argue with me. Much smarter thinkers than me have written extensively on it, and it's a widely held view. It's an indictment of one's own curiosity when the response to a new idea is to suggest the introducer is somehow lacking.
It's not really a new idea though. I just don't think it is a particularly good one.
The cool thing about mathematics is that we can use finite reasoning to talk about things that are otherwise hard to grasp, and that are yet part of our shared reality. Saying that the reals don't exist is pretty much the same as saying that the natural numbers don't exist. After all, you are going to have a hard time to name each and every one of them. Oh, you say that countability makes a difference here? Well, that's a purely mathematical concept, and if you don't believe that mathematics is real, how are you going to convince me that this concept makes sense?
> Saying that the reals don't exist is pretty much the same as saying that the natural numbers don't exist
I mean... it's really not. The natural numbers have a straightforwards definition, where one can theorize the 'existence' of them pretty straightforwardly.
Are you familiar with the definition of the reals? The reals don't appear anywhere in nature, and are only useful as modeling really. You can't 'measure' a real-valued quantity and get a result that is not rational or at least computable.
The complex numbers over the rationals are more 'real' in that you can measure complex numbers with rational coeficients.
> Well, that's a purely mathematical concept, and if you don't believe that mathematics is real, how are you going to convince me that this concept makes sense?
I'm not sure you understand exactly what you're talking about. Mathematical constructivism doesn't claim that mathematics is not real. In fact, quite the opposite. It's typically a view held by very experienced mathematicians.
Well regardless countability is easily shown to be constructivist by first constructing a finite description of the natural numbers (and showing that the description of any natural number is itself finite and decidable).
Then you show that you can create decidable functions mapping each element of particular sets onto the natural numbers. It is trivial to construct these from any alphabet, including our own. Same with the rationals, etc.
Then you get to the reals and you ask questions like 'what does it mean to have a set of rationals' [1], 'what does it mean to have a least upper bound', etc.
[1] a constructivist would say a decision procedure to determine if a number is in the set. I.e., a set is real if you can decide whether a thing is in it or not. From this it follows that significant portions of the real numbers do not exist because there is no decision procedure that can produce a set of rationals for which they are the least upper bound.
> he does not discuss the halting of his machines at all, and makes no provision for the computational processes undertaken by his machines ever to stop; in particular, he has no convention as in contemporary accounts of a halt state for the machines
So instead of asking whether they halt, Turing asked whether they ever print a particular symbol. Of course one could call that symbol the halting symbol, and adopt the convention that printing the halting symbol amounts to halting. So while Turing did not name it the "Halting Problem" he proved an obviously equivalent result.