Earley Parser

Martin Rau 📧

July 16, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


In 1968, Earley introduced his parsing algorithm, capable of parsing all context-free grammars in cubic space and time. This entry contains a formalization of an executable Earley parser. We base our development on Jones' extensive paper proof of Earley's recognizer and Obua's formalization of context-free grammars and derivations. We implement and prove correct a functional recognizer modeling Earley's original imperative implementation and extend it with the necessary data structures to enable the construction of parse trees, following the work of Scott. We then develop a functional algorithm that builds a single parse tree, and we prove its correctness. Finally, we generalize this approach to an algorithm for a complete parse forest and prove soundness.


BSD License


Session Earley_Parser