Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem

Reference. Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem

We begin by explaining how any context-free grammar encodes a functor of operads from a freely generated operad into a certain “operad of spliced words”. This motivates a more general notion of CFG over any category $𝐶$ , defined as a finite species $𝑆$ equipped with a color denoting the start symbol and a functor of operads $𝑝 : 𝐹 𝑟 𝑒 𝑒 [𝑆] \to 𝑊 [𝐶]$ into the operad of spliced arrows in $𝐶$ . We show that many standard properties of CFGs can be formulated within this framework, and that usual closure properties of CF languages generalize to CF languages of arrows. We also discuss a dual fibrational perspective on the functor $𝑝$ via the notion of “displayed” operad, corresponding to a lax functor of operads $𝑊 [𝐶] \to 𝑆 𝑝 𝑎 𝑛 (𝑆 𝑒 𝑡)$ .

We then turn to the Chomsky-Schützenberger Representation Theorem. We describe how a non-deterministic finite state automaton can be seen as a category $𝑄$ equipped with a pair of objects denoting initial and accepting states and a functor of categories $𝑄 \to 𝐶$ satisfying the unique lifting of factorizations property and the finite fiber property. Then, we explain how to extend this notion of automaton to functors of operads, which generalize tree automata, allowing us to lift an automaton over a category to an automaton over its operad of spliced arrows. We show that every CFG over a category can be pulled back along a ND finite state automaton over the same category, and hence that CF languages are closed under intersection with regular languages. The last important ingredient is the identification of a left adjoint $𝐶 [-] : 𝑂 𝑝 𝑒 𝑟 𝑎 𝑑 \to 𝐶 𝑎 𝑡$ to the operad of spliced arrows functor, building the “contour category” of an operad. Using this, we generalize the C-S representation theorem, proving that any context-free language of arrows over a category $𝐶$ is the functorial image of the intersection of a $𝐶$ -chromatic tree contour language and a regular language.

Cite

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

BibTeX

bibtex · 11 lines

