一句话：提出首个高效、实用且经 Coq 证明正确的静态可消解歧义方案，并集成到 OCaml 解析器。
传统编程语言语法通常无歧义，但近期工作提出使用歧义文法并把消歧推迟给用户。若歧义文法接受的所有程序都能被无歧义重写，则称解析器具有可消解歧义；然而对所有程序静态保证这一点很难，先前工作仅用基于属性的测试部分解决。本文提出首个高效、实用且被证明正确的静态可消解歧义方案。方法上引入可拆分产生式、算符序列以及与标准解析器协同工作的 grouper 等关键概念。作者用 Coq 机器化证明静态可消解性，并通过实现该方案并集成到标准 OCaml 解析器的关键部分，展示其效率和实用适用性。
Traditionally, a grammar defining the syntax of a programming language is typically both context free and unambiguous. However, recent work suggests that an attractive alternative is to use ambiguous grammars,thus postponing the task of resolving the ambiguity to the end user. If all programs accepted by an ambiguous grammar can be rewritten unambiguously, then the parser for the grammar is said to be resolvably ambiguous. Guaranteeing resolvable ambiguity statically---for all programs---is hard, where previous work only solves it partially using techniques based on property-based testing. In this paper, we present the first efficient, practical, and proven correct solution to the statically resolvable ambiguity problem. Our approach introduces several key ideas, including splittable productions, operator sequences, and the concept of a grouper that works in tandem with a standard parser. We prove static resolvability using a Coq mechanization and demonstrate its efficiency and practical applicability by implementing and integrating resolvable ambiguity into an essential part of the standard OCaml parser.
@article{paperbot2118,
title = {Statically Resolvable Ambiguity},
author = {Viktor Palmkvist and Elias Castegren and Philipp Haller and David Broman},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571251}
}