Algebraic Characterizations of Classes of Regular Languages in DynFO

Barloy, Corentin; Tschirbs, Felix; Vortmeier, Nils; Zeume, Thomas

doi:10.4230/LIPIcs.STACS.2026.9

Algebraic Characterizations of Classes of Regular Languages in DynFO

Corentin Barloy

Ruhr University Bochum, Germany Felix Tschirbs

Ruhr University Bochum, Germany Nils Vortmeier

Ruhr University Bochum, Germany Thomas Zeume

Ruhr University Bochum, Germany

Abstract

This paper explores the fine-grained structure of classes of regular languages maintainable in fragments of first-order logic within the dynamic descriptive complexity framework of Patnaik and Immerman. A result by Hesse states that the class of regular languages is maintainable by first-order formulas even if only unary auxiliary relations can be used. Another result by Gelade, Marquardt, and Schwentick states that the class of regular languages coincides with the class of languages maintainable by quantifier-free formulas with binary auxiliary relations.

We refine Hesse’s result and show that with unary auxiliary data $\exists^{*}\forall^{*}$ -formulas can maintain all regular languages. We then obtain precise algebraic characterizations of the classes of languages maintainable with quantifier-free formulas and positive $\exists^{*}$ -formulas in the presence of unary auxiliary relations.

Keywords and phrases:

Dynamic descriptive complexity, formal languages, monoid theory

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Complexity theory and logic ; Theory of computation

\rightarrow

Algebraic language theory ; Theory of computation

\rightarrow

Regular languages

Acknowledgements:

We thank the reviewers for their careful reading and insightful comments, which significantly improved the quality of this article.

Funding:

All authors are supported by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation), grant 532727578.

Editors:

Meena Mahajan, Florin Manea, Annabelle McIver, and Nguyễn Kim Thắng

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

In seminal work by Schützenberger as well as McNaugthon and Papert, the class of regular languages has been characterized algebraically as the class of languages with finite syntactic monoids [16] and logically as the class of languages definable by monadic second-order sentences [1]. In subsequent work, a multitude of algebraic and logical characterisations have been obtained for subclasses of regular languages, including a characterization of the class of star-free regular languages (languages describable by regular expressions without Kleene star but with negation) as the class of languages with finite aperiodic monoids and definable in first-order logic [17, 9]; and the characterization of piecewise testable languages (languages describable by the set of subwords appearing in the word) as languages with $\mathcal{J}$ -trivial syntactic monoids and definable by first-order formulas without quantifier alternation [18].

Here we are interested in algebraic properties of formal languages defined in the dynamic descriptive complexity framework of Patnaik and Immerman [10]. In this framework, strings are subject to changes, and the goal is to maintain membership within a language via logical formulas, possibly using auxiliary information stored in auxiliary relations (which need to be updated by logical formulas as well). An important class of languages in this setting are the languages maintainable via first-order formulas, called DynFO. It has been shown early on that DynFO contains all regular and even all context-free languages [10, 4].

The goal of this paper is to initiate a search for connections between algebra and dynamic descriptive complexity classes. This is in a similar spirit as the search for connections between algebra and logics initiated by Schützenberger, McNaugthon and Papert for the static realm, as sketched above. Our guiding question is:

Are there restrictions of DynFO that lead to natural subclasses of the regular languages with nice algebraic characterizations?

For answering this question, it is natural to first identify restrictions of DynFO that can still maintain all regular languages. This has been studied in prior work. A result by Hesse states that the class of regular languages is maintainable by first-order formulas even if only very restricted auxiliary information, namely only unary relations, can be used [6, Theorem 2.8]¹¹1A variant of this result has already been reported in [10], but additional built-in arithmetic has been used as auxiliary information.. A seminal result by Gelade, Marquardt, and Schwentick states that, if binary auxiliary relations can be used, then the class of regular languages coincides with the class DynProp of languages maintainable by quantifier-free formulas [4, Theorem 3.2].

We refine the result by Hesse. Denote by UDyn $\Sigma_{2}$ the class of languages maintainable by $\exists^{*}\forall^{*}$ -formulas using unary auxiliary relations.

Theorem 1.

All regular language are in UDyn $\Sigma_{2}$ .

This result can be obtained by close inspection of Hesse’s proof, which maintains properties of the execution graph of finite state automata. Here, we provide an algebraic reformulation of the proof relying on Green’s relations (see Section 3).

Thus, when looking for restrictions of DynFO that correspond to natural subclasses of the regular languages with nice algebraic characterizations, one can explore (a) fragments of (binary) DynProp, or (b) fragments of UDyn $\Sigma_{2}$ .

We obtain results along both directions. For binary DynProp, it is natural to further restrict the auxiliary relations. We precisely characterize the languages in DynProp with unary auxiliary relations by algebraic properties of their syntactic monoids (see Section 4).

Theorem 2.

A regular language is in UDynProp if any only if its syntactic monoid is a group.

For UDyn $\Sigma_{2}$ , it is natural to further restrict the syntactic structure of formulas used for updates. We precisely characterize the languages maintainable by positive $\exists^{*}$ -formulas, denoted UDyn $\Sigma_{1}^{+}$ , by the algebraic properties of their ordered syntactic monoids (see Section 5).

Theorem 3.

A regular language is in UDyn $\Sigma_{1}^{+}$ if and only if its ordered syntactic monoid is in $\mathbf{J}^{+}\ast\mathbf{G}$ .

Here, $\mathbf{J}^{+}\ast\mathbf{G}$ denotes the wreath product of the classes $\mathbf{J}^{+}$ and $\mathbf{G}$ .

In the proofs of both Theorem 2 and Theorem 3, the “if” direction requires to provide update formulas for all regular languages whose (ordered) syntactic monoids satisfy some property and is standard. The “only-if” direction requires to prove lower bounds against DynProp (resp. UDyn $\Sigma_{1}^{+}$ ) for all non-group languages (resp. all languages whose ordered syntactic monoid is not in $\mathbf{J}^{+}\ast\mathbf{G}$ ). To this end we prove a lower bound for a single language using variants of the Substructure lemma [4] (see also [20]) and lift this lower bounds to all languages without the property using algebraic insights.

We leave open the question to find a precise algebraic characterization of languages in UDyn $\Sigma_{1}$ , i.e., languages maintainable by (not necessarily positive) $\exists^{*}$ -formulas and unary auxiliary relations. We discuss challenges towards answering this question in Section 6.

2 Preliminaries

In this section, also to fix notation, we recall basics of dynamic descriptive complexity and algebraic formal language theory.

2.1 Dynamic descriptive complexity

In this paper, we are interested in the dynamic membership problem for fixed regular languages. Let $L\subseteq\Sigma^{*}$ be a language over some alphabet $\Sigma$ . The input structure for the dynamic membership problem ${\textsc{Member}}(L)$ of $L$ is an encoding of a word $w=w_{1}\cdots w_{n}$ as a relational structure over the domain $\{1,\ldots,n\}$ of the positions of the word. This structure has (1) for every $\sigma\in\Sigma$ a unary relation $W_{\sigma}$ for storing the positions of $w$ that contain $\sigma$ and (2) a binary relation $\leq$ representing the linear order of the positions of $w$ . Following Patnaik and Immerman as well as Gelade et al. [10, 4], each $w_{i}$ is either in $\Sigma$ or $\epsilon$ , i.e., each position $i\in[n]$ can occur in at most one relation $W_{\sigma}$ . For the sake of simplicity, we denote both input words and their encoding by the same symbol $w$ .

In the dynamic membership problem, the input structure can be changed by operations of the form $\textsc{set}_{\sigma}(y)$ , for $\sigma\in\Sigma\cup\{\epsilon\}$ . A concrete change $\textsc{set}_{\sigma}(i)$ instantiates $y$ and sets the symbol at position $i$ to $\sigma$ . The dynamic membership problem ${\textsc{Member}}(L)$ asks whether the current input structure encodes a word in $L$ , i.e. whether $w_{1}\cdots w_{n}\in L$ .

We will explore the resources needed for maintaining the dynamic membership problem within the dynamic descriptive complexity framework of Patnaik and Immerman [10].

A dynamic program $\Pi$ stores the input structure as well as a set ${\mathcal{A}}$ of auxiliary relations over some (relational) schema $\tau_{\text{aux}}$ and over the same domain as the input word. For every auxiliary relation symbol $R\in\tau_{\text{aux}}$ and every change operation $\textsc{set}_{\sigma}$ , the program $\Pi$ has an update formula $\varphi_{\sigma}^{R}(\bar{x};y)$ , which can access input and auxiliary relations. Whenever the current input word $w$ is changed by $\textsc{set}_{\sigma}(i)$ to the new input word $w^{\prime}$ , the new auxiliary relation $R^{{\mathcal{A}}^{\prime}}$ in the updated set ${\mathcal{A}}^{\prime}$ consists of all tuples $\bar{a}$ such that $\varphi_{\sigma}^{A}(\bar{a};i)$ is satisfied in the structure $(w^{\prime},{\mathcal{A}})$ .

A dynamic program $\Pi$ maintains the dynamic membership problem ${\textsc{Member}}(L)$ if it has a distinguished auxiliary bit $q$ (i.e., a $0$ -ary auxiliary relation), which always indicates whether the current input word is in $L$ . More precisely, following Patnaik and Immerman, we assume that the initial input word $w_{0}$ is empty and the initial auxiliary structure ${\mathcal{A}}_{0}$ is initialized by a first-order formula depending on $w_{0}$ . The program $\Pi$ maintains ${\textsc{Member}}(L)$ , if after changing $w_{0}$ to $w^{\prime}$ by any sequence of changes and subsequently applying the corresponding update formulas starting from $(w_{0},{\mathcal{A}}_{0})$ , the obtained bit $q$ is true if and only if $w^{\prime}\in L$ .

The dynamic problem ${\textsc{Member}}(L)$ is in the class DynFO if it can be maintained by a dynamic program with FO update formulas and an FO initialization formula. It is in $k$ -ary DynFO if all auxiliary relations are at most $k$ -ary. For a class ${\mathcal{C}}$ of formulas, it is in Dyn ${\mathcal{C}}$ if all update formulas are in ${\mathcal{C}}$ and the initialization formula is in FO.

Throughout this paper we assume that formulas are in prenex normal form. Among the classes ${\mathcal{C}}$ we study are the class Prop of quantifier-free formulas; the class $\Sigma_{1}$ of $\exists^{*}$ -formulas (i.e., formulas in prenex form with only existential quantifiers); and the class $\Sigma_{2}$ of $\exists^{*}\forall^{*}$ -formulas (i.e., formulas in prenex form starting with a block of existential quantifiers followed by a block of universal quantifiers). We also consider the variants $\textsf{Prop}^{+}$ , $\Sigma_{1}^{+}$ and $\Sigma_{2}^{+}$ where negations may only be used directly in front of the linear order symbol $\leq$ . A focus will be on programs that can only use unary auxiliary relations, in which case we denote classes by UDyn ${\mathcal{C}}$ for classes ${\mathcal{C}}$ of update formulas.

Example 4.

We show that the regular language $\mathtt{\Sigma^{*}aa\Sigma^{*}}$ over $\Sigma=\{a,b\}$ is in UDyn $\Sigma_{1}$ , so, can be maintained using only unary auxiliary relations and update formulas in prenex form that only use existential quantifiers.

Our goal is to maintain a unary relation $N$ that stores all positions $j$ such that the next letter to the right of $j$ that does not contain $\epsilon$ is an $a$ . This relation can directly be maintained using both $\Sigma_{1}$ and $\Pi_{1}$ update formulas. As $\Pi_{1}$ update formulas are not allowed, we store a slightly differently defined relation $N^{\prime}$ and an additional bit $c$ . If the flag $c$ is true, the relation $N^{\prime}$ is equal to $N$ . If $c$ is false, then $N^{\prime}$ is the complement of $N^{\prime}$ , that is, contains all position $j$ such that either all positions to the right of $j$ are $\epsilon$ or the first positions that is not $\epsilon$ is a $b$ . Using this relation, we can obtain $N$ as $N(j)=(\neg c\land\neg N^{\prime}(j))\lor(c\land N^{\prime}(j))$ .

