Symbolic and automatic differentiation of languages

Reference. Symbolic and automatic differentiation of languages

Conal Elliott · ICFP · 2021 · parsing · PDF · DOI · pldb

Formal languages are usually defined in terms of set theory. Choosing type theory instead gives us languages as type-level predicates over strings. Applying a language to a string yields a type whose elements are language membership proofs describing how a string parses in the language. The usual building blocks of languages (including union, concatenation, and Kleene closure) have precise and compelling specifications uncomplicated by operational strategies and are easily generalized to a few general domain-transforming and codomain-transforming operations on predicates. A simple characterization of languages (and indeed functions from lists to any type) captures the essential idea behind language ``differentiation’‘ as used for recognizing languages, leading to a collection of lemmas about type-level predicates. These lemmas are the heart of two dual parsing implementations—using (inductive) regular expressions and (coinductive) tries—each containing the same code but in dual arrangements (with representation and primitive operations trading places). The regular expression version corresponds to symbolic differentiation, while the trie version corresponds to automatic differentiation. The relatively easy-to-prove properties of type-level languages transfer almost effortlessly to the decidable implementations. In particular, despite the inductive and coinductive nature of regular expressions and tries respectively, we need neither inductive nor coinductive/bisimulation arguments to prove algebraic properties.

Cite

Cite as @elliottSymbolicAutomaticDifferentiation2021 (helia, typst) · \cite{elliottSymbolicAutomaticDifferentiation2021} (LaTeX)

BibTeX

bibtex · 15 lines

@article{elliottSymbolicAutomaticDifferentiation2021,
 title = {Symbolic and Automatic Differentiation of Languages},
 author = {Elliott, Conal},
 year = {2021},
 doi = {10.1145/3473583},
 urldate = {2024-11-10},
 journal = {Proceedings of the ACM on Programming Languages},
 volume = {5},
 number = {ICFP},
 pages = {1--18},
 langid = {english},
 abstract = {Formal languages are usually defined in terms of set theory. Choosing type theory instead gives us languages as type-level predicates over strings. Applying a language to a string yields a type whose elements are language membership proofs describing               how               a string parses in the language. The usual building blocks of languages (including union, concatenation, and Kleene closure) have precise and compelling specifications uncomplicated by operational strategies and are easily generalized to a few general domain-transforming and codomain-transforming operations on predicates.                          A simple characterization of languages (and indeed functions from lists to any type) captures the essential idea behind language ``differentiation'' as used for recognizing languages, leading to a collection of lemmas about type-level predicates. These lemmas are the heart of two dual parsing implementations---using (inductive) regular expressions and (coinductive) tries---each containing the same code but in dual arrangements (with representation and primitive operations trading places). The regular expression version corresponds to symbolic differentiation, while the trie version corresponds to automatic differentiation.             The relatively easy-to-prove properties of type-level languages transfer almost effortlessly to the decidable implementations. In particular, despite the inductive and coinductive nature of regular expressions and tries respectively, we need neither inductive nor coinductive/bisimulation arguments to prove algebraic properties.},
 issn = {2475-1421},
 month = {August}
}

hayagriva YAML (typst)

yaml · 16 lines

elliottSymbolicAutomaticDifferentiation2021:
  type: article
  title: Symbolic and Automatic Differentiation of Languages
  author: Elliott, Conal
  date: 2021-08
  page-range: 1-18
  serial-number:
    doi: 10.1145/3473583
    issn: 2475-1421
  language: en-US
  abstract: Formal languages are usually defined in terms of set theory. Choosing type theory instead gives us languages as type-level predicates over strings. Applying a language to a string yields a type whose elements are language membership proofs describing how a string parses in the language. The usual building blocks of languages (including union, concatenation, and Kleene closure) have precise and compelling specifications uncomplicated by operational strategies and are easily generalized to a few general domain-transforming and codomain-transforming operations on predicates. A simple characterization of languages (and indeed functions from lists to any type) captures the essential idea behind language ``differentiation'' as used for recognizing languages, leading to a collection of lemmas about type-level predicates. These lemmas are the heart of two dual parsing implementations—using (inductive) regular expressions and (coinductive) tries—each containing the same code but in dual arrangements (with representation and primitive operations trading places). The regular expression version corresponds to symbolic differentiation, while the trie version corresponds to automatic differentiation. The relatively easy-to-prove properties of type-level languages transfer almost effortlessly to the decidable implementations. In particular, despite the inductive and coinductive nature of regular expressions and tries respectively, we need neither inductive nor coinductive/bisimulation arguments to prove algebraic properties.
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    issue: ICFP
    volume: 5

