Advertisement

Languages Ordered by the Subword Order

  • Dietrich KuskeEmail author
  • Georg Zetzsche
Open Access
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11425)

Abstract

We consider a language together with the subword relation, the cover relation, and regular predicates. For such structures, we consider the extension of first-order logic by threshold- and modulo-counting quantifiers. Depending on the language, the used predicates, and the fragment of the logic, we determine four new combinations that yield decidable theories. These results extend earlier ones where only the language of all words without the cover relation and fragments of first-order logic were considered.

Keywords

Subword order First-order logic Counting quantifiers Decidable theories 

1 Introduction

The subword relation (sometimes called scattered subword relation) is a simple example of a well-quasi ordering [7]. This property allows its prominent use in the verification of infinite-state systems [4]. The subword relation can be understood as embeddability of one word into another. This embeddability relation has been considered for other classes of structures like trees, posets, semilattices, lattices, graphs etc. [8, 9, 10, 11, 14, 15, 16, 22, 23].

We are interested in logics over the subword order. Prior work on this has concentrated on first-order logic where the universe consists of all words over some alphabet. In this setting, we already have a rather precise picture about the border between decidability and undecidability: For the subword order alone, the \(\exists ^*\)-theory is decidable [17] and the \(\exists ^*\forall ^*\)-theory is undecidable [6, 12]. If we add constants to the signature, already the \(\exists ^*\)-theory becomes undecidable [6]. With regular predicates, the two-variable theory is decidable, but the three-variable theory is undecidable [12].

Thus, the decidable theories identified so far leave little room to express natural properties. First, the universe is confined to the set of all words and predicates for subsets quickly incur undecidability. Moreover, neither in the \(\exists ^*\)-, nor in the two-variable fragment of first-order logic, one can express the cover relation \(\mathbin {\sqsubset \!\!\!\!\cdot }\) (i.e., “u is a proper subword of v and there is no word properly between these two”). As another example, one cannot express threshold properties like “there are at most k subwords with a given property” in any of these two logics.

In this paper, we aim to identify decidable logics that are more expressive. To that end, we consider four additions to the expressivity of the logic:
  • Instead of all words over some alphabet, the universe is a language L.

  • We add regular predicates or constants to the structure.

  • Besides the subword order, we also consider the cover relation \(\mathbin {\sqsubset \!\!\!\!\cdot }\).

  • We add threshold and modulo counting quantifiers to the logic.

Formally, this means we consider structures of the form
$$\begin{aligned} (L,\sqsubseteq ,\mathbin {\sqsubset \!\!\!\!\cdot },(K\cap L)_{K\text { regular}},(w)_{w\in L}), \end{aligned}$$
where the universe is a language \(L\subseteq \varSigma ^*\), \(\sqsubseteq \) is the subword ordering, \(\mathbin {\sqsubset \!\!\!\!\cdot }\) is the cover relation, there is a predicate \(K\cap L\) for each regular \(K\subseteq \varSigma ^*\), and a constant symbol for each \(w\in L\). Moreover, we consider fragments of the logic \(\mathrm {C{+}MOD}\), which extends first-order logic by threshold- and modulo-counting quantifiers.

The key idea of this paper is to find decidable theories by varying the universe L and thereby either (i) simplify the structure \((L,\sqsubseteq )\) enough to obtain decidability even with the extensions above or (ii) generalize existing results that currently only apply to \(L=\varSigma ^*\). This leads to the following results.

  1. 1.

    First, we require L to be bounded. This means, we have \(L\subseteq w_1^*\cdots w_m^*\) for some words \(w_1,\ldots ,w_m\in \varSigma ^*\). Then, as soon as L is context-free, the \(\mathrm {C{+}MOD}\)-theory of the whole structure is decidable (Theorem 3.4).

     
  2. 2.

    To lift the boundedness restriction, we show that if L is regular, we still obtain decidability for the whole structure if we stay within the two-variable fragment \(\mathrm {C{+}MOD}^2\) (Corollary 4.8). This generalizes the decidability of the \(\mathrm {FO}^2\)-theory without the cover relation as shown in [12, Theorem 5.5].

     
  3. 3.

    Moreover, we consider a regular universe, but lift the two-variable requirement. To get decidability, we restrict quantifiers and available predicates: We show that for regular L, the \(\varSigma _1\)-theory of the structure \((L,\sqsubseteq )\) is decidable (Theorem 5.1). In the case \(L=\varSigma ^*\), this had been shown in [17, Prop. 2.2].

     
  4. 4.

    Finally, we place a further restriction on L, but in return obtain decidability with constants. We show that if L is regular and every letter is “frequent” in L (see Sect. 6), then the \(\varSigma _1\)-theory of the structure \((L,\sqsubseteq ,(w)_{w\in L})\) is decidable (Theorem 6.2). Note that, by [6, Theorem 3.3], this theory is undecidable if \(L=\varSigma ^*\).

     

Our first result is shown by a first-order interpretation of the structure in \((\mathbb {N},+)\). Since \(L\subseteq w_1^*\cdots w_n^*\), instead of words, one can argue about vectors \((x_1,\ldots ,x_n)\in \mathbb {N}^n\) for which \(w_1^{x_1}\cdots w_n^{x_n}\in L\). For the interpretation, we use the fact that semilinearity of context-free languages yields a Presburger formula expressing \(w_1^{x_1}\cdots w_n^{x_n}\in L\) for \((x_1,\ldots ,x_n)\in \mathbb {N}^n\). Moreover, Presburger definability of \(w_1^{x_1}\cdots w_n^{x_n}\sqsubseteq w_1^{y_1}\cdots w_n^{y_n}\) for \((x_1,\ldots ,x_n)\in \mathbb {N}^n\) and \((y_1,\ldots ,y_n)\in \mathbb {N}^n\) is a simple consequence of the subword relation being rational, which was observed in [12]. The first-order interpretation of our structure in \((\mathbb {N},+)\) then enables us to employ decidability of the \(\mathrm {C{+}MOD}\)-theory of the latter structure [1, 5, 21]. (Note that this decidability does not follow directly from Presburger’s result since in first-order logic, one cannot make statements like “the number of witnesses \(x\in \mathbb {N}\) satisfying ... is even”). A similar interpretation in \((\mathbb {N},+)\) was used in [6] for various algorithms concerning \((\varSigma ^*,\sqsubseteq ,(w)_{w\in \varSigma ^*})\) for fragments of \(\mathrm {FO}\) related to bounded languages.

Our second result extends an approach from [12] for decidability of the \(\mathrm {FO}^2\)-theory of the structure \((\varSigma ^*,\sqsubseteq ,(L)_{L\text { regular}})\). The authors of [12] provide a quantifier elimination procedure showing that every unary relation \(\mathrm {FO}^2\)-definable in this structure is regular. Our extended quantifier-elimination procedure uses the same invariant, now relying on the following two properties:
  • The class of regular languages is closed under counting images under unambiguous rational relations.

    This can be shown either directly or (as we do here) using weighted automata [20].

  • The proper subword, the cover, and the incomparability relation are unambiguous rational.

Our third result extends the decidability of the \(\varSigma _1\)-theory of \((\varSigma ^*,\sqsubseteq )\) from [17]. In [17], decidability is a consequence of the fact that every finite partial order can be embedded into \((\varSigma ^*,\sqsubseteq )\) if \(|\varSigma |\ge 2\). This certainly fails for general regular languages: \((a^*,\sqsubseteq )\) can only accomodate linear orders. However, we can distinguish two cases: If L is a bounded language, then decidability of the \(\varSigma _1\)-theory of \((L,\sqsubseteq )\) follows from our first result. If L is not bounded, then we show that again every finite partial order embeds into \((L,\sqsubseteq )\). To this end, we first extend a well-known property of unbounded regular languages, namely that there are \(x,u,v,y\in \varSigma ^*\) with \(x\{u,v\}^*y\subseteq L\) such that \(|u|=|v|\) and \(u\ne v\). We show that here, uv can be chosen so that uv is a primitive word. We then observe that for large enough n, any embedding of the word \((uv)^{n-1}\) into \((uv)^{n}\) must hit either the left-most position or the right-most position in \((uv)^{n}\). This enables us to argue that for large enough n, sending a tuple \((t_1,\ldots ,t_m)\in \{0,1\}^m\) to \(xv^{t_1}(uv)^n\cdots v^{t_m}(uv)^ny\) is in fact an embedding of \((\{0,1\}^m,\le )\) into \((L,\sqsubseteq )\), where \(\le \) denotes coordinate-wise comparison. Since any partial order with \(\le m\) elements embeds into \((\{0,1\}^m,\le )\), this completes the proof.