We now describe the update formulas for maintaining $N^{\prime}$ and $c$ . We additionally use unary auxiliary relations $W^{o}_{\sigma}$ to store the old input word before the change. These are trivial to maintain.

$\blacksquare$

In case of a change of the form $\textsc{set}_{b}(i)$ , we set $c=1$ and the relation $N^{\prime}$ after the update is equal to $N$ . A position $j$ is in $N^{\prime}$ if $j\in N$ before the change and either $i\leq j$ or there is a position between $i$ and $j$ that is an $a$ . The corresponding update formula for $N^{\prime}$ is $\varphi_{b}^{N^{\prime}}(j;i)=\exists k\big[N(j)\wedge\big(i\leq j\vee(j<i% \wedge j<k\wedge k<i\wedge W_{a}(k))\big)\big]$ , where $x<y$ is an abbreviation for $x\leq y\wedge\neg(x=y)$ .
$\blacksquare$

In case of a change of the form $\textsc{set}_{a}(i)$ , we set $c=0$ and the relation $N^{\prime}$ after the update is the complement of $N$ . A position $j$ is in $N^{\prime}$ if $j\not\in N$ before the change and either $i\leq j$ or there is a position between $i$ and $j$ that is a $b$ . The corresponding update formula for $N^{\prime}$ is $\varphi_{a}^{N^{\prime}}(j;i)=\exists k\big[\neg N(j)\wedge\big(i\leq j\vee(j<% i\wedge j<k\wedge k<i\wedge W_{b}(k))\big)\big]$ .

\blacksquare

In case of a change $\textsc{set}_{\epsilon}(i)$ , the update depends on the old symbol at position $i$ . If the symbol was an $a$ , the relation $N^{\prime}$ is equal to $N$ after the update and we set $c=1$ . If the removed $a$ was the first letter to the right of $j$ , then we have to check the first letter to the right of $i$ . Otherwise, the change is not relevant for position $j$ . So, if $j<i$ , the next letter from $j$ is an $a$ if and only if $N(j)$ and $N(i)$ were both true before the change, or there is an $a$ between $j$ and $i$ and $N(j)$ was already true.

If the change replaces $b$ with $\epsilon$ , the relation $N^{\prime}$ is the complement of $N$ after the update and we set $c=0$ . If $j<i$ , the next letter from $j$ is not an $a$ if and only if $N(j)$ and $N(i)$ were both false before the change, or there is a $b$ between $j$ and $i$ and $N(j)$ was false. The update formula is

	$\displaystyle\varphi_{\epsilon}^{N^{\prime}}(j;i)=\exists k\Big[$
	$\displaystyle W^{o}_{a}(i)\wedge\Big((i\leq j\wedge N(j))\vee\big(j<i\wedge N(% j)\wedge(N(i)\vee(j<k\wedge k<i\wedge W_{a}(k)))\big)\Big)\vee$
	$\displaystyle W^{o}_{b}(i)\wedge\Big((i\leq j\wedge\neg N(j))\vee\big(j<i% \wedge\neg N(j)\wedge(\neg N(i)\vee(j<k\wedge k<i\wedge W_{b}(k)))\big)\Big)% \Big].$

Similarly, we can maintain a unary auxiliary relation $P$ that contains all positions $j$ such that the next letter to the left of $j$ that does not contain $\epsilon$ is an $a$ .

We now describe the maintenance of the bit $q$ that is set to $1$ whenever $w$ is in $L=\Sigma^{*}aa\Sigma^{*}$ .

$\blacksquare$

In case of a change $\textsc{set}_{a}(i)$ , the new word $w$ is in $L$ if and only if $q$ or one of $N(i)$ and $P(i)$ was already true before the change.
$\blacksquare$

In case of a change $\textsc{set}_{b}(i)$ , we have $w\in L$ if and only if there exists a position $k>i$ with an $a$ such that $N(k)$ holds, or there exists a position $k<i$ with an $a$ such that $P(k)$ holds.
$\blacksquare$

In case of a change $\textsc{set}_{\epsilon}(i)$ it holds $w\in L$ if and only if there exists a position $k>i$ with an $a$ such that $N(k)$ holds, or there exists a position $k<i$ with an $a$ such that $P(k)$ holds, or both $N(i)$ and $P(i)$ hold.

These conditions can easily be described by existential update formulas. $\lrcorner$

During our study, we will need the following closure properties. For a language $L$ over alphabet $\Sigma$ and a letter $\sigma\in\Sigma$ , we define $L\sigma^{-1}=\{w\mid w\sigma\in L\}$ and $\sigma^{-1}L=\{w\mid\sigma w\in L\}$ .

Lemma 5.

Let $L$ be a language over alphabet $\Sigma$ and $\textsf{Dyn${\mathcal{C}}$}\in\{\textsf{UDynProp},\textsf{UDyn$\Sigma_{1}^{+}$}\}$ . If ${\textsc{Member}}(L)$ can be maintained in Dyn ${\mathcal{C}}$ , then so can

(a)

${\textsc{Member}}(h^{-1}(L))$ for any mapping $h:\Gamma\to\Sigma^{*}$ and any alphabet $\Gamma$ ,
(b)

${\textsc{Member}}(L\sigma^{-1})$ and ${\textsc{Member}}(\sigma^{-1}L)$ , for any $\sigma\in\Sigma$ .

2.2 Monoids

For DynFO and many of its natural restrictions that possess favourable closure properties, we follow Skovberg Frandsen, Miltersen, and Skyum [19] in studying dynamic problems for monoids rather than languages. A monoid $(M,\cdot)$ is a set $M$ equipped with a binary operation $\cdot$ that is associative and has an identity element, i.e., the operation satisfies $(x\cdot y)\cdot z=x\cdot(y\cdot z)$ for all elements $x,y,z\in M$ and there is an element $1\in M$ such that $1\cdot x=x\cdot 1=x$ for all $x\in M$ . A monoid is a group if every element $x$ has an inverse, i.e. an element $y$ such that $x\cdot y=y\cdot x=1$ . An element $e$ is said to be idempotent if $e\cdot e=e$ . For an integer $n>0$ and $x\in M$ , the $n$ -fold product of $x$ is denoted by $x^{n}$ . It is well known that every element $x\in M$ has a unique power that is idempotent [12, Prop. II.6.31] called idempotent power of $x$ and denoted by $x^{\omega}$ .

A morphism $\varphi:M\rightarrow N$ between two monoids is a mapping such that $\varphi(1)=1$ and $\varphi(x\cdot y)=\varphi(x)\cdot\varphi(y)$ for every $x,y\in M$ . A submonoid $N$ of a monoid $M$ is a subset of $M$ that is a monoid, i.e., it contains $1$ and is closed under $\cdot$ , meaning $x\cdot y\in N$ for all $x,y\in N$ . A monoid $N$ is a quotient of $M$ if there exists a surjective morphism from $M$ to $N$ . We say that $N$ divides $M$ if $N$ is the quotient of a submonoid of $M$ . A language $L$ is recognized by a monoid $M$ if there is a morphism $\varphi:\Sigma^{*}\rightarrow M$ and $P\subseteq M$ such that $L=\varphi^{-1}(P)$ . The regular languages are precisely those recognized by a finite monoid (see for instance [12, Theorem IV.3.21]).

For a monoid $M$ , we consider dynamic programs over the alphabet $M$ and define the problem of evaluating a sequence of elements in $M$ . We say that a dynamic program $\Pi$ maintains the dynamic membership problem ${\textsc{Member}}(M)$ if there are $|M|$ dedicated auxiliary bits that respectively store for every $x\in M$ whether the maintained word evaluates to $x$ . Similarly the dynamic problem StrictPrefix (resp. StrictSuffix) is maintained via one dedicated unary relation for each $x\in M$ that stores the value $1\leq i\leq n$ if the prefix $w_{1}\cdot\ldots\cdot w_{i-1}$ (resp. suffix $w_{i+1}\cdot\ldots\cdot w_{n}$ ) evaluates to $x$ . In this setting, the symbol $\epsilon$ and the neutral element $1$ of $M$ can be used interchangeably. For instance, the initial word $w_{0}$ can either be the empty word or $1^{n}$ .

An important monoid is the monoid of functions $f:Q\rightarrow Q$ for a set $Q$ . The operation is the composition and the neutral element is the identity function. Given a deterministic finite state automaton with transition function $\delta:\Sigma^{*}\rightarrow(Q\rightarrow Q)$ , its transition monoid is the image $\delta(\Sigma^{*})$ . The syntactic monoid of a regular language is the transition monoid of its minimal automaton. It is the smallest monoid that recognizes the language and reflects many properties of its regular language. Indeed, the syntactic monoid possesses more information than its regular language, as exposed by the following claim. A class of formulas ${\mathcal{C}}$ is closed under $\lor$ (resp. $\land$ , resp. $\neg$ ) if for every $\varphi,\psi\in{\mathcal{C}}$ , we also have $\varphi\lor\psi$ (resp. $\varphi\land\psi$ , resp. $\neg\varphi$ ) in ${\mathcal{C}}$ . All classes under inspection in this paper possesses this property.

Fact 6.

Let ${\mathcal{C}}$ be a class of formulas closed under $\lor$ . Let $L$ be a regular language with syntactic monoid $M$ and $k$ a number, then

{\textsc{Member}}(M)\in k\textit{-ary }\textsf{Dyn${\mathcal{C}}$}\Rightarrow{% \textsc{Member}}(L)\in k\textit{-ary }\textsf{Dyn${\mathcal{C}}$}.

We will see in Section 4 and Section 5 that when the class of formulas under consideration is well-behaved, the converse of this claim is also true.

We conclude this section by stating that maintainability of ${\textsc{Member}}(M)$ for a monoid implies maintainability of ${\textsc{Member}}(N)$ for every $N$ that divides $M$ .

Fact 7.

Let ${\mathcal{C}}$ be a class of formulas closed under $\lor$ and $k$ any number. Let $M$ be a monoid such that ${\textsc{Member}}(M)\in k\textit{-ary }\textsf{Dyn${\mathcal{C}}$}$ . Then for every $N$ that divides $M$ we have ${\textsc{Member}}(N)\in k\textit{-ary }\textsf{Dyn${\mathcal{C}}$}$ .

3 The regular languages of UDyn $\Sigma_{2}$

In this section we prove that every regular language can be maintained by $\Sigma_{2}$ -formulas and only unary relations. That is, we prove the following.

Theorem 8 (Restatement of Theorem 1).

For any regular language $L$ : ${\textsc{Member}}(L)$ is in UDyn $\Sigma_{2}$ .

The proof is algebraic by nature, hence we show that ${\textsc{Member}}(M)$ for a syntactic monoid $M$ can be maintained and then apply Fact 6. The approach towards proving Theorem 8 is as in Hesse [6]: We want to exhibit maintainable unary relations that allow to compute the evaluation of every infix of a word from $M^{*}$ . This is formalized in the following lemma.

Lemma 9.

Let $M$ be a finite monoid. There is a dynamic program $\Pi$ that maintains unary auxiliary relations over a schema $\tau_{M}$ such that

i)

$\Pi$ only uses $\Sigma_{2}$ update formulas, and
ii)

for every $x\in M$ there is a $\Sigma_{2}$ formula $\psi_{x}(j,k)$ over the schema of $\Pi$ that is satisfied if and only if the infix $w_{j+1}\cdots w_{k-1}$ of the input word $w$ evaluates to $x$ .

The definition of the auxiliary relations and the proof of the lemma relies on the local theory of monoids, as developed by Green [5]. We first show that Theorem 8 follows.

