A Snippet of the proof from the bookIn Michael Sipser's book, they prove that ALL_CFG = { G | G is a CFG and L(G) = Σ∗ } is undecidable using accepting computation histories and PDAs. My question is how exactly (with details of implementation)does a PDA go on to compare two configurations and figure out that the first properly yields the second.

I know that the computation histories are encoded in a convenient manner (reversing), but I couldn't seem to figure out how and what the PDA really does.

  • $\begingroup$ What is "the mentioned language"? Please edit your question to make it self-contained. Please define all notation. How do your question about comparing two configuration relate to the first sentence of your post? $\endgroup$
    – D.W.
    Apr 5 '20 at 23:14
  • $\begingroup$ What is "ALL_CFG"? It would help to define this notation before using it. $\endgroup$
    – D.W.
    Apr 7 '20 at 17:57
  • 1
    $\begingroup$ The answer would be rather verbose to write. The idea is that you can check that the input is of the form $\#w\#w^R\#w\#w^R\# \ldots$, and you can extend this to have the various $w$'s slightly different, following the local computation rules of the Turing machine. Perhaps the original paper bothered to list all the details. $\endgroup$ Apr 7 '20 at 18:00
  • 1
    $\begingroup$ A few more details are in Hendrik Jan's note (see Section 3). You can also check the original papers cited there. $\endgroup$ Apr 7 '20 at 18:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.