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.

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.

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.

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!

This just might take forever.

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.

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

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.

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

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?

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

https://youtu.be/2H8629BCbkM

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

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)

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.

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.

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.

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.