Proof of Theorem 8.

We prove that ${\textsc{Member}}(M)$ is in UDyn $\Sigma_{2}$ for the syntactic monoid of a regular language. As UDyn $\Sigma_{2}$ is closed under disjunction, this implies the result due to Fact 6. Towards this end, let $\Pi$ be the dynamic program and $\psi_{x}$ the formulas expressing the evaluation of infixes of the input word, as given by Lemma 9. Note that the formulas $\psi_{x}$ give the evaluation of the input word ahead of a change. To maintain ${\textsc{Member}}(M)$ , we need the evaluation after a change. Suppose a change $\textsc{set}_{\sigma}(i)$ occurs. The formula

\displaystyle\psi_{x}^{\sigma}(j,k;i)

\displaystyle=\Big[(j<i<k)\land\Big(\bigvee_{\stackrel{{\scriptstyle y,z\in M}% }{{y\sigma z=x}}}\psi_{y}(j,i)\land\psi_{z}(i,k)\Big)\Big]\lor\Big[(i\leq j% \lor k\leq i)\land\psi_{x}(j,k)\Big]

then expresses that the infix from position $j+1$ to position $k-1$ of the changed input word evaluates to $x$ . As the formulas $\psi_{x},\psi_{y},\psi_{z}$ are not in the scope of a negation and no further quantifiers are used, the formula is also in $\Sigma_{2}$ .

Now, the formula

\varphi(i)=\exists j,k\Big[\min(j)\land\max(k)\land\Big(\bigvee_{\stackrel{{% \scriptstyle v,y,z\in M}}{{yvz=x}}}W_{y}(j)\land W_{z}(k)\land\psi_{v}^{\sigma% }(j,k;i)\Big)\Big],

with $\min(j)=\forall i(i\leq j\rightarrow i=j)$ and $\max(k)=\forall i(i\geq k\rightarrow i=k)$ expresses that $w$ evaluates to $x$ after the change on position $i$ , for any fixed $x\in M$ . This formula still has only one alternation of quantifiers and belongs to $\Sigma_{2}$ . Together with the update formulas of $\Pi$ , we have a dynamic Dyn $\Sigma_{2}$ program for ${\textsc{Member}}(M)$ . $\hfill\blacktriangleleft$

In the remainder of this section, we recall Green’s relations and use them to define the unary relations contained in the schema $\tau_{M}$ of the program $\Pi$ from Lemma 9. The proof that these relations satisfy conditions (i) and (ii) from Lemma 9 is delegated to the full version of this paper.

Green’s relations.

The local theory of finite monoids studies the structure of monoids by considering properties of sets of elements that behave the same way. It is based on the so-called Green’s relations, which are a generalization of the notion of divisibility for any monoid. Over the integers, the divisibility relation is a partial order, whereas Green’s relations for arbitrary monoids are preorders, that is, reflexive and transitive relations. Fix a monoid $M$ . Its Green’s preorders are defined by, for $x,y\in M$ :

$\blacksquare$

$x\leq_{\mathcal{R}}y$ whenever there exists $\alpha\in M$ such that $x=y\alpha$ ,
$\blacksquare$

$x\leq_{\mathcal{L}}y$ whenever there exists $\alpha\in M$ such that $x=\alpha y$ ,
$\blacksquare$

$x\leq_{\mathcal{J}}y$ whenever there exists $\alpha,\beta\in M$ such that $x=\alpha y\beta$ ,
$\blacksquare$

$x\leq_{\mathcal{H}}y$ whenever $x\leq_{\mathcal{R}}y$ and $x\leq_{\mathcal{L}}y$ .

The Green’s classes $\mathcal{R}$ , $\mathcal{L}$ , $\mathcal{J}$ and $\mathcal{H}$ of $M$ are the equivalence classes of the preorders. For instance, two elements $x,y\in M$ are equivalent for $\mathcal{R}$ , denoted by $x\mathcal{R}y$ , if and only if $x\leq_{\mathcal{R}}y$ and $y\leq_{\mathcal{R}}x$ . It follows from the definitions that $\mathcal{H}\subseteq\mathcal{R}\subseteq\mathcal{J}$ and $\mathcal{H}\subseteq\mathcal{L}\subseteq\mathcal{J}$ . Note that for any green relation $\mathcal{K}$ among the four, $\leq_{\mathcal{K}}$ induces a partial order on the set of $\mathcal{K}$ -classes. The order $\leq_{\mathcal{J}}$ is of particular interest: assume there is an element $x$ in some $\mathcal{J}$ -class $J$ . Then, for any $y,z\in M$ , $y x z$ belongs to a $\mathcal{J}$ -class $I$ with $I\leq_{\mathcal{J}}J$ . Therefore, if a factor of a word $w_{1}\cdots w_{n}\in M^{*}$ evaluates to some element of a $\mathcal{J}$ -class $J$ , the whole word evaluates to an element from a class $J^{\prime}$ with $J^{\prime}\leq_{\mathcal{J}}J$ . There is an analogous statement for $\mathcal{R}$ -classes and $\mathcal{L}$ -classes that we will use repeatedly throughout the paper: if an element $x$ is a prefix of another element $y$ , that is there exists $\alpha$ such that $x\alpha=y$ , then we have $y\leq_{\mathcal{R}}x$ . Likewise, if $x$ is a suffix of $y$ , so there exists $\alpha$ such that $\alpha x=y$ , then $y\leq_{\mathcal{L}}x$ .

Example 10.

The syntactic monoid of $\mathtt{(aa)^{\ast}}$ is $\mathbb{Z}_{2}$ , the cyclic group with two elements $1$ and $a$ such that $a\cdot a=1$ . Both elements are $\mathcal{H}$ -equivalent (and therefore also $\mathcal{R}$ -, $\mathcal{L}$ -, and $\mathcal{J}$ -equivalent). In fact, in groups, all elements are always $\mathcal{H}$ -equivalent.

Example 11.

The syntactic monoid of $\mathtt{(a+b)^{*}a(a+b)^{*}}$ is usually denoted by $U_{1}$ . It has two elements $1$ and $a$ such that $a\cdot x=x\cdot a=a$ for every element $x$ . The two elements are in distinct classes for all of Green’s relations, and $1\geq_{\mathcal{J}}a$ .

Example 12.

The syntactic monoid of $\mathtt{(a+b)^{*}a}$ is usually denoted by $U_{2}$ . It has three elements $1$ , $a$ and $b$ such that $a$ and $b$ are idempotent and $a\cdot b=b$ and $b\cdot a=a$ . The elements $a$ and $b$ are $\mathcal{R}$ -equivalent (and therefore also $\mathcal{J}$ -equivalent), but not $\mathcal{L}$ -equivalent. The neutral element $1$ is alone in its $\mathcal{J}$ -class which is $\mathcal{J}$ -smaller than the one of $a$ and $b$ .

Unary auxiliary relations for expressing evaluations of infixes.

The proof of Lemma 9 relies on the fact that finite monoids have only finitely many $\mathcal{J}$ -classes. Therefore, when we evaluate a word from left to right, there is only a finite number of changes of $\mathcal{J}$ -classes. We make that intuition explicit. In the following, for a word $w=w_{1}\cdots w_{n}\in M^{*}$ , we write $w[j,k]$ to denote the subword $w_{j}\cdots w_{k}$ of $w$ between indices $j$ and $k$ . For an element $x$ , we denote by $\mathcal{J}(x)$ its $\mathcal{J}$ -class. When it is clear from the context, we identify a word in $M^{*}$ by its evaluation. The following lemma is about the evaluation of a word $w\in M^{*}$ from left to right, that is evaluating $w_{1}$ , $w_{1}w_{2}$ , $w_{1}w_{2}w_{3}$ , $\ldots$ , $w_{1}\cdots w_{n}$ in that order. It states that, except for a constant number of times (depending on $M$ and not on $w$ ), the $\mathcal{J}$ -class of the partial evaluations does not change.

Lemma 13.

Let $w$ be a word from $M^{*}$ of size $n$ and $j\leq n$ a position. Then there exist integers $j=\ell_{0}<\ell_{1}<\cdots<\ell_{m}=n+1$ with $m\leq|M|$ such that:

i)

for $0\leq s<m$ and $\ell_{s}\leq i<\ell_{s+1}$ , $w[j,\ell_{s}]\ \mathcal{J}\ w[j,i]$ ,
ii)

for $0\leq s<m-1$ , $w[j,\ell_{s+1}-1]\ \cancel{\mathcal{J}}\ w[j,\ell_{s+1}]$ .

There is a symmetric statement from right to left. That is, there exists integers $0=\ell_{m}<\cdots<\ell_{1}<\ell_{0}=j$ with $m\leq|M|$ such that:

i)

for $0\leq s<m$ and $\ell_{s+1}<i\leq\ell_{s}$ , $w[\ell_{s},j]\ \mathcal{J}\ w[i,j]$ ,
ii)

for $0\leq s<m-1$ , $w[\ell_{s+1}-1,j]\ \cancel{\mathcal{J}}\ w[\ell_{s+1},j]$ .

The relations promised in Lemma 9 contain the information, for every position $i$ , of the evaluation of the prefixes obtained in the decomposition of Lemma 13 applied to $i$ . In the following, we slightly abuse notation and write $x\geq_{\mathcal{J}}J$ to mean that the $\mathcal{J}$ -class of $x$ is at least $J$ with respect to the order of $\mathcal{J}$ -classes.

Let $w$ be a word from $M^{*}$ , $i$ a position in the word, $y\in M$ and $J$ a $\mathcal{J}$ -class of $M$ . Let $k$ be the greatest position such that $y\cdot w[j+1,k]\geq_{\mathcal{J}}J$ . Then we define $R_{\geq J,y}(j)$ as the evaluation of $w[j+1,k]$ (notice that this is not $y\cdot w[j+1,k]$ ). Similarly, let $k$ be the least position such that $w[k,j-1]\cdot y\geq_{\mathcal{J}}J$ . Then we write $L_{\geq J,y}(j)$ for the evaluation of $w[k,j-1]$ . When $y=1$ , we simply write $R_{\geq J}$ and $L_{\geq J}$ . We also define $\bar{R}_{\geq J,y}$ and $\bar{L}_{\geq J,y}$ for the variants that include $j$ in the intervals. Note that it is not clear how to compute one from the other without access to successor predicates.

Definition 14.

Let $M$ be a monoid. The schema $\tau_{M}$ is defined as the following set of relations, where $x,y\in M$ and $J$ is a $\mathcal{J}$ -class of $M$ :

$\blacksquare$

$R_{\geq J,y,x}$ that contains $j$ if and only if $R_{\geq J,y}(j)=x$ ,
$\blacksquare$

$L_{\geq J,y,x}$ that contains $j$ if and only if $L_{\geq J,y}(j)=x$ ,
$\blacksquare$

their variants $\bar{R}_{\geq J,y,x}$ and $\bar{L}_{\geq J,y,x}$ .

