Reference. Towards Kleene Algebra with recursion

Haas Leiß · CSL · 1992 · parsing kleene-algebra · DOI
We extend Kozen’s theory KA of Kleene Algebra to axiomatize parts of the equational theory of context-free languages, using a least fixed-point operator μ instead of Kleene’s iteration operator*.

Cite
Cite as @leis_towards_1992 (helia, typst) · \cite{leis_towards_1992} (LaTeX)
BibTeX
bibtex · 15 lines
@inproceedings{leis_towards_1992,
 title = {Towards {Kleene} {Algebra} with recursion},
 author = {Leiß, Haas},
 year = {1992},
 isbn = {978-3-540-47285-8},
 doi = {10.1007/BFb0023771},
 booktitle = {Computer {Science} {Logic}},
 editor = {Börger, Egon and Jäger, Gerhard and Kleine Büning, Hans and Richter, Michael M.},
 pages = {242--256},
 publisher = {Springer},
 address = {Berlin, Heidelberg},
 keywords = {Continuous Model, Equational Theory, Finite Automaton, Regular Expression, Regular Language},
 language = {en},
 abstract = {We extend Kozen's theory KA of Kleene Algebra to axiomatize parts of the equational theory of context-free languages, using a least fixed-point operator μ instead of Kleene's iteration operator*.}
}
hayagriva YAML (typst)
yaml · 21 lines
leis_towards_1992:
  type: article
  title: Towards {Kleene} {Algebra} with recursion
  author: Leiß, Haas
  date: 1992
  editor:
  - Börger, Egon
  - Jäger, Gerhard
  - Kleine Büning, Hans
  - Richter, Michael M.
  page-range: 242-256
  serial-number:
    doi: 10.1007/BFb0023771
    isbn: 978-3-540-47285-8
  abstract: We extend Kozen's theory KA of Kleene Algebra to axiomatize parts of the equational theory of context-free languages, using a least fixed-point operator μ instead of Kleene's iteration operator*.
  parent:
    type: proceedings
    title: Computer {Science} {Logic}
    publisher:
      name: Springer
      location: Berlin, Heidelberg
Download: leis_towards_1992.bib · leis_towards_1992.yml
Cited by (5)

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

We present Dependent Lambek Calculus (Lambek𝙳), a domain-specific dependent type theory for verified parsing and formal grammar theory. In Lambek𝙳, 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𝙳 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

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

A typed, algebraic approach to parsing krishnaswami_typed_2019PLDI · 2019
In this paper, we recall the definition of the context-free expressions (or µ-regular expressions), an algebraic presentation of the context-free languages. Then, we define a core type system for the context-free expressions which gives a compositional criterion for identifying those context-free expressions which can be parsed unambiguously by predictive algorithms in the style of recursive descent or LL(1). Next, we show how these typed grammar expressions can be used to derive a parser combinator library which both guarantees linear-time parsing with no backtracking and single-token lookahead, and which respects the natural denotational semantics of context-free expressions. Finally, we show how to exploit the type information to write a staged version of this library, which produces dramatic increases in performance, even outperforming code generated by the standard parser generator tool ocamlyacc.
DOI · pldb

Infinitary Axiomatization of the Equational Theory of Context-Free Languages grathwohl_infinitary_2013EPTCS · 2013
We give a natural complete infinitary axiomatization of the equational theory of the context-free languages, answering a question of Lei\\textbackslashss\ (1992).
DOI

Context-Free Languages, Coalgebraically winterCFLCALCO · 2011
We give a coalgebraic account of context-free languages using the functor D(X) = 2 × XA for deterministic automata over an alphabet A, in three different but equivalent ways: (i) by viewing context-free grammars as D-coalgebras; (ii) by defining a format for behavioural differential equations (w.r.t. D) for which the unique solutions are precisely the context-free languages; and (iii) as the D-coalgebra of generalized regular expressions in which the Kleene star is replaced by a unique fixed point operator. In all cases, semantics is defined by the unique homomorphism into the final coalgebra of all languages, paving the way for coinductive proofs of context-free language equivalence. Furthermore, the three characterizations can serve as the basis for the definition of a general coalgebraic notion of context-freeness, which we see as the ultimate long-term goal of the present study.
DOI
Cites 14 works (1 here)
With notes (1)

Action logic and pure induction prattActionLogicPure1991Logics in AI · 1991
In Floyd-Hoare logic, programs are dynamic while assertions are static (hold at states). In action logic the two notions become one, with programs viewed as on-the-fly assertions whose truth is evaluated along intervals instead of at states. Action logic is an equational theory ACT conservatively extending the equational theory REG of regular expressions with operations preimplication a→b (had a then b) and postimplication b←a (b if-ever a). Unlike REG, ACT is finitely based, makes a∗ reflexive transitive closure, and has an equivalent Hilbert system. The crucial axiom is that of pure induction, (a→a)∗ = a→a.
DOI
External (13)
leis_towards_1992 reference entries/refs/leis_towards_1992/leis_towards_1992.hel