Scooping the Loop Snooper (2000)

[blewboarwastake]

http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html

[photochemsyn]

This halting problem animation proof would work perfectly here:

https://www.youtube.com/watch?v=92WHN-pAFCs

[frob]

Pullum keeps a slightly updated version of this poem on his website: http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html

It adjusts the phrasing in a few places to make the meter flow more naturally. Apparently it also fixes a small error in the original proof, which, for the life of me, I cannot find.

I've used this poem to teach the halting problem to a variety of people for almost a decade and a half. Reading the one linked here just didn't sound right.

[dang → frob]

Ok, changed to that from https://www.cs.rice.edu/~vardi/comp409/scooping.pdf. Thanks!

[Jerrrry]

assuming unbounded time and memory.

not being pedantic.

you can exhaustively enumerate all inputs for a program.

tautologically self-references aside, axiomatically, yes, we can determine if a program will halt, if it has a finite amount of time, or memory.

if it doesn't [have unbounded range], then it must [terminate], but it is very, very, very hard to determine if that is the case.

but not impossible.

and this nuance being lost seems so pedantic, but so integral to the claim, that I can't help but think those who repeat this sans the disclaimer, do not _truly_ understand the paradox

[Kranar → Jerrrry]

This isn't true in any meaningful way and doesn't really make much sense, it's really just repeating the conclusion of the halting problem in the form of an assumption. Any algorithm that halts will do so, by definition, after a finite amount of time and use a finite amount of space, so saying "assuming unbounded time and memory" is begging the question and taking the conclusion as an assumption.

The very problem is that there is no algorithm that can output whether an arbitrary algorithm on a given input needs unbounded time to begin with.

>if it doesn't [have unbounded range], then it must [terminate], but it is very, very, very hard to determine if that is the case.

This is also false. You can limit the scope of the halting problem to algorithms that have a range of one single input and the halting problem is still undecidable. Heck, you can limit the halting problem to algorithms that don't even take any input whatsoever, they just have a start button and either they halt or do not halt, and that problem is still undecidable. The range has nothing to do with it.

[bruce343434 → Kranar]

Yes it does. This is about turning the computer from a turing machine into a finite automaton. Finite automata can be analyzed for halting in finite time, turing machines can’t. And computers as we know them are not turing machines (which are by definition infinite) but they are state machines, and finite ones at that.

[Kranar → bruce343434]

There is no way to turn a Turing Machine into a finite automaton.

All finite automatons are guaranteed to halt, and do so in linear time. There is nothing to analyze the answer is always true.

[bruce343434 → Kranar]

No but I’m saying: computers are not turing machines because they are not infinite. So they must be finite automata.

[Jerrrry → Kranar]

exhaustively enumerating all inputs (and thus, outputs) to a program does, without infinite time or memory, turn it into an automaton.

you could then, since having gone over EVERY INPUT...conclude Yes or No, that it Does or Doesn't, HALT.

wtf am i missing

[danielheath → Jerrrry]

Taking infinite time to determine whether it halts is not considered a valid answer.

When do you give up and decide it’s not going to terminate? Your answer will be wrong for any program which simply waits one second longer.

[Jerrrry → danielheath]

that part is understood.

a dripping faucet, for example - is it dripping at 10 drips per hour? or 5 drips per hour? did it stop dripping? no way to tell - the period between drops could be one moment longer than you observed - it could had dripped right after you stopped observing it.

this upper limit is called the busy beaver function. but it is only applicable to turing machines, which we don't build, because we don't have an infinite tape.

[Animats → Jerrrry]

That's correct. With determinism and finite memory, you must eventually either repeat a previous state, or halt.

This is useful. Verifiers which work by symbolic execution examine large numbers of cases they work through the control flow. Each case can contain a large number of states; you only need one case for each control flow pattern. Now, some programs run into combinatorial explosion when you do that. The number of cases to be examined grows rapidly. That means halting detection is NP-hard, not impossible. There's a difference.

The Microsoft Static Driver Verifier operates on the assumption that if symbolic execution doesn't terminate after a reasonable amount of automatic analysis, your driver doesn't get to run in the kernel. This is a good, practical solution.

[andreareina → Animats]

Checking my understanding: Are you saying that the halting problem is computable (if still completely infeasible in general) for all finite deterministic machines, and that the uncomputability of the busy beaver sequence[1] is due to the infinite memory of Turing machines even though the busy beavers themselves are finite?

ETA: wait that doesn't make sense because it's equivalent to computing the busy beaver number for the program under consideration. What am I missing?

[1] I'm aware there's no unique BB sequence, I don't know that the rigorous phrasing is.

[Animats → andreareina]

Checking my understanding: Are you saying that the halting problem is computable (if still completely infeasible in general) for all finite deterministic machines

Yes. There's even a practical way to check if a finite deterministic machine has repeated a previous state. Run two of them in parallel, in lockstep so that one takes two steps while the other takes one. If they ever have identical state, they're in a loop. This takes 1.5x the compute power plus 2x as much memory, so it's far cheaper than storing all previous states.

(Some early mainframe era educational interpreter supposedly did this, to stop simple student infinite loops quickly in a batch system.)

Here's a paper on the busy beaver problem which discusses upper bounds.[1] The key here is that the upper bound on states is not computable. However, if you force an upper bound by limiting memory, it becomes computable. But really hard. That paper discusses how very rapidly the number of states grows for that problem.

[1] https://homepages.hass.rpi.edu/heuveb/Teaching/Logic/CompLog...

[andreareina → Animats]