Regarding our fourth result, we know from [6] that decidability of the \(\varSigma _1\)-theory of \((L,\sqsubseteq ,(w)_{w\in L})\) does not hold for every regular L: Undecidability holds already for \(L=\{a,b\}^*\). Therefore, we require that every letter is frequent in L, meaning that in some automaton for L, every letter occurs in every cycle. In case L is bounded, we can again invoke our first result. If L is not bounded, we deduce from the frequency condition that for every \(w\in \varSigma ^*\), there are only finitely many words in L that do not have w as a subword. Removing those finitely many words preserves unboundedness, so that every finite partial order embeds in L above w. We then proceed to show that for such languages, any \(\varSigma _1\)-sentence is effectively equivalent to a sentence where constants are only used to express that all variables take values above a certain word w. Since every finite partial order embeds above w, this implies decidability.

The full version of this work is available as [18].

2 Preliminaries

Throughout this paper, let \(\varSigma \) be some finite alphabet. A word \(u=a_1a_2\dots a_m\) with \(a_1,a_2,\dots ,a_m\in \varSigma \) is a subword of a word \(v\in \varSigma ^*\) if there are words \(v_0,v_1,\dots ,v_m\in \varSigma ^*\) with \(v=v_0a_1v_1a_2v_2\cdots a_mv_m\). In that case, we write \(u\sqsubseteq v\); if, in addition, \(u\ne v\), then we write \(u\sqsubset v\) and call u a proper subword of v. If \(u,w\in \varSigma ^*\) such that \(u\sqsubset w\) and there is no word v with \(u\sqsubset v\sqsubset w\), then we say that w is a cover of u and write \(u\mathbin {\sqsubset \!\!\!\!\cdot }w\). This is equivalent to saying \(u\sqsubseteq w\) and \(|u|+1=|w|\) where |u| is the length of the word u. If neither u is a subword of v nor vice versa, then the words u and v are incomparable and we write \(u\parallel v\). For instance, \(aa\sqsubset babbba\), \(aa\mathbin {\sqsubset \!\!\!\!\cdot }aba\), and \(aba\parallel aabb\).

Let \(\mathcal S=(L,(R_i)_{i\in I},(w_j)_{j\in J})\) be a structure, i.e., L is a set, \(R_i\subseteq L^{n_i}\) is a relation of arity \(n_i\) (for all \(i\in I\)), and \(w_j\in L\) for all \(j\in J\). Then, formulas \(\varphi \) of the logic \(\mathrm {C{+}MOD}\) are defined by the following grammar:
$$ \varphi \,{:}{:}= (s=t)\mid R_i(s_1,\dots ,s_{n_i}) \mid \lnot \varphi \mid \varphi \vee \varphi \mid \exists x\,\varphi \mid \exists ^{\ge k}x\,\varphi \mid \exists ^{p \bmod q}x\,\varphi $$
where \(s,t,s_1,\dots ,s_{n_i}\) are variables or constants \(w_j\) with \(j\in J\), \(i\in I\), \(k\in \mathbb {N}\), and \(p,q\in \mathbb {N}\) with \(p<q\). We call \(\exists ^{\ge k}\) a threshold counting quantifier and \(\exists ^{p \bmod q}\) a modulo counting quantifier. The semantics of these quantifiers is defined as follows:
  • \(\mathcal S\models \exists ^{\ge k}x\,\alpha \) iff \(|\{w\in L\mid \mathcal S \models \alpha (w)\}|\ge k\)

  • \(\mathcal S\models \exists ^{p \bmod q}x\,\alpha \) iff \(|\{w\in L\mid \mathcal S \models \alpha (w)\}|\in p+q\mathbb {N}\)

For instance, \(\exists ^{0 \bmod 2}x\,\alpha \) expresses that the number of elements of the structure satisfying \(\alpha \) is even. Then \(\bigl (\exists ^{0 \bmod 2}x\,\alpha \bigr )\vee \bigl (\exists ^{1 \bmod 2}x\,\alpha \bigr )\) holds iff only finitely many elements of the structure satisfy \(\alpha \). The fragment \(\mathrm {FO{+}MOD}\) of \(\mathrm {C{+}MOD}\) comprises all formulas not containing any threshold counting quantifier. First-order logic \(\mathrm {FO}\) is the set of formulas from \(\mathrm {C{+}MOD}\) not mentioning any counting quantifier. Let \(\varSigma _1\) denote the set of first-order formulas of the form \(\exists x_1\,\exists x_2\dots \exists x_n:\psi \) where \(\psi \) is quantifier-free; these formulas are also called existential.

The threshold quantifier \(\exists ^{\ge k}\) can be expressed using the existential quantifier, only. Consequently, the logics \(\mathrm {FO{+}MOD}\) and \(\mathrm {C{+}MOD}\) are equally expressive. The situation changes when we restrict the number of variables that can be used in a formula: Let \(\mathrm {FO{+}MOD}^2\) and \(\mathrm {C{+}MOD}^2\) denote the set of formulas from \(\mathrm {FO{+}MOD}\) and \(\mathrm {C{+}MOD}\), respectively, that use the variables x and y, only. Then, the existence of \({\ge }3\) elements in the structure is expressible in \(\mathrm {C{+}MOD}^2\), but not in \(\mathrm {FO{+}MOD}^2\).

In this paper, we will consider the following structures:
  • The largest one is \((L,\sqsubseteq ,\mathbin {\sqsubset \!\!\!\!\cdot },(K\cap L)_{K\text { regular}},(w)_{w\in L})\) for some \(L\subseteq \varSigma ^*\). The universe of this structure is the language L, we have two binary predicates (\(\sqsubseteq \) and \(\mathbin {\sqsubset \!\!\!\!\cdot }\)), a unary predicate \(K\cap L\) for every regular language K, and we can use every word from L as a constant.

  • The other extreme is the structure \((L,\sqsubseteq )\) for some \(L\subseteq \varSigma ^*\) where we consider only the binary predicate \(\sqsubseteq \).

  • Finally, we will also prove results on the intermediate structure \((L,\sqsubseteq ,(w)_{w\in L})\) that has a binary relation and any word from the language as a constant.

For any structure \(\mathcal {S}\) and any of the logics \(\mathcal L\), the \(\mathcal L\)-theory of \(\mathcal {S}\) is the set of sentences from \(\mathcal L\) that hold in \(\mathcal {S}\).

A non-deterministic finite automaton is called non-degenerate if every state lies on a path from an initial to a final state. A language \(L\subseteq \varSigma ^*\) is bounded if there are a number \(n\in \mathbb {N}\) and words \(w_1,w_2,\dots ,w_n\in \varSigma ^*\) such that \(L\subseteq w_1^*\,w_2^*\cdots w_n^*\). Otherwise, it is unbounded.

For a monoid M, a subset \(S\subseteq M\) is called rational if it is a homomorphic image of a regular language. In other words, there exists an alphabet \(\varDelta \), a regular \(R\subseteq \varDelta ^*\), and a homomorphism \(h:\varDelta ^*\rightarrow M\) with \(S=h(R)\). In particular, if \(\varSigma _1,\varSigma _2\) are alphabets and \(M=\varSigma _1^*\times \varSigma _2^*\), then a subset \(S\subseteq \varSigma _1^*\times \varSigma _2^*\) is rational iff there is an alphabet \(\varDelta \), a regular \(R\subseteq \varDelta ^*\), and homomorphisms \(h_i:\varDelta ^*\rightarrow \varSigma _i^*\) with \(S=\{(h_1(w),h_2(w))\mid w\in R\}\). This fact is known as Nivat’s theorem [2].

For an alphabet \(\varGamma \), a word \(w\in \varGamma ^*\), and a letter \(a\in \varGamma \), let \(|w|_a\) denote the number of occurrences of the letter a in the word w. The Parikh vector of w is the tuple \(\varPsi _\varGamma (w)=(|w|_a)_{a\in \varGamma }\in \mathbb {N}^\varGamma \). Note that \(\varPsi _\varGamma \) is a homomorphism from the free monoid \(\varGamma ^*\) onto the additive monoid \((\mathbb {N}^\varGamma ,+)\).

3 The \(\mathrm {FO{+}MOD}\)-Theory with Regular Predicates