Download: elliottSymbolicAutomaticDifferentiation2021.bib · elliottSymbolicAutomaticDifferentiation2021.yml

Cited by (1)

Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus intrinsic-verification-of-parsersPLDI · 2025

We present Dependent Lambek Calculus (Lambek ${\begin{matrix} \end{matrix}}^{𝙳}$ ), a domain-specific dependent type theory for verified parsing and formal grammar theory. In Lambek ${\begin{matrix} \end{matrix}}^{𝙳}$ , linear types are used as a syntax for formal grammars, and parsers can be written as linear terms. The linear typing restriction provides a form of intrinsic verification that a parser yields only valid parse trees for the input string. We demonstrate the expressivity of this system by showing that the combination of inductive linear types and dependency on non-linear data can be used to encode commonly used grammar formalisms such as regular and context-free grammars as well as traces of various types of automata. Using these encodings, we define parsers for regular expressions using deterministic automata, as well as examples of verified parsers of context-free grammars.

We present a denotational semantics of our type theory that interprets the linear types as functions from strings to sets of abstract parse trees and terms as parse transformers. Based on this denotational semantics, we have made a prototype implementation of Lambek ${\begin{matrix} \end{matrix}}^{𝙳}$ using a shallow embedding in the Agda proof assistant. All of our examples parsers have been implemented in this prototype implementation.

PDF · DOI · arXiv (extended version) · Source code · pldb

Cites 41 works (2 here)

With notes (2)

Applicative programming with effects mcbride-2008-applicativeJFP · 2008

In this article, we introduce Applicative functors – an abstract characterisation of an applicative style of effectful programming, weaker than Monads and hence more widespread. Indeed, it is the ubiquity of this programming pattern that drew us to the abstraction. We retrace our steps in this article, introducing the applicative pattern by diverse examples, then abstracting it to define the Applicative type class and introducing a bracket notation that interprets the normal application syntax in the idiom of an Applicative functor. Furthermore, we develop the properties of applicative functors and the generic operations they support. We close by identifying the categorical structure of applicative functors and examining their relationship both with Monads and with Arrow.

PDF · DOI · pldb

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 (39)

Source repository for 'Symbolic and automatic differentiation of languages' (2021)
Combining predicate transformer semantics for effects: a case study in parsing regular languages (2020)
The Agda standard library (2020)
Generalized convolution and efficient language recognition (2019)
Weighted automata (Droste, Kuske; unpublished) (2019)
The simple essence of automatic differentiation (2018)
Dualizing generalized algebraic data types by matrix transposition (2018)
Formal languages, formally and coinductively (2017)
Well-founded recursion with copatterns and sized types (2016)
Equational reasoning about formal languages in coalgebraic style (Abel, draft) (2016)
Convolution as a unifying concept: Applications in separation logic, interval calculi, and concurrency (2016)
Intrinsic verification of a regular expression matcher (Korkut, Trifunovski, Licata; draft) (2016)
Propositions as types (2015)
Copatterns: Programming infinite structures by observations (2013)
A constructive theory of regular languages in Coq (2013)
Certified Parsing of Regular Languages (2013)
Yacc is dead (2010)
Regular expressions in Agda (2009)
A Brief Overview of Agda – A Functional Language with Dependent Types (2009)
Dependently typed programming in Agda (2009)
Combinator Parsing: A Short Tutorial (2009)
Semi-continuous sized types and termination (2008)
Evaluating Derivatives: Principles and Techniques of Algorithmic Differentiation (2nd ed.) (2008)
Derivatives of rational expressions with multiplicity (2005)
Some recent applications of semiring theory (Golan) (2005)
Algebraic Foundation of Statistical Parsing: Semiring Parsing (Liu, PhD thesis) (2004)
Parsec: A practical parser library (2001)
Generalizing generalized tries (2000)
The art of computer programming, volume 3: (2nd ed.) sorting and searching (1998)
Parsing Inside-Out (Goodman, PhD thesis) (1998)
Partial derivatives of regular expressions and finite automaton constructions (1996)
Monadic parser combinators (Hutton, Meijer) (1996)
A generalization of the trie data structure (1995)
A tutorial on co-induction and functional programming (1995)
On automatic differentiation (Griewank) (1989)
Intuitionistic Type Theory (Martin-Löf, Bibliopolis) (1984)
The algebraic theory of context-free languages (1963)
On the definition of a family of automata (1961)
Über die gegenseitige Lage gleicher Teile gewisser Zeichenreihen (Thue) (1912)