@article{mellis_zeilberger_2022,
 title = {Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem},
 author = {Paul-André Melliès and Noam Zeilberger},
 year = {2022},
 eprint = {2212.09060},
 archiveprefix = {arXiv},
 url = {https://arxiv.org/abs/2212.09060},
 journal = {Electronic Notes in Theoretical Informatics and Computer Science},
 volume = {1},
 doi = {10.46298/entics.10508}
}

hayagriva YAML (typst)

yaml · 15 lines

mellis_zeilberger_2022:
  type: article
  title: Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem
  author:
  - Melliès, Paul-André
  - Zeilberger, Noam
  date: 2022
  url: https://arxiv.org/abs/2212.09060
  serial-number:
    arxiv: '2212.09060'
    doi: 10.46298/entics.10508
  parent:
    type: periodical
    title: Electronic Notes in Theoretical Informatics and Computer Science
    volume: 1

Download: mellis_zeilberger_2022.bib · mellis_zeilberger_2022.yml

Cited by (1)

The categorical contours of the Chomsky-Schützenberger representation theorem mellies-2025-theLMCS · 2025

We develop fibrational perspectives on context-free grammars and on nondeterministic finite-state automata over categories and operads. A generalized CFG is a functor from a free colored operad (aka multicategory) generated by a pointed finite species into an arbitrary base operad: this encompasses classical CFGs by taking the base to be a certain operad constructed from a free monoid, as an instance of a more general construction of an operad of spliced arrows

𝒲︀ 𝒞︀

for any category

𝒞︀

. A generalized NFA is a functor from an arbitrary bipointed category or pointed operad satisfying the unique lifting of factorizations and finite fiber properties: this encompasses classical word automata and tree automata without

𝜖

-transitions, but also automata over non-free categories and operads. We show that generalized context-free and regular languages satisfy suitable generalizations of many of the usual closure properties, and in particular we give a simple conceptual proof that context-free languages are closed under intersection with regular languages. Finally, we observe that the splicing functor

𝒲︀ : Cat \to Oper

admits a left adjoint

𝒞︀ : Oper \to Cat

, which we call the contour category construction since the arrows of

𝒞︀ 𝒪︀

have a geometric interpretation as oriented contours of operations of

𝒪︀

. A direct consequence of the contour / splicing adjunction is that every pointed finite species induces a universal CFG generating a language of tree contour words. This leads us to a generalization of the Chomsky-Schützenberger Representation Theorem, establishing that a subset of a homset

𝐿 \subseteq 𝒞︀ (𝐴, 𝐵)

is a CFL of arrows if and only if it is a functorial image of the intersection of a

𝒞︀

-chromatic tree contour language with a regular language.

DOI · arXiv

Cites 31 works (6 here)

With notes (6)

Displayed Categories ahrens-lumsdaine-2019lmcs · 2019

We introduce and develop the notion of displayed categories. A displayed category over a category C is equivalent to “a category D and functor F : D –> C”, but instead of having a single collection of “objects of D” with a map to the objects of C, the objects are given as a family indexed by objects of C, and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Grothendieck fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as certain displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories. We therefore propose displayed categories as a basis for the development of fibrations in the type-theoretic setting, and similarly for various other notions whose classical definitions involve equality on objects. Besides giving a conceptual clarification of such issues, displayed categories also provide a powerful tool in computer formalisation, unifying and abstracting common constructions and proof techniques of category theory, and enabling modular reasoning about categories of multi-component structures. As such, most of the material of this article has been formalised in Coq over the UniMath library, with the aim of providing a practical library for use in further developments.

We introduce and develop the notion of displayed categories. A displayed category over a category $𝐶$ is equivalent to “a category $𝐷$ and functor $𝐹 : 𝐷 \to 𝐶$ , but instead of having a single collection of “objects of $𝐷$ ” with a map to the objects of $𝐶$ , the objects are given as a family indexed by objects of $𝐶$ , and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Grothendieck fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as certain displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories. We therefore propose displayed categories as a basis for the development of fibrations in the type-theoretic setting, and similarly for various other notions whose classical definitions involve equality on objects. Besides giving a conceptual clarification of such issues, displayed categories also provide a powerful tool in computer formalisation, unifying and abstracting common constructions and proof techniques of category theory, and enabling modular reasoning about categories of multi-component structures. As such, most of the material of this article has been formalised in Coq over the UniMath library, with the aim of providing a practical library for use in further developments.

DOI · arXiv

An Isbell duality theorem for type refinement systems mellies-2017-anMSCS · 2017

Any refinement system (= functor) has a fully faithful representation in the refinement system of presheaves, by interpreting types as relative slice categories, and refinement types as presheaves over those categories. Motivated by an analogy between side effects in programming and context effects in linear logic, we study logical aspects of this ‘positive’ (covariant) representation, as well as of an associated ‘negative’ (contravariant) representation. We establish several preservation properties for these representations, including a generalization of Day’s embedding theorem for monoidal closed categories. Then, we establish that the positive and negative representations satisfy an Isbell-style duality. As corollaries, we derive two different formulas for the positive representation of a pushforward (inspired by the classical negative translations of proof theory), which express it either as the dual of a pullback of a dual or as the double dual of a pushforward. Besides explaining how these constructions on refinement systems generalize familiar category-theoretic ones (by viewing categories as special refinement systems), our main running examples involve representations of Hoare logic and linear sequent calculus.

DOI · arXiv

Functors are type refinement systems mellies_zeilberger_2015POPL · 2015

The standard reading of type theory through the lens of category theory is based on the idea of viewing a type system as a category of well-typed terms. We propose a basic revision of this reading: rather than interpreting type systems as categories, we describe them as functors from a category of typing derivations to a category of underlying terms. Then, turning this around, we explain how in fact any functor gives rise to a generalized type system, with an abstract notion of typing judgment, typing derivations and typing rules. This leads to a purely categorical reformulation of various natural classes of type systems as natural classes of functors.

The main purpose of this paper is to describe the general framework (which can also be seen as providing a categorical analysis of refinement types), and to present a few applications. As a larger case study, we revisit Reynolds’ paper on “The Meaning of Types” (2000), showing how the paper’s main results may be reconstructed along these lines.

PDF · DOI · pldb

Linear logic girard_linear_1987TCS · 1987

The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.

DOI

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

External (25)

Classical linear logic, cobordisms and categorial grammars (2020)
Automata Minimization: a Functorial Approach (2020)
A bifibrational reconstruction of Lawvere’s presheaf hyperdoctrine (2016)
The Hopf algebra of Möbius intervals (2010)
To CNF or not to CNF? An Efficient Yet Presentable Version of the CYK Algorithm (2009)
The cartesian closed bicategory of generalised species of structures (2008)
On the Expressive Power of Abstract Categorial Grammars: Representing Context-Free Formalisms (2004)
Higher Operads, Higher Categories (2004)
Operads in algebra, topology, and physics (2002)
Towards Abstract Categorial Grammars (2001)
Distributors at work (2000)
Combinatorial species and tree-like structures (1997)
Cohomology of Monoids in Monoidal Categories (1997)
Tree automata techniques and applications (1997)
Maps, hypermaps, and triangle groups (1994)
Drawing Curves Over Number Fields (1990)
A note on context-free languages (1989)
How to cover a grammar (1989)
Geometry of Interaction 1: Interpretation of System F (1989)
Multicategories revisited (1989)
Parsing Theory - Volume I: Languages and Parsing (1988)
Foncteurs analytiques et espèces de structures (1986)
Une théorie combinatoire des séries formelles (1981)
Ordinal sums and equational doctrines (1969)
The Algebraic Theory of Context-Free Languages* (1963)