Reference. Parsing with derivatives: A functional pearl

Matthew Might, David Darais, Daniel Spiewak · ICFP · 2011 · parsing · PDF · DOI · pldb

We present a functional approach to parsing unrestricted context-free grammars based on Brzozowski’s derivative of regular expressions. If we consider context-free grammars as recursive regular expressions, Brzozowski’s equational theory extends without modification to context-free grammars (and it generalizes to parser combinators). The supporting actors in this story are three concepts familiar to functional programmers - laziness, memoization and fixed points; these allow Brzozowski’s original equations to be transliterated into purely functional code in about 30 lines spread over three functions.

Yet, this almost impossibly brief implementation has a drawback: its performance is sour - in both theory and practice. The culprit? Each derivative can double the size of a grammar, and with it, the cost of the next derivative.

Fortunately, much of the new structure inflicted by the derivative is either dead on arrival, or it dies after the very next derivative. To eliminate it, we once again exploit laziness and memoization to transliterate an equational theory that prunes such debris into working code. Thanks to this compaction, parsing times become reasonable in practice.

We equip the functional programmer with two equational theories that, when combined, make for an abbreviated understanding and implementation of a system for parsing context-free languages.

Cite
Cite as @mightParsingDerivativesFunctional2011 (helia, typst) · \cite{mightParsingDerivativesFunctional2011} (LaTeX)
BibTeX
bibtex · 16 lines
@inproceedings{mightParsingDerivativesFunctional2011,
 title = {Parsing with derivatives: a functional pearl},
 author = {Might, Matthew and Darais, David and Spiewak, Daniel},
 year = {2011},
 isbn = {978-1-4503-0865-6},
 doi = {10.1145/2034773.2034801},
 url = {https://dl.acm.org/doi/10.1145/2034773.2034801},
 urldate = {2024-04-29},
 booktitle = {Proceedings of the 16th {ACM} {SIGPLAN} international conference on {Functional} programming},
 pages = {189--195},
 publisher = {ACM},
 address = {Tokyo Japan},
 month = {September},
 language = {en},
 shorttitle = {Parsing with derivatives}
}
hayagriva YAML (typst)
yaml · 23 lines
mightParsingDerivativesFunctional2011:
  type: article
  title:
    value: 'Parsing with derivatives: a functional pearl'
    short: Parsing with derivatives
  author:
  - Might, Matthew
  - Darais, David
  - Spiewak, Daniel
  date: 2011-09
  page-range: 189-195
  url:
    value: https://dl.acm.org/doi/10.1145/2034773.2034801
    date: 2024-04-29
  serial-number:
    doi: 10.1145/2034773.2034801
    isbn: 978-1-4503-0865-6
  parent:
    type: proceedings
    title: Proceedings of the 16th {ACM} {SIGPLAN} international conference on {Functional} programming
    publisher:
      name: ACM
      location: Tokyo Japan
Download: mightParsingDerivativesFunctional2011.bib · mightParsingDerivativesFunctional2011.yml
Cited by (2)

CoStar: A verified ALL(*) parser lasserCoStarVerifiedALL2021PLDI · 2021
Parsers are security-critical components of many software systems, and verified parsing therefore has a key role to play in secure software design. However, existing verified parsers for context-free grammars are limited in their expressiveness, termination properties, or performance characteristics. They are only compatible with a restricted class of grammars, they are not guaranteed to terminate on all inputs, or they are not designed to be performant on grammars for real-world programming languages and data formats. In this work, we present CoStar, a verified parser that addresses these limitations. The parser is implemented with the Coq Proof Assistant and is based on the ALL(*) parsing algorithm. CoStar is sound and complete for all non-left-recursive grammars; it produces a correct parse tree for its input whenever such a tree exists, and it correctly detects ambiguous inputs. CoStar also provides strong termination guarantees; it terminates without error on all inputs when applied to a non-left-recursive grammar. Finally, CoStar achieves linear-time performance on a range of unambiguous grammars for commonly used languages and data formats.
PDF · DOI · pldb

Zippy LL(1) parsing with derivatives EdelmannZippy2020PLDI · 2020
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 part of Scallion, a parser combinators framework in Scala with enumeration and pretty printing capabilities.
DOI · pldb
Cites 19 works (5 here)
With notes (5)

Total parser combinators danielssonTotalParserCombinators2010ICFP · 2010

A monadic parser combinator library which guarantees termination of parsing, while still allowing many forms of left recursion, is described. The library’s interface is similar to those of many other parser combinator libraries, with two important differences: one is that the interface clearly specifies which parts of the constructed parsers may be infinite, and which parts have to be finite, using dependent types and a combination of induction and coinduction; and the other is that the parser type is unusually informative.

The library comes with a formal semantics, using which it is proved that the parser combinators are as expressive as possible. The implementation is supported by a machine-checked correctness proof.

PDF · DOI · pldb

Regular-expression derivatives re-examined owensRegularexpressionDerivativesReexamined2009JFP · 2009
Abstract Regular-expression derivatives are an old, but elegant, technique for compiling regular expressions to deterministic finite-state machines. It easily supports extending the regular-expression operators with boolean operations, such as intersection and complement. Unfortunately, this technique has been lost in the sands of time and few computer scientists are aware of it. In this paper, we reexamine regular-expression derivatives and report on our experiences in the context of two different functional-language implementations. The basic implementation is simple and we show how to extend it to handle large character sets (e.g., Unicode). We also show that the derivatives approach leads to smaller state machines than the traditional algorithm given by McNaughton and Yamada.
PDF · DOI · pldb

An efficient context-free parsing algorithm Earley1970CACM · 1970
A parsing algorithm which seems to be the most efficient general context-free algorithm known is described. It is similar to both Knuth’s LR(k) algorithm and the familiar top-down algorithm. It has a time bound proportional to n3 (where n is the length of the string being parsed) in general; it has an n2 bound for unambiguous grammars; and it runs in linear time on a large class of grammars, which seems to include most practical context-free programming language grammars. In an empirical comparison it appears to be superior to the top-down and bottom-up algorithms studied by Griffiths and Petrick.
DOI

On the translation of languages from left to right KNUTH1965607I&C · 1965
There has been much recent interest in languages whose grammar is sufficiently simple that an efficient left-to-right parsing algorithm can be mechanically produced from the grammar. In this paper, we define LR(k) grammars, which are perhaps the most general ones of this type, and they provide the basis for understanding all of the special tricks which have been used in the construction of parsing algorithms for languages with simple structure, e.g. algebraic languages. We give algorithms for deciding if a given grammar satisfies the LR(k) condition, for given k, and also give methods for generating recognizes for LR(k) grammars. It is shown that the problem of whether or not a grammar is LR(k) for some k is undecidable, and the paper concludes by establishing various connections between LR(k) grammars and deterministic languages. In particular, the LR(k) condition is a natural analogue, for grammars, of the deterministic condition, for languages.
DOI

Derivatives of Regular Expressions brzozowskiDerivativesRegularExpressions1964JACM · 1964
Kleene’s regular expressions, which can be used for describing sequential circuits, were defined using three operators (union, concatenation and iterate) on sets of sequences. Word descriptions of problems can be more easily put in the regular expression language if the language is enriched by the inclusion of other logical operations. However, in the problem of converting the regular expression description to a state diagram, the existing methods either cannot handle expressions with additional operators, or are made quite complicated by the presence of such operators.In this paper the notion of a derivative of a regular expression is introduced and the properties of derivatives are discussed. This leads, in a very natural way, to the construction of a state diagram from a regular expression containing any number of logical operators.
DOI
External (14)
mightParsingDerivativesFunctional2011 reference entries/refs/mightParsingDerivativesFunctional2011/mightParsingDerivativesFunctional2011.hel