Checking if two yacc grammars are equivalent

Question

You've written a yacc grammar (or some other LALR grammar in the tool of your choice), and you've decided that you want to refactor some productions for efficiency, clarity, whatever. For example, you had:

xs : xs ';' x
   | xs ';'
   | x

You want to make it more obvious that there can be multiple semicolons, so you rewrite it as:

semi_plus : semi_plus ';'
          | ';'
xs : xs semi_plus x
   | x

OK, so, looks plausible... but did I actually do the refactoring correctly? It would be great if I could pass these declarations to a tool that would tell me if the grammars are equivalent or not. (For now, let us consider solely the question of whether or not we recognize the same languages.)

One knee-jerk reaction is to quote that context free grammar equivalence is undecidable. In fact, even the problem of determining if a CFG is regular is undecidable. But yacc does not recognize CFGs: it recognizes deterministic context free grammars, and for these, it is known that equivalence is decidable. But has anyone implemented any of these decision procedures?

Labanna

The link you provide with text "equivalence is decidable" does not, in fact, provide any references relevant to that question. Indeed, when Hopcroft and Ullman wrote their magnificent text, it was not yet known whether equivalence of two DCFLs is decidable. That fact was not proven until 1997, and afaik it is still not known whether or not there is a polynomial time algorithm. You appear to be confusing regularity with DCFLs, in some way: equivalence of DFAs is straightforward (and the algo is in H&U iirc) but a DCFL might not be regular. – Transude

Thank you for the fix rici; I did read somewhere that DCFL/DPDA equivalence was decidable but I must have pasted in the wrong link. The link is fixed now (I've decided to link straight to Stirling's proof, on the recommendation of Bob Atkey) – Labanna

Answer 1

(A very late answer; I hope that it is still useful.)

There is indeed an implementation. It is even co-authored by Sénizergues, who originally proved that the equivalence problem for deterministic context-free languages (DCFL) is decidable:

Patrick Henry, Géraud Sénizergues: LALBLC A Program Testing the Equivalence of dpda's. CIAA 2013: 169-180

Beware that the above algorithm may run for a very long time in the worst case.

---

For readers interested in foundations of computer science:

In general, it is still poorly understood how efficient future algorithms for the problem could possibly be. That is, little is known about the inherent computational complexity of the problem. A recent paper

Wenbo Zhang, Qiang Yin, Huan Long, and Xian Xu. Bisimulation Equivalence of Pushdown Automata Is Ackermann-Complete. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 141:1-141:14

reviews the state of the art on this and related problems in the introduction. It states that the fastest known algorithm for the DCFL equivalence problem has a running time which is at most a tower of exponentials, as given in the following paper.

Petr Jancar: Equivalences of Pushdown Systems Are Hard. FoSSaCS 2014: 1-28

Regarding lower bounds on the complexity of the problem, the abovementioned survey says that very little is known. In particular, we don't even know whether the problem is NP-hard. And admittedly, nondeterministic polynomial time is dwarfed by the tower-of-exponentials running time regime of the best known algorithm.

Gibran