2つの異なる.yファイル間の等価性を確認する

Question

私の元の.yファイルは、ある程度のシフト/リダクションと削減/削減の競合を引き起こします。
そこで、これらの競合を解消するためにいくつかのルールを変更しました。そして私は新しいバージョンと古いバージョンとの間の等価性を手動で検証することができます。

しかし、私は新しいバージョンが自動的に元のバージョンと同等であることを検証したいですか？どうやって？

Answer 1

一般的に、2つのCFGの等価性は決めることができないため、等価性を自動的に証明することはできません。このよく知られた結果の証明は、計算能力に関するあらゆる教科書に見出すことができます。

決定可能な特殊なケースがいくつかありますが、そのほとんどは特に有用ではありません。たとえば、すべての文を列挙するだけで、2つの有限言語の等価性を証明できます。それぞれの最小限のDFAを構築して比較することで、2つの正規言語の等価性を証明することができます。その他

yacc/bisonの場合、他の変更を行わずに適切な優先順位宣言を追加してshift-reduce競合を「削除」することに成功した場合（他の問題を「修正」する古典的な方法）、単純に解析テーブル（またはbisonの--reportの出力を調べて、変更がなかったことを確認します。つまり、優先順位宣言によってbisonのデフォルトの競合解決がエンコードされ、警告のみが削除されます）reduce-reduce競合解決は優先順位によって影響を受けませんこれはreduce-reduce競合警告を削除した変更には適用されませんが、変更が簡単であれば、生成されたオートマトンを比較して手動で証明を作成することができます。

証拠があったとしても、網羅的なテストをしたいと思うと思います。結局のところ、証明に誤りがあるかもしれません。