基于导数与拉链的 LL(1) 解析
形式语言与自动机理论
2021-01-22 v2 数据结构与算法
摘要
在本文中，我们提出了一种高效、函数式且经形式化验证的 LL(1) 上下文无关表达式解析算法，该算法基于形式语言导数的概念。导数解析是一种优雅的解析技术，在一般情况下其最坏情况时间复杂度为立方级且实际性能较慢。我们将导数解析算法特化到 LL(1) 上下文无关表达式，其中在给定单个前瞻记号的情况下即可选择候选式。我们形式化了 LL(1) 表达式的概念并展示了如何高效检查 LL(1) 性质。接下来，我们提出了一种新颖的针对 LL(1) 表达式的线性时间导数解析算法，其运行于受拉链启发的数据结构上。我们在 Coq 中证明了该算法的正确性，并给出了一个作为 Scala 中解析器组合子框架的实现，具备枚举与漂亮打印能力。
引用
@article{arxiv.1911.12737,
title = {LL(1) Parsing with Derivatives and Zippers},
author = {Romain Edelmann and Jad Hamza and Viktor Kunčak},
journal= {arXiv preprint arXiv:1911.12737},
year = {2021}
}
备注
Appeared at PLDI'20 under the title "Zippy LL(1) Parsing with Derivatives"