Hacker News Reader

The best way the halting problem was explained to me was to think of it like this: imagine you write your perfect halting detection program. It reads in the contents of some program, and returns true if it halts or false if it doesn't.

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.

Doesn't this assume that your program can reliably access it's own source-code? Can it? It can of course read some file containing some source-code. But assume it accesses some file which contains the source-code of some other program, then wouldn't your logic still hold the same, since from the point of your program it is simply reading some file?

Even if it can't access its source code, you can... you know what the code is

Doesn't matter. Doesn't have to be the executing source, can work with compiled representations; the original Turing paper "compiles" every program to a single giant integer.

No, it has nothing to do with source code.

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

Like V, P is a special program that takes a program as input. It then asks the verifier: if the input program is given itself as input, does it halt? And then it behaves in the opposite manner: if the verifier says that I(I) halts, then P deliberately infinite-loops. Otherwise P halts.

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.

Even if the code isn't public... it still exists. And since we are talking about "does their exist any possible program it can't determine", we know that some sequence of bytes will be that program, and therefore it is possible to exist.

But why do I have to accept your arbitrary program? Why couldn't I only consider programs that come with a proof that they terminate? I don't care how you made the proof, maybe you used some restrictive programming language that can only express concepts that terminate, or your program implements paxos and you prove it by some embedding into Coq. Some restrictions though: the proof has to be formulated in a way that's compact and takes linear-time to check [1], and the proof goes down to some formalization of first-order logic that we can agree on.

[1]: Yes, I think this is possible. [2]

[2]: https://github.com/digama0/mm0#introduction

After a bit of searching, proof carrying code seems to be related to what I'm describing [3].

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

[3] https://people.eecs.berkeley.edu/~necula/pcc.html

Author here. Cool story about odd perfect examples. That said, my post is not trying to find a way to crack the halting problem, and thereby demonstrate it is not real. Turing wrote a most excellent proof, and I stand by it wholeheartedly. I even cite another famous numeric example of a program we still do not know if it will terminate for all numbers: the Collatz conjecture.

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.

Important mistype. It should read: "The proof does NOT stop us from knowing that SOME programs will or will not halt.

It does however apply to more properties than merely halting: https://en.wikipedia.org/wiki/Rice's_theorem

You may also be interested in Willard's Self-Verifying Theories: https://en.wikipedia.org/wiki/Self-verifying_theories

A bit tangential, but turings proof only works with some very strict assumptions.

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

I believe that it's not a proof by contradiction, but a direct proof of a negative statement. Subtle distinction:

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

After some digging I found several blogs that make the same distinction as you do.

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.

Sorry to say, this example has nothing to do with the halting problem. Rather, I would say, it's a reformulation of a(n unsolved) mathematical problem to the question whether a certain function halts on a certain input (being "no input", as the function is nullary). Or, if you insist, we can regard it as a trivial instance of the halting problem.

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

Therefore if the domain D of F is finite, the answer to the halting problem of F is trivially yes: A_D is a decision algorithm for F. (This has noting to do with the question whether we know D or not!)

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.

> An instance of the halting problem asks, given (a partial recursive) function F, whether there is an decision algorithm A

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

> The answer is "yes, there is a decision algorithm"?

Indeed.

> What would that decision algorithm be for this particular function (odd_perfect_number)?

Either of

  () => True

or

  () => False

where '()' represents the empty input.

> And what is its answer?

I'd be a Fields medal candidate if I knew ;)

> Does it exist? Definitely.

I am unsure how you reached this conclusion?

Interesting. Nitpick: Odd perfect numbers are no more in the 10^300 range but nowl provably beyond 10^1500. The Wikipedia links to a math paper to that extend.

If it definitely exists, don't we then know that this program will definitely halt?

Only from algebraic and philosophical standpoints. This knowledge is not 100% precise unless a specific number is found.

Nobody cares about the halting problem from a specific standpoint. If it's algebraically guaranteed to halt, it halts. When it halts is entirely meaningless for purposes of the halting problem.

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)

In fairness, though, the halting problem doesn't care if you can predict if SOME programs halt... you have to predict if ALL programs halt.

There's that, too. (Well, we don't have to predict anything. We have to show that halting or not is a decidable condition, and we've shown it isn't. Even if we had shown it was decidable, there still might be programs where we practically can't figure out it halts. So is the beauty of math - it gives us the gestalt of the world without caring about the world :)

> Nobody cares about the halting problem from a specific standpoint. If it's algebraically guaranteed to halt, it halts. When it halts is entirely meaningless for purposes of the halting problem.

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

If you've prove a finite upper bound,then you've proven the program will halt. You don't need to know what the exact number is.

The trick with boundaries does not stand true for evasive predicates on unbounded data.

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.