检查两个 yacc 语法是否等效

Question

您已经编写了 yacc 语法（或您选择的工具中的其他一些 LALR 语法），并且您决定要重构一些产生式以提高效率、清晰度等。例如，您有：

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

您想让更明显的是可以有多个分号，因此您将其重写为：

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

好吧，看起来似乎有道理……但是我真的正确地进行了重构吗？如果我可以将这些声明传递给一个工具来告诉我语法是否等效，那就太好了。 （现在，让我们只考虑我们是否识别相同语言的问题。）

一个下意识的反应是引用上下文无关语法等价是不可判定的。事实上，即使确定 CFG 是否是正则的问题也是不可判定的。但 yacc 不识别 CFG：它识别确定性上下文无关语法，并且对于这些语法，已知等价是可判定的。但有人实施过这些决策程序吗？

Answer 1

（一个很晚的答案；我希望它对某些人有用。）

确实有一个实现。它甚至是由 Sénizergues 共同创作的，他最初证明了确定性上下文无关语言 (DCFL) 的等价问题是可判定的：

帕特里克·亨利、热罗·塞尼泽格： LALBLC 一个测试 dpda 等价性的程序。 CIAA 2013：169-180

请注意，上述算法在最坏的情况下可能会运行很长时间。

---

对于对计算机科学基础感兴趣的读者：

总的来说，人们对于未来算法解决该问题的效率可能有多高仍知之甚少。也就是说，人们对问题的“固有”计算复杂性知之甚少。最近的一篇论文

张文波、殷强、龙欢、徐贤。

下推自动机的互模拟等价是阿克曼完备的。

第 47 届自动机、语言和编程国际研讨会 (ICALP 2020)。莱布尼茨国际信息学学报 (LIPIcs)，第 168 卷，第 141:1-141:14

在引言中回顾了这方面的最新技术和相关问题。 它指出 DCFL 等价问题的最快已知算法的运行时间最多是一个指数塔，如下文所示。

Petr Jancar：

下推系统的等价性很难

。 FoSSaCS 2014：1-28

关于问题复杂性的下限，上述调查表明人们知之甚少。特别是，我们甚至不知道问题是否是 NP 困难的。不可否认，与最佳“已知”算法的指数塔运行时间机制相比，非确定性多项式时间显得相形见绌。