These unary relations satisfy conditions (i) and (ii) of Lemma 9, see the full version. The idea to compute the evaluation of an infix $w]j,k[$ with these relations is to use them to compute the decomposition of $w]j,n]$ given by Lemma 13. This can be done by existentially quantifying the positions $l_{0},\ldots,l_{m}$ and checking the properties of the decomposition using uniquely universal quantifiers. The first $l_{s}$ after $k$ allows to deduce the $\mathcal{R}$ -class of $w]j,k[$ : indeed, $w]j,l_{s}[$ is $\mathcal{J}$ -equivalent to $w]j,k[$ by the definition of the decomposition, which is strengthened into $\mathcal{R}$ -equivalence because one is a prefix of the other. Using the second decomposition of Lemma 13, from rigth to left, we also deduce the $\mathcal{L}$ -class of $w]j,k[$ . This identify the $\mathcal{H}$ -class of the infix, then more technical work is needed to compute precisely the evaluation.

4 The regular languages of UDynProp

If binary auxiliary relations are allowed, the quantifier-free fragment DynProp of DynFO is powerful enough to maintain all regular languages [4]. In this section, we provide a characterization of the regular languages that can be maintained using quantifier-free update formulas if only unary auxiliary relations are permitted. These are precisely the regular languages that are recognized by a group. Intuitively, a computation in a group can be reversed at any moment using the presence of inverses. That is, if a computation on $x y$ ends in some memory state, it is possible to retrieve the memory state after the computation of $x$ . We denote by $\mathbf{G}$ this class of languages.

Theorem 15 (Restatement of Theorem 2).

For any regular language $L$ :

${\textsc{Member}}(L)\in\textsf{UDynProp}$ if and only if the syntactic monoid of $L$ is a group.

We first show that every regular group language can be maintained in UDynProp, using a simple adaptation of the dynamic program that maintains all regular languages using binary auxiliary relations. Then we prove that other regular languages cannot be maintained. For this, we adapt a lower bound result from [21] to show that UDynProp cannot maintain the regular language “there is at least one $\mathtt{a}$ ” and then generalize this result to all regular languages whose syntactic monoid is not a group.

4.1 Maintaining regular group languages with quantifier-free formulas

We show that unary auxiliary relations and quantifier-free update formulas are sufficient to maintain the evaluation problems of groups. The upper bound from Theorem 15 follows.

Lemma 16.

If $G$ is a group, then the problems ${\textsc{Member}}(G)$ , ${\textsc{StrictPrefix}}(G)$ and ${\textsc{StrictSuffix}}(G)$ are in UDynProp.

Proof sketch..

Gelade et al. [4] explain how to maintain membership, strict prefixes and suffixes for all regular languages with binary auxiliary relations. Their approach can directly be used to maintain these problems for monoids. For every monoid element $g$ , the corresponding update formulas use a bit $Q_{g}$ to indicate whether the whole input evaluates to $g$ and three further auxiliary relations:

$\blacksquare$

a unary relation $P_{g}$ that contains all positions $i$ such that the prefix ending at position $i-1$ evaluates to $g$ ,
$\blacksquare$

a unary relation $S_{g}$ that contains all positions $i$ such that the suffix starting at position $i+1$ evaluates to $g$ , and
$\blacksquare$

a binary relation $I_{g}$ that contains all pairs $(i,j)$ of positions such that the infix starting at position $i+1$ and ending at position $j-1$ evaluates to $g$ .

Assume that the element at position $p$ is set to the monoid element $g_{1}$ . Let $i, j$ be positions with $i<p-1$ and $j>p+1$ . After the change, the infix from position $i+1$ to position $j-1$ evaluates to the element $g_{0}\cdot g_{1}\cdot g_{2}$ , where $g_{0}$ is the result of evaluating the infix from position $i+1$ to position $p-1$ and $g_{2}$ is the result of evaluating the infix from position $p+1$ to position $j-1$ . Both elements $g_{0}$ and $g_{2}$ can be read from the auxiliary relations of the form $I_{g}$ without using quantifiers, given the position $p$ of the change and the positions $i, j$ for which the auxiliary relations are updated.

If the monoid is a group, we can replace atoms $I_{g}(i,j)$ in the update formulas as follows. Let $g_{w}$ be the result of evaluating the whole input and let $g_{p},g_{s}$ be the evaluations of the prefix up to position $i-1$ and the suffix starting from position $j+1$ , respectively. Let $g_{i}$ and $g_{j}$ be the elements at position $i$ and $j$ . All of these elements can be obtained from the input and auxiliary relations without using quantifiers, given $i$ and $j$ . From $g_{w}=g_{p}\cdot g_{i}\cdot g\cdot g_{j}\cdot g_{s}$ , for the evaluation $g$ of the infix from position $i+1$ to position $j-1$ , we obtain $g$ as $g=g_{i}^{-1}\cdot g_{p}^{-1}\cdot g_{w}\cdot g_{s}^{-1}\cdot g_{j}^{-1}$ , as every group element has an inverse.

So, we replace any atom $I_{g}(i,j)$ by the formula $\bigvee_{g=g_{i}^{-1}\cdot g_{p}^{-1}\cdot g_{w}\cdot g_{s}^{-1}\cdot g_{j}^{-% 1}}Q_{w}\wedge W_{g_{i}}(i)\wedge W_{g_{j}}(j)\wedge P_{g_{p}}(i)\wedge S_{g_{% s}}(j)$ and obtain update formulas that only use at most unary auxiliary relations. The result follows. $\hfill\blacktriangleleft$

4.2 Lower bound for regular non-group languages

We want to show that Lemma 16 is optimal and any language whose syntactic monoid is not a group cannot be maintained in UDynProp. The proof is in three steps. First, we show that a specific regular language cannot be maintained in UDynProp. We generalize this and show that UDynProp cannot maintain the membership problem for any monoid that is not a group. At last, we infer that one cannot maintain any regular language whose syntactic monoid is not a group by exploiting known closure properties of this class of languages.

4.2.1 A regular language that is not in UDynProp

Schwentick and Zeume [21] have shown that the graph reachability problem for so-called 1-layer graphs – edges may only exist from the start node $s$ to some set $A$ of nodes and from this set $A$ to the target node $t$ – is not in UDynProp. Very similarly, one can show that one cannot maintain in UDynProp whether a set is empty, where changes add elements to the set or remove elements from it. We adapt the proof to show that the regular language $\mathtt{(a+b)^{*}a(a+b)^{*}}$ , that is, the language of all words over the alphabet $\{\mathtt{a},\mathtt{b}\}$ that contain an $\mathtt{a}$ , is also not in UDynProp. The subtle difference between these problems is that the positions of a word are linearly ordered, but the elements of a set are not. However, despite this additional structure, basically the same proof goes through. We provide some more detail, also because we want to adapt the proof techniques in Section 5.

As proof technique we use the Substructure Lemma [4], which basically says that if two substructures including their auxiliary relations are isomorphic and subject to changes that respect that isomorphism, then also the auxiliary relations that result from applying quantifier-free update formulas are isomorphic.

We make this more formal. For any natural number $n$ , we write $[n]$ for the set $\{1,\ldots,n\}$ . If $w$ is a word of some length $n$ , $I$ is a subset of $[n]$ and ${\mathcal{A}}$ is a set of auxiliary relations, we write $(w,{\mathcal{A}})_{|I}$ to denote the restriction of $(w,{\mathcal{A}})$ to the positions $I$ . Let $w,w^{\prime}$ be words of length $n\leq m$ respectively and let $\pi$ be a mapping from $[n]$ to $[m]$ . We call $\pi$ order-preserving if $i<i^{\prime}$ implies $\pi(i)<\pi(i^{\prime})$ . Two sequences $\alpha=\delta_{1}\cdots\delta_{\ell}$ and $\alpha^{\prime}=\delta^{\prime}_{1}\cdots\delta^{\prime}_{\ell}$ of changes of $w$ and $w^{\prime}$ , respectively, are $\pi$ -respecting if for every pair $\delta_{i},\delta^{\prime}_{i}$ of changes it holds that if $\delta_{i}=\textsc{set}_{\sigma}(j)$ for some symbol $\sigma$ and some position $j$ , then $\delta^{\prime}_{i}=\textsc{set}_{\sigma}(\pi(j))$ .

If $\alpha$ is a sequence of changes and $\Pi$ is a dynamic program, we denote by $\Pi_{\alpha}(w,{\mathcal{A}})$ the pair of word and auxiliary relations that is obtained by applying the changes $\alpha$ and the corresponding update formulas from $\Pi$ to the word $w$ and the auxiliary relations ${\mathcal{A}}$ .

Lemma 17 (Substructure Lemma [4, Lemma 1]).

Let $\Pi$ be a dynamic UDynProp program and let $w\in\Sigma^{n}$ and $w^{\prime}\in\Sigma^{m}$ be two words over the alphabet $\Sigma$ . Further, let ${\mathcal{A}}$ and ${\mathcal{A}}^{\prime}$ be sets of at most unary auxiliary relations over the domain of $w$ and $w^{\prime}$ and the schema of $\Pi$ . Assume there are $I\subseteq[n]$ and $I^{\prime}\subseteq[m]$ such that $(w,{\mathcal{A}})_{|I}$ and $(w^{\prime},{\mathcal{A}}^{\prime})_{|I^{\prime}}$ are isomorphic via some order-preserving isomorphism $\pi$ . Then $\pi$ is also an order-preserving isomorphism from $\Pi_{\alpha}(w,{\mathcal{A}})_{|I}$ to $\Pi_{\alpha^{\prime}}(w^{\prime},{\mathcal{A}}^{\prime})_{|I^{\prime}}$ , for any $\pi$ -respecting sequences $\alpha$ and $\alpha^{\prime}$ of changes.

To obtain a lower bound via the Substructure Lemma, we need to find isomorphic substructures such that two sequences of isomorphism-respecting changes lead to words that differ with respect to membership in a regular language. To find such structures, we use Higman’s Lemma.

Lemma 18 (see [8, Chapter 6]).

Let $(w_{i},\mathcal{A}_{i})_{i\geq 1}$ be a sequence of words $w_{i}\in\Sigma^{i}$ and sets ${\mathcal{A}}_{i}$ of relations over a unary schema and over the domain of $w_{i}$ . There exists two integers $n<m$ , a subset $I\subseteq[m]$ and a mapping $\pi:[n]\rightarrow I$ such $\pi$ is a order-preserving isomorphism from $w_{n}$ to $w_{m|I}$ .

We now show the desired result.

Lemma 19 (c.f. [21, Proposition 4.8]).

The language $\mathtt{(a+b)^{*}a(a+b)^{*}}$ is not in UDynProp.

Proof.

Assume towards a contradiction that there is a dynamic UDynProp program $\Pi$ that maintains $\mathtt{(a+b)^{*}a(a+b)^{*}}$ . We consider the sequence $(w_{i},{\mathcal{A}}_{i})_{i\geq 1}$ , where $w_{i}$ is the word $\mathtt{a}^{i}$ and ${\mathcal{A}}_{i}$ are auxiliary relations that $\Pi$ obtains when starting from an empty input word of size $i$ and setting all positions to $\mathtt{a}$ . By Lemma 18, there are $n<m$ , $I\subseteq[m]$ and $\pi$ such that $\pi$ is an order-preserving isomorphism from $(w_{n},{\mathcal{A}}_{n})$ to $(w_{m},{\mathcal{A}}_{m})_{|I}$ .

The sequences $\alpha=\textsc{set}_{b}(1)\cdots\textsc{set}_{b}(n)$ and $\alpha^{\prime}=\textsc{set}_{b}(\pi(1))\cdots\textsc{set}_{b}(\pi(n))$ are $\pi$ respecting, so according to Lemma 17, the structures $\Pi_{\alpha}(w_{n},{\mathcal{A}}_{n})$ and $\Pi_{\alpha^{\prime}}(w_{m},{\mathcal{A}}_{m})_{|I}$ are also isomorphic, which means that $\Pi$ gives the same answer regarding whether the words are in the language $\mathtt{(a+b)^{*}a(a+b)^{*}}$ . But the first word only consists of $\mathtt{b}$ after the changes are applied, so does not belong to the language, while the second word still contains at least one $\mathtt{a}$ , contradicting the assumption that $\Pi$ maintains the language. $\hfill\blacktriangleleft$

4.2.2 UDynProp cannot maintain any regular non-group language

We now lift the unmaintainability result of Lemma 19 to all regular languages whose syntactic monoid is not a group. First, we observe that UDynProp cannot maintain the membership problem of any monoid that is not a group.

Lemma 20.

If $M$ is a monoid that is not a group, then ${\textsc{Member}}(M)$ is not in UDynProp.

Proof.

The syntactic monoid $U_{1}$ of the language $\mathtt{(a+b)^{*}a(a+b)^{*}}$ has only the elements $1$ and $a$ , where $1$ is the neutral element and $a$ acts as a zero: $1\cdot x=x\cdot 1=x$ and $a\cdot x=x\cdot a=a$ for every $x\in\{1,a\}$ . As $a$ has no inverse, $U_{1}$ is not a group. It follows from Fact 6 and Lemma 19 that ${\textsc{Member}}(U_{1})$ is not in UDynProp.

Now assume that for some arbitrary non-group monoid $M$ the problem ${\textsc{Member}}(M)$ is in UDynProp. We first claim that $U_{1}$ is a submonoid of $M$ . To see that, observe that $M$ must have an element $x$ whose idempotent power is not the identity. Otherwise, if $x^{\omega}=1$ for every element $x\in M$ , then let $n>0$ be chosen such that $x^{n}=1$ is the idempotent. Then $x\cdot x^{n-1}=x^{n-1}\cdot x=1$ holds, so $x$ has the inverse $x^{n-1}$ , so $M$ is a group, contradicting the assumption. Therefore, $M$ has an idempotent $e$ that is different from $1$ and $\{1,e\}$ is a submonoid of $M$ that is isomorphic to $U_{1}$ .

As $U_{1}$ is a submonoid of $M$ and in particular divides $M$ , assuming ${\textsc{Member}}(M)\in\textsf{UDynProp}$ leads to a contradiction, as from Fact 7 the false statement ${\textsc{Member}}(U_{1})\in\textsf{UDynProp}$ would follow. $\hfill\blacktriangleleft$

Now we have to translate Lemma 20 from monoids to languages, that is, we need a converse to Fact 6. So, we have to prove that if UDynProp can maintain some regular language, it can also maintain the membership problem of its syntactic monoid.

We employ the theory of (pseudo)varieties, which goes back to Eilenberg [3].

Let ${\mathcal{L}}$ be a class of regular languages over the alphabet $\Sigma$ . It is closed under Boolean operations if $L_{1}\cup L_{2}$ , $L_{1}\cap L_{2}$ and $L_{1}^{c}$ are in ${\mathcal{L}}$ for any $L_{1},L_{2}\in{\mathcal{L}}$ . It is closed under quotients if $\sigma^{-1}L=\{w\ |\ \sigma w\in L\}$ and $L\sigma^{-1}=\{w\ |\ w\sigma\in L\}$ are in ${\mathcal{L}}$ for any $L\in{\mathcal{L}}$ and $\sigma\in\Sigma$ . It is closed under inverse morphisms if $\mu^{-1}(L)$ is in ${\mathcal{L}}$ for any $L\in{\mathcal{L}}$ , where $\Gamma$ is any alphabet and $\mu:\Gamma\rightarrow\Sigma^{*}$ is a function that is extended to $\Gamma^{*}$ letter-wise.

A class ${\mathcal{V}}$ of regular languages is a (pseudo)variety if it is closed under Boolean operations, quotients and inverse morphisms. We often omit the “pseudo” and simply call such classes “varieties”. For this work, the following result is used.

Lemma 21 ([3], see [12, Theorem XIII.4.10]).

Let ${\mathcal{V}}$ be a variety of regular languages and let $M$ be the syntactic monoid of some language $L\in{\mathcal{V}}$ . Then any language recognized by $M$ is also in ${\mathcal{V}}$ .

This implies that the converse of Fact 6 holds for UDynProp.

Fact 22.

Let ${\mathcal{C}}$ be a class of formulas such that the regular languages $L$ with ${\textsc{Member}}(L)\in\textsf{UDyn${\mathcal{C}}$}$ form a variety. Let $L$ be a regular language and $M$ its syntactic monoid:

{\textsc{Member}}(L)\in\textsf{UDyn${\mathcal{C}}$}\Rightarrow{\textsc{Member}% }(M)\in\textsf{UDyn${\mathcal{C}}$}.

Proof.

Assume that ${\textsc{Member}}(L)$ is in UDyn ${\mathcal{C}}$ and that $M$ is its syntactic monoid. For each $x\in M$ , the monoid $M$ recognizes the language of all sequences of monoid elements that evaluate to $x$ , so by Lemma 21, this language is also in UDyn ${\mathcal{C}}$ . A dynamic UDyn ${\mathcal{C}}$ program for ${\textsc{Member}}(M)$ maintains these languages for each $x\in M$ . $\hfill\blacktriangleleft$

The “only if” direction of Theorem 15 follows: observe that the regular languages of UDynProp form a variety, as UDynProp is trivially closed under Boolean operations, but also closed under quotients and inverse morphisms due to Lemma 5. Therefore, by Fact 22, if UDynProp can maintain a regular language, it can also maintain the membership problem of its corresponding syntactic monoid. But, by Lemma 20, UDynProp cannot maintain this problem for any monoid that is not a group.

5 The regular languages of UDyn $\Sigma_{1}^{+}$

In this section, we provide a characterization of the regular languages that can be maintained using positive $\Sigma_{1}$ -formulas if only unary auxiliary relations are permitted. Here, positive $\Sigma_{1}$ -formulas are $\exists^{*}$ -formulas that may not use negations in the quantifier-free part, with the only exception that negations can be used directly in front of the built-in linear order $\leq$ .

An inspection of the proof of Theorem 15 shows that positive quantifier-free formulas and therefore in particular $\Sigma_{1}^{+}$ -formulas can maintain all regular languages recognized by groups. It is also known that $\Sigma_{1}^{+}$ -formulas can express all regular languages recognized by the class $\mathbf{J}^{+}$ of ordered monoids (see Section 5.1 for a definition). It turns out that languages maintainable in UDyn $\Sigma_{1}^{+}$ are exactly those recognizable by ordered monoids from the wreath product $\mathbf{J}^{+}\ast\mathbf{G}$ of $\mathbf{J}^{+}$ and $\mathbf{G}$ . Intuitively, this class contains monoids that first do a “group computation” followed by a “ $\mathbf{J}^{+}$ -computation” (see Section 5.1 for a formalization).

Theorem 23 (Restatement of Theorem 3).

For any regular language $L$ :
${\textsc{Member}}(L)\in\textsf{UDyn$\Sigma_{1}^{+}$}$ if and only if the ordered syntactic monoid of $L$ is in $\mathbf{J}^{+}\ast\mathbf{G}$ .

We will show, in Section 5.2, that every regular language recognized with $\mathbf{J}^{+}\ast\mathbf{G}$ is in UDyn $\Sigma_{1}^{+}$ . Then, in Section 5.3, we prove that other regular languages cannot be maintained. To this end, we first show that the language $\mathtt{b^{*}}$ cannot be maintained, using an adaptation of the substructure lemma to UDyn $\Sigma_{1}^{+}$ . Finally, relying on a characterization of $\mathbf{J}^{+}\ast\mathbf{G}$ , we show that if another language could be maintained, then so could the language $\mathtt{b^{*}}$ . We therefore look at monoids supplemented with additional ordering information.

5.1 Ordered monoids and wreath products

For the characterization obtained in Section 4, we exploited that the class of languages maintainable in UDynProp is a variety and can therefore be studied by looking at the syntactic monoids of its languages. Unfortunately, the class UDyn $\Sigma_{1}^{+}$ of languages is not a variety, as it is not closed under complementation: we will later see that the language $\mathtt{(a+b)^{*}a(a+b)^{*}}$ can be maintained, but its complement $\mathtt{b^{*}}$ cannot. As both languages are recognized by the same monoid $U_{1}=\{1,a\}$ , the information provided by syntactic monoids alone is not sufficient for understanding UDyn $\Sigma_{1}^{+}$ .

Ordered monoids.

An algebraic theory for classes of regular languages satisfying all the requirements of a variety but complementation has been developed by Pin [11]. In this theory, syntactic monoids are supplemented by an additional order. An ordered monoid is a pair $(M,\leq)$ where $M$ is a monoid and $\leq$ is a partial order on $M$ compatible with the operation, that is, $xx^{\prime}\leq yy^{\prime}$ whenever $x\leq y$ and $x^{\prime}\leq y^{\prime}$ . We write $\uparrow x$ for the set of all elements $y$ with $y\geq x$ . We call $P\subseteq M$ an upset if it is closed under $\uparrow$ , that is, if $\uparrow x\subseteq P$ for all $x\in P$ . A morphism from $(M,\leq)$ to $(N,\leq)$ is a monoid morphism from $M$ to $N$ such that for all $x,y\in M$ , $x\leq y$ implies $\varphi(x)\leq\varphi(y)$ . The notions quotient, submonoid and division for monoids can be transferred to ordered monoids using this new notion of morphism.

A language $L$ is recognized by $(M,\leq)$ if there is a (monoid) morphism $\varphi:\Sigma^{*}\rightarrow M$ and an upset $P$ such that $L=\varphi^{-1}(P)$ . The syntactic ordered monoid $(M,\leq)$ for a regular language $L$ consists of the transition monoid $M$ of the minimal automaton and an order $\leq$ such that $\delta_{1}\leq\delta_{2}$ for $\delta_{1},\delta_{2}\in M$ if for some $\delta_{3}\in M$ and any state $q$ of the minimal automaton it holds that if $\delta_{3}(\delta_{1}(q))$ is an accepting state, so is $\delta_{3}(\delta_{2}(q))$ .

Example 24.

Recall that $U_{1}=\{1,a\}$ is the syntactic monoid of $\mathtt{(a+b)^{*}a(a+b)^{*}}$ , and therefore also of its complement $\mathtt{b^{*}}$ . However, these languages can be distinguished by their syntactic ordered monoids. Let $U_{1}^{+}$ (resp. $U_{1}^{-}$ ) be the ordered monoid $U_{1}$ equipped with the order $1\leq a$ (resp. $1\geq a$ ). Then $U_{1}^{+}$ is the syntactic ordered monoid of $\mathtt{(a+b)^{*}a(a+b)^{*}}$ , whereas $U_{1}^{-}$ is the syntactic ordered monoid of $\mathtt{b^{*}}$ . Note that $\mathtt{b^{*}}$ cannot be recognized by $U_{1}^{+}$ because it is the inverse image of $1$ , which is not an upset.

A prominent example of a class of languages defined via ordered monoids is $\mathbf{J}^{+}$ .

Definition 25.

We denote by $\mathbf{J}^{+}$ the class of all languages whose syntactic ordered monoid has the property that $1\leq x$ for every $x\in M$ .

It is known²²2In that reference, all orders are reversed. In particular, recognition is defined in terms of downsets. [2, Theorem 3.4] that this class coincides with the class of regular languages expressible by $\Sigma_{1}$ -formulas. A simple inspection of the proof gives that all formulas are furthermore $\Sigma_{1}^{+}$ -formulas.

Ordered wreath products.

A successful application of wreath products has been to decompose languages into simpler ones, e.g. in the celebrated decomposition theorem of Krohn and Rhodes [7]. One intuition for these products comes from the cascading of finite state automata. Suppose that ${\mathcal{A}}_{1}$ is a deterministic finite state automaton over $\Sigma$ with state set $Q$ , and ${\mathcal{A}}_{2}$ is a deterministic finite state automaton over $Q\times\Sigma$ . On input $w$ , their cascade product ${\mathcal{A}}_{2}\circ{\mathcal{A}}_{1}$ first annotates $w$ with the states reached in its run in ${\mathcal{A}}_{1}$ . Then the resulting enhanced word is fed into ${\mathcal{A}}_{2}$ to check for acceptance.

The algebraic counterpart of this cascade product is the semidirect product of monoids. Here, we use the version for ordered monoids introduced by Pin and Weil [13]. Let $(M,\leq)$ and $(N,\leq)$ be two ordered monoids. To ease notation, we make the common notational convention to denote the operation of $M$ additively.³³3Note that it does not mean that $M$ is commutative. The semidirect product of $(M,\leq)$ and $(N,\leq)$ is defined with respect to a given left action. A left action $\cdot$ of $(N,\leq)$ on $(M,\leq)$ is a map $(y,x)\mapsto y\cdot x$ from $N\times M$ to $M$ such that for every $x,x_{1}x_{2}\in M$ and $y,y_{1},y_{2}\in N$ satisfies the axioms (1) $(y_{1}y_{2})\cdot x=y_{1}\cdot(y_{2}\cdot x)$ , (2) $y\cdot(x_{1}+x_{2})=y\cdot x_{1}+y\cdot x_{2}$ , (3) $1\cdot x=x$ , (4) $y\cdot 1=1$ , (5) if $x_{1}\leq x_{2}$ then $y\cdot x_{1}\leq y\cdot x_{2}$ ; and (6) if $y_{1}\leq y_{2}$ then $y_{1}\cdot x\leq y_{2}\cdot x$ .

The semidirect product $(M,\leq)\ast(N,\leq)$ of $(M,\leq)$ and $(N,\leq)$ with respect to the left action $\cdot$ is the ordered monoid on $M\times N$ defined by the operation $(x_{1},y_{1})(x_{2},y_{2})=(x_{1}+y_{1}\cdot x_{2},y_{1}y_{2})$ for any $x_{1},x_{2}\in M$ and $y_{1},y_{2}\in N$ . The order on the product is defined componentwise, that is $(x_{1},y_{1})\leq(x_{2},y_{2})$ if and only if $x_{1}\leq x_{2}$ and $y_{1}\leq y_{2}$ .

Unfolding the definition for a longer product sheds light on the connection between the semidirect product on monoids and the cascaded product on automata. For $x_{1},\ldots,x_{n}\in M$ and $y_{1},\ldots,y_{n}\in N$ , the product in $M\ast N$ is (by using the axioms defining a left action):

(x_{1},y_{1})\cdots(x_{n},y_{n})=(x_{1}+y_{1}\cdot x_{2}+(y_{1}y_{2})\cdot x_{% 3}+\cdots+(y_{1}\cdots y_{n-1})\cdot x_{n},y_{1}\cdots y_{n})

(1)

Indeed, in a cascade product, the transition function when reading a letter in the first automaton changes according to the transition function realized so far by the second automaton. When reading the $i^{\text{th}}$ letter, the annotation is determined by $y_{1}\cdots y_{i-1}$ and the action $(y_{1}\cdots y_{i-1})\cdot x_{i}$ gives the transition function that is used.

The wreath product $\mathbf{V}\ast\mathbf{W}$ of two classes $\mathbf{V}$ and $\mathbf{W}$ of ordered monoids contains all ordered monoids that divide a semidirect product of the form $(M,\leq)\ast(N,\leq)$ for $(M,\leq)\in\mathbf{V}$ and $(N,\leq)\in\mathbf{W}$ .

$\blacktriangleright$ Remark 26.

We chose this definition of wreath products for simplicity. While it already exists in the literature, a most standard choice for $\mathbf{V}\ast\mathbf{W}$ would have been to take all ordered monoids dividing $M^{N}\times N$ endowed with some specific order and operation, when $(M,\leq)\in\mathbf{V}$ and $(N,\leq)\in\mathbf{W}$ . In fact, both definitions are equivalent when both $\mathbf{V}$ and $\mathbf{W}$ are closed under direct products. This is the case for the classes under study here, that is for $\mathbf{J}^{+}$ and $\mathbf{G}$ . Furthermore, the only result on wreath products that is used out-of-the-shelf is Theorem 4.11 in [13] (stated as Theorem 31 here). Therein, the equivalence between all definitions is proved (see their Proposition 3.5, our definition is (1) and the alternative one is (2)).

5.2 Maintaining regular languages in $\mathbf{J}^{+}\ast\mathbf{G}$ with positive $\Sigma_{1}$ -formulas

We will now show that unary auxiliary relations and positive $\Sigma_{1}$ -formulas are sufficient to maintain the evaluation problems of ordered monoids in $\mathbf{J}^{+}\ast\mathbf{G}$ . The upper bound from Theorem 23 then follows from the following Fact 27 which is the analogon of Fact 6 for ordered monoids. For an ordered monoid $(M,\leq)$ , define ${\textsc{Member}}(M,\leq)$ to be the problem that, for a word $w$ subject to changes, maintain a dedicated bit $q_{x}$ that holds $1$ whenever $w\in\uparrow x$ , for every $x\in M$ .

Fact 27.

Let ${\mathcal{C}}$ be a class of formulas closed under $\lor$ . Further let $L$ be a regular language and $(M,\leq)$ its syntactic ordered monoid. Then:

{\textsc{Member}}(M,\leq)\in\textsf{UDyn${\mathcal{C}}$}\Rightarrow{\textsc{% Member}}(L)\in\textsf{UDyn${\mathcal{C}}$}.

Lemma 28.

If $(M,\leq)\in\mathbf{J}^{+}\ast\mathbf{G}$ , then ${\textsc{Member}}(M,\leq)$ is in UDyn $\Sigma_{1}^{+}$ .

Proof sketch..

We show how to maintain ${\textsc{Member}}(M,\leq)$ when $(M,\leq)=(J,\leq)\ast(G,\leq)$ for a fixed left action, where $(J,\leq)\in\mathbf{J}^{+}$ and $G$ is a group. The result then follows from Fact 7, that can be easily extended to ordered monoids.

Let $w=(x_{1},g_{1})\cdots(x_{n},g_{n})$ be the input word, where $x_{i}\in J$ and $g_{i}\in G$ for all $i\leq n$ . Let $P=\uparrow(p,q)=(\uparrow p,\uparrow q)$ be an upset of $(M,\leq)$ , where $p\in J$ and $q\in G$ . We describe how to maintain whether $w$ evaluates in $P$ .

By Lemma 16, we can maintain all evaluations $g_{1}\cdots g_{i-1}$ of strict prefixes of the projection of $w$ to the component from $G$ in UDynProp, as well as the information whether $g_{1}\cdots g_{n}$ evaluates in $\uparrow q$ . The corresponding update formulas are actually positive: the original update formulas in [4] are positive and the adaptations of the proof of Lemma 16 do not introduce negations. This allows to maintain the values $(g_{1}\cdots g_{i-1})\cdot x_{i}\in J$ using positive quantifier-free formulas.

Using the Equation 1, we still need to determine whether $x_{1}+g_{1}\cdot x_{2}+(g_{1}g_{2})\cdot x_{3}+\cdots+(g_{1}\cdots g_{n-1})% \cdot x_{n}$ evaluates in $\uparrow p$ . As the membership problem of $(J,\leq)$ can be expressed by a $\Sigma_{1}^{+}$ formula [2, Theorem 3], $\Sigma_{1}^{+}$ update formulas can perform that evaluation. $\hfill\blacktriangleleft$

5.3 Lower bound for regular languages not in $\mathbf{J}^{+}\ast\mathbf{G}$

We want to show that Lemma 28 is optimal and any language whose ordered syntactic monoid is not in $\mathbf{J}^{+}\ast\mathbf{G}$ cannot be maintained in UDyn $\Sigma_{1}^{+}$ . The proof is in two steps. First, we show that the regular language $\mathtt{b^{*}}$ cannot be maintained in UDyn $\Sigma_{1}^{+}$ . We then introduce a characterization of $\mathbf{J}^{+}\ast\mathbf{G}$ that implies that if a language not recognized by $\mathbf{J}^{+}\ast\mathbf{G}$ could be maintained, then so could the language $\mathtt{b^{*}}$ .

5.3.1 A regular language that is not in UDyn $\Sigma_{1}^{+}$

We show that the language $b^{*}$ is not in UDyn $\Sigma_{1}^{+}$ by generalizing the substructure lemma from DynProp to UDyn $\Sigma_{1}^{+}$ and then applying it to $b^{*}$ .

The substructure lemma for UDynProp relies on the inability of quantifier-free formulas to access elements outside the isomorphic substructures. We adopt the lemma to allow existential quantification in update formulas by weakening the requirement on the substructures to be isomorphic. To this end, let $(w,\mathcal{A}),(w^{\prime},\mathcal{A}^{\prime})$ be words of length $n\leq m$ respectively annotated with sets of unary auxiliary relations $\mathcal{A},\mathcal{A}^{\prime}$ . For $i\in[n]$ , the type of $(w,\mathcal{A})_{|i}$ consists of $w_{i}$ and of the set of all relations of $\mathcal{A}$ containing $i$ . Let $\pi$ be a mapping from $[n]$ to $[m]$ . We say that $\pi$ is type-monotonic if the type of $(w,\mathcal{A})_{|i}$ is a subset of the type of $(w^{\prime},\mathcal{A}^{\prime})_{|\pi(i)}$ for all $i\in[n]$ , i.e. if whenever $R{{}^{\mathcal{A}}}(i)$ holds then so does $R{{}^{\mathcal{A^{\prime}}}}(\pi(i))$ . In this case, we say that $(w,{\mathcal{A}})$ and $(w^{\prime},{\mathcal{A}}^{\prime})_{|\pi([n])}$ are type-monotonic via $\pi$ .

Lemma 29 (Substructure lemma for UDyn $\Sigma_{1}^{+}$ ).

Let $\Pi$ be a dynamic UDyn $\Sigma_{1}^{+}$ -program and let $w\in\Sigma^{n}$ and $w^{\prime}\in\Sigma^{m}$ be two words over the alphabet $\Sigma$ . Further, let ${\mathcal{A}}$ and ${\mathcal{A}}^{\prime}$ be sets of at most unary auxiliary relations over the domain of $w$ and $w^{\prime}$ and the schema of $\Pi$ .

Assume there is $I\subseteq[m]$ such that $(w,{\mathcal{A}})$ and $(w^{\prime},{\mathcal{A}}^{\prime})_{|I}$ are type-monotonic via some order-preserving mapping $\pi$ . Then $\pi$ is also a type-monotonic mapping from $\Pi_{\alpha}(w,{\mathcal{A}})$ to $\Pi_{\alpha^{\prime}}(w^{\prime},{\mathcal{A}}^{\prime})_{|I}$ , for any $\pi$ -respecting sequences $\alpha$ and $\alpha^{\prime}$ of changes.

Proof.

We show the statement for a single change $\alpha=(\textsc{set}_{\sigma}(i))$ and $\alpha^{\prime}=(\textsc{set}_{\sigma}(\pi(i))$ with $i\in[n]$ ; the general statement follows by induction on the length of change sequences.

For showing that $\Pi_{\alpha}(w,{\mathcal{A}})$ and $\Pi_{\alpha^{\prime}}(w^{\prime},{\mathcal{A}}^{\prime})_{|I}$ are type-monotonic via $\pi$ , consider a unary relation symbol $R$ updated by formula $\varphi(x;y)\mathrel{\smash{\stackrel{{\scriptstyle\scriptscriptstyle{\text{% def}}}}{{=}}}}\;\exists z_{1}\dots\exists z_{k}\psi\in\Sigma_{1}^{+}$ when a change to $\sigma$ is made. Suppose $\varphi(j;i)$ evaluates to true in $(w,{\mathcal{A}})$ by choosing $z_{1},\dots,z_{k}$ as $j_{1},\ldots,j_{k}$ . Then $\varphi(\pi(j);\pi(i))$ evaluates to true in $(w^{\prime},{\mathcal{A}}^{\prime})$ by choosing $z_{1},\dots,z_{k}$ as $\pi(j_{1}),\ldots,\pi(j_{k})$ , because $(w,{\mathcal{A}})$ and $(w^{\prime},{\mathcal{A}}^{\prime})_{|I}$ are type-monotonic via $\pi$ and $\psi$ only contains positive atoms. $\hfill\blacktriangleleft$

To conclude, we apply Higman’s lemma in a similar fashion as in Section 4.

Lemma 30.

The language $\mathtt{b^{*}}$ is not in UDyn $\Sigma_{1}^{+}$ .

Proof.

Assume towards a contradiction that there is a dynamic UDyn $\Sigma_{1}^{+}$ -program $\Pi$ that maintains $\mathtt{b^{*}}$ . We consider the sequence $(w_{i},{\mathcal{A}}_{i})_{i\geq 1}$ , where $w_{i}$ is the word $\mathtt{a}^{i}$ and ${\mathcal{A}}_{i}$ are the auxiliary relations that $\Pi$ obtains when starting from an empty input word of size $i$ and setting all positions to $\mathtt{a}$ . By Lemma 18, there are $n<m$ , $I\subseteq[m]$ and $\pi$ such that $\pi$ is an order-preserving isomorphism from $(w_{n},{\mathcal{A}}_{n})$ to $(w_{m},{\mathcal{A}}_{m})_{|I}$ . This implies, in particular, that $\pi$ is type-monotonic on $(w_{n},{\mathcal{A}}_{n})$ and $(w_{m},{\mathcal{A}}_{m})_{|I}$ .

The sequences $\alpha=\textsc{set}_{b}(1)\cdots\textsc{set}_{b}(n)$ and $\alpha^{\prime}=\textsc{set}_{b}(\pi(1))\cdots\textsc{set}_{b}(\pi(n))$ are $\pi$ respecting, so according to Lemma 29, the structures $\Pi_{\alpha}(w_{n},{\mathcal{A}}_{n})$ and $\Pi_{\alpha^{\prime}}(w_{m},{\mathcal{A}}_{m})_{|I}$ are also type-monotonic. But then, because the first word belongs to the language after applying the changes, the program must also say so for the second word after applying the changes (as it must be monotonic on the answer bit). This is a contradiction, because the second word does not belong to the language after the changes. $\hfill\blacktriangleleft$

5.3.2 UDyn $\Sigma_{1}^{+}$ cannot maintain any regular non- $\mathbf{J}^{+}\ast\mathbf{G}$ language

To lift the unmaintainability result of Lemma 30 to all regular languages whose syntactic monoid is not in $\mathbf{J}^{+}\ast\mathbf{G}$ , we first show that UDyn $\Sigma_{1}^{+}$ cannot maintain the membership problem of such monoids and then lift this to all languages recognized by them.

We have seen that the definition of $\mathbf{J}^{+}\ast\mathbf{G}$ with the wreath product is useful to design algorithms using only formulas of low complexity and to obtain upper bounds. However, for understanding which monoids do not belong to the class, an equivalent characterization due to Pin and Weil [13] is helpful. Denote by $\mathbf{E}\mathbf{J}^{+}$ the class⁴⁴4Note Pin and Weil denote $\mathbf{E}\mathbf{J}^{+}$ by $\mathbf{B}\mathbf{G}^{+}$ and reverse the order. of languages whose syntactic ordered monoids satisfy $1\leq e$ for every idempotent $e$ . For instance, $\mathtt{(a+b)^{*}aa(a+b)^{*}}$ is not in $\mathbf{J}^{+}$ but in $\mathbf{E}\mathbf{J}^{+}$ , while $\mathtt{(ab)^{*}}$ is in neither. Furthermore, every group is in $\mathbf{E}\mathbf{J}^{+}$ as they have a single idempotent which is the identity.

Theorem 31 (Pin and Weil [13, Thm 4.11]).

$\mathbf{J}^{+}\ast\mathbf{G}=\mathbf{E}\mathbf{J}^{+}$

This characterization immediately yields $U_{1}^{-}$ as witness for non-membership in $\mathbf{J}^{+}\ast\mathbf{G}$ .

Lemma 32.

If $(M,\leq)\notin\mathbf{J}^{+}\ast\mathbf{G}$ , then $U_{1}^{-}$ divides $(M,\leq)$ .

Proof.

By definition of $\mathbf{E}\mathbf{J}^{+}$ , we can find an idempotent $e\in M$ such that $1\not\leq e$ . It implies in particular that $e$ is different from the identity. We consider the submonoid $(U_{1},\leq)$ of $(M,\leq)$ with $U_{1}=\{1,e\}$ and do a case distinction on $\leq$ :

$\blacksquare$

If $1\geq e$ , then $(U_{1},\leq)$ is exactly $U_{1}^{-}$ .
$\blacksquare$

If $1$ and $e$ are incomparable, then the order $\leq$ restricted to $U_{1}$ is the equality $=$ . We conclude by remarking that $U_{1}^{-}$ is a quotient of $(U_{1},=)$ , using the identity function.

$\hfill\blacktriangleleft$

Lemma 33.

If $(M,\leq)$ is an ordered monoid that is not in $\mathbf{J}^{+}\ast\mathbf{G}$ , then ${\textsc{Member}}(M,\leq)$ is not in UDyn $\Sigma_{1}^{+}$ .

Proof.

We first observe that UDyn $\Sigma_{1}^{+}$ cannot maintain ${\textsc{Member}}(U_{1}^{-})$ , due to Fact 27 and Lemma 19 and because $U_{1}^{-}$ is the ordered syntactic monoid of the language $\mathtt{b^{*}}$ .

Now assume, towards a contradiction, that ${\textsc{Member}}(M,<)$ is in UDyn $\Sigma_{1}^{+}$ for some monoid $(M,<)$ which is not in $\mathbf{J}^{+}\ast\mathbf{G}$ . By Lemma 32, $U_{1}^{-}$ is a submonoid of $(M,\leq)$ and hence ${\textsc{Member}}(U_{1}^{-})$ is in UDyn $\Sigma_{1}^{+}$ by Fact 7 straightforwardly extended to ordered monoids (it suffices to remark that the inverse image of an upset by a morphism is an upset), contradicting our observation from above. $\hfill\blacktriangleleft$

Now we have to translate the previous lemma from ordered monoids to languages, that is, we need a converse to Fact 27. To this end, we prove that if UDyn $\Sigma_{1}^{+}$ can maintain a regular language, it can also maintain the membership problem of its ordered syntactic monoid.

To this end, we use a variant of varieties that does not require closure under complementation. A class ${\mathcal{V}}$ of regular languages is a positive (pseudo)variety if it is closed under positive Boolean operations, quotients and inverse morphisms.

Examples of positive varieties are $\mathbf{V}\ast\mathbf{W}$ whenever $\mathbf{V}$ and $\mathbf{W}$ are positive varieties [13, Proposition 3.5]. Also UDyn $\Sigma_{1}^{+}$ is a positive variety, because it is closed under positive Boolean operations (because $\Sigma_{1}^{+}$ is closed under $\lor$ and $\land$ ) and under quotients and inverse morphisms (due to Lemma 5). The theorem of Eilenberg translates to positive varieties:

Theorem 34 (Pin [12, Theorem 4.12]).

Let ${\mathcal{V}}$ be a positive variety of regular languages and let $(M,\leq)$ be the syntactic ordered monoid of a language $L\in{\mathcal{V}}$ . Then any language recognized by $(M,\leq)$ is also in ${\mathcal{V}}$ .

This implies that the converse of Fact 27 holds for positive varieties.

Fact 35.

Let ${\mathcal{C}}$ be a class of formulas such that the regular languages of UDyn ${\mathcal{C}}$ form a positive variety. Let $L$ be a regular language and $(M,\leq)$ its syntactic ordered monoid:

{\textsc{Member}}(L)\in\textsf{UDyn${\mathcal{C}}$}\Rightarrow{\textsc{Member}% }(M,\leq)\in\textsf{UDyn${\mathcal{C}}$}.

Proof.

Assume that ${\textsc{Member}}(L)$ is in UDyn ${\mathcal{C}}$ . Let $\varphi:M^{*}\rightarrow M$ be the morphism that evaluates a word in $M^{*}$ , that is that maps $x_{1}\cdots x_{n}$ to the product of the $x_{i}$ for $1\leq i\leq n$ . For any fixed $x\in M$ , notice that $\uparrow x$ is an upset of $M$ . Thus ${\textsc{Member}}(\varphi^{-1}(\uparrow x))$ is in UDyn ${\mathcal{C}}$ for every $x\in M$ , by Theorem 34. A dynamic program for ${\textsc{Member}}(M)$ uses each of these programs to generate one bit of output. $\hfill\blacktriangleleft$

The “only if” direction of Theorem 23 now follows. By Fact 35 and because the regular languages of UDyn $\Sigma_{1}^{+}$ form a positive variety: if UDyn $\Sigma_{1}^{+}$ can maintain a regular language, it can also maintain the membership problem of its ordered syntactic monoid. But, by Lemma 33, UDyn $\Sigma_{1}^{+}$ cannot maintain this problem for any ordered monoid not in $\mathbf{J}^{+}\ast\mathbf{G}$ .

6 Conclusion

We characterized the regular languages of UDyn $\Sigma_{1}^{+}$ and UDynProp by properties of their (ordered) syntactic monoids. The most important fragment of DynFO for which a characterization remains open is UDyn $\Sigma_{1}$ (see also the discussion in the full version of this paper).

Open question.

Which regular languages are in UDyn $\Sigma_{1}$ , i.e. can be maintained by $\exists^{*}$ update formulas and unary auxiliary relations?

Two obstacles to an algebraic characterization of UDyn $\Sigma_{1}$ are (1) that $\Sigma_{1}$ is not closed under composition and thus UDyn $\Sigma_{1}$ is a priori not a (positive) variety; and (2) an absence of lower bounds techniques against UDyn $\Sigma_{1}$ . One path towards resolving (1) is via considering positive lp-varieties, which only require closure under positive Boolean operations and under quotients of inverses of length-preserving morphisms [14]. For (2), new lower bound techniques beyond the substructure lemma (and its variant used for UDyn $\Sigma_{1}^{+}$ ) seem to be necessary.

We shortly discuss the expressive power of UDyn $\Sigma_{1}$ . Consider the class $\mathbf{J}$ of languages that can be described by a Boolean combination of $\Sigma_{1}$ -formulas. This class is equal to the class of piecewise-testable languages [18]. We can show that UDyn $\Sigma_{1}$ is strictly more powerful than UDyn $\Sigma_{1}^{+}$ , by looking at the unordered counterpart of $\mathbf{J}^{+}\ast\mathbf{G}$ .

Lemma 36.

If $L$ is a regular language in $\mathbf{J}\ast\mathbf{G}$ , then ${\textsc{Member}}(L)$ is in UDyn $\Sigma_{1}$ .

Unfortunately, $\mathbf{J}\ast\mathbf{G}$ does not provide an exact characterization, because the language $\mathtt{\Sigma^{*}aa\Sigma^{*}}$ is in UDyn $\Sigma_{1}$ , but its ordered syntactic monoid is not in $\mathbf{J}\ast\mathbf{G}$ .

Conjecture 37.

Let $\mathcal{V}$ be the positive lp-variety of regular languages $L$ such that ${\textsc{Member}}(L)$ is in UDyn $\Sigma_{1}$ . Then $\mathbf{J}\ast\mathbf{G}\subsetneq\mathcal{V}\subseteq\Sigma_{2}\ast\mathbf{G}$ . In particular, $\mathtt{(\Sigma^{*}aa\Sigma^{*})^{c}}$ is not⁵⁵5Note that non-membership in $\Sigma_{2}\ast\mathbf{G}$ can be checked with the MeSCaL software [15]. in $\mathcal{V}$ .

Another direction is to explore (fragments of) the class of context-free languages. It is known that every context-free language can be maintained in DynFO [4], yet the known dynamic program requires $\Sigma_{1}$ -update formulas and $4$ -ary auxiliary relations.

Open question.

Which dynamic resources (quantifier-alterations, arity of auxiliary relations,…) are required for maintaining context-free languages?

References

[1] J. Büchi. Weak second-order arithmetic and finite automata. Mathematical Logic Quarterly, 6:66–92, 1960. doi:10.1007/978-1-4613-8928-6_22.
[2] Volker Diekert, Paul Gastin, and Manfred Kufleitner. A survey on small fragments of first-order logic over finite words. Int. J. Found. Comput. Sci., 19(3):513–548, 2008. doi:10.1142/S0129054108005802.
[3] Samuel Eilenberg. Automata, Languages and Machines, Vol. B. Academic Press Inc, 1976. URL: https://www.sciencedirect.com/bookseries/pure-and-applied-mathematics/vol/59/part/PB.
[4] Wouter Gelade, Marcel Marquardt, and Thomas Schwentick. The dynamic complexity of formal languages. ACM Trans. Comput. Logic, 13(3), 2012. doi:10.1145/2287718.2287719.
[5] J. A. Green. On the structure of semigroups. Annals of Mathematics, 54(1):163–172, 1951. URL: http://www.jstor.org/stable/1969317.
[6] William Hesse. Dynamic Computational Complexity. PhD thesis, University of Massachusetts Amherst, 2003.
[7] Kenneth Krohn and John Rhodes. Algebraic theory of machines. i. prime decomposition theorem for finite semigroups and machines. Transactions of the American Mathematical Society, 116:450–464, 1965. URL: http://www.jstor.org/stable/1994127.
[8] M. Lothaire. Combinatorics on Words. Cambridge Mathematical Library. Cambridge University Press, 2 edition, 1997.
[9] Robert McNaughton and Seymour A. Papert. Counter-Free Automata (M.I.T. research monograph no. 65). The MIT Press, 1971.
[10] Sushant Patnaik and Neil Immerman. Dyn-FO: A parallel, dynamic complexity class. J. Comput. Syst. Sci., 55(2):199–209, 1997. doi:10.1006/jcss.1997.1520.
[11] Jean-Éric Pin. A variety theorem without complementation. Russian Mathematics (Izvestija vuzov. Matematika), 39:80–90, 1995.
[12] Jean-Eric Pin. Mathematical foundations of automata theory. Lecture notes, 2014. URL: http://www.irif.fr/˜jep/PDF/MPRI/MPRI.pdf.
[13] Jean-Eric Pin and Pascal Weil. Semidirect products of ordered semigroups. Communications in Algebra, 30(1):149–169, 2002.
[14] Jean-Éric Pin and Howard Straubing. Some results on c-varieties. RAIRO - Theoretical Informatics and Applications, 39(1):239–262, March 2010. URL: http://eudml.org/doc/92759.
[15] Thomas Place and Marc Zeitoun. A first taste of mescal, a tool for solving membership problems for regular languages. In Giuseppa Castiglione and Sabrina Mantaci, editors, Implementation and Application of Automata - 29th International Conference, CIAA 2025, Palermo, Italy, September 22-25, 2025, Proceedings, volume 15981 of Lecture Notes in Computer Science, pages 281–298. Springer, 2025. doi:10.1007/978-3-032-02602-6_20.
[16] M. P. Schützenberger. Une théorie algébrique du codage. Séminaire Dubreil. Algèbre et théorie des nombres, 9:1–24, 1955. URL: http://eudml.org/doc/111094.
[17] M.P. Schützenberger. On finite monoids having only trivial subgroups. Information and Control, 8(2):190–194, 1965. doi:10.1016/S0019-9958(65)90108-7.
[18] Imre Simon. Piecewise testable events. In H. Brakhage, editor, Automata Theory and Formal Languages, pages 214–222, Berlin, Heidelberg, 1975. Springer Berlin Heidelberg. doi:10.1007/3-540-07407-4_23.
[19] Gudmund Skovbjerg Frandsen, Peter Bro Miltersen, and Sven Skyum. Dynamic word problems. J. ACM, 44(2):257–271, 1997. doi:10.1145/256303.256309.
[20] Thomas Zeume. Small dynamic complexity classes. PhD thesis, Technical University Dortmund, Germany, 2015. URL: https://hdl.handle.net/2003/34163.
[21] Thomas Zeume and Thomas Schwentick. On the quantifier-free dynamic complexity of reachability. Information and Computation, 240:108–129, 2015. MFCS 2013. doi:10.1016/j.ic.2014.09.011.

[bib.bib1] [1] J. Büchi. Weak second-order arithmetic and finite automata. Mathematical Logic Quarterly, 6:66–92, 1960. doi:10.1007/978-1-4613-8928-6_22.

[bib.bib2] [2] Volker Diekert, Paul Gastin, and Manfred Kufleitner. A survey on small fragments of first-order logic over finite words. Int. J. Found. Comput. Sci., 19(3):513–548, 2008. doi:10.1142/S0129054108005802.

[bib.bib3] [3] Samuel Eilenberg. Automata, Languages and Machines, Vol. B. Academic Press Inc, 1976. URL: https://www.sciencedirect.com/bookseries/pure-and-applied-mathematics/vol/59/part/PB.

[bib.bib4] [4] Wouter Gelade, Marcel Marquardt, and Thomas Schwentick. The dynamic complexity of formal languages. ACM Trans. Comput. Logic, 13(3), 2012. doi:10.1145/2287718.2287719.

[bib.bib5] [5] J. A. Green. On the structure of semigroups. Annals of Mathematics, 54(1):163–172, 1951. URL: http://www.jstor.org/stable/1969317.

[bib.bib6] [6] William Hesse. Dynamic Computational Complexity. PhD thesis, University of Massachusetts Amherst, 2003.

[bib.bib7] [7] Kenneth Krohn and John Rhodes. Algebraic theory of machines. i. prime decomposition theorem for finite semigroups and machines. Transactions of the American Mathematical Society, 116:450–464, 1965. URL: http://www.jstor.org/stable/1994127.

[bib.bib8] [8] M. Lothaire. Combinatorics on Words. Cambridge Mathematical Library. Cambridge University Press, 2 edition, 1997.

[bib.bib9] [9] Robert McNaughton and Seymour A. Papert. Counter-Free Automata (M.I.T. research monograph no. 65). The MIT Press, 1971.

[bib.bib10] [10] Sushant Patnaik and Neil Immerman. Dyn-FO: A parallel, dynamic complexity class. J. Comput. Syst. Sci., 55(2):199–209, 1997. doi:10.1006/jcss.1997.1520.

[bib.bib11] [11] Jean-Éric Pin. A variety theorem without complementation. Russian Mathematics (Izvestija vuzov. Matematika), 39:80–90, 1995.

[bib.bib12] [12] Jean-Eric Pin. Mathematical foundations of automata theory. Lecture notes, 2014. URL: http://www.irif.fr/˜jep/PDF/MPRI/MPRI.pdf.

[bib.bib13] [13] Jean-Eric Pin and Pascal Weil. Semidirect products of ordered semigroups. Communications in Algebra, 30(1):149–169, 2002.

[bib.bib14] [14] Jean-Éric Pin and Howard Straubing. Some results on c-varieties. RAIRO - Theoretical Informatics and Applications, 39(1):239–262, March 2010. URL: http://eudml.org/doc/92759.

[bib.bib15] [15] Thomas Place and Marc Zeitoun. A first taste of mescal, a tool for solving membership problems for regular languages. In Giuseppa Castiglione and Sabrina Mantaci, editors, Implementation and Application of Automata - 29th International Conference, CIAA 2025, Palermo, Italy, September 22-25, 2025, Proceedings, volume 15981 of Lecture Notes in Computer Science, pages 281–298. Springer, 2025. doi:10.1007/978-3-032-02602-6_20.

[bib.bib16] [16] M. P. Schützenberger. Une théorie algébrique du codage. Séminaire Dubreil. Algèbre et théorie des nombres, 9:1–24, 1955. URL: http://eudml.org/doc/111094.

[bib.bib17] [17] M.P. Schützenberger. On finite monoids having only trivial subgroups. Information and Control, 8(2):190–194, 1965. doi:10.1016/S0019-9958(65)90108-7.

[bib.bib18] [18] Imre Simon. Piecewise testable events. In H. Brakhage, editor, Automata Theory and Formal Languages, pages 214–222, Berlin, Heidelberg, 1975. Springer Berlin Heidelberg. doi:10.1007/3-540-07407-4_23.

[bib.bib19] [19] Gudmund Skovbjerg Frandsen, Peter Bro Miltersen, and Sven Skyum. Dynamic word problems. J. ACM, 44(2):257–271, 1997. doi:10.1145/256303.256309.

[bib.bib20] [20] Thomas Zeume. Small dynamic complexity classes. PhD thesis, Technical University Dortmund, Germany, 2015. URL: https://hdl.handle.net/2003/34163.

[bib.bib21] [21] Thomas Zeume and Thomas Schwentick. On the quantifier-free dynamic complexity of reachability. Information and Computation, 240:108–129, 2015. MFCS 2013. doi:10.1016/j.ic.2014.09.011.

Algebraic Characterizations of Classes of Regular Languages in DynFO

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Acknowledgements:

Funding:

Related Version:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Theorem 1.

Theorem 2.

Theorem 3.

2 Preliminaries

2.1 Dynamic descriptive complexity

Example 4.

Lemma 5.

2.2 Monoids

Fact 6.

Fact 7.

3 The regular languages of UDyn𝚺𝟐

Theorem 8 (Restatement of Theorem 1).

Lemma 9.

Proof of Theorem 8.

Green’s relations.

Example 10.

Example 11.

Example 12.

Unary auxiliary relations for expressing evaluations of infixes.

Lemma 13.

Definition 14.

4 The regular languages of UDynProp

Theorem 15 (Restatement of Theorem 2).

4.1 Maintaining regular group languages with quantifier-free formulas

Lemma 16.

Proof sketch..

4.2 Lower bound for regular non-group languages

4.2.1 A regular language that is not in UDynProp

Lemma 17 (Substructure Lemma [4, Lemma 1]).

Lemma 18 (see [8, Chapter 6]).

Lemma 19 (c.f. [21, Proposition 4.8]).

Proof.

4.2.2 UDynProp cannot maintain any regular non-group language

Lemma 20.

Proof.

Lemma 21 ([3], see [12, Theorem XIII.4.10]).

Fact 22.

Proof.

5 The regular languages of UDyn𝚺𝟏+

Theorem 23 (Restatement of Theorem 3).

5.1 Ordered monoids and wreath products

Ordered monoids.

Example 24.

Definition 25.

Ordered wreath products.

▶ Remark 26.

5.2 Maintaining regular languages in 𝐉+∗𝐆 with positive 𝚺𝟏-formulas

Fact 27.

Lemma 28.

Proof sketch..

5.3 Lower bound for regular languages not in 𝐉+∗𝐆

5.3.1 A regular language that is not in UDyn𝚺𝟏+

Lemma 29 (Substructure lemma for UDynΣ1+).

Proof.

Lemma 30.

Proof.

5.3.2 UDyn𝚺𝟏+ cannot maintain any regular non-𝐉+∗𝐆 language

Theorem 31 (Pin and Weil [13, Thm 4.11]).

Lemma 32.

Proof.

Lemma 33.

Proof.

Theorem 34 (Pin [12, Theorem 4.12]).

Fact 35.

Proof.

6 Conclusion

Open question.

3 The regular languages of UDyn $\Sigma_{2}$

5 The regular languages of UDyn $\Sigma_{1}^{+}$

$\blacktriangleright$ Remark 26.

5.2 Maintaining regular languages in $\mathbf{J}^{+}\ast\mathbf{G}$ with positive $\Sigma_{1}$ -formulas

5.3 Lower bound for regular languages not in $\mathbf{J}^{+}\ast\mathbf{G}$

5.3.1 A regular language that is not in UDyn $\Sigma_{1}^{+}$

Lemma 29 (Substructure lemma for UDyn $\Sigma_{1}^{+}$ ).

5.3.2 UDyn $\Sigma_{1}^{+}$ cannot maintain any regular non- $\mathbf{J}^{+}\ast\mathbf{G}$ language