A Note on Proofs of Earley’s Recognizer
摘要
This paper presents the formalization and verification (in the proof assistant Isabelle) of an abstract inductive version of Earley’s recognizer, relates it to the standard definition and derives an efficient one-pass algorithm for \(\varepsilon \) -free grammars. In particular it compares Jones development of Earley’s recognizer to our own and to the literature.