A Semantic Framework for PEGs

TL;DR

This paper introduces a formal rewriting logic semantics for PEGs, enabling better understanding, control of backtracking, and serving as a foundation for parser optimization and analysis.

Contribution

It develops a rewriting logic framework for PEGs, including a formal semantics for cuts, enhancing parser control and analysis capabilities.

Findings

Semantic framework for PEGs established

Cuts mechanism formalized within the framework

Executable semantics useful for testing and optimization

Abstract

Parsing Expression Grammars (PEGs) are a recognition-based formalism which allows to describe the syntactical and the lexical elements of a language. The main difference between Context-Free Grammars (CFGs) and PEGs relies on the interpretation of the choice operator: while the CFGs' unordered choice e | e' is interpreted as the union of the languages recognized by e and e, the PEGs' prioritized choice e/e' discards e' if e succeeds. Such subtle, but important difference, changes the language recognized and yields more efficient parsing algorithms. This paper proposes a rewriting logic semantics for PEGs. We start with a rewrite theory giving meaning to the usual constructs in PEGs. Later, we show that cuts, a mechanism for controlling backtracks in PEGs, finds also a natural representation in our framework. We generalize such mechanism, allowing for both local and global cuts with a precise, unified and formal semantics. Hence, our work strives at better understanding and controlling backtracks in parsers for PEGs. The semantics we propose is executable and, besides being a parser with modest efficiency, it can be used as a playground to test different optimization ideas. More importantly, it is a mathematical tool that can be used for different analyses.