A Semantic Framework for PEGs
summary
Presents an executable formalization that uses a rewriting logic executable specification (Maude) to add a throw operator (cut) to PEGs so failing certain subexpressions signals an error and prevents useless backtracking. Implements cuts by hand on JSON C and Titan grammars, measures parser rule applications, finds small overhead on valid inputs and savings on invalid ones (C tests show 2%–11% fewer rules). Provides a prototype parser and a repository and claims the framework can prove cuts preserve the language.
AI-written summary · about
chapters (12)
- 0:00Intro
- 0:37Parsing Expression Grammars (PEGs) (2)
- 1:35PEGs Semantics (excerpt)
- 3:41PEGs Cons: What is the language?
- 4:59PEGs Cons: How to Control the Backtracking?
- 6:30Using Rewriting Logic to reason about PEGS
- 7:35Rewriting Logic Specification
- 8:47Semantics Considering Global Errors
- 10:46Catching Local Errors
- 12:50Evaluation Results
- 13:27Conclusion
- 13:53Future Work
related talks
23mA Verified Packrat Parser Interpreter for Parsing Expression Grammars
14mFast Incremental PEG Parsing
44mParsing Text with a Virtual Machine
29mSemantic Transformation Framework for Rewriting Rules
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs
14mA Derivative-based Parser Generator for Visibly Pushdown Grammars
16mAutomatically Deriving Control-Flow Graph Generators from Operational Semantics
30mTrustworthy Formal Natural Language Specifications