The aim of this section is to prove that the full \(\mathrm {FO{+}MOD}\)-theory of the structure
$$ (L,\sqsubseteq ,\mathbin {\sqsubset \!\!\!\!\cdot },(K\cap L)_{K\,\text { regular}},(w)_{w\in L}) $$
is decidable for L bounded and context-free. This is achieved by interpreting this structure in \((\mathbb {N},+)\), i.e., in Presburger arithmetic whose \(\mathrm {FO{+}MOD}\)-theory is known to be decidable [1, 5, 21]. We start with three preparatory lemmas.

Lemma 3.1

Let \(K\subseteq \varSigma ^*\) be context-free, \(w_1,\dots ,w_n\in \varSigma ^*\), and \(g:\mathbb {N}^n\rightarrow \varSigma ^*\) be defined by \(g(\overline{m})=w_1^{m_1}\,w_2^{m_2}\cdots w_n^{m_n}\) for all \(\overline{m}=(m_1,m_2,\dots ,m_n)\in \mathbb {N}^n\). The set \(g^{-1}(K)=\{\overline{m}\in \mathbb {N}^n\mid g(\overline{m})\in K\}\) is effectively semilinear.

Proof

Let \(\varGamma =\{a_1,a_2,\dots ,a_n\}\) be an alphabet and define the monoid homomorphism \(f:\varGamma ^*\rightarrow \varSigma ^*\) by \(f(a_i)=w_i\) for all \(i\in [1,n]\).

Since the class of context-free languages is effectively closed under inverse homomorphisms and under intersections with regular languages, the language
$$ L=f^{-1}(K)\cap a_1^*a_2^*\cdots a_n^*=\{u\in a_1^*a_2^*\cdots a_n^*\mid f(u)\in K\} $$
is effectively context-free. Its Parikh image \(\varPsi _\varGamma (L)\subseteq \mathbb {N}^n\) is effectively semilinear [19]. Moreover, \(\varPsi _\varGamma (L)\) equals the set \(g^{-1}(K)\) from the lemma.    \(\square \)

Lemma 3.2

Let \(w_1,\dots ,w_n\in \varSigma ^*\) and \(g:\mathbb {N}^n\rightarrow \varSigma ^*\) be defined by \(g(\overline{m})=w_1^{m_1}\,w_2^{m_2}\cdots w_n^{m_n}\) for all \(\overline{m}=(m_1,m_2,\dots ,m_n)\in \mathbb {N}^n\). The set \(\{(\overline{m},\overline{n})\in \mathbb {N}^n\times \mathbb {N}^n\mid g(\overline{m})\sqsubseteq g(\overline{n})\}\) is semilinear.

Proof

Let \(\varGamma =\{a_1,a_2,\dots ,a_n\}\) be an alphabet and define the monoid homomorphism \(f:\varGamma ^*\rightarrow \varSigma ^*\) by \(f(a_i)=w_i\) for all \(i\in [1,n]\). One first shows that
$$ S_2=\{(u,v)\mid u,v\in a_1^*a_2^*\dots a_n^*,~f(v)\sqsubseteq f(v)\} $$
is rational. We now employ Nivat’s theorem. It tells us that there are a regular language R over some alphabet \(\varDelta \) and two homomorphisms \(h_1,h_2:\varDelta ^*\rightarrow \varGamma ^*\) so that we can write \( S_2=\{\bigl (h_1(w),h_2(w)\bigr )\mid w\in R\}. \) Since R is regular, its Parikh-image \(\varPsi _\varDelta (R)=\{\varPsi _\varDelta (w)\mid w\in R\}\) is semilinear [19]. There are monoid homomorphisms \(p_1,p_2:\mathbb {N}^\varDelta \rightarrow \mathbb {N}^n\) with \(\varPsi _\varGamma (h_i(w))=p_i(\varPsi _\varDelta (w))\) for all \(i\in \{1,2\}\) and \(w\in \varDelta ^*\). With these, the image \( H=\{\bigl (p_1(\varPsi _\varDelta (w)),p_2(\varPsi _\varDelta (w))\bigr )\mid w\in R\} \) of the set \(\varPsi _\varDelta (R)\) under the monoid homomorphism \((p_1,p_2):\mathbb {N}^\varDelta \rightarrow \mathbb {N}^n\times \mathbb {N}^n\) is semilinear. It turns out that this set equals the set from the lemma.    \(\square \)

Lemma 3.3

Let \(w_1,w_2,\dots ,w_n\in \varSigma ^*\), \(L\subseteq w_1^*w_2^*\cdots w_n^*\) be context-free, and \(g:\mathbb {N}^n\rightarrow \varSigma ^*\) be defined by \(g(\overline{m})=w_1^{m_1}w_2^{m_2}\cdots w_n^{m_n}\) for every tuple \(\overline{m}=(m_1,m_2,\dots ,m_n)\in \mathbb {N}^n\). Then there exists a semilinear set \(U\subseteq \mathbb {N}^n\) such that g maps U bijectively onto L.

Proof

The set U contains, for each \(u\in L\), the lexicographically minimal tuple \(\overline{m}\in \mathbb {N}^n\) with \(g(\overline{m})=u\). Then, Lemmas 3.1 and 3.2 and the closure of the class of semilinear sets under first-order definitions imply the required properties.    \(\square \)

Now we can prove the main result of this section.

Theorem 3.4

Let \(L\subseteq \varSigma ^*\) be context-free and bounded. Then the \(\mathrm {FO{+}MOD}\)-theory of \((L,\sqsubseteq ,\mathbin {\sqsubset \!\!\!\!\cdot },(K\cap L)_{K\text { regular}},(w)_{w\in L})\) is decidable.

Proof

It suffices to prove the decidability for the structure \(\mathcal {S}=(L,\sqsubseteq ,(K\cap L)_{K\text { regular}})\) since the theory of the structure from the theorem can be reduced to that of \(\mathcal {S}\) (\(x\mathbin {\sqsubset \!\!\!\!\cdot }y\) gets replaced by its definition and \(x\theta w\) by \(\exists y:y\in \{w\}\wedge x\theta y\) where \(\theta \) is any binary relation symbol).

Since L is bounded, there are words \(w_1,w_2,\dots ,w_n\in \varSigma ^*\) such that L is included in \(w_1^*\,w_2^*\cdots w_n^*\). For an n-tuple \(\overline{m}=(m_1,m_2,\dots ,m_n)\in \mathbb {N}^n\) we define \(g(\overline{m})= w_1^{m_1}w_2^{m_2}\cdots w_n^{m_n}\in \varSigma ^*\).

  1. 1.

    By Lemma 3.3, there is a semilinear set \(U\subseteq \mathbb {N}^n\) that is mapped by g bijectively onto L.

     
  2. 2.

    The set \(\{(\overline{m},\overline{n})\mid g(\overline{m})\sqsubseteq g(\overline{n})\}\) is semilinear by Lemma 3.2.

     
  3. 3.

    For any regular language \(K\subseteq \varSigma ^*\) the set \(\{\overline{m}\in \mathbb {N}^n\mid g(\overline{m})\in K\}\subseteq \mathbb {N}^n\) is effectively semilinear by Lemma 3.1.

     
From these semilinear sets, we obtain first-order formulas \(\lambda (\overline{x})\), \(\sigma (\overline{x},\overline{y})\), and \(\kappa _K(\overline{x})\) in the language of \((\mathbb {N},+)\) such that, for any \(\overline{m},\overline{n}\in \mathbb {N}^n\), we have
  1. 1.

    \((\mathbb {N},+)\models \lambda (\overline{m})\iff \overline{m}\in U\),

     
  2. 2.

    \((\mathbb {N},+)\models \sigma (\overline{m},\overline{n})\iff g(\overline{m})\sqsubseteq g(\overline{n})\), and

     
  3. 3.

    \((\mathbb {N},+)\models \kappa _K(\overline{m})\iff g(\overline{m})\in K\).

     
