71–80 of 116 posts
Earlier quoted context omitted.
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.
Earlier quoted context omitted.
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…
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 clas…
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)
Earlier quoted context omitted.
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…
This just might take forever.
Earlier quoted context omitted.
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 st…
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…
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.
Earlier quoted context omitted.
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...
This comment really didn't age well https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-prov...
Earlier quoted context omitted.
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. https://en.wikipedia.org/wiki/Rice%27s_theorem#Proof_by_redu... (*) > Rice's theorem states that all non-trivial semantic properties of programs are undecidable. A…
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.
Earlier quoted context omitted.
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…
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.
Earlier quoted context omitted.
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 clas…
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.
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.
Earlier quoted context omitted.
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.
Earlier quoted context omitted.
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 clas…
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...
https://www.quantamagazine.org/amateur-mathematicians-find-f...
Not sure why that github still lists so many undecideds.