I meant, given a turing machine, judge whether a pushdown automaton will halt.
Pushdown automaton: a finite state machine with a stack
If so, is there any unsolvable problem weaker than halting problem?
[Math] Can turing machine solve halting problem on a pushdown automaton
pushdown-automataturing-machines
Related Solutions
I think the following portion from your question is most important:
But, the halting-detection machines used by the Busy Beaver researchers don't have too much power. They have too little power. Currently they can't solve $n=5$. OK, so we give them some more power. Maybe at some point they can solve $n=5$ ... but they still can't solve $n=6$. Maybe we can give them enough power to solve $n=6$, or $n=7$
or ....
... so my question is: is there some 'special' value of $n$, say $n=m$ where this has to stop. Where, somehow, the only way to solve $n=m$, is by a machine that has 'too much' power? But why would that be?
The solution to solving $\Sigma(5)$ isn't simply giving Turing machines "more power." The reason we don't know $\Sigma(5)$ right now is because there are 5-state Turing machines which mathematicians believe will never halt, but have not been able to prove will never halt. The problem is not as simple as just enumerating through all of the 5-state Turing machines since once you've done that, you still need to figure out if the Turing machine halts or not, which, as you know, is not a trivial problem. We've been able to do this for 4-state Turing machines, but we don't know yet if we can do this for 5-state Turing machines because there may very well be 5-state Turing machines which we can never prove to be halting/non-halting within the system of classical mathematics (that is, ZFC).
Now, you've asked what is the magic number is: What is the magic number $n=m$ such that we will never be able to solve for $\Sigma(n)$? As I've said above, that magic number could very well be $n=5$, but that hasn't been proven yet. However, mathematicians have proven that $\Sigma(1919)$ is indeed un-knowable within ZFC. Before explaining this, I think it might be helpful to quote your question again:
Then again, these machine don't do any explicit analysis of the machines involved ... they just happen to give the right value. So, maybe there is still some value of $n$ where the approach of actually trying to analyze and predict the behavior of machine starts to break down for some fundamental, again possibly self-referential, reason?
My answer to this question is yes, there is a 1919-state Turing machine such that trying to predict if the machine halts would be fundamentally unsolvable within our system of mathematics. See, the way mathematicians proved $\Sigma(1919)$ is unsolvable is by constructing a 1919-state Turing machine $M$ which halts if there is a contradiction within ZFC and never halts if ZFC is consistent. However, there's no way to prove ZFC is consistent using the axioms of ZFC because of Godel's Second Incompleteness Theorems. This means we can never use the ZFC axioms of mathematics to prove machine $M$ ever halts or not because doing so would constitute a proof that ZFC is consistent. Thus, mathematicians can't predict if machine $M$ halts or not because of Godel's Incompleteness Theorem, which means that the busy-beaver problem for 1919-state Turing machines is unsolvable.
I hope this gives you some more insight into why $\Sigma(n)$ is solvable for small values of $n$ but unsolvable for larger values of $n$. Anyway, I am certainly not an expert in theory of computation, so if someone would like to add an alternate explanation/clarifying comments to my answer, feel free. Thanks!
Best Answer
Yes, the halting problem for PDAs is decideable. The current snapshot of a PDA is determined by: the unread symbols in the input, the state of the deterministic control, the symbol on top of the stack.
Here's a two-tape TM that decides whether a PDA $P$ will halt on input $x$:
The input $x$ is written on the first tape.
The machine simulates the PDA using the first tape for storage. In particular, the first tape will contain the input $x$ (the machine erases the input symbols as it reads them), the current state of the PDA's finite control, and also a list of all symbols on the simulated PDA's stack.
After it simulates a step of the PDA, the TM appends the current snapshot of the PDA onto the second tape. It copies over the remaining input, the current state, and the symbol at the top of the stack.
So the second tape contains a list of every snapshot that the PDA has ever been in.
Every time the TM copies over a new snapshot, it should check to see whether that exact snapshot has occurred on the tape already. If it has, the PDA has entered into a loop and will never halt. The TM should reject.
The PDA will either halt within finitely many steps, or will loop forever. There are $Q\times n \times \Gamma$ possible snapshots, where $Q$ is the current PDA state, $n$ is the number of symbols in the input, and $\Gamma$ is the number of symbols in the stack alphabet. For this reason, the machine will either halt within $Q\times n\times \Gamma$ steps, or (by the pigeonhole principle) loop forever. The problem is therefore decideable.