One then defines, from an \(\mathrm {FO{+}MOD}\)-formula \(\varphi (x_1,\dots ,x_k)\) in the language of \(\mathcal {S}\), an \(\mathrm {FO{+}MOD}\)-formula \(\varphi '(\overline{x_1},\dots ,\overline{x_k})\) in the language of \((\mathbb {N},+)\) such that
$$ (\mathbb {N},+)\models \varphi '(\overline{m_1},\dots ,\overline{m_k}) \iff \mathcal {S}\models \varphi (g(\overline{m_1}),\dots ,g(\overline{m_k})). $$
(This construction can be found in the full version [18] and increases the formula size at least exponentially.)

Consequently, any sentence \(\varphi \) from \(\mathrm {FO{+}MOD}\) in the language of \(\mathcal {S}\) is translated into an equivalent sentence \(\varphi '\) in the language of \((\mathbb {N},+)\). By [1, 5, 21], validity of the sentence \(\varphi '\) in \((\mathbb {N},+)\) is decidable.    \(\square \)

4 The \(\mathrm {C{+}MOD}\) \(^2\)-Theory with Regular Predicates

It is the aim of this section to show that the \(\mathrm {C{+}MOD}^2\)-theory of the structure \((L,\sqsubseteq ,\mathbin {\sqsubset \!\!\!\!\cdot },(K\cap L)_{K\text { regular}},(w)_{w\in L})\) is decidable for any regular language L. To this aim, we first show that the \(\mathrm {C{+}MOD}^2\)-theory of
$$ \mathcal {S}=(\varSigma ^*,\sqsubseteq ,\mathbin {\sqsubset \!\!\!\!\cdot },(L)_{L\text { regular}}) $$
is decidable. This decidability proof extends the proof from [12] for the decidability of the \(\mathrm {FO}^2\)-theory of \((\varSigma ^*,\sqsubseteq ,(L)_{L\text { regular}})\). It provides a quantifier-elimination procedure (see Sect. 4.3) that relies on the following two properties:
  1. 1.

    The class of regular languages is closed under counting images under unambiguous rational relations (Sect. 4.2) and

     
  2. 2.

    the proper subword, the cover, and the incomparability relation are unambiguous rational (Sect. 4.1).

     

4.1 Unambiguous Rational Relations

Recall that, by Nivat’s theorem, a relation \(R\subseteq \varSigma ^*\times \varSigma ^*\) is rational if there exist an alphabet \(\varGamma \), a homomorphism \(h:\varGamma ^*\rightarrow \varSigma ^*\times \varSigma ^*\), and a regular language \(S\subseteq \varGamma ^*\) such that h maps S surjectively onto R. We call R an unambiguous rational relation if, in addition, h maps S injectively (and therefore bijectively) onto R. Note that these are precisely the relations accepted by unambiguous 2-tape-automata.

While the class of rational relations is closed under unions, this is not the case for unambiguous rational relations (e.g., \(R=\{(a^mba^n,a^m)\mid m,n\in \mathbb {N}\}\cup \{(a^mba^n,a^n)\mid m,n\in \mathbb {N}\}\) is the union of unambiguous rational relations but not unambiguous). But it is closed under disjoint unions.

Lemma 4.1

For any alphabet \(\varSigma \), the cover relation \(\mathbin {\sqsubset \!\!\!\!\cdot }\) and the relation \(\sqsubset \setminus \mathbin {\sqsubset \!\!\!\!\cdot }\) are unambiguous rational.

Proof

For \(i\in \{1,2\}\), let \(\varSigma _i=\varSigma \times \{i\}\) and \(\varGamma =\varSigma _1\cup \varSigma _2\). Furthermore, let the homomorphism \(\mathrm {proj}_i:\varGamma ^*\rightarrow \varSigma ^*\) be defined by \(\mathrm {proj}_i(a,i)=a\) and \(\mathrm {proj}_i(a,3-i)=\varepsilon \) for all \(a\in \varSigma \). Finally, let the homomorphism \(\mathrm {proj}:\varGamma ^*\rightarrow \varSigma ^*\times \varSigma ^*\) be defined by \(\mathrm {proj}(w)=(\mathrm {proj}_1(w),\mathrm {proj}_2(w))\).

  • The regular language
    $$ \mathrm {Sub}= \left( \bigcup _{a\in \varSigma }\Bigl (\bigl (\varSigma _2\setminus \{(a,2)\}\bigr )^*\, (a,2)\,(a,1)\Bigr )\right) ^* {\varSigma _2}^*. $$
    is mapped bijectively onto the subword relation.
  • Let S be the regular language of words from \(\mathrm {Sub}\) with precisely one more occurrence of letters from \(\varSigma _2\) than from \(\varSigma _1\). Then S is mapped bijectively onto the relation \(\mathbin {\sqsubset \!\!\!\!\cdot }\), hence this relation is unambiguous rational.

  • Similarly, let \(S'\) denote the regular language of all words from \(\mathrm {Sub}\) with at least two more occurrences of letters from \(\varSigma _2\) than from \(\varSigma _1\). It is mapped bijectively onto the relation \(\sqsubset \setminus \mathbin {\sqsubset \!\!\!\!\cdot }\), i.e., \(\sqsubset \setminus \mathbin {\sqsubset \!\!\!\!\cdot }\) is unambiguous rational.    \(\square \)

Lemma 4.2

For any alphabet \(\varSigma \), the incomparability relation
$$ \mathbin {\parallel }=\{(u,v)\in \varSigma ^*\times \varSigma ^*\mid \text {neither }u\sqsubseteq v\text { nor }v\sqsubseteq u\} $$
is unambiguous rational.

Proof

We will show that the following three relations are unambiguous rational:
The result follows since \(\parallel \) is the disjoint union of these relations. Let \(\varSigma _i\), \(\varGamma \), \(\mathrm {proj}_i\), and \(\mathrm {proj}\) be defined as in the previous proof. First, the regular language
$$ \mathrm {Inc}_2=(\varSigma _2\varSigma _1)^*\cdot \{(a,2)(b,1)\mid a,b\in \varSigma , a\ne b\} \cdot (\varSigma _2\varSigma _1)^*. $$
is mapped by \(\mathrm {proj}\) bijectively onto \(R_2\).
From [12, Lemma 5.2], we learn that \((u,v)\in R_1\cup R_2\) if, and only if,
  • \(u=a_1a_2\dots a_\ell u'\) for some \(\ell \ge 1\), \(a_1,\dots ,a_\ell \in \varSigma \), \(u'\in \varSigma ^*\), and

  • \(v\in (\varSigma \setminus \{a_1\})^*a_1\,(\varSigma \setminus \{a_2\})^*a_2\cdots (\varSigma \setminus \{a_{\ell -1}\})^*a_{\ell -1}\, (\varSigma \setminus \{a_\ell \})^+ v'\) for some word \(v'\in \varSigma ^*\) with \(|u'|=|v'|\).

Consequently, \(\mathrm {proj}\) maps the following language bijectively onto \(R_1\cup R_2\):
$$ \mathrm {Inc}_{1,2}= \left( \bigcup _{a\in \varSigma } \Bigl ( \bigl (\varSigma _2\setminus \{(a,2)\}\bigr )^*(a,2)(a,1) \Bigr ) \right) ^* \cdot \bigcup _{a\in \varSigma } \Bigl (\bigl (\varSigma _2\setminus \{(a,2)\}\bigr )^+(a,1)\Bigr ) \cdot \left( \varSigma _2\varSigma _1\right) ^* $$
and since \(\mathrm {Inc}_2\subseteq \mathrm {Inc}_{1,2}\), \(\mathrm {proj}\) maps \(\mathrm {Inc}_1=\mathrm {Inc}_{1,2}\setminus \mathrm {Inc}_2\) bijectively onto \(R_1\). The claim regarding \(R_3\) follows analogously.    \(\square \)

4.2 Closure Properties of the Class of Regular Languages

Let \(R\subseteq \varSigma ^*\times \varSigma ^*\) be an unambiguous rational relation and \(L\subseteq \varSigma ^*\) a regular language. We want to show that the languages of all words \(u\in \varSigma ^*\)
$$\begin{aligned}&\text { with }|\{v\in L\mid (u,v)\in R\}|\ge k\end{aligned}$$
(1)
$$\begin{aligned}&(\text {with }|\{v\in L\mid (u,v)\in R\}|\in p+q\mathbb {N}\text {, respectively}) \end{aligned}$$
(2)
are effectively regular for all \(k\in \mathbb {N}\) and all \(0\le p<q\), respectively (this does not hold for arbitrary rational relations). It is straightforward to work out direct automata constructions for this. However, the full details of this are somewhat cumbersome. Instead, we provide a proof via weighted automata, which enables us to split the two constructions into several simple steps.

Let S be a semiring. A function \(r:\varSigma ^*\rightarrow S\) is realizable over S if there are \(n\in \mathbb {N}\), \(\lambda \in S^{1\times n}\), a homomorphism \(\mu :\varSigma ^*\rightarrow S^{n\times n}\), and \(\nu \in S^{n\times 1}\) with \(r(w)=\lambda \cdot \mu (w)\cdot \nu \) for all \(w\in \varSigma ^*\). The triple \((\lambda ,\mu ,\nu )\) is a presentation of dimension n or a weighted automaton for r.

In the following, we consider the semiring \(\mathbb {N}^\infty \), i.e., the set \(\mathbb {N}\cup \{\infty \}\) together with the commutative operations \(+\) and \(\cdot \) (with \(x+\infty =\infty \) for all \(x\in \mathbb {N}\cup \{\infty \}\), \(x\cdot \infty =\infty \) for all \(x\in (\mathbb {N}\cup \{\infty \})\setminus \{0\}\), and \(0\cdot \infty =0\)). Sometimes, we will argue about sums of infinitely many elements from \(\mathbb {N}^\infty \), which are defined as expected.

Proposition 4.3

Let \(\varGamma \) and \(\varSigma \) be alphabets, \(f:\varGamma ^*\rightarrow \varSigma ^*\) a homomorphism, and \(\chi :\varGamma ^*\rightarrow \mathbb {N}^\infty \) a realizable function over \(\mathbb {N}^\infty \). Then the following function r is effectively realizable over \(\mathbb {N}^\infty \):
$$ r=\chi \circ f^{-1}:\varSigma ^*\rightarrow \mathbb {N}^\infty :u\mapsto \sum _{\begin{array}{c} w\in \varGamma ^*\\ f(w)=u \end{array}}\chi (w) $$

Proof

The homomorphism f can be written as \(f=f_2\circ f_1\) where \(f_1:\varGamma ^*\rightarrow \varGamma ^*\) is non-expanding (i.e., \(f_1(a)\in \varGamma \cup \{\varepsilon \}\) for all \(a\in \varGamma \)) and \(f_2:\varGamma ^*\rightarrow \varSigma ^*\) is non-erasing (i.e., \(f_2(a)\in \varSigma ^+\) for all \(a\in \varGamma \)). Then \(r=(\chi \circ f_1^{-1})\circ f_2^{-1}\). Then \(\chi '=\chi \circ f_1^{-1}\) is effectively realizable by [3, Lemma 2.2(b)].

Let \((\lambda ,\mu ,\nu )\) be a presentation of dimension n for \(\chi '\). For \(\sigma \in \varSigma \cup \{\varepsilon \}\), set \(\varGamma _\sigma =\{b\in \varGamma \mid f_2(b)=\sigma \}\). Furthermore, define the matrix \(M\in (\mathbb {N}^\infty )^{n\times n}\) by
$$ M_{ij}= {\left\{ \begin{array}{ll} \infty &{} \text {if there is }w\in \varGamma _\varepsilon ^*\text { with }n<|w|\le 2n\text { and }\mu (w)_{ij}>0\\ \sum _{w\in \varGamma _\varepsilon ^{\le n}}\mu (w)_{ij} &{}\text {otherwise.} \end{array}\right. } $$
Then \(M_{ij}=\sum _{w\in \varGamma _\varepsilon ^*}\mu (w)_{ij}\) for all \(i,j\in [1,n]\). Setting \(\lambda ' =\lambda \cdot M\) and
$$ \mu '(a) =\sum _{b\in \varGamma _a} \bigl (\mu (b)\cdot M\bigr ) \text { for all }a\in \varSigma $$
defines the presentation \((\lambda ',\mu ',\nu )\) for the function \(r=\chi '\circ f_2^{-1}\).    \(\square \)

Lemma 4.4

Let \(R\subseteq \varSigma ^*\times \varSigma ^*\) be an unambiguous rational relation and \(L\subseteq \varSigma ^*\) be regular. Then the following function r is effectively realizable over \(\mathbb {N}^\infty \):
$$ r:\varSigma ^*\rightarrow \mathbb {N}^\infty :u\mapsto |\{v\in L\mid (u,v)\in R\}| $$

Proof

Since R is unambiguous rational, so is \(R\cap (\varSigma ^*\times L)\), i.e., there are an alphabet \(\varGamma \), homomorphisms \(f,g:\varGamma ^*\rightarrow \varSigma ^*\), and a regular language \(S_L\subseteq \varGamma ^*\) such that
$$ (f,g):\varGamma ^*\rightarrow \varSigma ^*\times \varSigma ^* :w\mapsto \bigl (f(w),g(w)\bigr ) $$
maps \(S_L\) bijectively onto \(R\cap (\varSigma ^*\times L)\). Since \(S_L\) is regular, its characteristic function \(\chi \) is effectively realizable by [20, Prop. 3.12]. One then shows that r is the function \(\chi \circ f^{-1}\) as in Proposition 4.3.    \(\square \)

We now come to the main result of this section.

Proposition 4.5

Let \(R\subseteq \varSigma ^*\times \varSigma ^*\) be an unambiguous rational relation and \(L\subseteq \varSigma ^*\) be regular. Then, for \(k\in \mathbb {N}\) and for \(p,q\in \mathbb {N}\) with \(p<q\), the set H of words w satisfying (1) and (2), respectively, is effectively regular.

Let R denote the rational relation mentioned before Lemma 4.1. Then a word \(a^mba^n\) has \({\ge }2\)R-partners” iff it has an even number of “R-partners” iff \(m\ne n\). Hence, the above proposition does not hold for arbitrary rational relations.

Proof

Let r be the function from Lemma 4.4. Setting \(x\equiv y\) iff \(x=y\) or \(k\le x,y<\infty \) defines a congruence \(\equiv \) on \(\mathbb {N}^\infty \). Then \(S_k^\infty =\mathbb {N}^\infty /\mathord {\equiv }\) is a finite semiring and the function \(s:\varSigma ^*\rightarrow S_k^\infty :u\mapsto [r(u)]\) is effectively realizable. Since the semiring \(S_k^\infty \) is finite, the “level sets” \(s^{-1}([i])=\{u\in \varSigma ^*\mid s(u)\equiv i\}\) are effectively regular by [20, Prop. 4.5]. Since \(s^{-1}([k])\!\cup \! s^{-1}([\infty ])\) is the language of words u satisfying (1), the first result follows.

For the second language, we consider the congruence \(\mathord {\equiv }\subseteq \mathbb {N}^\infty \times \mathbb {N}^\infty \) with \(x\equiv y\) iff \(x=y\) or \(q\le x,y<\infty \) and \(x-y\in q\mathbb {N}\).    \(\square \)

4.3 Quantifier Elimination for \(\mathrm {C{+}MOD}^2\)

Our decision algorithm employs a quantifier alternation procedure, i.e., we will transform an arbitrary formula into an equivalent one that is quantifier-free. As usual, the heart of this procedure handles formulas \(\psi =\mathrm {Q}y\,\varphi \) where \(\mathrm {Q}\) is a quantifier and \(\varphi \) is quantifier-free. Since the logic \(\mathrm {C{+}MOD}^2\) has only two variables, any such formula \(\psi \) has at most one free variable. In other words, it defines a language K. The following lemma shows that this language is effectively regular, such that \(\psi \) is equivalent to the quantifier-free formula \(x\in K\).

Lemma 4.6

Let \(\varphi (x,y)\) be a quantifier-free formula from \(\mathrm {C{+}MOD}^2\) in the language of the structure \(\mathcal {S}=(\varSigma ^*,\sqsubseteq ,\mathbin {\sqsubset \!\!\!\!\cdot },(L)_{L\text { regular}})\). Then the sets
$$ \{x\in \varSigma ^*\mid \mathcal {S}\models \exists ^{\ge k}y\,\varphi \}\text { and } \{x\in \varSigma ^*\mid \mathcal {S}\models \exists ^{p \bmod q}y\,\varphi \} $$
are effectively regular for all \(k\in \mathbb {N}\) and all \(p,q\in \mathbb {N}\) with \(p<q\).

Proof

Since \(\varphi \) is quantifier-free, we can rewrite it into a Boolean combination of formulas of the form \(x\in K\) and \(y\in L\) for some regular languages K and L, \(x\sqsubseteq y\) and \(y\sqsubseteq x\), and \(x\mathbin {\sqsubset \!\!\!\!\cdot }y\) and \(y\mathbin {\sqsubset \!\!\!\!\cdot }x\).

There are six possible relations between the two variables x and y in the partial order: we can have \(x=y\), \(x\mathbin {\sqsubset \!\!\!\!\cdot }y\) or vice versa, \(x\sqsubset y\wedge \lnot x\mathbin {\sqsubset \!\!\!\!\cdot }y\) or vice versa, or \(x\parallel y\). Let \(\theta _i(x,y)\) for \(1\le i\le 6\) be formulas describing these relations.

Hence \(\varphi \) is equivalent to \(\bigvee _{1\le i\le 6}\bigl (\theta _i\wedge \varphi )\). In this formula, any occurrence of \(\varphi \) appears in conjunction with precisely one of the formulas \(\theta _i\). Depending on this formula \(\theta _i\) (i.e., the relation between x and y), we can simplify \(\varphi \) to \(\varphi _i\) by replacing the atomic subformulas that compare x and y by true or false. As a result, the formula \(\varphi \) is equivalent to \(\bigvee _{1\le i\le 6}\bigl (\theta _i\wedge \varphi _i)\) where the formulas \(\varphi _i\) are Boolean combinations of formulas of the form \(x\in K\) and \(y\in L\) for some regular languages K and L.

Now let \(k\in \mathbb {N}\). Since the formulas \(\theta _i\) are mutually exclusive, we get
$$ \exists ^{\ge k}y\,\varphi \equiv \exists ^{\ge k}y\,\bigvee _{1\le i\le 6}(\theta _i\wedge \varphi _i) \equiv \bigvee _{(*)} \bigwedge _{1\le i\le 6} \exists ^{\ge k_i}y\,(\theta _i\wedge \varphi _i) $$
where the disjunction \((*)\) extends over all \((k_1,\dots ,k_6)\in \mathbb {N}^6\) with \(\sum _{1\le i\le 6}k_i=k\).
Hence it suffices to show that
$$\begin{aligned} \{x\in \varSigma ^*\mid \exists ^{\ge k}y\,(\theta _i \wedge \varphi )\} \end{aligned}$$
(3)
is effectively regular for all \(1\le i\le 6\), all \(k\in \mathbb {N}\), and all Boolean combinations \(\varphi \) of formulas of the form \(x\in K\) and \(y\in L\) where K and L are regular languages. We can find regular languages \(K_M\) and \(L_M\) and a finite set I such that \(\varphi \) is equivalent to \( \bigvee _{M\in I} \left( x\in K_M \wedge y\in L_M \right) \) and such that this disjunction is exclusive. Hence the set from (3) equals the union of the sets
$$ \{x\in \varSigma ^*\mid \exists ^{\ge k}y\,(\theta _i \wedge x\in K_M\wedge y\in L_M)\} =K_M\cap \underbrace{\{x\in \varSigma ^*\mid \exists ^{\ge k}y\in L_M:\theta _i\}}_{H_M} $$
for \(M\in I\). The set \(H_M\) is effectively regular by Proposition 4.5 and Lemmas 4.1 and 4.2. Since the language in the claim of the lemma is a Boolean combination of such sets, the first claim is demonstrated; the second follows similarly.    \(\square \)

The only atomic formulas with a single variable x are \(x\in L\) with L regular, \(x=x\), \(x\sqsubseteq x\) (which are equivalent to \(x\in \varSigma ^*\)), and \(x\mathbin {\sqsubset \!\!\!\!\cdot }x\) (which is equivalent to \(x\in \emptyset \)). Hence, any quantifier-free formula with a single free variable x is a Boolean combination of statements of the form \(x\in L\). Lemma 4.6 thus implies:

Theorem 4.7

Let \(\mathcal {S}=(\varSigma ^*,\sqsubseteq ,\mathbin {\sqsubset \!\!\!\!\cdot },(L)_{L\text { regular}})\). Let \(\varphi (x)\) be a formula from \(\mathrm {C{+}MOD}^2\). Then the set \(\{x\in \varSigma ^*\mid \mathcal {S}\models \varphi \}\) is effectively regular.

Corollary 4.8

Let \(L\subseteq \varSigma ^*\) be a regular language. Then the \(\mathrm {C{+}MOD}^2\)-theory of the structure \(\mathcal {S}_L=(L,\sqsubseteq ,\mathbin {\sqsubset \!\!\!\!\cdot },(K\cap L)_{K\text { regular}},(w)_{w\in L})\) is decidable.

Proof

Let \(\varphi \in \mathrm {C{+}MOD}^2\) be a sentence. We build \(\varphi _L\) by (1) restricting all quantifications to L, (2) replace \(x\theta w\) by \(\exists y:y\in \{w\}\wedge x\theta y\), and dually for \(y\theta w\) for all \(w\in L\) and all binary relations \(\theta \).

With \(\mathcal {S}\) the structure from Theorem 4.7, we obtain \(\mathcal {S}\models \varphi _L\iff \mathcal {S}_L\models \varphi \). By Theorem 4.7, the language \(\{x\mid \mathcal {S}\models \varphi _L\}\) is regular (since \(\varphi _L\) is a sentence, it is \(\emptyset \) or \(\varSigma ^*\)). Hence \(\varphi _L\) holds iff this set is nonempty, which is decidable.    \(\square \)

5 The \(\varSigma _1\)-Theory

In this section, we study for which regular languages L the \(\varSigma _1\)-theory of the structure \((L,\sqsubseteq )\) is decidable. If L is bounded, then decidability follows from Theorem 3.4. In the case of \((\varSigma ^*,\sqsubseteq )\), decidability is known as well [17]. Here, we prove decidability for every regular language L. Note that in terms of quantifier block alternation, this is optimal: The \(\varSigma _2\)-theory is undecidable already in the simple case of \((\{a,b\}^*,\sqsubseteq )\) [6].

Theorem 5.1

For every regular \(L\subseteq \varSigma ^*\), the \(\varSigma _1\)-theory of \((L,\sqsubseteq )\) is decidable.

Observe that very generally, the \(\varSigma _1\)-theory of a partially ordered set \((P,\le )\) is decidable if every finite partial order embeds into \((P,\le )\): In that case, a formula with n variables is satisfied in \((P,\le )\) if and only if it is satisfied for some finite partial order with at most n elements. This is used to obtain decidability for the case \(L=\varSigma ^*\) with \(|\varSigma |\ge 2\) in [17].

As mentioned above, if L is bounded, decidability follows from Theorem 3.4. If L is unbounded, it is well-known that there is a subset \(x\{p,q\}^*y\subseteq L\) such that \(|p|=|q|\) and \(p\ne q\) (see Lemma 5.2). Since in that case, the monoids \((\{a,b\}^*,\cdot )\) and \((\{p,q\}^*,\cdot )\) are isomorphic, it is tempting to assume that \((\{a,b\}^*,\sqsubseteq )\) embeds into \((\{p,q\}^*,\sqsubseteq )\) and thus into \((x\{p,q\}^*y,\sqsubseteq )\). However, that is not the case. If \(L=\{ab,ba\}^*\), then the downward closure of any infinite subset of L includes all of L. Since, on the other hand, \((\{a,b\}^*,\sqsubseteq )\) has infinite downward closed strict subsets such as \(a^*\), it cannot embed into \((L,\sqsubseteq )\). Nevertheless, the rest of this section demonstrates that every finite partial order embeds into \((L,\sqsubseteq )\) whenever L is an unbounded regular language. By the previous paragraph, this implies Theorem 5.1.

We recall a well-known property of unbounded regular languages.

Lemma 5.2

If \(L\subseteq \varSigma ^*\) is not bounded, then there are \(x,y,p,q\in \varSigma ^*\) such that \(|p|=|q|\), \(p\ne q\), and \(x\{p,q\}^*y\subseteq L\).

Proof

Let A be any non-degenerate deterministic finite automaton accepting L. Then at least one strongly connected component of A is not a cycle since otherwise, L would be bounded. Hence, there is a state s and prefix-incomparable words u, v, each of which is read on a cycle starting in s. Since u and v are prefix-incomparable, the words \(p=uv\) and \(q=vu\) are distinct, but equally long. Since A is non-degenerate, there are words \(x,y\in \varSigma ^*\) with \(x\{p,q\}^*y\subseteq L\).    \(\square \)

To have some control over how words can embed, we prove a stronger version of Lemma 5.2. Two words \(p,q\in \varSigma ^*\) are conjugate if there are \(x,y\in \varSigma ^*\) with \(p=xy\) and \(q=yx\). A word \(p\in \varSigma ^*\) is primitive if there is no \(q\in \varSigma ^*\) with \(p\in qq^+\).

Proposition 5.3

For every unbounded regular language \(L\subseteq \varSigma ^*\), there are \(x,u,v,y\in \varSigma ^*\) such that \(|u|=|v|\), the word uv is primitive, and \(x\{u,v\}^*y\subseteq L\).

Proof

Since L is unbounded and regular, Lemma 5.2 yields words \(x,y,p,q\in \varSigma ^*\) with \(|p|=|q|\), \(p\ne q\), and \(x\{p,q\}^*y\subseteq L\). Then the words \(r=pq\) and \(s=pp\) are not conjugate, because every conjugate of a square is a square. Moreover, \(|r|=|s|\), and \(x\{r,s\}^*y\subseteq x\{p,q\}^*y\subseteq L\). Let \(n=|r|\), \(u=rs^{n-1}\), and \(v=s^n\). Towards a contradiction, suppose \(uv=rs^{2n-1}\) is not primitive. Then there is a word \(w\in \varSigma ^*\) with \(rs^{2n-1}\in ww^+\). Depending on whether \(|w|\ge n\) or \(|w|<n\), we have \(n\le |w^t|\le n^2\) either for \(t=1\) or for \(t=n\). It follows that r is a prefix of \(w^t\) and that \(w^t\) is a suffix of \(s^n\), implying that r is a factor of \(s^n\). Since r and s are not conjugate, this is impossible.    \(\square \)

We are now ready to describe how to embed a finite partial order into \((L,\sqsubseteq )\). Observe that every finite partial order with m elements embeds into \((\{0,1\}^m,\le )\) where \(\le \) is the componentwise order. Hence, it suffices to embed this partial order into \((\{u,v\}^*,\sqsubseteq )\). We do this as follows. Let \(n=|uv|+m+3\) and define, for a tuple \(t=(t_1,\ldots ,t_m)\in \{0,1\}^m\),
$$ \varphi _m(t_1,\ldots ,t_m)=v^{t_1} (uv)^n \cdots v^{t_m} (uv)^n. $$
Then, clearly, \(s\le t\) implies \(\varphi _m(s)\sqsubseteq \varphi _m(t)\). The converse requires a careful analysis of how prefixes of \(\varphi _m(s)\) can embed into prefixes of \(\varphi _m(t)\). For \(x,y\in \varSigma ^*\), we write \(x\hookrightarrow y\) if x, but no word xa with \(a\in \varSigma \) is a subword of y. In other words, \(x\hookrightarrow y\) if x is a prefix-maximal subword of y. This gives us a criterion for non-embeddability: If x has a strict prefix \(x_0\) with \(x_0\hookrightarrow y\), then certainly \(x\not \sqsubseteq y\). In this case, the word \(x_1\) with \(x=x_0x_1\) is called residue. We show the following:

Lemma 5.4

Let \(u,v\in \varSigma ^*\) be words such that \(|u|=|v|\) and uv is primitive. Then, for all \(\ell ,n\in \mathbb {N}\) with \(n>|uv|+\ell +2\), we have
  1. (i)

    \((uv)^n\hookrightarrow v(uv)^n\),

     
  2. (ii)

    \((uv)^\ell v(uv)^{n-\ell -1} \hookrightarrow (uv)^n\), and

     
  3. (iii)

    \((uv)^{1+\ell } v(uv)^{n-\ell -2} \hookrightarrow v(uv)^n\).

     

For this lemma, it is crucial to observe that for a primitive word w and \(n>|w|+1\), any embedding of \(w^{n-1}\) into \(w^{n}\) must either hit the left-most or the right-most position in \(w^{n}\). To conclude that \(s\not \le t\) implies \(\varphi _m(s)\not \sqsubseteq \varphi _m(t)\), we argue about prefixes of the form \(p_i=v^{s_1}(uv)^n\cdots v^{s_{i}}(uv)^n\) and \(q_i=v^{t_1}(uv)^n\cdots v^{t_{i}}(uv)^n\) for \(i\in [1,m]\). If \(s\not \le t\), let \(i\in [1,m]\) be the index with \(s_i=1\), \(t_i=0\) and \(s_j\le t_j\) for all \(j\in [1,i-1]\). Then clearly \(p_{i-1}\sqsubseteq q_{i-1}\). In fact, Lemma 5.4 (i) implies that even \(p_{i-1}\hookrightarrow q_{i-1}\), since \(x\hookrightarrow y\) and \(x'\hookrightarrow y'\) imply \(xy\hookrightarrow x'y'\). Then, by Lemma 5.4 (ii), \(p_{i}=p_{i-1} v(uv)^{n-1}(uv)\) has a residue of uv in \(q_i=q_{i-1}(uv)^n\). To conclude \(\varphi _m(s)\not \sqsubseteq \varphi _m(t)\), it remains to be shown that this can never be rectified when considering prefixes \(p_j\) and \(q_j\) for \(j=i+1,\ldots ,m\). To this end, Lemma 5.4 (ii) and (iii) tell us that if \(p_j\) has a residue of \((uv)^\ell \) in \(q_j\), then the word \(p_{j+1}\) has a residue of \((uv)^\ell \) or even \((uv)^{\ell +1}\) in \(q_{j+1}\).

6 The \(\varSigma _1\)-Theory with Constants

In this section, we study for which languages L the structure \((L,\sqsubseteq ,(w)_{w\in L})\) has a decidable \(\varSigma _1\)-theory. From Theorem 3.4, we know that this is the case whenever L is bounded. However, there are very simple languages for which decidability is lost: If \(|\varSigma |\ge 2\), then the \(\varSigma _1\)-theory of \((\varSigma ^*,\sqsubseteq ,(w)_{w\in \varSigma ^*})\) is undecidable [6]. Here, we present a sufficient condition for the \(\varSigma _1\)-theory of \((L,\sqsubseteq ,(w)_{w\in \varSigma ^*})\) to be decidable.

Let \(L\subseteq \varSigma ^*\). We say that a letter \(a\in \varSigma \) is frequent in L if there is a real constant \(\delta >0\) so that \(|w|_a\ge \delta \cdot |w|\) for all but finitely many \(w\in L\). Our sufficient condition requires that all letters be frequent in L. If L is regular, this is equivalent to saying that in every non-degenerate automaton for L, every cycle contains every letter. An example of such a language is \(\{ab,ba\}^*\).

We shall prove that this condition implies decidability of the \(\varSigma _1\)-theory of \((L,\sqsubseteq ,(w)_{w\in \varSigma ^*})\). If L is bounded, decidability already follows from Theorem 3.4. In case L is unbounded, we employ our results from Sect. 5 to show another embeddability result. For \(w\in \varSigma ^*\), let \(w\mathord \uparrow =\{u\in \varSigma ^*\mid w\sqsubseteq u\}\) denote the upward closure of \(\{w\}\) in \((\varSigma ^*,\sqsubseteq )\). We will show that if L is unbounded, then for each \(w\in \varSigma ^*\), the decomposition of \(L=(L\setminus w\mathord \uparrow )\cup (L\cap w\mathord \uparrow )\) yields two simple parts: The set \(L\setminus w\mathord \uparrow \) is finite and the set \(L\cap w\mathord \uparrow \) embeds every finite partial order. This simplifies the conditions under which a \(\varSigma _1\)-sentence is satisfied.

Lemma 6.1

Let \(L\subseteq \varSigma ^*\) be an unbounded regular language where every letter is frequent. For every \(w\in \varSigma ^*\), the set \(L\setminus w\mathord {\uparrow }\) is finite and \(L\cap w\mathord {\uparrow }\) is unbounded.

Proof

In a non-degenerate automaton A for L, every cycle must contain every letter. Therefore, if A has n states and \(v\in L\) has \(|v|>n\cdot |w|\), then a computation for v must contain some state more than |w| times, which implies \(w\sqsubseteq v\) and hence \(v\notin L\setminus w\mathord {\uparrow }\). Therefore, \(L\setminus w\mathord {\uparrow }\) is finite. This implies that \(L\cap w\mathord {\uparrow }\) is unbounded: Otherwise \(L=(L\cap w\mathord {\uparrow })\cup (L\setminus w\mathord {\uparrow })\) would be bounded as well.    \(\square \)

Theorem 6.2

Let \(L\subseteq \varSigma ^*\) be an unbounded regular language where every letter is frequent. Then the \(\varSigma _1\)-theory of \((L,\sqsubseteq ,(w)_{w\in L})\) is decidable.

Proof

For decidability, we may assume that we are given a formula \(\varphi \) that is a disjunction of conjunctions of literals of the following forms (where x and y are arbitrary variables and w an arbitrary word from L):

Step 1. We first show that literals of types (i) and (iv) can be eliminated. To this end, we observe that for each \(w\in L\), both of the sets \(\{u\in L\mid u\sqsubseteq w\}\), and \(\{u\in L\mid w\not \sqsubseteq u\}\) are finite (in the latter case, this follows from Lemma 6.1). Thus, every conjunction that contains a literal \(x\sqsubseteq w\) or \(w\not \sqsubseteq x\), constrains x to finitely many values. Therefore, we can replace this conjunction with a disjunction of conjunctions that result from replacing x by one of these values. (Here, we might obtain literals \(u\sqsubseteq v\) or \(u\not \sqsubseteq v\), but those can be replaced by other equivalent formulas). We repeat this until there are no more literals of the form (i) and (iv).

Step 2. We now eliminate literals of the form (ii). Note that the language \(\{u\in L\mid u\not \sqsubseteq w\}\) is upward closed in \((L,\sqsubseteq )\). Since L is regular, we can compute the finite set of minimal elements of this set. Thus, \(x\not \sqsubseteq w\) is equivalent to a finite disjunction of literals of the form \(w'\sqsubseteq x\). The resulting formula \(\psi \) is a disjunction of conjunction of literals of the form (iii), (v), (vi).

Step 3. To check satisfiability, we may assume that \(\psi \) is a conjunction of literals of the form (iii), (v), (vi). We can write \(\psi \) as \(\gamma _1\wedge \gamma _2\), where \(\gamma _1\) is a conjunction of literals of the form (iii) and \(\gamma _2\) is a conjunction of literals of the form (v) and (vi). We claim that \(\psi \) is satisfiable if and only if \(\gamma _2\) is satisfiable in some partial order. The “only if” direction is trivial, so suppose \(\gamma _2\) is satisfied by some finite partial order \((P,\le )\) and let \(w\in \varSigma ^*\) be a concatenation of all words occurring in \(\gamma _1\). By Lemma 6.1, \(L\cap w\mathord {\uparrow }\) is unbounded, which implies that \((P,\le )\) can be embedded into \((L\cap w\mathord {\uparrow },\sqsubseteq )\) (see Sect. 5). This means, there exists a satisfying assignment where even \(w\sqsubseteq x\) for every variable x. In particular, it satisfies \(\psi =\gamma _1\wedge \gamma _2\).    \(\square \)

Open Questions

We did not consider complexity issues. In particular, from [13], we know that the \(\mathrm {FO}^2\)-theory of the structure \((\varSigma ^*,\sqsubseteq ,(w)_{w\in \varSigma ^*})\) can be decided in elementary time. We are currently working out the details for the extension of this result to the \(\mathrm {C{+}MOD}^2\)-theory of the structure \((L,\sqsubseteq ,(w)_{w\in L})\) for regular languages L. We reduced the \(\mathrm {FO{+}MOD}\)-theory of the full structure (for L context-free and bounded) to the \(\mathrm {FO{+}MOD}\)-theory of \((\mathbb {N},+)\), which is known to be decidable in elementary time [5]. Our reduction increases the formula exponentially due to the need of handling statements of the form “there is an even number of pairs \((x,y)\in \mathbb {N}^2\) such that ...” It should be checked whether the proof from [5] can be extended to handle such statements in \(\mathrm {FO{+}MOD}\) for \((\mathbb {N},+)\) directly.

Finally, our results raise an interesting question: For which regular languages L does the structure \((L,\sqsubseteq ,(w)_{w\in L})\) have a decidable \(\varSigma _1\)-theory? If every letter is frequent in L, we have decidability. For example, this applies to \(L=\{ab,ba\}^*\) or \(L=\{ab,baa\}^*\cup bb\{abb\}^*\). If \(L=\varSigma ^*\) for \(|\varSigma |\ge 2\), we have undecidability [6].

References

  1. 1.
    Apelt, H.: Axiomatische Untersuchungen über einige mit der Presburgerschen Arithmetik verwandten Systeme. Z. Math. Logik Grundlagen Math. 12, 131–168 (1966)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Berstel, J.: Transductions and Context-Free Languages. Teubner Studienbücher, Stuttgart (1979)CrossRefGoogle Scholar
  3. 3.
    Droste, M., Gastin, P.: Weighted automata and weighted logics. In: Droste, M., Kuich, W., Vogler, H. (eds.) Handbook of Weighted Automata, pp. 176–211. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-01492-5_5CrossRefGoogle Scholar
  4. 4.
    Finkel, A., Schnoebelen, Ph.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256, 63–92 (2001)Google Scholar
  5. 5.
    Habermehl, P., Kuske, D.: On Presburger arithmetic extended with modulo counting quantifiers. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 375–389. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46678-0_24CrossRefGoogle Scholar
  6. 6.
    Halfon, S., Schnoebelen, Ph., Zetzsche, G.: Decidability, complexity, and expressiveness of first-order logic over the subword ordering. In: Proceedings of the Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), pp. 1–12. IEEE Computer Society (2017)Google Scholar
  7. 7.
    Higman, G.: Ordering by divisibility in abstract algebras. Proc. London Math. Soc. 2, 326–336 (1952)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Ježek, J., McKenzie, R.: Definability in substructure orderings. I: finite semilattices. Algebra Univers. 61(1), 59–75 (2009)Google Scholar
  9. 9.
    Ježek, J., McKenzie, R.: Definability in substructure orderings. III: finite distributive lattices. Algebra Univers. 61(3–4), 283–300 (2009)Google Scholar
  10. 10.
    Ježek, J., McKenzie, R.: Definability in substructure orderings. IV: finite lattices. Algebra Univers. 61(3–4), 301–312 (2009)Google Scholar
  11. 11.
    Ježek, J., McKenzie, R.: Definability in substructure orderings. II: finite ordered sets. Order 27(2), 115–145 (2010)Google Scholar
  12. 12.
    Karandikar, P., Schnoebelen, Ph.: Decidability in the logic of subsequences and supersequences. In: Harsha, P., Ramalingam, G. (eds.) Proceedings of the 35th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics, vol. 45, pp. 84–97. Leibniz-Zentrum für Informatik (2015)Google Scholar
  13. 13.
    Karandikar, P., Schnoebelen, Ph.: The height of piecewise-testable languages with applications in logical complexity. In: Talbot, J.-M., Regnier, L. (eds.) Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics, vol. 62, pp. 37:1–37:22 (2016)Google Scholar
  14. 14.
    Kudinov, O.V., Selivanov, V.L.: Undecidability in the homomorphic quasiorder of finite labelled forests. J. Log. Comput. 17(6), 1135–1151 (2007)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Kudinov, O.V., Selivanov, V.L., Yartseva, L.V.: Definability in the subword order. In: Ferreira, F., Löwe, B., Mayordomo, E., Mendes Gomes, L. (eds.) CiE 2010. LNCS, vol. 6158, pp. 246–255. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-13962-8_28CrossRefGoogle Scholar
  16. 16.
    Kudinov, O.V., Selivanov, V.L., Zhukov, A.V.: Definability in the h-quasiorder of labeled forests. Ann. Pure Appl. Logic 159(3), 318–332 (2009)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Kuske, D.: Theories of orders on the set of words. Theor. Inf. Appl. 40, 53–74 (2006)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Kuske, D., Zetzsche, G.: Languages ordered by the subword order. CoRR, abs/1901.02194 (2019)Google Scholar
  19. 19.
    Parikh, R.: On context-free languages. J. ACM 13(4), 570–581 (1966)CrossRefGoogle Scholar
  20. 20.
    Sakarovitch, J.: Rational and recognisable power series. In: Droste, M., Kuich, W., Vogler, H. (eds.) Handbook of Weighted Automata, pp. 105–174. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-01492-5_4CrossRefGoogle Scholar
  21. 21.
    Schweikardt, N.: Arithmetic, first-order logic, and counting quantifiers. ACM Trans. Comput. Log. 6(3), 634–671 (2005)MathSciNetCrossRefGoogle Scholar
  22. 22.
    Thinniyam, R.S.: Definability of recursive predicates in the induced subgraph order. In: Ghosh, S., Prasad, S. (eds.) ICLA 2017. LNCS, vol. 10119, pp. 211–223. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54069-5_16CrossRefGoogle Scholar
  23. 23.
    Thinniyam, R.S.: Defining recursive predicates in graph orders. Logical Methods Comput. Sci. 14(3:21), 1–38 (2018)MathSciNetzbMATHGoogle Scholar

Copyright information

© The Author(s) 2019

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Authors and Affiliations

  1. 1.Technische Universität IlmenauIlmenauGermany
  2. 2.Max Planck Institute for Software Systems (MPI-SWS)KaiserslauternGermany

Personalised recommendations