I'm aware that the halting problem is solvable for PDAs, but I have recently discovered that I am wrong about how to actually do it. I used to think that you could detect an infinite loop by meeting these four conditions:
- arrive at the same state as you were in previously
- with the same top symbol as you had last time
- without consuming anything on the stack, and
- without consuming any input.
...but this appears to actually be untrue for nondeterministic PDAs. Consider this machine:
It accepts the empty string, but it matches all of my infinite-loop detecting criteria in the first state before it can do so.
The following version even contains infinite paths to accepting the empty string:
I am coding a NPDA simulator in Scheme, and while I am happy to accept that the halting problem is solvable for a PDA, I am clearly wrong about how it is accomplished. How can it actually be done?