驗證兩個不同的.y文件之間的等價性

Question

我的原始.y文件導致一些轉換/減少並減少/減少衝突。
所以我改變了一些規則來消除這些衝突。我可以手動驗證新版本和舊版本之間的等效性。

但是，我想驗證新版本是否自動等同於原始版本？怎麼樣？

Answer 1

在一般情況下，由於兩個CFG的等價性是不可判定的，所以不可能自動證明等價。關於這個衆所周知的結果的證明可以在任何關於可計算性的教科書中找到。

有一些可確定的特殊情況，但其中大多數並不特別有用。例如，您可以通過簡單列舉所有句子來證明兩種有限語言的等價性。你可以通過構造它們各自的最小DFA和比較來證明兩種正則語言的等價性。等等

在yacc/bison的情況下，如果您通過添加適當的優先級聲明而不做其他更改（一種經典的方法來「修復」懸而未決的問題），從而成功地「消除」只需檢查分析表（或者野牛--report的輸出以驗證沒有變化;也就是說，優先聲明編碼了bison的默認衝突解決方案，因此只刪除了警告。由於reduce-reduce衝突解決方案不受優先級影響，這將不適用於刪除減少 - 減少衝突警告的更改，但如果更改足夠簡單，則可能仍然可以基於比較生成的自動機而手動構建證明。即使你有證據，我想你也會想做詳盡的測試。畢竟，證明中可能存在錯誤。