[indolering]

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.

[darby_nine]

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.

[mafuy]

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.

[arethuza]

Was it this one?

https://scottaaronson.blog/?p=2725

[mafuy]

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.

[Maxatar]

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.

[Tainnor]

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.

[FartyMcFarter]

> 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.

[Maxatar]

>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.

[FartyMcFarter]

> 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.

[arethuza]

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:

https://github.com/bbchallenge/bbchallenge-undecided-index/b...

[SkiFire13]

This comment really didn't age well https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-prov...

[arethuza]

Ha! - I had no idea thanks

[SkiFire13]

To be fair, the announcement I linked was published 2 hours after your comment. It was just perfect timing.

[jononor]

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.

[kragen]

bounded model checking is indeed a thing, but it's bounded

[arethuza]

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.

[kragen]

awesome!

[ted_dunning]

Apparently, there is news on this:

https://www.quantamagazine.org/amateur-mathematicians-find-f...

Not sure why that github still lists so many undecideds.

[chuckadams]

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.

[chimprich]

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.

[darby_nine]

> 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.

[dcow]

The universe is a quantum computer that computes itself, so it’s certainly possible.

[shannifin]

> "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?

[jhanschoo]

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.

[enugu]

Quantum computers can't solve the halting problem but that is not Penrose's argument which is not summarized well in the quote.

[Tainnor]

> 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).

[bionhoward]

Relevant video about MIP*=RE

https://youtu.be/2H8629BCbkM

[ykonstant]

Lovely video!

[anon291]

> Figuring out whether a single given program halts is decidable

Whether any single given program? No, it's not decidable. For many programs, sure.

[gnramires]

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)

[tsimionescu]

> 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.

[lou1306]

> 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.

[tsimionescu]

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.

[lou1306]

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.

[lostmsu]

Not sure what are you trying to say. Surely the "subset of instances" is non-Turing complete.

[isaacfrond]

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>

[tsimionescu]

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.

[Tainnor]

> 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).

[frabert]

> 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.

[anon291]

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.

[FartyMcFarter]

What do you mean by dressing it up as a theorem? It is a theorem because there's a proof for it.

[Tainnor]

For example, here's a formally verified proof in Lean: https://github.com/leanprover-community/mathlib4/blob/124731...