Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Regular expressions over countable words

Thomas Colcombet, A V Sreejith

TL;DR

The paper addresses the problem of extending regular-language theory to languages indexed by countable linear orders. It introduces five classes of regular expressions over countable words and proves expressive equivalences with both logical fragments of MSO/FO and algebraic varieties of o-monoids, thereby generalizing classical finite-word results. A key contribution is a detailed structural analysis of o-monoids via J-classes and a comprehensive translation framework from algebra to expressions, enabling constructive expressions from algebraic data. The work solidifies a triad of equivalences among logic, algebra, and expressions in the countable-word setting and provides decidability results for definability within these classes. This has implications for the automatic reasoning about countable structures and strengthens the foundational understanding of regular languages beyond finite words.

Abstract

We investigate the expressive power of regular expressions for languages of countable words and establish their expressive equivalence with logical and algebraic characterizations. Our goal is to extend the classical theory of regular languages - defined over finite words and characterized by automata, monadic second-order logic, and regular expressions - to the setting of countable words. In this paper, we introduce and study five classes of expressions: marked star-free expressions, marked expressions, power-free expressions, scatter-free expressions, and scatter expressions. We show that these expression classes characterize natural fragments of logic over countable words and possess decidable algebraic characterizations. As part of our algebraic analysis, we provide a precise description of the relevant classes in terms of their J-class structure. These results complete a triad of equivalences - between logic, algebra, and expressions - in this richer setting, thereby generalizing foundational results from classical formal language theory.

Regular expressions over countable words

TL;DR

The paper addresses the problem of extending regular-language theory to languages indexed by countable linear orders. It introduces five classes of regular expressions over countable words and proves expressive equivalences with both logical fragments of MSO/FO and algebraic varieties of o-monoids, thereby generalizing classical finite-word results. A key contribution is a detailed structural analysis of o-monoids via J-classes and a comprehensive translation framework from algebra to expressions, enabling constructive expressions from algebraic data. The work solidifies a triad of equivalences among logic, algebra, and expressions in the countable-word setting and provides decidability results for definability within these classes. This has implications for the automatic reasoning about countable structures and strengthens the foundational understanding of regular languages beyond finite words.

Abstract

We investigate the expressive power of regular expressions for languages of countable words and establish their expressive equivalence with logical and algebraic characterizations. Our goal is to extend the classical theory of regular languages - defined over finite words and characterized by automata, monadic second-order logic, and regular expressions - to the setting of countable words. In this paper, we introduce and study five classes of expressions: marked star-free expressions, marked expressions, power-free expressions, scatter-free expressions, and scatter expressions. We show that these expression classes characterize natural fragments of logic over countable words and possess decidable algebraic characterizations. As part of our algebraic analysis, we provide a precise description of the relevant classes in terms of their J-class structure. These results complete a triad of equivalences - between logic, algebra, and expressions - in this richer setting, thereby generalizing foundational results from classical formal language theory.
Paper Structure (22 sections, 29 theorems, 18 equations, 2 figures)

This paper contains 22 sections, 29 theorems, 18 equations, 2 figures.

Table of Contents

  1. Introduction and contributions
  2. Preliminaries: Languages and Logic
  3. Linear orderings
  4. Countable words
  5. "First-order@first-order logic", "monadic second-order@monadic second-order logic" and logics in between
  6. Regular Expressions
  7. Examples
  8. Operations on Languages
  9. Algebras and "o-monoids"
  10. "o-monoids", "o-algebras", "recognizability"
  11. Structure theorem for "o-monoids"
  12. "Profinite identities" characterize "varieties" of "o-monoids"
  13. Types of "J-classes" and their link with "identities"
  14. From "o-monoids" to regular expressions
  15. General structure of the translation from algebra to expressions
  16. ...and 7 more sections

Key Result

Theorem 2

main theorem Let $\monoid$ be the "syntactic" "o-monoid" of a language $L\subseteq\words\alphabet$, then: Furthermore, the problem of deciding whether a language is definable by any of the above expression is decidable.

Figures (2)

  • Figure 1: The "omega@omega power" (resp. "omega*@omega* power") "powers@omega power" lie in the same "L-class" (resp. "R-class"). The "shuffle power" lies in a unique "H-class".
  • Figure 2: Subsets of $M$ involved in an inductive step.

Theorems & Definitions (42)

  • Example 1
  • Theorem 2: main theorem
  • Example 3
  • Definition 4
  • Remark 5
  • Lemma 6
  • Example 7
  • Example 8
  • Example 9
  • Example 10
  • ...and 32 more