Search code examples
bisonyacc

Validating the equivalence between 2 different .y files


My original .y file leads to some shift/reduce and reduce/reduce conflicts.
So I changed some rules to eliminate these conflicts. And I can validate the equivalence between the new and old version manually.

However, I want to validate the new version is equivalent to the original one automatically? How?


Solution

  • In the general case, it is not possible to automatically prove equivalence because the equivalence of two CFGs is undecidable. A proof for this well-known result can be found in any textbook on computability.

    There are some special cases which are decidable, but most of them are not particularly useful. For example, you can prove equivalence of two finite languages by simply enumerating all sentences. You can prove equivalence of two regular languages by constructing their respective minimal DFAs and comparing. Etc.

    In the case of yacc/bison, if you succeeded in "eliminating" shift-reduce conflicts by adding appropriate precedence declarations without making other changes (a classic way to "fix" the dangling else problem), you could simply examine the parse tables (or the output of bison's --report to verify that there were no changes; that is, that the precedence declarations encoded bison's default conflict resolution and so only removed the warnings. Since reduce-reduce conflict resolution cannot be affected by precedence, this won't apply to changes which removed reduce-reduce conflict warnings, but if the changes were simple enough you might still be able to manually construct a proof based on comparing the generated automata.

    Even if you had a proof, you would want to do exhaustive testing, I think. After all, there might be an error in the proof.