### Abstract

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.

### License

BSD License

### Topics

- Computer science/Algorithms

### Session Earley_Parser

- Limit
- CFG
- Derivations
- Earley
- Earley_Fixpoint
- Earley_Recognizer
- Earley_Parser
- Examples

## Cite

×

Earley_Parser-AFP

    @article{Earley_Parser-AFP,
      author  = {Martin Rau},
      title   = {Earley Parser},
      journal = {Archive of Formal Proofs},
      month   = {July},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Earley_Parser.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Aug 8, 2023 : Isabelle2022