Now, all I have to do is write a program that includes an embedded version of your program. My program reads in the contents of itself and passes it to the embedded program. Now, all my program has to do is take the output of the embedded halt checker, and do the opposite; if the halt checker says the program halts, just keep looping. If it says I don't halt, exit immediately.
Now, you might think this is cheating, because it is using your own program against you. However, this is at the core of the problem; it has to work for ALL programs, even ones written with knowledge of your program.
[1]: Yes, I think this is possible. [2]
So I guess my point is: Does it really matter that you can come up with arbitrary programs that I will be unable to determine if they halt, if I can build up an entire OS platform of provably correct machine code with correctness proofs that I can scan out of a file to verify?
Ultimately, here's the point of re-framing it like this in the first place:
Now it's just a tooling problem.
I recognize that this is a very big 'just'.
The halting verifier program V never accesses itself. It takes two parameters: a program to check for halting (P) and an input to the program (I). It's job is to test whether P(I) (the program applied to the input) will halt.
To trick the halting verifier V we construct a diabolic P like this:
program P(I) {
if (V(I, I) == YES) { // if Verifier says I(I) halts
inifinite_loop(); // ... then do *not* halt
} else {
halt(); // ... otherwise halt
}
}
Given that P, we ask the verifier the devastating question: V(P, P).
Does P halt if given itself as input; does P(P) halt?
V cannot decide. Note that if we consider P(P), then it means that in the above program, the input parameter I becomes P itself: I = P. And so the V(I, I) == YES expression is actually testing V(P, P) == YES.
But V(P, P) is the devastating question itself!
If V(P, P) yields YES (P(P) halts) P goes into an infinite loop (P(P) in fact fails to halt), and so V has calculated the wrong answer: the actual behavior of P(P) contradicts the YES answer from V(P, P), rendering V incorrect. The same problem occurs if V(P, P) yields NO.
Note that P contains no self refererence. The fact that P is applied to itself as P(P) doesn't come from P; it comes from the way P is used. P is used that way when we ask the verifier V(P, P). The verifier itself is checking what happens if P is given itself as input. P can happily accept other programs as the input I, programs which are not itself.
What P needs is a way to embed V, because it relies on it. The assumption is that whatever halting verifier V someone tries to develop, it has to be public. So that is to say, some CS researcher claims he or she has developed a universal halting verifier algorithm V and they publish it. Then, promptly, their adversary takes the algorithm V and sticks it into their program P(I) as a subroutine, and has an instant test case which defeats V.
The tricky thing is not self-reference, but the fact that P contains the verifier and turns it against itself. The self-reference is instigated from the outside by choice of inputs. In other words, the devastating question V(P, P) is what perpetrates the self-reference which breaks V.
Notice my description: "Turing proved that no general algorithm can be formulated that can answer this question across all possible programs." The operative part here is "across ALL possible programs". The proof does stop us from knowing that SOME programs will or will not halt. It only stops us from being able to determine this for EVERY possible program. My post explores a very specific subset of programs that we can prove will terminate, then asks what pattern(s) underlie such programs, and then explores the use of such patterns in a variety of interesting problems. It is this last result that most intrigued me, and caused me to write about it.
- Clasical logic as the foundation for math.
- Proofs by contradiction work.
- That the church turing thesis holds.
I guess these are kinda two sides of the same coin. But still worth noting.
Direct proof of negative statement: Assuming P is true, there is a contradiction. Thus, P is false.
Proof by contradiction: Assuming P is not true, there is a contradiction. Thus, P is true.
The key bit is that in constructive mathematics, "P is not true" does not imply "P is false."
However, basically all of literature calls the undecidability of the halting problem a proof by contradiction.
So I guess that there are some intuitionists that make that distinction. I'm not sure that I'd call it a direct or constructive proof though.
The thing is that if you follow constructive reasoning and you assume that the church turing thesis is true, then all of math becomes somewhat small. No more uncountably infinite stuff, no dense reals, computable objects only e.t.c.
I feel like we've painted mathematics into a dogmatic corner, and tbh I have no idea how to get out of it.
An instance of the halting problem asks, given (a partial recursive) function F, whether there is an decision algorithm A (aka. Boolean valued algorithm) on the universe of inputs U of F that calculates the domain of F (those inputs where F takes a value, ie. halts; ie, A(x) <=> F halts on x, where x in U).
For any finite subset S = {s_1, ..., s_n} of U, there is a trivial decision algorithm on U that calculates S:
def A_S(x):
for s in (s_1, ..., s_n):
if x == s:
return True
return False
If U is finite, then D is finite, so the answer to the halting problem of F is trivially yes.
If F is a thunk (nullary function), then U is finite, ie. the singleton set of "no input", so the answer to the halting problem of F is trivially yes.
odd_perfect_number is a thunk.
> so the answer to the halting problem of F is trivially yes.
The answer is "yes, there is a decision algorithm"? What would that decision algorithm be for this particular function (odd_perfect_number)? And what is its answer?
Indeed.
> What would that decision algorithm be for this particular function (odd_perfect_number)?
Either of
() => True
() => False
> And what is its answer?
I'd be a Fields medal candidate if I knew ;)
I am unsure how you reached this conclusion?
But the thing is, it isn't algebraically guaranteed either - we still don't know if an odd perfect number exists. (I'm not sure where the "Definitely. Somewhere in 10^300 range." is coming from. There's nothing definite about the existence, only constraints that need to be satisfied if it exists)
Halting problem from a specific standpoint is a popular area of research. Microsoft Research in particular has been active in this area, and Windows device drivers and other kernel event handlers are analyzed to prove that they will halt in a reasonable amount of time to avoid locking up the OS.
https://www.microsoft.com/en-us/research/publication/t2-temp...
Please note that suggested odd perfect number search algorithm in Python uses an evasive predicate on a big integer which is unbounded.
This means that a typical tracer (or verifier in Turing terms) won't be able to infer the upper bound for the given example.
But the truth is that halting dilemma is real and despite any attempt to "unwind" or "simplify" the control and data flows, there is a real barrier. It is in the math.
My favorite example: finding an odd perfect number. Euler stated: "Whether (...) there are any odd perfect numbers is a most difficult question". More recently, Carl Pomerance has presented a heuristic argument suggesting that indeed no odd perfect number should exist. [1]
Does it exist? Definitely. Somewhere in 10^300 range. What is the exact value? Nobody knows. You can write a program that finds an odd perfect number:
Will this program ever complete?Maybe. However nobody can say for sure. Avoiding recursion or some kind of groups won't give you any favor.
This is the halting problem in all of its glory.
[1] https://en.wikipedia.org/wiki/Perfect_number