I see! I didn't make the connection that bounding the memory necessarily bounds the number of steps as well. Obvious in hindsight.

[jmalicki → Jerrrry]

The other huge thing a ton of people miss when repeating is that the undecidability is between "definitely terminates" vs. "definitely does not terminate".

A ton of useful stuff (for instance in compiler optimizers) can be done with deciding between "trivial to prove it terminates" vs. "who knows, this instance of the problem is hard! I'll just skip this optimization in this ridiculously non-representatively rare case."

[Stratoscope → Jerrrry]

  You say that you are not being pedantic,
  So why does that make me feel so frantic?

  If we need unbounded ranges and time,
  Is that in your lifetime, or possibly mine?

  Someday we have to compare all our notes,
  So none will have learned it only by rote.

[tgv → Jerrrry]

You’re talking about FSAs. The fact that we cannot build a real TM is irrelevant.

If you’re only concerned with physically realizable computing: the number of states can easily become too large to be analyzable.

[joe_the_user]

Godel's theorem and the halting problem began as having difficult and obscure proofs. Today, you can find "one page" proofs of either. And these proofs depend strongly on a variety of computation processes going from obscure to obvious for the average person.

Is it "obvious" you can produce program Y that doesn't halt if program X halts? Do you understand one program can be taken as input string of another? If so, the Halting Problem proof in Sudkamp's Languages and Machines, my undergraduate text in the 90s, can indeed take just a page.

[dang]

Related:

Scooping the Loop Snooper: Proof That the Halting Problem Is Undecidable (2000) - https://news.ycombinator.com/item?id=20956756 - Sept 2019 (33 comments)

Scooping the Loop Snooper (2000) - https://news.ycombinator.com/item?id=10077471 - Aug 2015 (2 comments)

[bqmjjx0kac]

If Dr. Seuss had a PhD in CS.

[bradrn → bqmjjx0kac]

Pullum is in fact a well-known linguist.

[xmprt]

Looks like this is from UC Santa Cruz. I wonder what it's doing on Rice's page.

[6gvONxR4sf7o]

I don’t follow this proof. If Q takes an executable program, then Q(x) is executable, but Q alone isn’t. So you can ask questions about Q(Q(x)), but Q(Q) shouldn’t type check, as the inner Q isn’t executable without an argument. Am I being dumb? How would you do this proof with types?

[Kranar → 6gvONxR4sf7o]

Define P(A, S) as the function that takes as input an algorithm A and a string S and returns true if A(S) halts, and false if A(S) does not halt. The claim is that P does not exist.

Assume P exists, let Q(S) be the function that takes a string S and halts if P(Q, S) returns false, otherwise it loops forever. Q(S) is not some whacky function either, in TypeScript it could be implemented as follows:

    function P(A: (S: string) => void, S: string): boolean;

    function Q(S: string): void {
      if(P(Q, S)) {
        while(true) {}
      }
    }

But then you have the following contradiction:

If P(Q, S) returns false, then that implies Q(S) runs forever, but by definition Q(S) halts when P(Q, S) returns false, so P was incorrect about Q(S).

If P(Q, S) returns true, then that implies Q(S) halts, but by definition Q(S) loops forever when P(Q, S) returns true, so P was incorrect about Q(S).

This exhausts all possibilities, hence our assumption that there is such a P must be false.

[6gvONxR4sf7o → Kranar]

Okay, you got me thinking about this more generally, and it seems like this sort of proof can disprove all sorts of checkers:

    function HasPropertyX(A: (S: string) => void, S: string): boolean;

    function Q(S: string): void {
        if(HasPropertyX(Q, S)) {
            AvoidHavingX();
        } else {
            HaveX();
        }
    }

For example, no program can exist that checks whether another program raises an exception on some argument (pseudocode, since I don't really know typescript):

    function RaisesException(A: (S: string) => void, S: string): boolean;

    function Q(S: string): void {
        if(RaisesException(Q, S)) {
            pass;
        } else {
            raise Exception;
        }
    }

and no program can exist that determines whether a given bit of code blows up the planet:

    function BlowsUpThePlanet(A: (S: string) => void, S: string): boolean;

    function Q(S: string): void {
        if(BlowsUpThePlanet(Q, S)) {
            pass;
        } else {
            HitTheBigRedButtonAndGoKaboom();
        }
    }

and you can't even test whether f(x) is true:

    function ReturnsTrue(A: (S: string) => boolean, S: string): boolean;

    function Q(S: string): boolean {
        return not ReturnsTrue(Q,S);
    }

It seems like it any property you can exhibit in HaveX cannot be checked for, leading me to think that this is a proof that you can't definitively check for pretty much anything in programs, but that seems too far.

Am I getting this right? How far does this go? Is there a deeper theorem about the limitations of program checking that brings this all together?

[Kranar → 6gvONxR4sf7o]

You are absolutely correct and you have discovered Rice's Theorem [1]. The fact that you generalized the halting problem on your own is a very good indication that you fundamentally understand it.

[1] https://en.wikipedia.org/wiki/Rice%27s_theorem

[6gvONxR4sf7o → Kranar]

I certainly do feel like I understand it better now. Thanks again for the pointers!

[6gvONxR4sf7o → Kranar]

Ah, thanks for spelling it out with the typescript. That’s clearer to me now!

[enedil → 6gvONxR4sf7o]

Well, if you know anonymous function, it should be easy to understand what happens. Functions are first-class objects here. Q is a procedure that takes an arbitrary procedure. It's not that you run the procedure. In fact, it's another way around, you want to say something about the source code of the function, not the result of applying it.

[throwaway81523]

(2000), worth a read.