LL(1) Parsing with Derivatives and Zippers

TL;DR

This paper introduces a new, efficient, formally verified LL(1) parser based on derivatives and zippers, improving performance and correctness for parsing context-free expressions.

Contribution

It develops a linear-time, formally verified parsing algorithm for LL(1) expressions using derivatives and zippers, with a practical Scala implementation.

Findings

Linear-time parsing algorithm for LL(1) expressions

Formal verification of the parser correctness in Coq

Implementation as a Scala parser combinator framework

Abstract

In this paper, we present an efficient, functional, and formally verified parsing algorithm for LL(1) context-free expressions based on the concept of derivatives of formal languages. Parsing with derivatives is an elegant parsing technique, which, in the general case, suffers from cubic worst-case time complexity and slow performance in practice. We specialise the parsing with derivatives algorithm to LL(1) context-free expressions, where alternatives can be chosen given a single token of lookahead. We formalise the notion of LL(1) expressions and show how to efficiently check the LL(1) property. Next, we present a novel linear-time parsing with derivatives algorithm for LL(1) expressions operating on a zipper-inspired data structure. We prove the algorithm correct in Coq and present an implementation as a parser combinators framework in Scala, with enumeration and pretty printing capabilities.