Second-Order Finite Automata

In its most traditional setting, automata theory has been used as a framework for the representation and manipulation of (possibly infinite) sets of strings. This framework has been generalized in many ways to allow the representation of sets of more elaborate combinatorial objects, such as trees [10], partial orders [36], graphs [6], pictures [19], etc. Such notions of automata have encountered innumerous applications in fields such as formal verification [5, 20], finite model theory [16], concurrency theory [34], parameterized complexity [11, 12], etc. Still, these generalized notions of automata share in common the fact that they are designed to represent (possibly infinite) sets of isolated objects.

In this work, we combine traditional finite automata with ordered decision diagrams (ODDs) of bounded width to introduce a formalism that can be used to represent and manipulate sets of sets of strings, or alternatively speaking, classes of languages. We call this combined formalism second-order finite automata. We will show that the width of an ODD is a useful parameter when studying classes of languages from a complexity-theoretic point of view. Additionally, we will use second-order finite automata to show that several computational problems involving ordered decision diagrams are fixed-parameter tractable when parameterized by width.

Given a finite alphabet Σ and a number \({w}\in {{\mathbb {N}}_+}\), a (Σ,w)-ODD is a sequence \({{D}} = {B}_{1}{B}_{2}{\dots } {B}_{{k}}\) of (Σ,w)-layers. Each such a layer B_i has a set of left-states (a subset of \(\{1,\dots ,{w}\}\)), a set of right-states (also a subset of \(\{1,\dots ,{w}\}\)), and a set of transitions, labeled with letters in Σ, connecting left states to right states. We require that for each \(i\in \{1,\dots ,k-1\}\), the set of right-states of the layer B_i is equal to the set of left states of the layer B_i+ 1. The language of an ODD D is the set of strings labelling paths from its set of initial states (a subset of the left states of B₁) to its final states (a subset of the right states of B_k). Since the number of distinct (Σ,w)-layers is finite, the set \({{\mathscr{B}}({\Sigma }, {w})}\) of all (Σ,w)-layers can itself be regarded as an alphabet. A finite automaton \({\mathcal {F}}\) over the alphabet \({{\mathscr{B}}({\Sigma }, {w})}\) is said to be a second-order finite automaton if each string \({{D}} = {B}_{1}{\dots } {B}_{{k}}\) in the language \({\mathscr{L}}(\mathcal {F})\) accepted by \(\mathcal {F}\) is a valid ODD. In this case, the second language of \(\mathcal {F}\) is defined as the class \({{{\mathscr{L}}}_{2}({\mathcal {F}})} = \{{{\mathscr{L}}({{D}})} : {{D}}\in {{{\mathscr{L}}}({\mathcal {F}})}\}\) of languages accepted by ODDs in \({{{\mathscr{L}}}({\mathcal {F}})}\). We say that a class of languages \(\mathcal {X}\) is regular-decisional if there is some second-order finite automaton \(\mathcal {F}\) such that \({{{\mathscr{L}}}_{2}({\mathcal {F}})} = \mathcal {X}\).

Canonical Forms for Second Order Finite Automata

Our main result (Theorem 10) states that second-order finite automata can be effectively canonized with respect to their second languages. More specifically, there is an algorithm that maps each second-order finite automaton \({\mathcal {F}}\) to a second-order finite automaton \(\mathcal {C}_{2}({\mathcal {F}})\), called the second canonical form of \({\mathcal {F}}\), in such a way that the following three properties are satisfied. First, \(\mathcal {C}_{2}({\mathcal {F}})\) and \({\mathcal {F}}\) have the same second language. That is to say, \({{{\mathscr{L}}}_{2}(\mathcal {C}_{2}({\mathcal {F}}))}= {{{\mathscr{L}}}_{2}({\mathcal {F}})}\). Second, any two second-order finite automata \({\mathcal {F}}\) and \({\mathcal {F}}^{\prime }\) with identical second languages are mapped to the same canonical form. More formally, \({{{\mathscr{L}}}_{2}({\mathcal {F}})} = {{{\mathscr{L}}}_{2}({\mathcal {F}}^{\prime })}\Rightarrow \mathcal {C}_{2}({\mathcal {F}}) = \mathcal {C}_{2}({\mathcal {F}}^{\prime })\). Third, \({{{\mathscr{L}}}(\mathcal {C}_{2}({\mathcal {F}}))} = \{\mathcal {C}({{D}}) : {{D}}\in {{{\mathscr{L}}}({\mathcal {F}})}\}\). Here, \(\mathcal {C}({{D}})\) is the unique deterministic, complete, normalized^{Footnote 1} ODD with minimum number of states with the same language as D. Intuitively, the language of \(\mathcal {C}_{2}({\mathcal {F}})\) consists precisely of the set of canonical forms of ODDs in the language of \({\mathcal {F}}\). For this reason, we say that Theorem 10 is a canonical form of canonical forms theorem. From a complexity-theoretic point of view, \(\mathcal {C}_{2}({\mathcal {F}})\) can be constructed in time \(2^{\mathsf {nSt}({\mathcal {F}})\cdot 2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}}\), where \(\mathsf {nSt}({\mathcal {F}})\) is the number of states of \({\mathcal {F}}\). Additionally this construction can be sped up to time \(2^{\mathsf {nSt}({\mathcal {F}})\cdot 2^{O(|{\Sigma }|\cdot {w} \cdot \log {w})}}\) if all ODDs in \({{{\mathscr{L}}}({\mathcal {F}})}\) are deterministic and complete (Observation 11).

We note that canonizing a second-order finite automaton \({\mathcal {F}}\) with respect to its second language \({{{\mathscr{L}}}_{2}({\mathcal {F}})}\) is not equivalent to canonizing \({\mathcal {F}}\) with respect to its language \({{{\mathscr{L}}}({\mathcal {F}})}\). For instance, let D and \({{D}}^{\prime }\) be distinct ODDs such that \({{\mathscr{L}}({{D}})} = {{\mathscr{L}}({{D}}^{\prime })}\). Let \({\mathcal {F}}\) and \({\mathcal {F}}^{\prime }\) be second-order finite automata with \({{{\mathscr{L}}}({\mathcal {F}})} = \{{{D}}\}\) and \({{{\mathscr{L}}}({\mathcal {F}}^{\prime })} = \{{{D}}^{\prime }\}\). Then the languages of \({\mathcal {F}}\) and \({\mathcal {F}}^{\prime }\) are distinct (\({{{\mathscr{L}}}({\mathcal {F}})} \neq {{{\mathscr{L}}}({\mathcal {F}}^{\prime })}\)) even though their second languages are equal (\({{{\mathscr{L}}}_{2}({\mathcal {F}})} = \{{{\mathscr{L}}({{D}})}\} = \{{{\mathscr{L}}({{D}}^{\prime })}\} = {{{\mathscr{L}}}_{2}({\mathcal {F}}^{\prime })}\)).

At a high level, what our canonization algorithm does is to eliminate ambiguity in the language of a given second-order finite automaton. More specifically, any two ODDs D and \({{D}}^{\prime }\) with \({{\mathscr{L}}({{D}})}={{\mathscr{L}}({{D}}^{\prime })}\) in the language of a second-order finite automaton \({\mathcal {F}}\) correspond to a single ODD \(\mathcal {C}({{D}})=\mathcal {C}({{D}}^{\prime })\) in the language of \(\mathcal {C}_{2}({\mathcal {F}})\). This implies almost immediately that the collection of regular-decisional classes of languages is closed under union, intersection, set difference, and even under a suitable notion of complementation. Furthermore, emptiness of intersection and inclusion for the second languages of second-order finite automata are decidable (Theorem 13). It is interesting to note that non-emptiness of intersection for the second languages of second-order finite automata can be tested in fixed-parameter tractable time, where the parameter is the maximum width of an ODD accepted by one of the input automata (Observation 14). Finally, closure under several operations that are specific to classes of languages, such as pointwise union, pointwise intersection and pointwise negation, among others can also be obtained as a direct corollary (Corollary 16) of a technical lemma from [15].

Main Technical Tool

Let \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\) be the set of all (Σ,w)-ODDs and \({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\) be the set of all deterministic, complete (Σ,w)-ODDs. The main technical tool of this work (Theorem 9) states that the transduction \(\mathfrak {can}[{\Sigma },{w}] = \{({{D}},\mathcal {C}({{D}})) : {{D}}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\}\) is \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\)-regular. In other words, there is an NFA with \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\) states accepting the language \(\{{{D}}\otimes \mathcal {C}({{D}}) : {{D}}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\}\). Additionally, the transduction \(\widehat {\mathfrak {can}}[{\Sigma },{w}] = \{({{D}},\mathcal {C}({{D}})) : {{D}}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\}\), whose domain is restricted to deterministic, complete ODDs, is \(2^{O(|{\Sigma }|\cdot {w} \cdot \log {w})}\)-regular.

Most results of our work follow as a consequence of Theorem 9. If we do not take complexity theoretic issues into account, then some of our decidability results also follow by employing other notions of canonizing relations (see Section 7 for further discussion on this topic). Nevertheless, the transductions \(\mathfrak {can}[{\Sigma },{w}]\) and \(\widehat {\mathfrak {can}}[{\Sigma },{w}]\) enjoy special properties that make them attractive from a complexity theoretic point of view. In particular, as we will see next, these transductions have applications in the fixed-parameter tractability theory of computational problems related to ordered decision diagrams ODDs. It is worth noting that ODDs comprise the well studied notion of ordered binary decision diagrams (OBDDs) with fixed variable ordering as a special case. And indeed, the width parameter has relevance in several contexts, such as learning theory [17], the theory of pseudo-random generators [18], the theory of symbolic algorithms [15], and structural graph theory [13]. Additionally, Theorem 9 implies that the set \(\{\mathcal {C}({{D}}) : {{D}}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\}\) of all minimized, deterministic, complete ODDs accepting the language of some ODD in \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\) is regular (Corollary 12), and therefore, can be accepted by some deterministic finite automaton \({\mathcal {F}}\). This result may be of independent interest since the fact that the canonical form \(\mathcal {C}({{D}})\) has minimum number of states among all deterministic, complete ODDs with the same language as D is a relevant complexity theoretic information about the language \({{\mathscr{L}}({{D}})}\). One interesting consequence of this result is that there is a bijection b from the set of accepting paths of \({\mathcal {F}}\) and the class of languages accepted by ODDs in \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\). Additionally, the ODD corresponding to each such a path \(\mathfrak {p}\) has minimum number of states among all deterministic, complete ODDs accepting the language \(b(\mathfrak {p})\).

Algorithmic Applications

Although ODDs of constant width constitute a simple computational model, they can already be used to represent many interesting functions. It is worth noting that for each width w ≥ 3, the class of functions that can be represented by ODDs of constant width is at least as difficult to learn in the PAC-learning model as the problem of learning DNFs [17]. Additionally, the study of ODDs of constant width is still very active in the theory of pseudo-random generators [18]. Our main results can be used to show that several width/size minimization problems for nondeterministic and deterministic ODDs can be solved in fixed parameter tractable time when parameterized by width. For instance, we show that given an ODD D of length k and width w over an alphabet Σ, one can compute in time \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot {k}\) an ODD \({{D}}^{\prime }\) of minimum width such that \({{\mathscr{L}}({{D}}^{\prime })}={{\mathscr{L}}({{D}})}\). A more efficient algorithm, running in time \(2^{O(|{\Sigma }|\cdot {w} \cdot \log {w})}\cdot {k}\) can be obtained if the input ODD is deterministic (Theorem 20). Our algorithm is in fact more general and can be used to minimize other complexity measures, such as number of states and number of transitions among all ODDs belonging to the language of a given second-order finite automaton \({\mathcal {F}}\) (Theorem 19).

Our algorithm for width minimization of ODDs parameterized by width naturally can be used to minimize the width of ordered binary decision diagrams (OBDDs), since OBDDs with a fixed variable ordering correspond to ODDs over a binary alphabet. Width minimization problems for OBDDs have been considered before in the literature [3, 4], but previously known algorithms are exponential on the size of the OBDD even for OBDDs of constant width, and even in the case of when one is not allowed to vary the order of the input variables. Our FPT result shows that width minimization for OBDDs of constant width with a fixed variable ordering can be achieved in polynomial time.

As a second application of our main results, we show that the problem of counting the number of distinct functions computable by ODDs of a given width w and a given length k can be solved in time \(2^{2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}}\cdot {k}^{O(1)}\). This running time can be improved to \(2^{2^{O(|{\Sigma }|\cdot {w} \cdot \log {w})}}\cdot {k}^{O(1)}\) if we are interested in counting the number of functions computable by deterministic, complete ODDs of width w and length k (Corollary 24). We note that this restricted case is relevant because ordered binary decision diagrams (OBDDs) defined in the literature are usually deterministic and complete. Our results imply that counting the number of functions computable by OBDDs of width w with a fixed variable ordering can be solved in time polynomial in the number of variables. This improves exponentially on the approach of explicit enumeration without repetitions, which takes time exponential in k. This result is obtained as a consequence of a more general theorem analyzing the complexity of the problem counting functions represented by ODDs of a given length in the language of a given second-order finite automaton \({\mathcal {F}}\) (Theorem 22).

The reminder of this paper is organized as follows. Next, in Section 2, we define some basic concepts and state well-known results concerning finite automata and ordered decision diagrams. Subsequently, in Section 3, we formally define the notion of second-order finite automata and state our main results (Theorem 9 and Theorem 10). In Section 4, we state several closure properties for second-order finite automata. In Section 5, we discuss several algorithmic applications of our main results. In Section 6 we prove Theorem 9. Finally, in Section 7 we draw some concluding remarks and establish connections with related work.

2.1 Basics

We denote by \({\mathbb {N}} \doteq \lbrace {0, 1, \ldots }\rbrace \) the set of natural numbers (including zero), and by \({{\mathbb {N}}_+} \doteq {\mathbb {N}}\setminus \lbrace {0}\rbrace \) the set of positive natural numbers. For each \(c \in {{\mathbb {N}}_+}\), we let \({[{{c}}]} \doteq \lbrace {1, 2, \ldots , {c}}\rbrace \) and \(\llbracket {{c}}\rrbracket \doteq \lbrace {0, 1, \ldots , {c}-1}\rbrace \). For each finite set X, we let \({\mathcal {P}({X})} \doteq \lbrace {X^{\prime } \colon X^{\prime } \subseteq {X}}\rbrace \) denote the power set of X. For each two sets X and Y, each function \(f\colon {X} \rightarrow {Y}\) and each subset \(X^{\prime }\subseteq X\), we let \(f|_{X^{\prime }}\) denote the restriction of f to \(X^{\prime }\), i.e. the function \(f|_{X^{\prime }} \colon X^{\prime } \rightarrow Y\) such that \(f|_{X^{\prime }}(x) = f(x)\) for each \(x \in X^{\prime }\).

2.1.1 Alphabets and Strings

An alphabet is any finite, non-empty set Σ. A string over an alphabet Σ is any finite sequence of symbols from Σ. The empty string, denoted by λ, is the unique string of length zero. We denote by Σ^∗ the set of all strings over Σ, including the empty string λ, and by \({\Sigma }^{+} \doteq {\Sigma }^{*}\setminus \lbrace {\lambda }\rbrace \) the set of all non-empty strings over Σ. A language over Σ is any subset L of Σ^∗. In particular, for each \({k} \in {\mathbb {N}}\), we let Σ^k be the language of all strings of length k over Σ. We say that an alphabet Σ is ordered if it is endowed with a total order <_Σ : Σ ×Σ. Such an order <_Σ is extended naturally to a lexicographical order \(\prec _{{\Sigma }}\subseteq {\Sigma }^{*}\times {\Sigma }^{*}\) on the set Σ^∗. Unless stated otherwise, we assume that each alphabet considered in this paper is endowed with a fixed total order.

2.1.2 Finite Automata

A finite automaton (FA) over an alphabet Σ is a tuple \({\mathcal {F}} = ({{\Sigma },{Q},{I},{F},{T}})\), where Q is a finite set of states, \({I}\subseteq {Q}\) is a set of initial states, \({F}\subseteq {Q}\) is a set of final states and \({{T}\subseteq {Q}\times {\Sigma }\times {Q}}\) is a set of transitions. The size of \({\mathcal {F}}\) is defined as \(\lvert {{\mathcal {F}}}\rvert \doteq \lvert {{Q}}\rvert + \lvert {{T}}\rvert \cdot \log {\lvert {{\Sigma }}\rvert }\). We denote the number of states of \({\mathcal {F}}\) by \(\mathsf {nSt}({\mathcal {F}})\doteq \lvert {{Q}}\rvert \), and the number of transitions of \({\mathcal {F}}\) by \(\mathsf {nTr}({\mathcal {F}}) \doteq \lvert {{T}}\rvert \).

Let s ∈Σ^∗, and \({q},{{q}^{\prime }}\in {Q}\). We say that s reaches \({{q}^{\prime }}\) from q if either s = λ and \({q}={{q}^{\prime }}\), or if \({s} = {\sigma }_{1}\dots {\sigma }_{{k}}\) for some \(k\in {{\mathbb {N}}_+}\) and there is a sequence

of transitions such that q₀ = q, \({q}_{{k}} = {{q}^{\prime }}\) and (q_i,σ_i+ 1,q_i+ 1) ∈ T for each i ∈ [k − 1]. We say that \({\mathcal {F}}\) acceptss if there exist states q ∈ I and \({{q}^{\prime }}\in {F}\) such that s reaches \({{q}^{\prime }}\) from q. The language of \({\mathcal {F}}\) is defined as the set

of all finite strings over Σ accepted by \({\mathcal {F}}\). For \(\alpha \!\in \! {\mathbb {N}}\), we say that a language \({L}\!\subseteq \! {\Sigma }^{*}\) is α-regular if there exists a finite automaton with at most α states such that \({{{\mathscr{L}}}({\mathcal {F}})} = {L}\).

We say that \({\mathcal {F}}\) is deterministic if \({\mathcal {F}}\) contains exactly one initial state, i.e. \(\lvert {{I}}\rvert = 1\), and for each q ∈ Q and each σ ∈Σ, there exists at most one state \({{q}^{\prime }} \in {Q}\) such that \(({{q},{\sigma },{{q}^{\prime }}})\) is a transition in T. We say that \({\mathcal {F}}\) is complete if it has at least one initial state, and for each q ∈ Q and each σ ∈Σ, there exists at least one state \({{q}^{\prime }} \in {Q}\) such that \(({{q},{\sigma },{{q}^{\prime }}})\) is a transition in T. We say that \({\mathcal {F}}\) is reachable if for each state q ∈ Q, there is a sequence of transitions from some initial state of \({\mathcal {F}}\) to q. If \({\mathcal {F}}\) is a reachable finite automaton, then for each state q ∈ Q, we let lex(q) denote the lexicographically first string that reaches q from some initial state, according to the order ≺_Σ. We say that \({\mathcal {F}}\) is normalized if Q = ⟦n⟧ for some \(n\in {{\mathbb {N}}_+}\), and \({q}<{{q}^{\prime }}\) if and only if \(\mathsf {lex}({q}) \prec _{{\Sigma }} \mathsf {lex}({{q}^{\prime }})\) for each \({q},{{q}^{\prime }} \in {Q}\).

In what follows, we may write \({Q}({\mathcal {F}})\), \({T}({\mathcal {F}})\), \({I}({\mathcal {F}})\) and \({F}({\mathcal {F}})\) to refer to the sets Q, T, I and F, respectively.

The following theorem, stating the existence of canonical forms for finite automata, is one of the most fundamental results in automata theory.

Theorem 1

For each finite automaton \({\mathcal {F}}\), there exists a unique finite automaton \(\mathcal {C}({\mathcal {F}})\) with minimum number of states such that \(\mathcal {C}(\mathcal {F})\) is deterministic, complete, normalized, and satisfies \({\mathscr{L}}(\mathcal {C}(\mathcal {F})) = {\mathscr{L}}(\mathcal {F})\).

We note that given a (possibly non-deterministic) finite automaton \({\mathcal {F}}\), the canonical form \(\mathcal {C}({\mathcal {F}})\) of \({\mathcal {F}}\) can be obtained by the following process. First, one applies Rabin’s power-set construction to \({\mathcal {F}}\) in order to obtain a deterministic, complete finite automaton \({\mathcal {F}}^{\prime }\) that accepts the same language as \({\mathcal {F}}\). Subsequently, by using Hopcroft’s algorithm [25] for instance, one minimizes \({\mathcal {F}}^{\prime }\) in order to obtain a deterministic finite automaton \({\mathcal {F}}^{\prime \prime }\) that accepts the same language as \({\mathcal {F}}\) and has the minimum number of states. At this point, the finite automaton \({\mathcal {F}}^{\prime \prime }\) is unique up to renaming of states. Thus, as a last step, one obtains the canonical form \(\mathcal {C}({\mathcal {F}})\) by renaming the states of \({\mathcal {F}}^{\prime \prime }\) in such a way that the normalization property is satisfied. Note that the automaton \(\mathcal {C}({\mathcal {F}})\) is finally syntactically unique. In particular, for each two finite automata \({\mathcal {F}}\) and \({\mathcal {F}}^{\prime }\), \({{{\mathscr{L}}}({\mathcal {F}})} = {{{\mathscr{L}}}({\mathcal {F}}^{\prime })}\) if and only if \(\mathcal {C}({\mathcal {F}}) = \mathcal {C}({\mathcal {F}}^{\prime })\).

2.2 Ordered Decision Diagrams

2.2.1 Layers

Let Σ be an alphabet and \({w}\in {{\mathbb {N}}_+}\). A (Σ,w)-layer is a tuple \({B} \doteq ({{\ell },{r}, {T}, {I}, {F}, {\iota }, {\phi }})\), where \({\ell } \subseteq \llbracket {{w}}\rrbracket \) is a set of left states, \(r \subseteq \llbracket {w}\rrbracket \) is a set of right states, \(T \subseteq \ell \times {\Sigma } \times r\) is a set of transitions, \(I \subseteq \ell \) is a set of initial states, \(F \subseteq r\) is a set of final states and ι,ϕ ∈{0,1} are Boolean flags satisfying the two following conditions:

1. 1.

   if ι = 0, then I = ∅;

2. 2.

   if ϕ = 0, then F = ∅.

In what follows, we may write ℓ(B), r(B), T(B), I(B), F(B), ι(B) and ϕ(B) to refer to the sets ℓ, r, T, I and F and to the Boolean flags ι and ϕ, respectively.

We let \({{\mathscr{B}}({\Sigma }, {w})}\) denote the set of all (Σ,w)-layers. Note that \({{\mathscr{B}}({\Sigma }, {w})}\) is non-empty and has at most \(2^{{\mathcal {O}}(\lvert {{\Sigma }}\rvert \cdot {w}^{2})}\) elements. Therefore, \({{\mathscr{B}}({\Sigma }, {w})}\) may be regarded as an alphabet.

2.2.2 Ordered Decision Diagrams

Let Σ be an alphabet and \({w},{k}\in {{\mathbb {N}}_+}\). A (Σ,w)-ordered decision diagram (or simply, (Σ,w)-ODD) of length k is a string \({{D}} \doteq {B}_{1} {\cdots } {B}_{{k}} \in {{\mathscr{B}}({\Sigma }, {w})}^{{k}}\) of length k over the alphabet \({{\mathscr{B}}({\Sigma }, {w})}\) satisfying the following conditions:

1. 1.

   for each i ∈ [k − 1], ℓ(B_i+ 1) = r(B_i);

2. 2.

   ι(B₁) = 1 and, for each i ∈{2,…,k}, ι(B_i) = 0;

3. 3.

   ϕ(B_k) = 1 and, for each i ∈ [k − 1], ϕ(B_i) = 0.

Intuitively, Condition 1 expresses that for each i ∈ [k − 1], the set of right states of B_i can be identified with the set of left states of B_i+ 1. Condition 2 guarantees that only the first layer of an ODD is allowed to have initial states. Analogously, Condition 3 guarantees that only the last layer of an ODD is allowed to have final states.

Let D = B₁⋯B_k be a (Σ,w)-ODD of length k, for some \({k}\in {{\mathbb {N}}_+}\). We let \(\mathsf {len}({D})\doteq {k}\) denote the length of D, \(\mathsf {nSt}({{D}})\doteq \lvert {{\ell }({B}_{1})}\rvert + {\sum }_{i\in {[{{k}}]}} \lvert {{r}({B}_{i})}\rvert \) denote the number of states of D, \(\mathsf {nTr}({{D}}) \doteq \lvert {{T}({B}_{1})}\rvert + {\sum }_{i\in {[{{k}}}]} \lvert {{T}({B}_{i})}\rvert \) denote the number of transitions of D,

denote the width of D. We remark that w(D) ≤ w.

For each subset \(\mathcal {S}\subseteq {{\mathscr{B}}({\Sigma }, {w})}\) and each positive integer \({k} \in {{\mathbb {N}}_+}\), we denote by \(\mathcal {S}^{\circ {k}}\) the set of all (Σ,w)-ODDs of length k whose layers belong to the set \(\mathcal {S}\). Additionally, for each subset \(\mathcal {S}\subseteq {{\mathscr{B}}({\Sigma }, {w})}\), we denote by \(\mathcal {S}^{\circledast } \doteq \bigcup _{{k}\in {{\mathbb {N}}_+}} \mathcal {S}^{\circ {k}}\) the set of all (Σ,w)-ODDs whose layers belong to the set \(\mathcal {S}\). In particular, we denote by \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\) the set of all (Σ,w)-ODDs of length k, and we denote by \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\) the set of all (Σ,w)-ODDs.

2.2.3 Length Typed Subsets of Σ^k

Let Σ be an alphabet and \({k}\in {{\mathbb {N}}_+}\). In this work, it is convenient to assume that subsets of Σ^k are typed with their length. This can be achieved by viewing each subset \({L} \subseteq {\Sigma }^{{k}}\) as a pair of the form (k,L). We let \(\mathcal {P}_{{k}}({\Sigma }) = \lbrace {({{k},{L}}) \colon {L}\subseteq {\Sigma }^{{k}}}\rbrace \) be the set of all length typed subsets of Σ^k. Given length typed sets (k,L₁) and (k,L₂), we define \(({k},{L}_{1})\cup ({k},{L}_{2}) \doteq ({k},{L}_{1}\cup {L}_{2})\), \(({k},{L}_{1})\cap ({k},{L}_{2}) \doteq ({k},{L}_{1}\cap {L}_{2})\), \(({k},{L}_{1})\backslash ({k},{L}_{2}) \doteq ({k},{L}_{1}\backslash {L}_{2})\), \(({k},{L}_{1})\otimes ({k},{L}_{2}) \doteq ({k},{L}_{1}\otimes {L}_{2})\), and for maps \(g:{\Sigma }\rightarrow {\Sigma }^{\prime }\) and \(h:{\Sigma }^{\prime }\rightarrow {\Sigma }\), we let \(g({k},{L}) \doteq ({k},g({L}))\) and \(h^{-1}({k},{L}) \doteq ({k},h^{-1}({L}))\).

2.2.4 Language Accepted by an ODD

Let Σ be an alphabet, \({w},{k}\in {{\mathbb {N}}_+}\), D = B₁⋯B_k be an ODD in \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\) and s = σ₁⋯σ_k be a string in Σ^k. A valid sequence for s in D is a sequence of transitions

such that \({\mathfrak {p}}_{i+1} = {\mathfrak {q}}_{i}\) for each i ∈ [k − 1], and \(({{\mathfrak {p}}_{i},{\sigma }_{i},{\mathfrak {q}}_{i}})\in {T}({B}_{i})\) for each i ∈ [k]. Such a valid sequence is called accepting for s if, additionally, \({\mathfrak {p}}_{1}\) is an initial state in I(B₁) and \({\mathfrak {q}}_{{k}}\) is a final state in F(B_k). We say that D acceptss if there exists an accepting sequence for s in D. The language of D is defined as the (length-typed) set

of all strings accepted by D. Note that every string accepted by D has length k.

In Fig. 1, we depict an ODD \({D}\in {{{\mathscr{B}}(\lbrace {0,1}\rbrace , 2)}^{\protect \circ {5}}}\) whose language is the length-typed set \({{\mathscr{L}}({{D}})}=({5,\lbrace {{s}={\sigma }_{1}\cdots {\sigma }_{5}\in \lbrace {0,1}\rbrace ^{5} \colon {\sigma }_{1}+\cdots +{\sigma }_{5} \equiv 0 \pmod 2}\rbrace })\) of all binary strings of length 5 with an even number of occurrences of the symbol ‘1’. For instance,

is an accepting sequence in D for the string 01010, which has two occurrences of the symbol ‘1’.

2.2.5 Deterministic and Complete ODDs

Let Σ be an alphabet and \({w}\in {{\mathbb {N}}_+}\). A (Σ,w)-layer B is called deterministic if the following conditions are satisfied:

1. 1.

   if ι(B) = 1, then I(B) = ℓ(B) and \(\lvert {{\ell }({B})}\rvert = 1\);

2. 2.

   for each \({\mathfrak {p}} \in {\ell }({B})\) and each σ ∈Σ, there exists at most one right state \({\mathfrak {q}} \in {r}(B)\) such that \(({{\mathfrak {p}}, {\sigma }, {\mathfrak {q}}}) \in T(B)\).

A (Σ,w)-layer B is called complete if the following conditions are satisfied:

1. 1.

   if ι(B) = 1, then I(B)≠∅;

2. 2.

   for each \({\mathfrak {p}} \in {\ell }({B})\) and each σ ∈Σ, there exists at least one right state \({\mathfrak {q}} \in {r}(B)\) such that \(({{\mathfrak {p}}, {\sigma }, {\mathfrak {q}}}) \in T(B)\).

We let \({\widehat {{\mathscr{B}}}({\Sigma }, {w})}\) be the subset of \({{\mathscr{B}}({\Sigma }, {w})}\) comprising all deterministic, complete (Σ,w)-layers.

Observation 2

Let Σ be an alphabet, and \({w} \in {{\mathbb {N}}_+}\).

1. 1.

   The alphabet \({\widehat {{\mathscr{B}}}({\Sigma }, {w})}\) has \(2^{O(|{\Sigma }|{w} \log {w})}\) layers.

2. 2.

   The alphabet \({{\mathscr{B}}({\Sigma }, {w})}\) has \(2^{O(|{\Sigma }|{w}^{2})}\) layers.

Proof

1. 1.

   Let Σ be an alphabet, and \(x,y\in \{0,1,\dots ,{w}\}\). We note that there are at most

   $$d({\Sigma},x,y)=\binom{{w}}{x}\binom{{w}}{y}(x+1)(1+2^{y})y^{|{\Sigma}|x} = w^{O(|{\Sigma}|w)} = 2^{O(|{\Sigma}|w \log w)}$$

   deterministic complete layers with x left states, y right states and transitions labeled by symbols in Σ. Indeed, there are \(\binom {w}{x}\) ways of choosing x left states, out of the set \(\{1,\dots ,w\}\), \(\binom {w}{y}\) ways of choosing y right states out of the set \(\{1,\dots ,w\}\), (w + 1) ways of choosing the initial set of states I(B) together with the initial flag ι(B) (because I(B) = ∅ if ι(B) = 0 and |I(B)| = 1 if ι(B) = 1, due to determinism), 1 + 2^y ways of choosing the subset of final states F(B) together with the final flag ϕ(B) (because F(B) = 0 if ϕ(B) = 0 and F(B) is an arbitrary subset of r(B) if ϕ(B) = 1), and y^|Σ|x ways of choosing the transition relation T(B) (because there are x left states, and for each such state q and each symbol a ∈Σ there are y ways of choosing the unique transition with label a leaving q). Therefore, we have that \(|{\widehat {{\mathscr{B}}}({\Sigma }, {w})}|\leq {\sum }_{x,y=0}^{{w}} d({\Sigma },x,y) = (w+1)^{2}\cdot 2^{O(|{\Sigma }|{w}\log w)} = 2^{O(|{\Sigma }|{w} \log {w})}\).

2. 2.

   By a similar analysis we can conclude that for each alphabet Σ, and each \(x,y\in \{0,1,\dots ,{w}\}\) there are at most at most

   $$ n({\Sigma},x,y)=\binom{w}{x}\binom{w}{y}(1+2^{x})(1+2^{y})2^{|{\Sigma}|xy} = 2^{O(|{\Sigma}|w^{2})} $$

   (possibly nondeterministic) layers with x left state, y right states, and transitions labeled with symbols from Σ. The essential differences are that in the nondeterministic case, there are (1 + 2^x) ways of choosing the set of initial states together with the initial flag (because I(B) = ∅ if ι(B) = 0, and I(B) may be an arbitrary subset of ℓ(B) if ι(B) = 1), and that there are 2^|Σ|xy ways of choosing the transition relation T(B) (because there are x left states, and for each such a state q and each symbol a ∈Σ there are 2^y ways of choosing the set of transitions with label a leaving q). Therefore, we have that \(|{{\mathscr{B}}({\Sigma }, {w})}|\leq {\sum }_{x,y=0}^{{w}} n({\Sigma },x,y) = (w+1)^{2}\cdot 2^{O(|{\Sigma }|{w}^{2})} = 2^{O(|{\Sigma }|{w}^{2})}\).

□

Let \({k}\in {{\mathbb {N}}_+}\) and \({D} = {B}_{1}\cdots {B}_{{k}} \in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\). We say that D is deterministic (complete, resp.) if for each i ∈ [k], B_i is a deterministic (complete, resp.) layer. We remark that if D is deterministic, then there exists at most one valid sequence in D for each string in Σ^k. On the other hand, if D is complete, then there exists at least one valid sequence in D for each string in Σ^k.

For each \({k} \in {{\mathbb {N}}_+}\), we denote by \({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\) the subset of \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\) comprising all deterministic, complete (Σ,w)-ODDs of length k. We denote by \({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\) the subset of \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\) comprising all deterministic, complete (Σ,w)-ODDs.

2.2.6 Isomorphism of ODDs

Let Σ be an alphabet, \({w},{k}\in {{\mathbb {N}}_+}\), and let D = B₁⋯B_k and \({{D}^{\prime }} = {{B}^{\prime }}_{1}\cdots {{B}^{\prime }}_{{k}}\) be two ODDs in \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\). An isomorphism from D to \({{D}^{\prime }}\) is a sequence \(\overline {\pi } \doteq \langle {\pi _{0},\ldots ,\pi _{{k}}}\rangle \) of functions that satisfy the following conditions:

1. 1.

   \(\pi _{0}\colon {\ell }({B}_{0})\rightarrow {\ell }({{B}^{\prime }}_{0})\) is a bijection from ℓ(B₀) to \({\ell }({B^{\prime }}_{0})\);

2. 2.

   \(\pi _{0}{|_{{I}({B}_{0})}}\) is a bijection from I(B₀) to \({I}({{B}^{\prime }}_{0})\);

3. 3.

   for each i ∈ [k], \(\pi _{i}\colon {r}({B}_{i})\rightarrow {r}({{B}^{\prime }}_{i})\) is a bijection from r(B_i) to \(r(B^{\prime }_{i})\);

4. 4.

   \(\pi _{{k}}{|_{{F}({B}_{{k}})}}\) is a bijection from F(B_k) to \({F}({B^{\prime }}_{{k}})\);

5. 5.

   for each i ∈ [k], each left state \({\mathfrak {p}}\in {\ell }({B}_{i})\), each symbol σ ∈Σ and each right state \(\mathfrak {q}\in r(B_{i})\), \(({\mathfrak {p},\sigma ,\mathfrak {q}})\in T(B_{i})\) if and only if \(({\pi _{i-1}(\mathfrak {p}),\sigma ,\pi _{i}(\mathfrak {q})})\in T(B^{\prime }_{i})\).

We remark that if \(\overline {\pi } = \langle {\pi _{0},\ldots ,\pi _{{k}}}\rangle \) is an isomorphism from D to \({{D}^{\prime }}\), then the sequence \(\overline {\pi }^{-1} \doteq \langle {\pi _{0}^{-1},\ldots ,\pi _{{k}}^{-1}}\rangle \) is an isomorphism from \({{D}^{\prime }}\) to D, where \(\pi _{i}^{-1}\) denotes the inverse function of π_i for each i ∈⟦k + 1⟧ . We say that D and \({{D}^{\prime }}\) are isomorphic if there exists an isomorphism \(\overline {\pi }\) between D and \({{D}^{\prime }}\). The following proposition is immediate.

Proposition 3

Let Σ be an alphabet, \({w} \in {{\mathbb {N}}_+}\), and let D and \({{D}^{\prime }}\) be two (Σ,w)-ODDs. If D and \({{D}^{\prime }}\) are isomorphic, then \({{\mathscr{L}}({D})} = {{\mathscr{L}}({{D}^{\prime }})}\).

2.2.7 Normalized ODDs.

Let Σ be an alphabet, \({w}\in {{\mathbb {N}}_+}\), and let B be a (Σ,w)-layer. We say that B is reachable if for each right state \({\mathfrak {q}}\in {r}({B})\), there exist a symbol σ ∈Σ and a left state \({\mathfrak {p}}\in {\ell }({B})\) such that \(({{\mathfrak {p}} {\sigma },{\mathfrak {q}}})\) is a transition in T(B). If B is reachable, then we let \(\chi _{{B}} \colon {r}({B}) \rightarrow {\ell }({B}) \times {\Sigma }\) be the function such that for each right state \({\mathfrak {q}} \in {r}({B})\),

where the minimum is taken lexicographically, i.e., for each two left states \({\mathfrak {p}}, {\mathfrak {p}}^{\prime } \in {\ell }({B})\) and each two symbols σ,τ ∈Σ, we have that \(({{\mathfrak {p}},{\sigma }})<({{\mathfrak {p}}^{\prime },{\tau }})\) if and only if \({\mathfrak {p}}<{\mathfrak {p}}^{\prime }\), or \({\mathfrak {p}}={\mathfrak {p}}^{\prime }\) and σ <_Στ. (Recall we are assuming that the alphabet Σ is endowed with a fixed total order \(<_{{\Sigma }}\subseteq {\Sigma }\times {\Sigma }\).) We say that B is well-ordered if it is a reachable, deterministic layer such that for each two right states \({\mathfrak {q}},{\mathfrak {q}}^{\prime }\in {r}({B})\), we have that \({\mathfrak {q}}<{\mathfrak {q}}^{\prime }\) if and only if \(\chi _{{B}}({\mathfrak {q}})<\chi _{{B}}({\mathfrak {q}}^{\prime })\). We say that B is contiguous if ℓ(B) = ⟦w₁⟧ and r(B) = ⟦w₂⟧ for some w₁,w₂ ∈ [w]. Then, we say that B is normalized if it is both well-ordered and contiguous.

Let \({k}\in {{\mathbb {N}}_+}\) and D = B₁⋯B_k be an ODD in \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\). We say that D is reachable/well-ordered/contiguous/normalized if for each i ∈ [k], the layer B_i is reachable/well-ordered/contiguous/normalized. Note that D is normalized if and only if it is both well-ordered and contiguous.

2.2.8 Minimized ODDs

Let Σ be an alphabet, \({w},{k}\in {{\mathbb {N}}_+}\), and let D = B₁⋯B_k be a deterministic, complete ODD in \({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\). We say that D is minimized if for each \({w}^{\prime }\in {{\mathbb {N}}_+}\) and each \({{D}^{\prime }}={{B}^{\prime }}_{1}\cdots {{B}^{\prime }}_{{k}}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w}^{\prime })}^{\protect \circ {{k}}}}\), with \({{\mathscr{L}}({{D}})} = {{\mathscr{L}}({D^{\prime }})}\), we have that \(\mathsf {nSt}({D}) \leq \mathsf {nSt}({{D}^{\prime }})\). In other words, D is minimized if no deterministic, complete ODD with the same language as D has less states than D. The following theorem is the analog of Theorem 1 in the realm of the theory of ordered decision diagrams.

Theorem 4

Let Σ be an alphabet, \({w},{k}\in {{\mathbb {N}}_+}\), and let D be an ODD in \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\). There exists a unique minimized ODD \(\mathcal {C}({{D}}) \in {{\widehat {{\mathscr{B}}}({\Sigma }, 2^{{w}})}^{\protect \circ {{k}}}}\) such that \(\mathcal {C}({{D}})\) is deterministic, complete, normalized and satisfies \({{\mathscr{L}}(\mathcal {C}({{D}}))} = {{\mathscr{L}}({{D}})}\). Additionally, if \({{D}}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\) then \(\mathcal {C}({{D}})\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\).

We call the ODD \(\mathcal {C}({{D}})\) of Theorem 4 the canonical form of D. We note that \(\mathcal {C}({{D}})\) is unique not only up to isomorphism, but also unique up to equality. In particular, this implies that for each alphabet Σ, each \({w},{w}^{\prime },{k}\in {\mathbb {N}}\), and each two ODDs \({{D}}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\) and \({{D}^{\prime }}\in {{{\mathscr{B}}({\Sigma }, {w}^{\prime })}^{\protect \circ {{k}}}}\) with \({{\mathscr{L}}({{D}})} = {{\mathscr{L}}({D^{\prime }})}\), we have that \(\mathcal {C}({{D}}) = \mathcal {C}({{D}^{\prime }})\). The construction of \(\mathcal {C}({{D}})\) follows a similar process to the construction of canonical forms of OBDDs with a fixed variable, or equivalently, read-once oblivious branching programs [37].

2.3 Regular Transductions

Let Σ₁ and Σ₂ be two alphabets. In this work, a (Σ₁,Σ₂)-transduction is a binary relation \(\mathfrak {t}\subseteq {\Sigma }_1^{+}\times {\Sigma }_2^{+}\) where |s| = |u| for each \(({s},{u})\in \mathfrak {t}\). We let

be the image of \(\mathfrak {t}\), and we let

be the domain of \(\mathfrak {t}\). We say that a (Σ₁,Σ₂)-transduction \(\mathfrak {t}\) is functional if, for each string \({s}\in {\Sigma }_1^{+}\), there exists at most one string \({u}\in {\Sigma }_2^{+}\) such that \(({{s},{u}})\in \mathfrak {t}\).

Let Σ₁, Σ₂ and Σ₃ be three (not-necessarily distinct) alphabets. If \(\mathfrak {t}\) is a (Σ₁,Σ₂)-transduction and \(\mathfrak {t}^{\prime }\) is a (Σ₂,Σ₃)-transduction, then the composition of \(\mathfrak {t}\) with \(\mathfrak {t}^{\prime }\) is defined as the (Σ₁,Σ₃)-transduction

For each language \({L}\subseteq {\Sigma }_1^{+}\), we let

be the (Σ₁,Σ₁)-transduction derived from L. Then, for each language \({L}\subseteq {\Sigma }_1^{+}\) and each (Σ₁,Σ₂)-transduction \(\mathfrak {t}\), we let

be the image of L under \(\mathfrak {t}\).

2.3.1 Tensor Product

Let \({\Sigma }_{1},\ldots ,{\Sigma }_{{\mathfrak {a}}}\) be \({\mathfrak {a}}\) alphabets and \({k} \in {{\mathbb {N}}_+}\). For each \(i\in {[{{\mathfrak {a}}}]}\), let s_i = σ_i,1⋯σ_i,k be a string of length k over the alphabet Σ_i. The tensor product of \({s}_{1},\ldots ,{s}_{{\mathfrak {a}}}\) is defined as the string

of length k over the alphabet \({\Sigma }_{1}\times \cdots \times {\Sigma }_{{\mathfrak {a}}}\). For each \(i\in {[{{\mathfrak {a}}}]}\), let \({L}_{i}\subseteq {\Sigma }_{i}^{+}\) be a language over Σ_i. The tensor product of \({L}_{1}, \ldots , {L}_{{\mathfrak {a}}}\) is defined as the language

2.3.2 Regular transductions

For \(\alpha \in {{\mathbb {N}}_+}\), we say that a (Σ₁,Σ₂)-transduction \(\mathfrak {t}\) is α-regular if the language

is α-regular. The following proposition states some straightforward quantitative properties of regular transductions.

Proposition 5

Let Σ₁,Σ₂ and Σ₃ be three alphabets, \(\mathfrak {t}\) be an α-regular (Σ₁,Σ₂)-transduction, \(\mathfrak {t}^{\prime }\) be a β-regular (Σ₂,Σ₃)-transduction, and let \(L\subseteq {\Sigma }_1^{+}\) be a γ-regular language, for some \(\alpha ,\upbeta ,\gamma \in \mathbb {N}_{+}\). The following statements hold.

1. 1.

   The languages \(\mathsf {Im}(\mathfrak {t})\) and \(\mathsf {Dom}(\mathfrak {t})\) are α-regular.

2. 2.

   The composition \(\mathfrak {t}\circ \mathfrak {t}^{\prime }\) is (α⋅β)-regular.

3. 3.

   The transduction \(\mathfrak {d}({L})\) is γ-regular.

4. 4.

   The language \(\mathfrak {t}({L})\) is (γ ⋅ α)-regular.

Proof

Let \({\mathcal {F}}_{\mathfrak {t}}\) be a finite automaton with α states and language \({{{\mathscr{L}}}({\mathcal {F}}_{\mathfrak {t}})}={\mathscr{L}}(\mathfrak {t})\), \({\mathcal {F}}_{\mathfrak {t}^{\prime }}\) be a finite automaton with β states and language \({{{\mathscr{L}}}({\mathcal {F}}_{\mathfrak {t}^{\prime }})}={\mathscr{L}}(\mathfrak {t}^{\prime })\), and let \({\mathcal {F}}_{{L}}\) be a finite automaton with γ states and language \({{{\mathscr{L}}}({\mathcal {F}}_{{L}})}={L}\). Note that, such automata \({\mathcal {F}}_{\mathfrak {t}}\), \({\mathcal {F}}_{\mathfrak {t}^{\prime }}\) and \({\mathcal {F}}_{{L}}\) exist, since by hypothesis \(\mathfrak {t}\) is α-regular, \(\mathfrak {t}^{\prime }\) is β-regular and L is γ-regular, respectively.

1. 1.

   We let \({\mathcal {F}}_{\mathsf {Im}(\mathfrak {t})}\) and \({\mathcal {F}}_{\mathsf {Dom}(\mathfrak {t})}\) be the finite automata over the alphabets Σ₂ and Σ₁, respectively, defined exactly as \(\mathcal {F}_{\mathfrak {t}}\) except for their transition sets, which is defined as follows:

   $$T(\mathcal{F}_{\mathsf{Im}(\mathfrak{t})})= \lbrace{({q,\tau,{q}^{\prime}}) \colon \exists \sigma\in{\Sigma}_1, ({q,({\sigma,\tau}),{q}^{\prime}})\in T(\mathcal{F}_{\mathfrak{t}})}\rbrace\text{, and}$$
   $$ {T}({\mathcal{F}}_{\mathsf{Dom}(\mathfrak{t})})= \lbrace{({{q},{\sigma},{{q}^{\prime}}}) \colon \exists {\tau}\in{\Sigma}_2, ({q,({\sigma,\tau}),{q}^{\prime}})\in T(\mathcal{F}_{\mathfrak{t}})}\rbrace\text{.} $$

   Clearly, \(\mathcal {F}_{\mathsf {Im}(\mathfrak {t})}\) and \(\mathcal {F}_{\mathsf {Dom}(\mathfrak {t})}\) have at most α states each. Moreover, \({\mathcal {F}}_{\mathsf {Im}(\mathfrak {t})}\) accepts a string \({u} \in {\Sigma }_2^{+}\) if and only if there exists a string \({s}\in {\Sigma }_1^{+}\) such that \({s}\otimes {u}\in {\mathscr{L}}(\mathfrak {t})\). Analogously, one can verify that \({\mathcal {F}}_{\mathsf {Dom}(\mathfrak {t})}\) accepts a string \({s} \in {\Sigma }_1^{+}\) if and only if there exists a string \({u}\in {\Sigma }_2^{+}\) such that \({s}\otimes {u}\in {\mathscr{L}}(\mathfrak {t})\). Therefore, the language of \({\mathcal {F}}_{\mathsf {Im}(\mathfrak {t})}\) is \({{{\mathscr{L}}}({\mathcal {F}}_{\mathsf {Im}(\mathfrak {t})})}=\mathsf {Im}(\mathfrak {t})\), and the language of \({\mathcal {F}}_{\mathsf {Dom}(\mathfrak {t})}\) is \({{{\mathscr{L}}}({\mathcal {F}}_{\mathsf {Dom}(\mathfrak {t})})}=\mathsf {Dom}(\mathfrak {t})\).

2. 2.

   We let \({\mathcal {F}}_{\mathfrak {t}\circ \mathfrak {t}^{\prime }}\) be the finite automaton over the alphabet Σ₁ ×Σ₃, with state set \(Q(\mathcal {F}_{\mathfrak {t}\circ \mathfrak {t}^{\prime }})=Q(\mathcal {F}_{\mathfrak {t}})\times Q(\mathcal {F}_{\mathfrak {t}^{\prime }})\), initial state set \(I(\mathcal {F}_{\mathfrak {t}\circ \mathfrak {t}^{\prime }})=I(\mathcal {F}_{\mathfrak {t}})\times I(\mathcal {F}_{\mathfrak {t}^{\prime }})\), final state set \(F(\mathcal {F}_{\mathfrak {t}\circ \mathfrak {t}^{\prime }})=F(\mathcal {F}_{\mathfrak {t}})\times F(\mathcal {F}_{\mathfrak {t}^{\prime }})\) and transition set

   $$ \begin{array}{@{}rcl@{}} {T}({\mathcal{F}}_{\mathfrak{t}\circ\mathfrak{t}^{\prime}})=\lbrace({({{p},{p}^{\prime}}),({{\sigma},{{\tau}^{\prime}}}),({{q},{{q}^{\prime}}})}) \colon \exists {\tau}\in{\Sigma}_2,\\ ({p},({{\sigma},{\tau}}),{q})\in{T}({\mathcal{F}}_{\mathfrak{t}}),({{p}^{\prime},({{\tau},{{\tau}^{\prime}}}),{{q}^{\prime}}})\in{T}({\mathcal{F}}_{\mathfrak{t}^{\prime}})\rbrace\text{.} \end{array} $$

   We remark \({\mathcal {F}}_{\mathfrak {t}\circ \mathfrak {t}^{\prime }}\) is a finite automaton with at most (α ⋅β) states. Moreover, \({\mathcal {F}}_{\mathfrak {t}\circ \mathfrak {t}^{\prime }}\) accepts a string s ⊗ v ∈ (Σ₁ ×Σ₃)⁺ if and only if there exists \({u}\in {\Sigma }_2^{+}\) such that \({s}\otimes {u}\in {\mathscr{L}}(\mathfrak {t})\) and \({u}\otimes {v}\in {\mathscr{L}}(\mathfrak {t}^{\prime })\). Therefore, the language of \({\mathcal {F}}_{\mathfrak {t}\circ \mathfrak {t}^{\prime }}\) is \({{{\mathscr{L}}}({\mathcal {F}}_{\mathfrak {t}\circ \mathfrak {t}^{\prime }})}={\mathscr{L}}(\mathfrak {t}\circ \mathfrak {t}^{\prime })\).

3. 3.

   We let \({\mathcal {F}}_{\mathfrak {d}({L})}\) be the finite automata over the alphabet Σ₁ ×Σ₁ defined exactly as \({\mathcal {F}}_{{L}}\) except for its transition set, which is defined as follows:

   $$ T(\mathfrak{d}({L}))= \lbrace{({q,({\sigma,\sigma}),{q}^{\prime}}) \colon ({q,\sigma,{q}^{\prime}})\in T(\mathcal{F}_{L})}\rbrace\text{.} $$

   Clearly, \(\mathcal {F}_{\mathfrak {d}({L})}\) has at most γ states. Moreover, \(\mathcal {F}_{\mathfrak {d}({L})}\) accepts a string s ⊗ u ∈ (Σ₁ ×Σ₁)⁺ if and only if u = s and \({s}\in {\mathscr{L}}(\mathfrak {t})\). Therefore, the language of \({\mathcal {F}}_{\mathfrak {d}({L})}\) is \({{{\mathscr{L}}}({\mathcal {F}}_{\mathfrak {d}({L})})}={\mathscr{L}}(\mathfrak {d}({L}))\).

4. 4.

   We let \({\mathcal {F}}_{\mathfrak {t}({L})}\) be the finite automaton over the alphabet Σ₁ ×Σ₃ such that \({\mathcal {F}}_{\mathfrak {t}({L})} = {\mathcal {F}}_{\mathsf {Im}(\mathfrak {d}(L)\circ \mathfrak {t})}\). Based on (2)–(4), \(\mathcal {F}_{\mathfrak {t}(L)}\) is a finite automaton with at most (γ ⋅ α) states and with language \({{{\mathscr{L}}}({\mathcal {F}}_{\mathfrak {t}({L})})}=\mathfrak {t}({L})=\mathsf {Im}(\mathfrak {d}({L})\circ \mathfrak {t})\).

□

In this section, we formally define the main object of study of this work, namely, the notion of second-order finite automata.

Definition 6 (Second-Order Finite Automata)

Let Σ be an alphabet and \({w} \in {{\mathbb {N}}_+}\). A finite automaton \({\mathcal {F}}\) over the alphabet \({{\mathscr{B}}({\Sigma }, {w})}\) is called a (Σ,w)-second-order finite automaton (SOFA) if \({{{\mathscr{L}}}({\mathcal {F}})} \subseteq {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\).

In other words, a (Σ,w)-second-order finite automaton \({\mathcal {F}}\) is a finite automaton over the alphabet \({{\mathscr{B}}({\Sigma }, {w})}\) such that each string D = B₁⋯B_k in \({{{\mathscr{L}}}({\mathcal {F}})}\) is a (Σ,w)-ODD, for some \({k}\in {{\mathbb {N}}_+}\).

From now on, for every (Σ,w)-second-order finite automaton \({\mathcal {F}}\), we may refer to \({{{\mathscr{L}}}({\mathcal {F}})}\) as the first language of \({\mathcal {F}}\). Since each string \({{D}}\in {{{\mathscr{L}}}({\mathcal {F}})}\) is a (Σ,w)-ODD, we can also associate with \({\mathcal {F}}\) a second language, denoted by \({{{\mathscr{L}}}_{2}({\mathcal {F}})}\), which consists of the set of languages accepted by ODDs in \({{{\mathscr{L}}}({\mathcal {F}})}\). More precisely, the second language of a (Σ,w)-second-order finite automaton \({\mathcal {F}}\) is defined as the set

Note that \({{{\mathscr{L}}}_{2}({\mathcal {F}})}\) is a possibly infinite subset of \(\bigcup _{{k}\in {{\mathbb {N}}_+}} \mathcal {P}_{{k}}({\Sigma })\). We say that a subset \(\mathcal {X} \subseteq \bigcup _{{k}\in {{\mathbb {N}}_+}} \mathcal {P}_{{k}}({\Sigma })\) is regular-decisional if there is a second-order finite automaton \({\mathcal {F}}\) such that \(\mathcal {X} = {{{\mathscr{L}}}_{2}({\mathcal {F}})}\).

Lemma 7

Let Σ be an alphabet and \({w}\in {{\mathbb {N}}_+}\). For each \(\mathcal {S}\subseteq {{\mathscr{B}}({\Sigma }, {w})}\), there exists a (Σ,w)-second-order finite automaton \({\mathcal {F}}_{\mathcal {S}}\) with \((\lvert {\mathcal {S}}\rvert +1)\) states such that \({{\mathscr{L}}({\mathcal {F}}_{\mathcal {S}})}\) \(= \mathcal {S}^{\circledast }\).

Proof

Let \({\mathcal {F}}_{\mathcal {S}}\) be the (Σ,w)-second-order finite automaton over the alphabet \(\mathcal {S}\), with state set \({Q}({\mathcal {F}}_{\mathcal {S}}) = \lbrace {{q}}\rbrace \cup \lbrace {{q}_{{B}} \colon {B} \in \mathcal {S}}\rbrace \), initial state set \({I}({\mathcal {F}}_{\mathcal {S}}) = \lbrace {{q}}\rbrace \), final state set \({F}({\mathcal {F}}_{\mathcal {S}}) = \lbrace {{q}_{{B}} \in {Q}({\mathcal {F}}_{\mathcal {S}}) \colon {\phi }({B}) = 1}\rbrace \ \) and transition set \( {T}({\mathcal {F}}_{\mathcal {S}}) = \lbrace ({q},{B}, {q}_{{B}}) \colon {B}\) \( \in \mathcal {S}, {\iota }({B}) = 1\rbrace \cup \lbrace ({{q}_{{B}}, {B}, {q}_{{{B}^{\prime }}}}) \colon {B}, {{B}^{\prime }} \in \mathcal {S}, {\ell }({{B}^{\prime }}) = {r}({B}), {\phi }({B}) =\) \( 0, {\iota }({{B}^{\prime }}) = 0\rbrace \text {.} \) Since each transition is labeled with some element from \(\mathcal {S}\), it should be clear that \({{\mathscr{L}}({\mathcal {F}}_{\mathcal {S}})} \subseteq \mathcal {S}^{\circledast }\). Now, let \({k}\in {\mathbb {N}}\) and \({{D}} = {B}_{1}{B}_{2}{\dots } {B}_{k}\) be an ODD in \(\mathcal {S}^{\circledast }\). Then it should be clear that the sequence of transitions \(({{q}, {B}_{1}, {q}_{{B}_{1}}}) ({q}_{{B}_{1}}, {B}_{2}, {q}_{{B}_{2}}) \dots \) \( ({q}_{{B}_{{{k}}-1}},\) \( {B}_{{k}}, {q}_{{B}_{{k}}})\) is an accepting sequence in \({\mathcal {F}}_{\mathcal {S}}\). This implies that \({{\mathscr{L}}({\mathcal {F}}_{\mathcal {S}})} \supseteq \mathcal {S}^{\circledast }\). □

The following Corollary is an immediate consequence of Lemma 7 and Observation 2.

Corollary 8

Let Σ be an alphabet, and \({w} \in {{\mathbb {N}}_+}\).

1. 1.

   The (Σ,w)-SOFA \({\mathcal {F}}_{{{\mathscr{B}}({\Sigma }, {w})}}\) has \(2^{O(|{\Sigma }|\cdot {w}^{2})}\) states and \({\mathscr{L}}(\mathcal {F}_{{\mathscr{B}}({\Sigma },{w})}) = {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\).

2. 2.

   The (Σ,w)-SOFA \({\mathcal {F}}_{{\widehat {{\mathscr{B}}}({\Sigma }, {w})}}\) has \(2^{O(|{\Sigma }|\cdot {w}\log {w})}\) states and \({\mathscr{L}}(\mathcal {F}_{\widehat {{\mathscr{B}}}({\Sigma },{w})}) = \widehat {{\mathscr{B}}}({\Sigma },{w})^{\protect \circledast }\).

Example 1

The Even Language

In Fig. 2, we depict a ({0,1},2)-second-order finite automaton \({{\mathcal {F}}}\) whose second language consists of all (length-typed) sets

of all binary strings of length k with an even number of occurrences of the symbol ‘1’, for each \({k}\in {{\mathbb {N}}_+}\). Note that, for each \({k}\in {{\mathbb {N}}_+}\), \({{\mathcal {F}}}\) accepts a unique ({0,1},2)-ODD of length k, whose language is Even_k. In particular, the language Even₅ is represented by the ODD depicted in Fig. 1, which is accept by \({\mathcal {F}}\) upon following the sequence of states q₀,q₁,q₁,q₁,q₂.

Example 2

The Hypercube Language.

The hypercube of dimension k can be defined as the graph H_k with vertex set V (H) = {0,1}^k and edge set

Intuitively, vertices of the hypercube H_k are strings in {0,1}^k and edges are pairs of strings from {0,1}^k that differ in exactly one position. From a formal language standpoint, the edge set of the graph H_k can be encoded by the language

Note that, \(\hat {H}_{{k}}\) is a language over the alphabet {0,1}^×2.

In Fig. 3, we depict a ({0,1}^×2,2)-second-order finite automaton \({\mathscr{H}}\) whose second language is \({{{\mathscr{L}}}_{2}({\mathscr{H}})} = \lbrace {\hat {H}_{{k}} \colon {k}\in {{\mathbb {N}}_+}}\rbrace \). Similarly to the second-order finite automaton illustrated in the previous example, for each \({k}\in {{\mathbb {N}}_+}\), \({\mathscr{H}}\) accepts a unique ({0,1}^×2,2)-ODD D_k of length k, whose language is \(\hat {H}_{{k}}\). In particular, the language \(\hat {H}_{5}\) is represented by the ODD D₅ depicted in Fig. 4, which is accept by \({\mathscr{H}}\) upon following the sequence of states q₀,q₁,q₁,q₁,q₂.

3.1 Main Results

The main result of this work (Theorem 10) states that second order finite automata can be canonized with respect to their second languages. In other words, there is an algorithm that sends each SOFA \({\mathcal {F}}\) to a SOFA \(\mathcal {C}_{2}({\mathcal {F}})\) with \({{\mathscr{L}}_{2}({\mathcal {F}})} = {{\mathscr{L}}_{2}(\mathcal {C}_{2}({\mathcal {F}}))}\) in such a way that \(\mathcal {C}_{2}({\mathcal {F}})=\mathcal {C}_{2}({\mathcal {F}}^{\prime })\) for any SOFA \({\mathcal {F}}^{\prime }\) with the same second language as \({\mathcal {F}}\). Indeed, \(\mathcal {C}_{2}({\mathcal {F}})\) satisfies the following interesting property: \({{{\mathscr{L}}}(\mathcal {C}_{2}({\mathcal {F}}))} = \{\mathcal {C}({{D}}) : {{D}} \in {{{\mathscr{L}}}({\mathcal {F}})}\}\). Here, for each ODD D, \(\mathcal {C}({{D}})\) denotes the unique deterministic, complete, normalized and minimized ODD with the same language as D, as specified in Theorem 4. In other words, the first language of \(\mathcal {C}_{2}({\mathcal {F}})\) is precisely the set of canonical forms of ODDs in the first language of \({\mathcal {F}}\).

We note that even though \({\mathcal {F}}\) and \(\mathcal {C}_{2}({\mathcal {F}})\) have the same second language, i.e. \({{\mathscr{L}}_{2}(\mathcal {C}_{2}({\mathcal {F}}))} = {{\mathscr{L}}_{2}({\mathcal {F}})}\), the first languages of \({\mathcal {F}}\) and \(\mathcal {C}_{2}({\mathcal {F}})\) may differ. In other words, it may be the case that \({{{\mathscr{L}}}(\mathcal {C}_{2}({\mathcal {F}}))} \neq {{{\mathscr{L}}}({\mathcal {F}})}\). As a simple example for this observation, let D be an ODD in \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\) for some alphabet Σ and \({w}\in {{\mathbb {N}}_+}\). Let \({\mathcal {F}}_{{{D}}}\) be the second order finite automaton such that \({{{\mathscr{L}}}({\mathcal {F}}_{{{D}}})} = \{{{D}}\}\). Then the language \({{{\mathscr{L}}}(\mathcal {C}_{2}({\mathcal {F}}_{{{D}}}))} =\{\mathcal {C}({{D}})\}\) is distinct from \({{{\mathscr{L}}}({\mathcal {F}}_{{{D}}})}\) whenever \(\mathcal {C}({{D}}) \neq {{D}}\). Therefore, canonization of a finite automaton \({\mathcal {F}}\) with respect to its second language \({{{\mathscr{L}}}_{2}({\mathcal {F}})}\) cannot be achieved by simply canonizing \({\mathcal {F}}\) with respect to its first language \({{{\mathscr{L}}}({\mathcal {F}})}\) according to Theorem 1.

The proof of our main result is a direct consequence of the following theorem, stating that the traditional minimization and canonization algorithm for ODDs can be simulated in terms of functional regular transductions.

Theorem 9 (Canonization as Transduction Theorem)

Let Σ be an alphabet and let \({w}\in {{\mathbb {N}}_+}\).

1. 1.

   The functional transduction \(\mathfrak {can}[{\Sigma },{w}] = \lbrace {({{{D}},\mathcal {C}({{D}})}) \colon {{D}}\in {{\mathscr{B}}({\Sigma },{w})^{\protect \circledast }}}\rbrace \) is \(2^{O(|{\Sigma }|\cdot w \cdot 2^{w})}\)-regular.

2. 2.

   The functional transduction \(\widehat {\mathfrak {can}}[{\Sigma },{w}] = \lbrace {({{{D}},\mathcal {C}({{D}})}) \colon {{D}}\in {\widehat {{\mathscr{B}}}({\Sigma },{w})^{\protect \circledast }}}\rbrace \) is \(2^{O(|{\Sigma }|\cdot w\cdot \log w)}\)-regular.

Intuitively, the transduction \(\mathfrak {can}[{\Sigma },{w}]\) is obtained as a composition of regular transductions that simulate the application of the usual steps in the canonization of a single ODD: determinization, elimination of unreachable states, merging of equivalent states and normalization. The transduction \(\widehat {\mathfrak {can}}[{\Sigma },{w}]\) is obtained by a similar process, except that one may skip the application of the determinization transduction, yielding in this way, a more efficient construction. Due to its technical nature, the proof of Theorem 9 will be postponed to Section 6. Next, we show how Theorem 9 can be used to provide a canonization procedure for second order finite automata. Later, in Section 5, we will provide some algorithmic applications of this theorem in the realm of the theory of ODDs of bounded width.

Theorem 10 (Canonical Form of Canonical Forms Theorem)

Let Σ be an alphabet (endowed with a total order <_Σ ⊂Σ×Σ), \({w}\in {{\mathbb {N}}_+}\), and let \({\mathcal {F}}\) be a (Σ,w)-SOFA. One can construct in time \(2^{\mathsf {nSt}({\mathcal {F}})\cdot 2^{{\mathcal {O}}(\lvert {{\Sigma }}\rvert \cdot {w}\cdot 2^{{w}})}}\) a deterministic, complete, normalized (Σ,2^w)-SOFA \(\mathcal {C}_{2}({\mathcal {F}})\) satisfying the following properties.

1. 1.

   \({{{\mathscr{L}}}(\mathcal {C}_{2}({\mathcal {F}}))} = \lbrace {\mathcal {C}({{D}}) \colon {{D}} \in {{{\mathscr{L}}}({\mathcal {F}})}}\rbrace \);

2. 2.

   \({{\mathscr{L}}_{2}(\mathcal {C}_{2}({\mathcal {F}}))}= {{{\mathscr{L}}}_{2}({\mathcal {F}})}\);

3. 3.

   For each \({w}^{\prime } \in {{\mathbb {N}}_+}\) and each \(({\Sigma },{w}^{\prime })\)-SOFA \({\mathcal {F}}^{\prime }\), if \({{{\mathscr{L}}}_{2}({\mathcal {F}}^{\prime })} = {{{\mathscr{L}}}_{2}({\mathcal {F}})}\), then \(\mathcal {C}_{2}({\mathcal {F}}^{\prime })= \mathcal {C}_{2}({\mathcal {F}})\).

Proof

Let \({\mathcal {F}}\) be a (Σ,w)-SOFA and \(\mathfrak {can}[{\Sigma },{w}]\) be the \(({{\mathscr{B}}({\Sigma }, {w})},{\widehat {{\mathscr{B}}}({\Sigma }, {w})})\)-transduction specified in Theorem 9. Then, the image of \({{{\mathscr{L}}}({\mathcal {F}})}\) under the transduction \(\mathfrak {can}[{\Sigma },{w}]\) is the language \(\mathfrak {can}[{\Sigma },{w}]({{{\mathscr{L}}}({\mathcal {F}})}) = \{\mathcal {C}({{D}}) : {{D}} \in {{{\mathscr{L}}}({\mathcal {F}})}\}\). Here, for each ODD \({{D}}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\), \(\mathcal {C}({{D}})\in {{\widehat {{\mathscr{B}}}({\Sigma }, 2^{{w}})}^{\protect \circledast }}\) denotes the unique ODD with minimum number of states such that \(\mathcal {C}({{D}})\) is deterministic, complete, normalized and satisfies \({{\mathscr{L}}(\mathcal {C}({{D}}))} = {{\mathscr{L}}({{D}})}\), as specified in Theorem 4. Since \(\mathfrak {can}[{\Sigma },{w}]\) is \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\)-regular, it follows from Proposition 5.(4), that one can construct a (Σ,2^w)-SOFA \({\mathcal {F}}^{\dagger }\) with \(\mathsf {nSt}({\mathcal {F}})\cdot 2^{{\mathcal {O}}(|{\Sigma }|\cdot {w}\cdot 2^{{w}})}\) states such that \({{{\mathscr{L}}}({\mathcal {F}}^{\dagger })} = \mathfrak {can}[{\Sigma },{w}]({{{\mathscr{L}}}({\mathcal {F}})})\). Now, let \(\mathcal {C}({\mathcal {F}}^{\dagger })\) be the unique finite automaton with minimum number of states such that \(\mathcal {C}({\mathcal {F}}^{\dagger })\) is deterministic, complete, normalized and satisfies \({{{\mathscr{L}}}(\mathcal {C}({\mathcal {F}}^{\dagger }))} = {{{\mathscr{L}}}({\mathcal {F}}^{\dagger })}\), as specified in Theorem 1. Then \(\mathcal {C}({\mathcal {F}}^{\dagger })\) can be constructed in time \(2^{\mathsf {nSt}\cdot 2^{{\mathcal {O}}(|{\Sigma }|\cdot {w}\cdot 2^{{w}})}}\) by applying the standard power-set construction to \({\mathcal {F}}^{\dagger }\), followed by a DFA minimization algorithm, such as Hopcroft’s algorithm. Now, by defining \(\mathcal {C}_{2}({\mathcal {F}})\) as \(\mathcal {C}({\mathcal {F}}^{\dagger })\), we have that \({{{\mathscr{L}}}(\mathcal {C}_{2}({\mathcal {F}}))} = \lbrace {\mathcal {C}({{D}}) \colon {{D}} \in {{{\mathscr{L}}}({\mathcal {F}})}}\rbrace \), and therefore, Condition 1 is satisfied. This immediately implies that \({{\mathscr{L}}_{2}(\mathcal {C}_{2}({\mathcal {F}}))}= {{{\mathscr{L}}}_{2}({\mathcal {F}})}\), since each ODD \({{D}}\in {{{\mathscr{L}}}({\mathcal {F}})}\) has the same language as its canonical form \(\mathcal {C}({{D}})\) in \({{{\mathscr{L}}}(\mathcal {C}_{2}({\mathcal {F}}))}\). Therefore, Condition 2 is also satisfied. Finally, \(\mathcal {C}_{2}({\mathcal {F}}) = \mathcal {C}_{2}({\mathcal {F}}^{\prime })\) for any \(({\Sigma },{w}^{\prime })\)-SOFA \({\mathcal {F}}^{\prime }\) satisfying \({{\mathscr{L}}_{2}({\mathcal {F}}^{\prime })}= {{\mathscr{L}}_{2}({\mathcal {F}})}\), since for any two ODDs \({{D}}\in {{{\mathscr{L}}}({\mathcal {F}})}\) and \({{D}}^{\prime }\in {{{\mathscr{L}}}({\mathcal {F}}^{\prime })}\), \({{\mathscr{L}}({{D}})} = {{\mathscr{L}}({{D}}^{\prime })}\) if and only if \(\mathcal {C}({{D}}) = \mathcal {C}({{D}}^{\prime })\). Therefore, Condition 3 is also satisfied. □

Let \({\mathcal {F}}\) be a (Σ,w)-SOFA. We call the (Σ,2^w)-SOFA \(\mathcal {C}_{2}({\mathcal {F}})\) specified in Theorem 10 the second canonical form of \({\mathcal {F}}\). We note that if all ODDs in the language \({\mathcal {F}}\) are deterministic and complete, then \(\mathcal {C}_{2}({\mathcal {F}})\) is actually a (Σ,w)-SOFA, and a faster canonization algorithm can be obtained, since in this case, the transduction \(\mathfrak {can}[{\Sigma },{w}]\) used in the proof of Theorem 10 can be replaced by the transduction \(\widehat {\mathfrak {can}}[{\Sigma },{w}]\), which is \(2^{O(|{\Sigma }|\cdot {w}\cdot \log {w})}\)-regular.

Observation 11

If \({\mathcal {F}}\) is a (Σ,w)-SOFA such that \({{{\mathscr{L}}}({\mathcal {F}})}\subseteq {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\), then \(\mathcal {C}_{2}({\mathcal {F}})\) is also a (Σ,w)-SOFA and can be constructed in time \(2^{\mathsf {nSt}({\mathcal {F}})\cdot 2^{{\mathcal {O}}(\lvert {{\Sigma }}\rvert \cdot {w}\log {w})}}\).

An immediate consequence of Theorem 9 and of Proposition 5.(1) is that for each alphabet Σ, and each \({w}\in {{\mathbb {N}}_+}\), the set of canonical forms of ODDs in \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\) is a regular set. The same holds for the set of canonical forms of ODDs in \({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\).

Corollary 12

Let Σ be an alphabet and \({w}\in {{\mathbb {N}}_+}\).

1. 1.

   The language \(\mathsf {Im}(\mathfrak {can}[{\Sigma },{w}]) = \{\mathcal {C}({{D}}) : {{D}}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\}\) is \(2^{O(|{\Sigma }|\cdot w\cdot 2^{w})}\)-regular.

2. 2.

   The language \(\mathsf {Im}(\widehat {\mathfrak {can}}[{\Sigma },{w}]) = \{\mathcal {C}({{D}}) : {{D}}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\}\) is \(2^{O(|{\Sigma }|\cdot w\cdot \log w)}\)-regular.

4.1 Basic Closure Properties

Theorem 10 implies that regular-decisional subsets of \(\bigcup _{{k}\in {{\mathbb {N}}_+}} \mathcal {P}_{{k}}({\Sigma })\) are closed under Boolean operations such as union, intersection and even a suitable notion of bounded width complementation. These closure properties are formally stated in Theorem 13 below. Let Σ be an alphabet and \({w}\in {{\mathbb {N}}_+}\). We denote by

the set of all sets of strings accepted by some deterministic, complete (Σ,w)-ODD. Moreover, given a subset \(\mathcal {S} \subseteq \bigcup _{{k}\in {{\mathbb {N}}_+}} \mathcal {P}_{{k}}({\Sigma })\), we denote by \(\overline {\mathcal {S}}^{{w}}\doteq \mathsf {Det}({\Sigma },{w}) \backslash \mathcal {S}\) the width-w complement of \(\mathcal {S}\).

Theorem 13

Let Σ be an alphabet, \({w}\in {{\mathbb {N}}_+}\), and let \({\mathcal {F}}\), \({\mathcal {F}}_{1}\) and \({\mathcal {F}}_{2}\) be (Σ,w)-second-order finite automata. The following statements hold.

1. 1.

   There is a (Σ,2^w)-second-order finite automaton \({\mathsf {intersec}_{2}({\mathcal {F}}_{1},{\mathcal {F}}_{2})}\) such that

   $$ \mathcal{L}_{2}({\mathsf{intersec}_{2}({\mathcal{F}_{1}}{\mathcal{F}_{2}})}) = \mathcal{L}_{2}({\mathcal{F}_{1}}) \cap \mathcal{L}_{2}({\mathcal{F}_{2}})\text{.} $$
2. 2.

   There is a (Σ,2^w)-second-order finite automaton \({\mathsf {union}_{2}({\mathcal {F}}_{1},{\mathcal {F}}_{2})}\) such that

   $$ \mathcal{L}_{2}({\mathsf{union}_{2}({\mathcal{F}_{1}}{\mathcal{F}_{2}})}) = \mathcal{L}_{2}({\mathcal{F}_{1}}) \cup \mathcal{L}_{2}({\mathcal{F}_{2}})\text{.} $$
3. 3.

   There is a (Σ,2^w)-second-order finite automaton \({\mathsf {diff}_{2}({\mathcal {F}}_{1},{\mathcal {F}}_{2})}\) such that

   $$ \mathcal{L}_{2}({\mathsf{diff}_{2}({\mathcal{F}_{1}}{\mathcal{F}_{2}})}) = \mathcal{L}_{2}({\mathcal{F}_{1}}) \backslash \mathcal{L}_{2}({\mathcal{F}_{2}})\text{.} $$
4. 4.

   There is a (Σ,w)-second-order finite automaton \({\mathcal {F}}({\Sigma },{w})\) such that

   $$ \mathcal{L}_{2}({\mathcal{F}({\Sigma},w)}) = \mathsf{Det}({\Sigma},{w})\text{.} $$
5. 5.

   For each \({w}^{\prime }\in {{\mathbb {N}}_+}\), there is a \(({\Sigma },2^{\max \limits \lbrace {{w},{w}^{\prime }}\rbrace })\)-second-order finite automaton \({\mathsf {compl}_{2}({\mathcal {F}},{w}^{\prime })}\) such that

   $$ {{\mathcal{L}}_{2}({\mathsf{compl}_{2}({\mathcal{F}},{w}^{\prime})})} = \overline{{{\mathcal{L}}_{2}({\mathcal{F}})}}^{{w}^{\prime}}\text{.} $$
6. 6.

   It is decidable whether \({{{\mathscr{L}}}_{2}({\mathcal {F}}_{1})}\cap {{{\mathscr{L}}}_{2}({\mathcal {F}}_{2})} = \emptyset \).

7. 7.

   It is decidable whether \({{{\mathscr{L}}}_{2}({\mathcal {F}}_{1})}\subseteq {{{\mathscr{L}}}_{2}({\mathcal {F}}_{2})}\).

Proof

Let \({\mathcal {F}}_{1}^{\prime }=\mathcal {C}_{2}({\mathcal {F}}_{1})\) and \({\mathcal {F}}_{2}^{\prime }=\mathcal {C}_{2}({\mathcal {F}}_{2})\) be the second canonical forms specified in Theorem 10 of the automata \({\mathcal {F}}_{1}\) and \({\mathcal {F}}_{2}\), respectively. It is well-known that regular languages are closed under intersection, union and complementation [26]. Consequently, there exist finite automata \({\mathsf {intersec}_{1}({\mathcal {F}}_{1}^{\prime },{\mathcal {F}}_{2}^{\prime })}\), \({\mathsf {union}_{1}({\mathcal {F}}_{1}^{\prime },{\mathcal {F}}_{2}^{\prime })}\) and \({\mathsf {compl}_{1}({\mathcal {F}}_{2}^{\prime })}\) over the alphabet \({\widehat {{\mathscr{B}}}({\Sigma }, 2^{{w}})}\), such that

\({{{\mathscr{L}}}({\mathsf {union}_{1}({\mathcal {F}}_{1}^{\prime },{\mathcal {F}}_{2}^{\prime })})} = {{{\mathscr{L}}}({\mathcal {F}}_{1}^{\prime })} \cup {{{\mathscr{L}}}({\mathcal {F}}_{2}^{\prime })}\) and \({{{\mathscr{L}}}({\mathsf {compl}_{1}({\mathcal {F}}_{2}^{\prime })})} = {\widehat {{\mathscr{B}}}({\Sigma }, 2^{{w}})}^{*} \setminus {{{\mathscr{L}}}({\mathcal {F}}_{2}^{\prime })}\).

Clearly,

Thus, \({\mathsf {union}_{2}({\mathcal {F}}_{1},{\mathcal {F}}_{2})} = {\mathsf {union}_{1}({\mathcal {F}}_{1}^{\prime },{\mathcal {F}}_{2}^{\prime })}\) is a (Σ,2^w)-second-order finite automaton with second language

Moreover, owing to the fact that any two ODDs with the same language have the same canonical form, one can verify that

Thus, \({\mathsf {intersec}_{2}({\mathcal {F}}_{1},{\mathcal {F}}_{2})} = {\mathsf {intersec}_{1}(\mathcal {F}_{1}^{\prime },\mathcal {F}_{2}^{\prime })}\) is a (Σ,2^w)-second-order finite automata with second language

Furthermore, we have that \({\mathsf {diff}_{2}({\mathcal {F}}_{1},{\mathcal {F}}_{2})} = {\mathsf {intersec}_{2}({\mathcal {F}}_{1},{\mathsf {compl}_{1}({\mathcal {F}}_{2}^{\prime })})}\) is a (Σ,2^w)-second-order finite automata with first language

Thus, since ODDs with the same language have the same canonical form, the second language of \({\mathsf {diff}_{2}({\mathcal {F}}_{1},{\mathcal {F}}_{2})}\) is

Based on Lemma 7, we let \({\mathcal {F}}({\Sigma },{w}) = {\mathcal {F}}_{\mathcal {S}}\) be the (Σ,w)-second-order finite automaton over the alphabet \(\mathcal {S}\), where \(\mathcal {S}={\widehat {{\mathscr{B}}}({\Sigma }, {w})}\). One can readily verify that \({{{\mathscr{L}}}_{2}({\mathcal {F}}({\Sigma },{w}))} =\mathsf {Det}({\Sigma },{w})\).

Now, let \({\mathcal {F}}^{\prime }=\mathcal {C}_{2}({\mathcal {F}})\) be the second canonical form specified in Theorem 10 of the automaton \({\mathcal {F}}\). For each \({w}^{\prime }\in {{\mathbb {N}}_+}\), we let \({\mathsf {compl}_{2}({\mathcal {F}},{w}^{\prime })} = {\mathsf {diff}_{2}({\mathcal {F}}({\Sigma },{w}^{\prime }),{\mathcal {F}}^{\prime })}\). It is straightforward that \({\mathsf {compl}_{2}({\mathcal {F}},{w}^{\prime })}\) is a \(({\Sigma },2^{\max \limits \lbrace {{w},{w}^{\prime }}\rbrace })\)-second-order finite automaton with second language

Finally, we note that deciding whether \({{{\mathscr{L}}}_{2}({\mathcal {F}}_{1})}\cap {{{\mathscr{L}}}_{2}({\mathcal {F}}_{2})}=\emptyset \) is equivalent to deciding whether \({{{\mathscr{L}}}({\mathcal {F}}_{1}^{\prime })}\cap {{{\mathscr{L}}}({\mathcal {F}}_{2}^{\prime })}=\emptyset \). Similarly, we have that deciding whether \({{{\mathscr{L}}}_{2}({\mathcal {F}}_{1})}\subseteq {{{\mathscr{L}}}_{2}({\mathcal {F}}_{2})}\) is equivalent to deciding whether \({{{\mathscr{L}}}({\mathcal {F}}_{1}^{\prime })}\subseteq {{{\mathscr{L}}}({\mathcal {F}}_{2}^{\prime })}\), which in turn is equivalent to deciding whether

Therefore, since disjointness of regular languages is a decidable problem [26], we obtain that the problems of verifying whether \({{{\mathscr{L}}}_{2}({\mathcal {F}}_{1})}\cap {{{\mathscr{L}}}_{2}({\mathcal {F}}_{2})}=\emptyset \) and verifying whether \({{{\mathscr{L}}}_{2}({\mathcal {F}}_{1})}\subseteq {{{\mathscr{L}}}_{2}({\mathcal {F}}_{2})}\) are both decidable. □

We note that all binary operations described in Theorem 13 are also defined when \({\mathcal {F}}_{1}\) is a (Σ,w₁)-second-order finite automaton and \({\mathcal {F}}_{2}\) is a (Σ,w₂)-second-order finite automaton, for distinct positive integers w₁ and w₂. Indeed, it suffices to view both finite automata as \(({\Sigma },\max \limits \lbrace {{w}_{1},{w}_{2}}\rbrace )\)-second-order finite automata. We also note that the SOFAs \({\mathsf {intersec}_{2}({\mathcal {F}}_{1},{\mathcal {F}}_{2})}\), \({\mathsf {union}_{2}({\mathcal {F}}_{1},{\mathcal {F}}_{2})}\) and \({\mathsf {diff}_{2}({\mathcal {F}}_{1},{\mathcal {F}}_{2})}\) are actually (Σ,w)-SOFAs if all ODDs in the languages \({{{\mathscr{L}}}({\mathcal {F}}_{1})}\) and \({{{\mathscr{L}}}({\mathcal {F}}_{2})}\) are deterministic and complete, since in this case one can use the more efficient construction given in Observation 11. Finally, it is worth remarking that non-emptiness of intersection of the second languages of SOFAs is not only decidable, but can be achieved in fixed-parameter tractable time (Observation 14).

Observation 14

Let Σ be an alphabet, and \({w}\in {{\mathbb {N}}_+}\) and \({\mathcal {F}}_{1}\) and \({\mathcal {F}}_{2}\) be (Σ,w)-SOFAs.

1. 1.

   One can determine whether \({{{\mathscr{L}}}_{2}({\mathcal {F}}_{1})}\cap {{{\mathscr{L}}}_{2}({\mathcal {F}}_{2})}\neq \emptyset \) in time \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot \mathsf {nSt}({\mathcal {F}}_{1})\cdot \mathsf {nSt}({\mathcal {F}}_{2})\).

2. 2.

   If all ODDs in \({{{\mathscr{L}}}({\mathcal {F}}_{1})}\) and \({{{\mathscr{L}}}({\mathcal {F}}_{2})}\) are deterministic and complete, then one one can can determine whether \({\mathscr{L}}_{2}({\mathcal {F}_{1}})\cap {\mathscr{L}}_{2}({\mathcal {F}_{2}})\neq \emptyset \) in time \(2^{O(|{\Sigma }|\cdot w \cdot \log w)}\cdot \mathsf {nSt}(\mathcal {F}_{1})\cdot \mathsf {nSt}(\mathcal {F}_{2})\).

Proof

Since \(\mathfrak {can}[{\Sigma },{w}]\) is \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\)-regular, for each i ∈{1,2}, one can construct from \({\mathcal {F}}_{i}\) a finite automaton \({\mathcal {F}}_{i}^{\prime }\) with \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot \mathsf {nSt}({\mathcal {F}}_{i})\) states such that \({{{\mathscr{L}}}({\mathcal {F}}_{i}^{\prime })} = \mathfrak {can}[{\Sigma },{w}]({{{\mathscr{L}}}({\mathcal {F}}_{i})}) = \{\mathcal {C}({{D}}) : {{D}}\in {{{\mathscr{L}}}({\mathcal {F}}_{i})}\}\). Therefore, testing whether \({{{\mathscr{L}}}_{2}({\mathcal {F}}_{1})} \cap {{{\mathscr{L}}}_{2}({\mathcal {F}}_{2})}\neq \emptyset \) is equivalent to testing whether \({{{\mathscr{L}}}({\mathcal {F}}_{1}^{\prime })}\cap {{{\mathscr{L}}}({\mathcal {F}}_{2}^{\prime })}\neq \emptyset \), which can be done in time \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot \mathsf {nSt}({\mathcal {F}}_{1})\cdot \mathsf {nSt}({\mathcal {F}}_{2})\). If the languages of the automata \({\mathcal {F}}_{1}\) and \({\mathcal {F}}_{2}\) only contain deterministic, complete ODDs, then one can apply a similar argument using the transduction \(\widehat {\mathfrak {can}}[{\Sigma },{w}]\) instead of \(\mathfrak {can}[{\Sigma },{w}]\) to infer that non-emptiness of intersection for the languages \({{{\mathscr{L}}}_{2}({\mathcal {F}}_{1})}\) and \({{{\mathscr{L}}}_{2}({\mathcal {F}}_{2})}\) can be tested in time \(2^{O(|{\Sigma }|\cdot {w} \cdot \log {w})}\cdot \mathsf {nSt}({\mathcal {F}}_{1})\cdot \mathsf {nSt}({\mathcal {F}}_{2})\). □

4.2 Closure Properties Specific for Language Classes

In this subsection, we show that regular-decisional classes of languages are also closed under operations that are specific to language classes. Let Σ₁ and Σ₂ be alphabets, and \(g:{\Sigma }_{1}\rightarrow {\Sigma }_{2}\) be a map from Σ₁ to Σ₂. Given languages \({L}\subseteq {\Sigma }_{1}^{+}\) and \(L^{\prime }\subseteq {\Sigma }_{2}^{+}\), we let

and

The following lemma from [15] states that several operations that are effective for regular languages may be realized on ODDs using maps that act layerwisely. Below, for ODDs \({{D}}={B}_{1}{B}_{2}\dots {B}_{{k}}\) and \({{D}}^{\prime } = {B}_{1}^{\prime }{B}_{2}^{\prime }\dots {B}_{{k}}^{\prime }\), we let \({{D}}\otimes {{D}}^{\prime } = ({B}_{1},{B}_{1}^{\prime })({B}_{2},{B}_{2}^{\prime }){\dots } ({B}_{{k}},{B}_{{k}}^{\prime })\).

Lemma 15 (Simulation Lemma (see Lemma 2 of 15))

Let Σ₁ and Σ₂ be alphabets, \({w}_{1},{w}_{2}\in {{\mathbb {N}}_+}\), and \(g:{\Sigma }_{1}\rightarrow {\Sigma }_{2}\) be a map from Σ₁ to Σ₂. There exist maps

1. 1.

   \(f_{\cup }:{{\mathscr{B}}({\Sigma }_{1}, {w}_{1})}\times {{\mathscr{B}}({\Sigma }_{2}, {w}_{2})} \rightarrow {{\mathscr{B}}({\Sigma }_{1}\cup {\Sigma }_{2}, {w}_{1}+{w}_{2})}\),

2. 2.

   \(f_{\cap }:{{\mathscr{B}}({\Sigma }_{1}, {w}_{1})}\times {{\mathscr{B}}({\Sigma }_{2}, {w}_{2})} \rightarrow {{\mathscr{B}}({\Sigma }_{1}\cup {\Sigma }_{2}, {w}_{1}\cdot {w}_{2})}\),

3. 3.

   \(f_{\otimes }:{{\mathscr{B}}({\Sigma }_{1}, {w}_{1})}\times {{\mathscr{B}}({\Sigma }_{2}, {w}_{2})} \rightarrow {{\mathscr{B}}({\Sigma }_{1}\times {\Sigma }_{2}, {w}_{1}\cdot {w}_{2})}\),

4. 4.

   \(f_{g}:{{\mathscr{B}}({\Sigma }_{1}, {w}_{1})}\rightarrow {{\mathscr{B}}({\Sigma }_{2}, {w}_{1})}\),

5. 5.

   \(f_{g^{-1}}:{{\mathscr{B}}({\Sigma }_{2}, {w}_{2})}\rightarrow {{\mathscr{B}}({\Sigma }_{1}, {w}_{2})}\),

6. 6.

   \(f_{\neg }:{\widehat {{\mathscr{B}}}({\Sigma }_{1}, {w}_{1})}\rightarrow {\widehat {{\mathscr{B}}}({\Sigma }_{1}, {w}_{1})}\),

such that for each (Σ₁,w₁)-ODD \({{D}}={B}_{1}{B}_{2}{\dots } {B}_{{k}}\), each (Σ₂,w₂)-ODD \({{D}}^{\prime } = {B}_{1}^{\prime }{B}_{2}^{\prime }\dots {B}_{{k}}^{\prime }\), and each deterministic, complete (Σ₁,w₁)-ODD \({{D}}^{\prime \prime }={B}_{1}^{\prime \prime }{B}_{2}^{\prime \prime }\dots {B}_{{k}}^{\prime \prime }\), the following hold.

1. 1.

   \(f_{\cup }({{D}} \otimes {{D}}^{\prime }) \doteq f_{\cup }({B}_{1},{B}_{1}^{\prime })f_{\cup }({B}_{2},{B}_{2}^{\prime }){\dots } f_{\cup }({B}_{{k}},{B}_{{k}}^{\prime })\) is a (Σ₁ ∪Σ₂,w₁ + w₂)-ODD such that

   $$ {\mathcal{L}(f_{\cup}({{D}} \otimes {{D}}^{\prime}))} = {\mathcal{L}({{D}})}\cup {\mathcal{L}({{D}}^{\prime})}. $$
2. 2.

   \(f_{\cap }({{D}} \otimes {{D}}^{\prime }) \doteq f_{\cap }({B}_{1},{B}_{1}^{\prime })f_{\cap }({B}_{2},{B}_{2}^{\prime }){\dots } f_{\cap }({B}_{{k}},{B}_{{k}}^{\prime })\) is a (Σ₁ ∪Σ₂,w₁ ⋅ w₂)-ODD such that

   $$ {\mathcal{L}(f_{\cap}({{D}} \otimes {{D}}^{\prime}))} = {\mathcal{L}({{D}})} \cap {\mathcal{L}({{D}}^{\prime})}. $$
3. 3.

   \(f_{\otimes }({{D}} \otimes {{D}}^{\prime }) \doteq f_{\otimes }({B}_{1},{B}_{1}^{\prime })f_{\otimes }({B}_{2},{B}_{2}^{\prime }){\dots } f_{\otimes }({B}_{{k}},{B}_{{k}}^{\prime })\) is a (Σ₁ ×Σ₂,w₁ ⋅ w₂)-ODD such that

   $$ {\mathcal{L}(f_{\otimes}({{D}} \otimes {{D}}^{\prime}))} = {\mathcal{L}({{D}})}\otimes {\mathcal{L}({{D}}^{\prime})}. $$
4. 4.

   \(f_{g}({{D}}) \doteq f_{g}({B}_{1})f_{g}({B}_{2}){\dots } f_{g}({B}_{{k}})\) is a (Σ₂,w₁)-ODD such that

   $$ {\mathcal{L}(f_{g}({{D}}))} = g({\mathcal{L}({{D}})}). $$
5. 5.

   \(f_{g^{-1}}({{D}}^{\prime }) \doteq f_{g^{-1}}({B}_{1}^{\prime })f_{g^{-1}}({B}_{2}^{\prime }){\dots } f_{g^{-1}}({B}_{{k}}^{\prime })\) is a (Σ₁,w₂)-ODD such that

   $$ {\mathcal{L}(f_{g^{-1}}({{D}}^{\prime}))} = g^{-1}({\mathcal{L}({{D}})}). $$
6. 6.

   \(f_{\neg }({{D}}) \doteq f_{\neg }({B}_{1}^{\prime \prime })f_{\neg }({B}_{2}^{\prime \prime }){\dots } f_{\neg }({B}_{{k}}^{\prime \prime })\) is a deterministic, complete (Σ₁,w)-ODD such that

   $$ {\mathcal{L}(f_{\neg}({{D}}))} = {\Sigma}^{k} \backslash {\mathcal{L}({{D}})}. $$

Lemma 15 immediately implies implies that the collection of regular-decisional classes of languages is effectively closed under several pointwise operations, as stated in the next corollary.

Corollary 16

Let Σ₁ and Σ₂ be alphabets, \({w}_{1},{w}_{2}\in {{\mathbb {N}}_+}\), \(g:{\Sigma }_{1}\rightarrow {\Sigma }_{2}\) be a map from Σ₁ to Σ₂, \({\mathcal {F}}\) be a (Σ₁,w₁)-SOFA, and \({\mathcal {F}}^{\prime }\) be a (Σ₂,w₂)-SOFA.

1. 1.

   Pointwise union. There is a SOFA \({\mathcal {F}}\dot {\cup }{\mathcal {F}}^{\prime }\) such that

   $$ {{\mathcal{L}}_{2}({\mathcal{F}}\dot{\cup}{\mathcal{F}}^{\prime})} = \{{\mathcal{L}({{D}})}\cup {\mathcal{L}({{D}}^{\prime})} : {{D}} \in {{\mathcal{L}}({\mathcal{F}})}, {D}^{\prime}\in {{\mathcal{L}}({\mathcal{F}}^{\prime})}, \mathsf{len}({{D}})=\mathsf{len}({{D}}^{\prime})\}. $$
2. 2.

   Pointwise intersection. There is a SOFA \({\mathcal {F}}\dot {\cap }{\mathcal {F}}^{\prime }\),

   $$ {{\mathcal{L}}_{2}({\mathcal{F}}\dot{\cap}{\mathcal{F}}^{\prime})} = \{{\mathcal{L}({{D}})}\cap {\mathcal{L}({{D}}^{\prime})} : {{D}}\in {{\mathcal{L}}({\mathcal{F}})}, {{D}}^{\prime}\in {{\mathcal{L}}({\mathcal{F}}^{\prime})}, \mathsf{len}({{D}})=\mathsf{len}({{D}}^{\prime})\}. $$
3. 3.

   Pointwise tensor product. There is a SOFA \({\mathcal {F}}\dot {\otimes }{\mathcal {F}}^{\prime }\),

   $$ {{\mathcal{L}}_{2}({\mathcal{F}}\dot{\otimes}{\mathcal{F}}^{\prime})} = \{{\mathcal{L}({{D}})}\otimes {\mathcal{L}({{D}}^{\prime})} : {{D}} \in {{\mathcal{L}}({\mathcal{F}})}, {{D}}^{\prime} \in {{\mathcal{L}}({\mathcal{F}}^{\prime})}, \mathsf{len}({{D}})=\mathsf{len}({{D}}^{\prime})\}. $$
4. 4.

   Pointwise map. There is a SOFA \(\dot {g}({\mathcal {F}})\) such that

   $$ {{\mathcal{L}}_{2}(\dot{g}({\mathcal{F}}))} = \{g({\mathcal{L}({{D}})}) : {{D}}\in {{\mathcal{L}}({\mathcal{F}})}\}. $$
5. 5.

   Pointwise inverse map: There is a SOFA \(\dot {g}^{-1}({\mathcal {F}}^{\prime })\) such that

   $$ {{\mathcal{L}}_{2}(\dot{g}^{-1}({\mathcal{F}}^{\prime}))} = \{g^{-1}({\mathcal{L}({{D}})}) : {{D}}\in {{\mathcal{L}}({\mathcal{F}}^{\prime})}\}. $$
6. 6.

   Pointwise negation: There is a SOFA \(\dot {\neg } {\mathcal {F}}\) such that

   $$ {{\mathcal{L}}_{2}(\dot{\neg}{\mathcal{F}})} = \{ ({k},{\Sigma}^{{k}})\backslash {\mathcal{L}({{D}})} : {{D}}\in {{\mathcal{L}}({\mathcal{F}})}, \mathsf{len}({{D}})={k}\}. $$

Proof

The proof follows directly from the fact that regular languages are closed under maps, together with Lemma 15. The SOFAs \(\dot {g}({\mathcal {F}})\), \(\dot {g}^{-1}({\mathcal {F}})\), and \(\dot {\neg }{\mathcal {F}}\) are obtained from \({\mathcal {F}}\) by replacing each transition \(({q},{B},{q}^{\prime })\) with the transitions \(({q},f_{g}({B}),{q}^{\prime })\), \(({q},f_{g^{-1}}({B}),{q}^{\prime })\), and \(({q},f_{\neg }({B}),{q}^{\prime })\) respectively. For the binary operations, we first compute a finite automaton \({\mathcal {F}}\otimes {\mathcal {F}}^{\prime }\) over the alphabet \({{\mathscr{B}}({\Sigma }_{1}, {w}_{1})}\times {{\mathscr{B}}({\Sigma }_{2}, {w}_{2})}\) that accepts a string \({{D}}\otimes {{D}}^{\prime } = ({B}_{1},{B}_{1}^{\prime })({B}_{2},{B}_{2}^{\prime }){\dots } ({B}_{{k}},{B}_{{k}}^{\prime })\) if and only if \({{D}}={B}_{1}{B}_{2}\dots {B}_{{k}}\) is accepted by \({\mathcal {F}}\) and \({{D}}^{\prime } = {B}_{1}^{\prime }{B}_{2}^{\prime }\dots {B}_{{k}}\) is accepted by \({\mathcal {F}}^{\prime }\). Subsequently we define \({\mathcal {F}}\dot {\cup }{\mathcal {F}}^{\prime }\), \({\mathcal {F}}\dot {\cap }{\mathcal {F}}^{\prime }\) and \({\mathcal {F}}{\dot \otimes }{\mathcal {F}}^{\prime }\) by replacing each transition \(({q},({B},{B}^{\prime }),{q}^{\prime })\) of \({\mathcal {F}}\otimes {\mathcal {F}}^{\prime }\) with the transitions \(({q},f_{\cup }({B},{B}^{\prime }),{q}^{\prime })\), \(({q},f_{\cap }({B},{B}^{\prime }),{q}^{\prime })\), and \(({q},f_{\otimes }({B},{B}^{\prime }),{q}^{\prime })\) respectively.

We exemplify how Lemma 15 can be used to complete the proof with the first item. The others follow an analogous argument. From the construction of \({\mathcal {F}}\dot {\cup }{\mathcal {F}}^{\prime }\), we have that \({{D}}\in {{{\mathscr{L}}}({\mathcal {F}})}\) and \({{D}}^{\prime }\in {{{\mathscr{L}}}({\mathcal {F}}^{\prime })}\) are such that \(\mathsf {len}({{D}})=\mathsf {len}({{D}}^{\prime })\) if and only if \(f_{\cup }({{D}}\otimes {{D}}^{\prime })\) belongs to \({{{\mathscr{L}}}({\mathcal {F}}\dot {\cup }{\mathcal {F}}^{\prime })}\). Since \({{\mathscr{L}}(f_{\cup }({{D}}\otimes {{D}}^{\prime }))} = {{\mathscr{L}}({{D}})}\cup {{\mathscr{L}}({{D}}^{\prime })}\), we have that \({{{\mathscr{L}}}_{2}({\mathcal {F}}\dot {\cup }{\mathcal {F}}^{\prime })} = \{{{\mathscr{L}}({{D}})}\cup {{\mathscr{L}}({{D}}^{\prime })} : {{D}}\in {{{\mathscr{L}}}({\mathcal {F}})}, {{D}}^{\prime }\in {{{\mathscr{L}}}({\mathcal {F}}^{\prime })}, \mathsf {len}(D)=\mathsf {len}(D^{\prime })\}\). □

In this section, we show that Theorems 9 and Theorem 10 can be used to provide novel algorithmic applications in the realm of the theory of ODDs of bounded width, and therefore also in the realm of the theory of ordered binary decision diagrams (OBDDs) of bounded width. In Section 5.1 we will show that several minimization problems for deterministic and nondeterministic ODDs can be solved in fixed parameter tractable time when parameterized by width. Subsequently, in Section 5.2 we will show that the problem of counting the number of distinct functions computable by some ODD of length k and width w can be solved in time h(|Σ|,w) ⋅ k^O(1) for a suitable \(h:{\mathbb {N}}\times {\mathbb {N}}\rightarrow {\mathbb {N}}\).

5.1 Width and Size Minimization of Nondeterministic ODDs

Models of computation comprised by ODDs of constant width have been studied in a variety of fields, such as symbolic computation, machine learning and property testing [3, 21, 33, 35]. In this section, we show that width minimization for ODDs is fixed-parameter tractable in the width parameter. Additionally, the space of ODDs where the minimization will take place may be selected as the language \({{{\mathscr{L}}}({\mathcal {F}})}\) of a given second-order finite automaton \({\mathcal {F}}\). Furthermore, if such a minimum width ODD \({{D}}^{\prime }\) with \({{\mathscr{L}}({{D}})}={{\mathscr{L}}({{D}}^{\prime })}\) exists in \({{{\mathscr{L}}}({\mathcal {F}})}\), then one can furthermore impose that \({{D}}^{\prime }\) has minimum number of states or minimum number of transitions.

As important special cases, if we set \({\mathcal {F}}\) to be the finite automaton accepting the language \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\) the minimization occurs in the space of all (possibly nondeterministic) ODDs of width at most w, while by setting \({\mathcal {F}}\) to be the finite automaton accepting the language \({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\), the minimization takes place over the space of deterministic, complete ODDs of width at most w.

Lemma 17

Let Σ be an alphabet, \({w}\in {{\mathbb {N}}_+}\), D be a (Σ,w)-ODD, and \({\mathcal {F}}\) be a (Σ,w)-SOFA. One can construct in time \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot \mathsf {nSt}({\mathcal {F}})\cdot {k}\) an acyclic (Σ,w)-SOFA \(X({{\mathcal {F}}}{{{D}}})\) with \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot \mathsf {nSt}({\mathcal {F}})\cdot {k}\) states such that \({{{\mathscr{L}}}(X({{\mathcal {F}}}{{{D}}}))} = \{{{D}}^{\prime }\in {{{\mathscr{L}}}({\mathcal {F}})} : {{\mathscr{L}}({{D}})} = {{\mathscr{L}}({{D}}^{\prime })}\}\).

Proof

Let \({\mathcal {F}}\) be a (Σ,w)-SOFA, and \({{D}} \in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\). Consider the \(({\widehat {{\mathscr{B}}}({\Sigma }, 2^{{w}})},\) \({{\mathscr{B}}({\Sigma }, {w})})\)-transduction \(\mathfrak {t}_{{{D}}} = \{(\mathcal {C}({{D}}),{{D}})\}\). Note that \(\mathfrak {t}_{{{D}}}\) is a singleton, and therefore, it is (k + 1)-regular, since the language \({L}(\mathfrak {t}_{{{D}}}) = \{\mathcal {C}({{D}})\otimes {{D}}\}\) is accepted by a finite automaton \(\hat {{\mathcal {F}}}\) with (k + 1) states \(\{{q}_{0},\dots ,{q}_{{k}}\}\). Here, q₀ is the unique initial state and q_k is the unique final state. Indeed, let \(\mathcal {C}({{D}}) = {B}_{1}^{\prime }{B}_{2}^{\prime }\dots {B}_{{k}}^{\prime }\). Note that this canonical form can be constructed in time 2^O(w) ⋅|Σ|⋅ k by applying the standard minimization algorithm for a single ODD (Theorem 4). Then, for each \(i\in \{0,\dots ,{k}-1\}\), the automaton has a unique transition leaving q_i, namely, the transition \(({q}_{i}, ({B}_{i}^{\prime },{B}_{i}) ,{q}_{i+1})\). It should be clear that \(\mathcal {C}({{D}})\otimes {{D}} = ({B}_{1}^{\prime },{B}_{1})({B}_{2}^{\prime },{B}_{2})\dots ({B}_{{k}}^{\prime },\)B_k). is the only string accepted by \(\hat {{\mathcal {F}}}\).

Now consider the transduction \(\mathfrak {can}[{\Sigma },{w}]\). Since this transduction is \(2^{O(|{\Sigma }|\cdot {w}\cdot 2^{{w}})}\)-regular (Theorem 9), it follows from Proposition 5.(2) that the transduction

is \((2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot {k})\)-regular, and therefore, the language

is \((2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot {k})\)-regular. Additionally, an automaton \({\mathcal {F}}^{\prime }\) accepting \(\mathsf {Dom}(\mathfrak {can}[{\Sigma },{w}]\circ \mathfrak {t}_{{{D}}})\) can be constructed in time \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot {k}\). This implies that one can construct in time \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot \mathsf {nSt}({\mathcal {F}})\cdot {k}\) a finite automaton \(X({{\mathcal {F}}}{{{D}}})\) with \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot \mathsf {nSt}({\mathcal {F}})\cdot {k}\) states accepting the language \(\mathsf {Dom}(\mathfrak {can}[{\Sigma },{w}]\circ \mathfrak {t}_{{{D}}}) \cap {{{\mathscr{L}}}({\mathcal {F}}_{{{D}}})} = \{{{D}}^{\prime }\in {{{\mathscr{L}}}({\mathcal {F}})} : {{\mathscr{L}}({{D}})} = {{\mathscr{L}}({{D}}^{\prime })}\}\). Since all ODDs accepted by \(X({{\mathcal {F}}}{{{D}}})\) have length k, we may assume that this automaton is acyclic, where the set of states is partitioned into a sequence of levels, and transitions can only exist from a given level to the next level in the sequence. □

Let \(\oplus :{\mathbb {N}} \times {\mathbb {N}} \rightarrow {\mathbb {N}}\) be a commutative, associative binary operation (typically \(\max \limits \) or + ), and \(\omega :{{\mathscr{B}}({\Sigma }, {w})}\rightarrow {\mathbb {N}}\) be a weighting function. Then the weight of an ODD \({{D}}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\) is defined as \(\omega _{\oplus }({{D}}) = \bigoplus _{i=1}^{{k}}\omega ({B}_{i})\).

Proposition 18

Let \(\omega :{{\mathscr{B}}({\Sigma }, {w})}\rightarrow {\mathbb {N}}\) be a fixed weighting function on the alphabet \({{\mathscr{B}}({\Sigma }, {w})}\) and \(\oplus :{\mathbb {N}} \times {\mathbb {N}} \rightarrow {\mathbb {N}}\) be one of the operations + or \(\max \limits \). Let \(\mathcal {J}\) be a (Σ,w)-SOFA and \(a\in {\mathbb {N}}\). Then, in time \(O(|\mathcal {J}|\cdot \log |\mathcal {J}| \cdot \log a)\), one can determine whether there is an ODD of weight at most a in \({{{\mathscr{L}}}(\mathcal {J})}\), and if yes, construct an ODD \({{D}}\in {{{\mathscr{L}}}(\mathcal {J})}\) of minimum weight. The time complexity can be improved to \(O(|\mathcal {J}|\cdot \log a)\) if \(\mathcal {J}\) is acyclic.

Proof

Let G = (V,E,γ) be the weighted directed graph with vertex set \(V={Q}(\mathcal {J})\), edge set \(E = \{({q},{q}^{\prime }) : \exists {B}\in {{\mathscr{B}}({\Sigma }, {w})}, ({q},{B},{q}^{\prime })\in {T}(\mathcal {J})\}\), and weighting function γ such that for each edge \(({q},{q}^{\prime })\in E\), \(\gamma ({q},{q}^{\prime }) = \{\min \limits \{\omega ({B})\} : ({q},{B},{q}^{\prime })\in {T}(\mathcal {J}), \omega ({B})\leq a\}\). Then there is an ODD \({{D}}\in {{{\mathscr{L}}}(\mathcal {J})}\) of weight at most a if and only if the weight of a shortest (weighted) path from some initial state q to some final state \({q}^{\prime }\) of \(\mathcal {J}\) is at most a. Let \(q_{0}q_{1}{\dots } q_{{k}}\) be such a shortest path. Then any ODD \({{D}} = {B}_{1}{B}_{2}\dots {B}_{{k}}\) where \(({q}_{i-1},{B},{q}_{i})\in {T}(\mathcal {J})\) for all i ∈ [k] is a valid solution. Using standard algorithms, the time for computing a shortest path is upper bounded by \(O((|E|+|V|\log |V|)\log a) = O(|{\mathcal {F}}| \cdot \log |{\mathcal {F}}| \cdot \log a)\). If by \(\mathcal {J}\) is acyclic, then this running time can be improved to \(O((|V|+|E|)\log a) = O(|{\mathcal {F}}|\cdot \log a)\). □

By combining Lemma 17 with Proposition 18 we obtain the following theorem.

Theorem 19

Let D be an ODD in \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\) and let \({\mathcal {F}}\) be a (Σ,w)-SOFA. One can determine in time \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot \mathsf {nSt}({\mathcal {F}})\cdot {k}\) whether there is an ODD \({{D}}^{\prime }\in {{{\mathscr{L}}}({\mathcal {F}})}\) such that \({{\mathscr{L}}({{D}}^{\prime })} = {{\mathscr{L}}({{D}})}\). Suppose such an ODD exists.

1. 1.

   One can construct in time \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot \mathsf {nSt}({\mathcal {F}})\cdot {k}\) an ODD \({{D}}^{\prime }\in {{{\mathscr{L}}}({\mathcal {F}})}\) of minimum width such that \({\mathscr{L}}({D}) = {\mathscr{L}}({D^{\prime }})\).

2. 2.

   One can construct in time \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot \mathsf {nSt}({\mathcal {F}})\cdot {k}\cdot \log {k}\) an ODD \({{D}}^{\prime }\in {{{\mathscr{L}}}({\mathcal {F}})}\) with minimum number of states such that \({\mathscr{L}}({D}) = {\mathscr{L}}({D^{\prime }})\).

3. 3.

   One can construct in time \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot \mathsf {nSt}({\mathcal {F}})\cdot {k}\cdot \log {k}\) an ODD \({{D}}^{\prime }\in {{{\mathscr{L}}}({\mathcal {F}})}\) with minimum number of transitions such that \({\mathscr{L}}({D}) = {\mathscr{L}}({D^{\prime }})\).

Proof

1. 1.

   In Proposition 18, set \(\mathcal {J} = X({{\mathcal {F}}}{{{D}}})\), a = w, \(\oplus (x,y) = \max \limits \{x,y\}\), and for each \({B}\in {{\mathscr{B}}({\Sigma }, {w})}\) set ω(B) = w(B). Then for each \({{D}}^{\prime }\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\), ω_⊕(D) = w(D). Therefore, by Proposition 18, one can construct in time \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot \mathsf {nSt}({\mathcal {F}})\cdot {k}\) an ODD \({{D}}^{\prime }\in {{{\mathscr{L}}}({\mathcal {F}})}\) of minimum width such that \({{\mathscr{L}}({{D}}^{\prime })} = {{\mathscr{L}}({{D}})}\).

2. 2.

   In Proposition 18, set \(\mathcal {J} = X({{\mathcal {F}}}{{{D}}})\), a = w ⋅ (k + 1), ⊕ (x,y) = x + y, and for each \({B}\in {{\mathscr{B}}({\Sigma }, {w})}\) set ω(B) = |ℓ(B)| + ϕ(B) ⋅|r(B)|. Then for each \({{D}}^{\prime }\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\), ω_⊕(D) = nSt(D). Therefore, by Proposition 18, one can construct in time \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot \mathsf {nSt}({\mathcal {F}})\cdot {k}\cdot \log {k}\) an ODD \({{D}}^{\prime }\in {{{\mathscr{L}}}({\mathcal {F}})}\) with minimum number of states such that \({{\mathscr{L}}({{D}}^{\prime })} = {{\mathscr{L}}({{D}})}\).

3. 3.

   In Proposition 18, set \(\mathcal {J} = X({{\mathcal {F}}}{{{D}}})\), a = |Σ|⋅ w² ⋅ k, ⊕ (x,y) = x + y, and for each \({B}\in {{\mathscr{B}}({\Sigma }, {w})}\) set ω(B) = |T(B)|. Then for each \({{D}}^{\prime }\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\), ω_⊕(D) = nTr(D). Therefore, by Proposition 18, one can construct in time \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot \mathsf {nSt}({\mathcal {F}})\cdot {k}\cdot \log {k}\) an ODD \({{D}}^{\prime }\in {{{\mathscr{L}}}({\mathcal {F}})}\) with minimum number of transitions such that \({{\mathscr{L}}({{D}}^{\prime })} = {{\mathscr{L}}({{D}})}\).

□

Let \(\mathcal {S}\subseteq {{\mathscr{B}}({\Sigma }, {w})}\). Then by plugging \({\mathcal {F}}_{\mathcal {S}}\) in Theorem 19, the following theorem, which can be used to address several minimization problems for ODDs over the space of ODDs in \(\mathcal {S}^{\circledast }\).

Theorem 20

Let D be an ODD in \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\) and let \(\mathcal {S}\subseteq {{\mathscr{B}}({\Sigma }, {w})}\). One can determine in time \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot {k}\) whether there is an ODD \({{D}}^{\prime }\in \mathcal {S}^{\circ {k}}\) such that \({{\mathscr{L}}({{D}}^{\prime })} = {{\mathscr{L}}({{D}})}\). Suppose such an ODD exists.

1. 1.

   One can construct in time \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})} \cdot {k}\) an ODD \({{D}}^{\prime }\in \mathcal {S}^{\circledast }\) of minimum width such that \({{\mathscr{L}}({D})} = {{\mathscr{L}}(D^{\prime })}\).

2. 2.

   One can construct in time \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot {k}\cdot \log {k}\) an ODD \({{D}}^{\prime }\in \mathcal {S}^{\circledast }\) with minimum number of states such that \({\mathscr{L}}({D}) = {\mathscr{L}}({D^{\prime }})\).

3. 3.

   One can construct in time \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\cdot {k} \cdot \log {k}\) an ODD \({{D}}^{\prime }\in \mathcal {S}^{\circledast }\) with minimum number of transitions such that \({\mathscr{L}}({D}) = {\mathscr{L}}({D^{\prime }})\).

5.2 Counting Functions Computable by ODDs of a Given Width.

Let Σ be an alphabet and \({w},{k}\in {{\mathbb {N}}_+}\). Each ODD \({{D}}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\) can be regarded as a representation of a function \(f_{{{D}}}:{\Sigma }^{{k}}\rightarrow \lbrace {0,1}\rbrace \). More precisely, for each s ∈Σ^k, f_D(s) = 1 if and only if \({s}\in {{\mathscr{L}}({{D}})}\). We say that f_D is the function computed by D.

In this subsection, we analyze the problem of counting the number of functions of type \({\Sigma }^{{k}}\rightarrow \{0,1\}\) that can be computed by some ODD of width w over the alphabet Σ. We note that to solve this problem it is not enough to count the number of ODDs in \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\). The caveat is that several ODDs in \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\) may represent the same function. Fortunately, we can solve the issue of multiple representatives for a given function by resorting to our canonical form of canonical forms theorem (Theorem 10).

It is well known that the problem of counting the number of strings of length k accepted by a given deterministic finite automaton \(\mathcal {A}\) can be solved in time polynomial in k and in the number of states of \(\mathcal {A}\). Below we state a more precise upper bound.

Proposition 21

Let \(\mathcal {A}\) be a deterministic finite automaton over an alphabet Γ. Then, for each \({k}\in {\mathbb {N}}\), one can count in time \(O(\mathsf {nSt}(\mathcal {A})\cdot {k}^{2}\cdot |{\Gamma }|\cdot \log |{\Gamma }|)\) the number of words of length k accepted by \(\mathcal {A}\).

Proof

Let \(\mathcal {A} = ({\Gamma },{Q},{I},{F},{T})\). Since \(\mathcal {A}\) is deterministic, I = {q₀} for some state q₀. Additionally, there is a bijection from the set words of length k accepted by \(\mathcal {A}\) to the set accepting sequences of transitions connecting the initial state q₀ to some final state in F.

We start by constructing a matrix \(M:\llbracket {{k}}\rrbracket \times {Q}\rightarrow {\mathbb {N}}\) such that for each i ∈ k and each q ∈ Q, the entry M(i,q) is equal to the number of valid sequences of transitions of length k − i from q to some final state in F. In particular, M(0,q₀) is the number of valid sequences of transitions of length k from q₀ to some final state in F. The matrix M is constructed by induction on k − i. In the base case, i = k. In this case, we set M(k,q) = 1 if q ∈ F, and set M(k,q) = 0 otherwise. Now, let i ⟦k − 1⟧ and assume that the value M(i + 1,q) has been determined for every q ∈ Q. Then, for each q ∈ Q, we let \(M(i,{q}) = {\sum }_{({q},{\sigma },{q}^{\prime })\in {T}} M(i+1,{q}^{\prime })\). In other words, M(i,q) is defined as the sum of all \(M(i,{q}^{\prime })\) for which \(({q},{\sigma },{q}^{\prime })\) is a transition in \(\mathcal {A}\) for some σ ∈Γ.

Since, there are at most |Γ|^k words of length k, we have that each entry of M can be represented using \({k}\cdot \log |{\Gamma }|\) bits. Additionally, the computation of each entry involves the summation of |Γ| entries, which in overall can be performed in time \(O({k}\cdot |{\Gamma }|\cdot \log {\Gamma })\). Since the matrix has \(({k}+1) \cdot \mathsf {nSt}(\mathcal {A})\) entries, the whole matrix can be constructed in time \(O(\mathsf {nSt}(\mathcal {A})\cdot {k}^{2}\cdot |{\Gamma }|\cdot \log |{\Gamma }|)\). □

Theorem 22

Let \({\mathcal {F}}\) be a (Σ,w)-second order finite automaton. For each \({k}\in {\mathbb {N}}\), one can count in time \(2^{\mathsf {nSt}({\mathcal {F}})\cdot 2^{{\mathcal {O}}(\lvert {{\Sigma }}\rvert \cdot {w}\cdot 2^{{w}})}}\cdot {k}^{2}\) the number of functions \(f:{\Sigma }^{{k}}\rightarrow \{0,1\}\) computable by some ODD of length k in \({{{\mathscr{L}}}({\mathcal {F}})}\).

Proof

By Theorem 10, one can construct in time \(2^{\mathsf {nSt}({\mathcal {F}})\cdot 2^{{\mathcal {O}}(\lvert {{\Sigma }}\rvert \cdot {w}\cdot 2^{{w}})}}\) a deterministic second-order finite automaton \(\mathcal {C}_{2}({\mathcal {F}})\) (with at most \(2^{\mathsf {nSt}({\mathcal {F}})\cdot 2^{{\mathcal {O}}(\lvert {{\Sigma }}\rvert \cdot {w}\cdot 2^{{w}})}}\) states) such that \({{{\mathscr{L}}}(\mathcal {C}_{2}({\mathcal {F}}))} = \{\mathcal {C}({{D}}) : {{D}}\in {{{\mathscr{L}}}({\mathcal {F}})}\}\). This implies that for each language \({L} \in {{\mathscr{L}}_{2}({\mathcal {F}})}\), there is a unique ODD \({{D}}\in {{{\mathscr{L}}}(\mathcal {C}_{2}({\mathcal {F}}))}\) such that \({{\mathscr{L}}({{D}})}={L}\). Therefore, counting the number of functions of type \({\Sigma }^{{w}}\rightarrow \{0,1\}\) computable by some ODD in \({{{\mathscr{L}}}({\mathcal {F}})}\) amounts to counting the number of ODDs of length k accepted by \(\mathcal {C}_{2}({\mathcal {F}})\). By setting \(\mathcal {A} = \mathcal {C}_{2}({\mathcal {F}})\) and \({\Gamma } = {{\mathscr{B}}({\Sigma }, 2^{{w}})}\) in Proposition 21, and by using the facts that \(|\mathcal {A}| = 2^{\mathsf {nSt}({\mathcal {F}})\cdot 2^{{\mathcal {O}}(\lvert {{\Sigma }}\rvert \cdot {w}\cdot 2^{{w}})}}\) and \(|{\Gamma }| = 2^{O(|{\Sigma }|\cdot 2^{{w}}\cdot {w})}\), we have that this counting problem can be solved in time \(2^{\mathsf {nSt}({\mathcal {F}})\cdot 2^{{\mathcal {O}}(\lvert {{\Sigma }}\rvert \cdot {w}\cdot 2^{{w}})}} \cdot {k}^{2}\). □

If all ODDs in the language of \({\mathcal {F}}\) are deterministic and complete then one can adapt the proof of Theorem 22 by using Observation 11 and by setting \({\Gamma } = {\widehat {{\mathscr{B}}}({\Sigma }, {w})}\) in order to obtain a more efficient counting algorithm.

Observation 23

Let \({\mathcal {F}}\) be a (Σ,w)-second order finite automaton such that \({{{\mathscr{L}}}({\mathcal {F}})}\subseteq {\widehat {{\mathscr{B}}}({\Sigma }, {w})}\). For each \({k}\in {\mathbb {N}}\), one can count in time \(2^{\mathsf {nSt}({\mathcal {F}})\cdot 2^{{\mathcal {O}}(\lvert {{\Sigma }}\rvert \cdot {w}\cdot \log {w})}}\cdot {k}^{2}\) the number of functions \(f:{\Sigma }^{{k}}\rightarrow \{0,1\}\) computable by some ODD of length k in \({{{\mathscr{L}}}({\mathcal {F}})}\).

By combining Lemma 7 with Theorem 22 and Observation 23, we obtain the following corollary.

Corollary 24

Let Σ be an alphabet, \({w} \in {{\mathbb {N}}_+}\), \(\mathcal {S}\subseteq {{\mathscr{B}}({\Sigma }, {w})}\), and \(\widehat {\mathcal {S}}\subseteq {\widehat {{\mathscr{B}}}({\Sigma }, {w})}\).

1. 1.

   One can count in time \(2^{2^{{\mathcal {O}}(\lvert {{\Sigma }}\rvert \cdot {w}\cdot 2^{{w}})}}\cdot {k}^{2}\) the number of functions \(f:{\Sigma }^{{k}}\rightarrow \{0,1\}\) computable by some ODD in \(\mathcal {S}^{\circledast }\).

2. 2.

   One can count in time \(2^{2^{{\mathcal {O}}(\lvert {{\Sigma }}\rvert \cdot {w}\cdot \log {w})}}\cdot {k}^{2}\) the number of functions \(f:{\Sigma }^{{k}}\rightarrow \{0,1\}\) computable by some ODD in \(\widehat {\mathcal {S}}^{\circledast }\).

Proof

By Lemma 7, one can construct SOFAs \({\mathcal {F}}_{\mathcal {S}}\) and \({\mathcal {F}}_{\widehat {\mathcal {S}}}\) with \((|\mathcal {S}|+1)\) and \((|\widehat {\mathcal {S}}|+1)\) states respectively such that \({{{\mathscr{L}}}({\mathcal {F}}_{\mathcal {S}})} = \mathcal {S}^{\circledast }\), and \({{{\mathscr{L}}}({\mathcal {F}}_{\widehat {\mathcal {S}}})} = \widehat {\mathcal {S}}^{\circledast }\). Since \(|\mathcal {S}| = 2^{O(|{\Sigma }|{w}^{2})}\), it follows from Theorem 22 that one can count the number of functions \(f:{\Sigma }^{{k}}\rightarrow \{0,1\}\) computable by ODDs in \(\mathcal {S}^{\circledast }\) in time \(2^{2^{{\mathcal {O}}(\lvert {{\Sigma }}\rvert \cdot {w}\cdot 2^{{w}})}}\cdot {k}^{2}\). Analogously, since \(|\widehat {\mathcal {S}}| = 2^{O(|{\Sigma }|{w} \log {w})}\), it follows from Observation 23 that one can count the number of functions \(f:{\Sigma }^{{k}}\rightarrow \{0,1\}\) computable by ODDs in \(\widehat {\mathcal {S}}^{\circledast }\) in time \(2^{2^{O(|{\Sigma }|\cdot {w} \cdot \log {w})}}\). □

In this section, we prove Theorem 9, which states that for each alphabet Σ, and each \({w}\in {{\mathbb {N}}_+}\) the following holds.

1. 1.

   The functional transduction \(\widehat {\mathfrak {can}}[{\Sigma },{w}] = \lbrace {({{{D}},\mathcal {C}({{D}})}) \colon {{D}}\in {\widehat {{\mathscr{B}}}({\Sigma },{w})^{\protect \circledast }}}\rbrace \) is \(2^{O(|{\Sigma }|\cdot w\cdot \log w)}\)-regular.

2. 2.

   The functional transduction \(\mathfrak {can}[{\Sigma },{w}] = \lbrace {({{{D}},\mathcal {C}({{D}})}) \colon {{D}}\in {{\mathscr{B}}({\Sigma },{w})^{\protect \circledast }}}\rbrace \) is \(2^{O(|{\Sigma }|\cdot w \cdot 2^{w})}\)-regular.

Although the complete proof of Theorem 9 is quite technical, it is possible to give an intuitive overview of the main steps in the proof. More specifically, we will show that the transduction \(\widehat {\mathfrak {can}}[{\Sigma },{w}]\) can be cast a composition

of regular transductions satisfying the following properties.

1. 1.

   \(\mathfrak {d}({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }})\) is a functional \(2^{O(|{\Sigma }|\cdot {w}\log {w})}\)-regular \(({\widehat {{\mathscr{B}}}({\Sigma }, {w})},{\widehat {{\mathscr{B}}}({\Sigma }, {w})})\)-transduction that sends each ODD \({{D}}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\) to itself. This transduction is used to limit the domain of \(\widehat {\mathfrak {can}}[{\Sigma },{w}]\) to deterministic, complete (Σ,w)-ODDs.

2. 2.

   \(\mathfrak {rea}[{\Sigma },{w}]\) is a functional \(2^{O(|{\Sigma }|\cdot {w} \cdot \log {w})}\)-regular \(({\widehat {{\mathscr{B}}}({\Sigma }, {w})},{\widehat {{\mathscr{B}}}({\Sigma }, {w})})\)-transduction that sends each ODD \({{D}}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\) to a reachable ODD \({{D}^{\prime }}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\) with \({{\mathscr{L}}({{D}})}={{\mathscr{L}}({{D}^{\prime }})}\). This transduction simulates the process of eliminating unreachable states from D.

3. 3.

   \(\mathfrak {mer}[{\Sigma },{w}]\) is a functional \(2^{O(|{\Sigma }|\cdot {w} \cdot \log {w})}\)-regular \(({\widehat {{\mathscr{B}}}({\Sigma }, {w})},{\widehat {{\mathscr{B}}}({\Sigma }, {w})})\)-transduction that sends each reachable, deterministic, complete ODD \({{D}}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\) to a minimized, deterministic, complete ODD \({{D}^{\prime }}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\) with \({{\mathscr{L}}({D})}={{\mathscr{L}}({D^{\prime }})}\). This transduction simulates the process of merging equivalent states in a ODD.

4. 4.

   \(\mathfrak {nor}[{\Sigma },{w}]\) is a functional \(2^{O(|{\Sigma }|\cdot {w} \cdot \log {w})}\)-regular \(({\widehat {{\mathscr{B}}}({\Sigma }, {w})},{\widehat {{\mathscr{B}}}({\Sigma }, {w})})\)-transduc tion that sends each deterministic, complete ODD \({D}\in {{\mathscr{B}}({{\Sigma }},{{w}})^{\protect \circledast }}\) to its normalized version \({{D}^{\prime }}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\). This transduction simulates the process of numbering the states of an ODD according to their lexicographical order. This guarantees that the ODD is unique not only up to isomorphism, but also syntactically unique.

Intuitively, the regular transductions above simulate the steps used in the standard ODD minimization algorithm. By using Proposition 5.(2), we have that the transduction \(\mathfrak {can}[{\Sigma },{w}]\) is \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\)-regular. The fact that each of the five transductions above is functional implies that \(\mathfrak {can}[{\Sigma },{w}]\) is also functional. Additionally, it is straightforward to note that \(\mathsf {Dom}(\widehat {\mathfrak {can}}[{\Sigma },{w}]) = {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\). Finally, a pair of ODDs \(({{D}},{{D}}^{\prime })\) belongs to \(\widehat {\mathfrak {can}}[{\Sigma },{w}]\) if and only if \({{D}}^{\prime }\) is deterministic, complete, minimized, normalized and \({{\mathscr{L}}({{D}})} = {{\mathscr{L}}({{D}}^{\prime })}\). In other words, if and only if \({{D}}^{\prime }\) is the canonical form \(\mathcal {C}({{D}})\) of Theorem 4.

Now, the transduction \(\mathfrak {can}[{\Sigma },{w}]\) can be obtained as the composition

Here, \(\mathfrak {det}[{\Sigma },{w}]\) is a functional 2-regular \(({{\mathscr{B}}({\Sigma }, {w})},{\widehat {{\mathscr{B}}}({\Sigma }, 2^{{w}})})\)-transduction that sends each ODD \({{D}}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\) to a deterministic, complete ODD \({{D}^{\prime }}\in {{{\mathscr{B}}({\Sigma }, 2^{{w}})}^{\protect \circledast }}\) with \({{\mathscr{L}}({D})}={{\mathscr{L}}({D^{\prime }})}\). This transduction simulates the application of the standard power set construction to the states of a ODD, and blows the width of the original ODD at most exponentially. Since \(\widehat {\mathfrak {can}}[{\Sigma },{w}]\) is \(2^{O(|{\Sigma }|\cdot {w} \cdot \log {w})}\)-regular, we have that \(\widehat {\mathfrak {can}}[{\Sigma },2^{{w}}]\) is \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\)-regular. This implies that \(\mathfrak {can}[{\Sigma },{w}]\) is also \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\)-regular.

Next, in Section 6.1, we will define two elementary types of regular transductions: the multimap transductions and the compatibility transductions. Subsequently we will define \(\mathfrak {det}[{\Sigma },{w}]\), \(\mathfrak {rea}[{\Sigma },{w}]\), \(\mathfrak {mer}[{\Sigma },{w}]\) and \(\mathfrak {nor}[{\Sigma },{w}]\) using these elementary transductions. The determinization transduction \(\mathfrak {det}[{\Sigma },{w}]\) will be defined in Section 6.2 and its properties analyzed in Lemma 27. The reachability transduction \(\mathfrak {rea}[{\Sigma },{w}]\) will be defined in Section 6.3, and its properties analyzed in Lemma 30. The merging transduction \(\mathfrak {mer}[{\Sigma },{w}]\) will be defined in Section 6.4, and its properties analyzed in Lemma 36. The normalization transduction will be defined Section 6.5 and its properties analyzed in Lemma 39. Finally, in Section 6.6 we will combine Observation 26 with these four lemmas to conclude the proof of Theorem 9.

6.1 Basic Transductions

Let Σ be an alphabet and \({R}\subseteq {\Sigma }\times {\Sigma }\) be a binary relation over Σ. For each \({k}\in {{\mathbb {N}}_+}\) and each string \({s}={\sigma }_{1}\cdots {\sigma }_{{k}}\in {\Sigma }^{{k}}\), we say that s is R-compatible if (σ_i,σ_i+ 1) ∈ R for each i ∈ [k − 1]. We let

be the R-compatibility transduction, i.e. the (Σ,Σ)-transduction that sends each R-compatible string s ∈Σ⁺ to itself.

Let Σ₁ and Σ₂ be two alphabets and \({R}\subseteq {\Sigma }_1\times {\Sigma }_2\) be a relation. We let

be the R-multimap transduction. If \({g}\colon {\Sigma }_1\rightarrow {\Sigma }_2\) is a map, then we write \(\mathfrak {mm}[{g}]\) to denote the transduction \(\mathfrak {mm}[{R_{g}}]\), where \(R_{g} \doteq \lbrace {({\sigma ,g(\sigma )}) \colon \sigma \in {\Sigma }_1}\rbrace \).

Proposition 25

Let Σ, Σ₁ and Σ₂ be three alphabets, and let \({R}\subseteq {\Sigma }\times {\Sigma }\) and \({{R}^{\prime }}\subseteq {\Sigma }_1\times {\Sigma }_2\) be binary relations. The following statements hold.

1. 1.

   The transduction \(\mathfrak {mm}[{{R}^{\prime }}]\) is 2-regular.

2. 2.

   The transduction \(\mathfrak {cp}[{R}]\) is \((\lvert {{\Sigma }}\rvert +2)\)-regular.

Proof

1. 1.

   We let \({\mathcal {F}}_{\mathfrak {mm}[{{R}^{\prime }}]}\) be the finite automaton with state set \({Q}({\mathcal {F}}_{\mathfrak {mm}[{R^{\prime }}]}) =\) \(\lbrace {q,{q}^{\prime }}\rbrace \), initial state set \(I(\mathcal {F}_{\mathfrak {mm}[{R^{\prime }}]}) = \lbrace {q}\rbrace \), final state set \(F_{\mathfrak {mm}[{R^{\prime }}]}=\lbrace {{q}^{\prime }}\rbrace \) and transition set \(T_{\mathfrak {mm}[{R^{\prime }}]} = \lbrace {({q,({\sigma ,\tau }),{q}^{\prime }})\colon ({\sigma ,\tau })\in R^{\prime }}\rbrace \cup \lbrace ({{q}^{\prime },({\sigma ,\tau }),{q}^{\prime }})\colon \) \(({\sigma ,\tau })\in R^{\prime }\rbrace \). Clearly, \(\mathcal {F}\) has exactly two states, namely q and \({q}^{\prime }\). Moreover, for each two strings \(s\in {\Sigma }_1^{+}\) and \(u\in {\Sigma }_2^{+}\), \({\mathcal {F}}_{\mathfrak {mm}[{{R}^{\prime }}]}\) accepts the string s ⊗ u ∈ (Σ₁ ×Σ₂)⁺ if and only if \(\lvert {{s}}\rvert =\lvert {{u}}\rvert \) and \(({{\sigma }_{i},{\tau }_{i}})\in {{R}^{\prime }}\) for each i ∈ [k], where s = σ₁⋯σ_k, u = τ₁⋯τ_k and \({k}=\lvert {{s}}\rvert \).

2. 2.

   We let \({\mathcal {F}}_{\mathfrak {cp}[{R}]}\) be the finite automaton over the alphabet Σ ×Σ, with state set \(Q(\mathcal {F}_{\mathfrak {cp}[{R}]})=\lbrace {q,{q}^{\prime }}\rbrace \cup \lbrace {q_{\sigma }\colon \sigma \in {\Sigma }}\rbrace \), initial state set \(I(\mathcal {F}_{\mathfrak {cp}[{R}]}) = \lbrace {q}\rbrace \), final state set \(F(\mathcal {F}_{\mathfrak {cp}[{R}]}) = \lbrace {{q}^{\prime }}\rbrace \) and transition set \({T}({\mathcal {F}}_{\mathfrak {cp}[{R}]}) = \lbrace {({{q},({{\sigma },{\sigma }}),{q}_{{\sigma }}}) \colon {\sigma } \in {\Sigma }}\rbrace \cup \lbrace {({{q}_{{\sigma }},({{\tau },{\tau }}),{q}_{{\tau }}}) \colon ({{\sigma },{\tau }}) \in {R}}\rbrace \cup \lbrace {({{q}_{{\sigma }},({{\tau },{\tau }}),{{q}^{\prime }}})\colon ({{\sigma },{\tau }})\in {R}}\rbrace \text {.}\) Clearly, \({\mathcal {F}}_{\mathfrak {cp}[{R}]}\) has at most \(\lvert {{\Sigma }}\rvert +2\) states. Moreover, it is not hard to check that, for each \({k}\in {{\mathbb {N}}_+}\), \({\mathcal {F}}_{\mathfrak {cp}[{R}]}\) accepts a string \({s}={\sigma }_{1}\cdots {\sigma }_{{k}} \in {\Sigma }^{{k}}\) if and only if (σ_i,σ_i+ 1) ∈ R for each i ∈ [k − 1]. Therefore, the language of \({\mathcal {F}}_{\mathfrak {cp}[{R}]}\) is \({{{\mathscr{L}}}({\mathcal {F}}_{\mathfrak {cp}[{R}]})} = {\mathscr{L}}(\mathfrak {cp}[{R}])\).

□

The next observation is a direct consequence of Proposition 5.(3) and Corollary 8.

Observation 26

Let Σ be an alphabet and \({w}\in {{\mathbb {N}}_+}\).

1. 1.

   \(\mathfrak {d}({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }})\) is \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\)-regular.

2. 2.

   \(\mathfrak {d}({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }})\) is \(2^{O(|{\Sigma }|\cdot {w} \cdot \log {w})}\)-regular.

6.2 Determinization Transduction

In this subsection, we define the determinization transduction \(\mathfrak {det}[{\Sigma },{w}]\), which intuitively simulates the application of the well known power-set construction to the layers of a (Σ,w)-ODD.

For each \({w}\in {{\mathbb {N}}_+}\), we let \({\Omega } \colon {\mathcal {P}(\llbracket {{w}}\rrbracket ))} \rightarrow \llbracket {2^{{w}}}\rrbracket \) be the bijection that sends each subset \({X} \subseteq \llbracket {{w}}\rrbracket \) to the natural number \({\Omega }({X}) \doteq {\sum }_{i \in {X}} 2^{i}\). In particular, we remark that Ω(∅) = 0 and Ω({i}) = 2ⁱ for each i ∈ X.

Let Σ be an alphabet, \({w}\in {{\mathbb {N}}_+}\), \({B}\in {{\mathscr{B}}({\Sigma }, {w})}\), \({X} \subseteq {\ell }({B})\) and \({\Sigma }^{\prime } \subseteq {\Sigma }\). We let \(\mathrm {\textbf {N}}({B},{X}, {\Sigma }^{\prime })\) be the set of all right states of B that are reachable from some left state in X by reading some symbol in \({\Sigma }^{\prime }\). More formally,

For each alphabet Σ and each \({w}\in {{\mathbb {N}}_+}\), we let \({\mathsf {pw}}[{\Sigma },{w}]\colon {{\mathscr{B}}({\Sigma }, {w})}\rightarrow {\widehat {{\mathscr{B}}}({\Sigma }, 2^{{w}})}\) be the map that sends each layer \({B} \in {{\mathscr{B}}({\Sigma }, {w})}\) to the deterministic, complete layer \({\mathsf {pw}}({B})\in {\widehat {{\mathscr{B}}}({\Sigma }, 2^{{w}})}\) defined as follows:

• \({\ell }({{\mathsf {pw}}({B})}) \doteq \begin {cases} \lbrace {{\Omega }({I}({B}))}\rbrace & \text { if } {\iota }({B}) = 1\\ \lbrace {{\Omega }({X}) \colon {X} \subseteq {\ell }({B})}\rbrace & \text { otherwise;} \end {cases}\)

• \({r}({{\mathsf {pw}}({B})}) \doteq \lbrace {{\Omega }({X}) \colon {X} \subseteq {r}({B})}\rbrace \);

• \({T}({{\mathsf {pw}}({B})}) \doteq \begin {cases} \{({{\Omega }({I}({B})), {\sigma }, {\Omega }(\mathrm {\textbf {N}}({B},{I}({B}), \lbrace {{\sigma }}\rbrace ))}, {\sigma } \in {\Sigma }\} & \text { if } {\iota }({B}) = 1 \\ \{({\Omega }({X}), {\sigma }, {\Omega } (\mathrm {\textbf {N}}({B},{X}, \lbrace {{\sigma }}\rbrace ) \colon {X} \subseteq {\ell }({B}), {\sigma }\in {\Sigma }\} & \text { otherwise; } \end {cases}\)

• \({I}({{\mathsf {pw}}({B})}) \doteq \begin {cases} \lbrace {{\Omega }({I}({B}))}\rbrace & \text {if } {\iota }({B}) = 1\\ \emptyset & \text {otherwise;} \end {cases}\)

• \({F}({{\mathsf {pw}}({B})}) \doteq \lbrace {{\Omega }({X}) \colon {X} \subseteq {r}({B}), {X} \cap {F}({B}) \neq \emptyset }\rbrace \);

• \({\iota }({{\mathsf {pw}}({B})}) \doteq {\iota }({B})\);

• \({\phi }({{\mathsf {pw}}({B})}) \doteq {\phi }({B})\).

Let Σ be an alphabet, \({w}\in {{\mathbb {N}}_+}\), and let \({B} \in {{\mathscr{B}}({\Sigma }, {w})}\). Since Ω is a bijection, there exists precisely one right state \({\mathfrak {q}} \in {r}({{\mathsf {pw}}({B})})\), namely \({\mathfrak {q}}={\Omega } (\mathrm {\textbf {N}}({B},{X}, \lbrace {{\sigma }}\rbrace ))\), such that \(({{\Omega }({X}), {\sigma }, {\mathfrak {q}}}) \in {T}({{\mathsf {pw}}({B})})\) for each subset \({X} \subseteq \llbracket {{w}}\rrbracket \) with Ω(X) ∈ ℓ(pw(B)) and each symbol σ ∈Σ. Furthermore, note that ι(pw(B)) = 1 implies ι(B) = 1. Thus, if ι(pw(B)) = 1, then I(pw(B)) = ℓ(pw(B)) = {Ω(I(B))}. As a result, pw(B) is indeed a deterministic, complete layer in \({\widehat {{\mathscr{B}}}({\Sigma }, 2^{{w}})}\).

Now, for each alphabet Σ and each positive integer \({w}\in {{\mathbb {N}}_+}\), we define the \(({{\mathscr{B}}({\Sigma }, {w})},{\widehat {{\mathscr{B}}}({\Sigma }, {w})})\)-transduction \(\mathfrak {det}[{\Sigma },{w}] \doteq \mathfrak {mm}[{\mathsf {pw}}[{\Sigma },{w}]]\). The next lemma states that \(\mathfrak {det}[{\Sigma },{w}]\) sends each ODD \({{D}}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\) to a deterministic, complete ODD \(D^{\prime }\in \widehat {{\mathscr{B}}}({\Sigma },{w})^{\protect \circledast }\) that has the same language as D.

Lemma 27 (Determinization Transduction)

For each alphabet Σ and each positive integer \({w}\in {{\mathbb {N}}_+}\), the following statements hold.

1. 1.

   \(\mathfrak {det}[{\Sigma },{w}]\) is functional.

2. 2.

   \(\mathsf {Dom}(\mathfrak {det}[{\Sigma },{w}]) \supseteq {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\).

3. 3.

   For each pair \(({{D}},{{D}^{\prime }})\in \mathfrak {det}[{\Sigma },{w}]\), if \({D}\in {{\mathscr{B}}({{\Sigma }},{{w}})^{\protect \circledast }}\), then \(D^{\prime }\in \widehat {{\mathscr{B}}}({\Sigma },{2^{w}})^{\protect \circledast }\) and \({\mathscr{L}}({D^{\prime }}) = {\mathscr{L}}({D})\).

4. 4.

   \(\mathfrak {det}[{\Sigma },{w}]\) is 2-regular.

Proof

First, we note that \(\mathsf {Dom}(\mathfrak {det}[{\Sigma },{w}]) = {{\mathscr{B}}({\Sigma }, {w})}^{+}\). This follows from the fact that pw is a map from the alphabet \({{\mathscr{B}}({\Sigma }, {w})}\) to the alphabet \({\widehat {{\mathscr{B}}}({\Sigma }, 2^{{w}})}\). Thus, for each \({k}\in {{\mathbb {N}}_+}\) and each string \({{D}}={B}_{1}\cdots {B}_{{k}}\in {{\mathscr{B}}({\Sigma }, {w})}^{{k}}\), there exists exactly one string \({{D}^{\prime }}\) over \({\widehat {{\mathscr{B}}}({\Sigma }, 2^{{w}})}\) such that \(({{{D}},{{D}^{\prime }}})\in \mathfrak {det}[{\Sigma },{w}]\), namely the string \({{D}^{\prime }}={{\mathsf {pw}}({{D}})}={{\mathsf {pw}}({B}_{1})}\cdots {{\mathsf {pw}}({B}_{{k}})}\). Consequently, \(\mathsf {Dom}(\mathfrak {det}[{\Sigma },{w}]) \supseteq {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\). Moreover, by the uniqueness of the string \({{D}^{\prime }}={{\mathsf {pw}}({{D}})}\) with \(({{{D}},{{D}^{\prime }}})\in \mathfrak {det}[{\Sigma },{w}]\) for each \({{D}}\in {{\mathscr{B}}({\Sigma }, {w})}^{+}\), we obtain that \(\mathfrak {det}[{\Sigma },{w}]\) is a functional transduction.

Now, let \({{D}} = {B}_{1}\cdots {B}_{{k}}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\) for some \({k} \in {{\mathbb {N}}_+}\). Since Ω is a bijection, for each i ∈ [k − 1], ℓ(pw(B_i+ 1)) = r(pw(B_i)) if and only if ℓ(B_i+ 1) = r(B_i). Furthermore, ι(pw(B_i)) = ι(B_i) and ϕ(pw(B_i)) = ϕ(B_i) for each i ∈ [k]. Thus, owing to fact that \({{D}}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\), \({{\mathsf {pw}}({{D}})}={{\mathsf {pw}}({B}_{1})}\cdots {{\mathsf {pw}}({B}_{{k}})}\in {{{\mathscr{B}}({\Sigma }, 2^{{w}})}^{\protect \circ {{k}}}}\). More specifically, pw(D) is a deterministic, complete ODD in \({{\widehat {{\mathscr{B}}}({\Sigma }, 2^{{w}})}^{\protect \circ {{k}}}}\). Indeed, this follows from the fact that pw(B_i) is a deterministic, complete (Σ,w)-layer for each i ∈ [k]. Thus, it just remains to prove that \({{\mathscr{L}}({{\mathsf {pw}}({{D}})})} = {{\mathscr{L}}({{D}})}\). Let s = σ₁⋯σ_k be a string in Σ^k.

First, suppose that \({s} \in {{\mathscr{L}}({{D}})}\). Then, there exists an accepting sequence

for s in D. Let X₀ = I(B₁) and, for each i ∈⟦k⟧, let X_i+ 1 = N(B_i+ 1X_i{σ_i+ 1}). Note that \(X_{i} \subseteq \ell (B_{i+1})\) for each i ∈⟦k⟧. Furthermore, for each i ∈ [k], we have that \(\mathfrak {q}_{i} \in X_{i}\), i.e. \(\mathfrak {q}_{i} \in \mathrm {\textbf {N}}({B_{i}}{X_{i-1}}{\lbrace {\sigma _{i}}\rbrace })\), otherwise \(({\mathfrak {p}_{i}, \sigma _{i}, \mathfrak {q}_{i}}) \not \in T(B_{i})\). Therefore,

is an accepting sequence for s in pw(D), and we obtain that \(s \in {\mathscr{L}}({{\mathsf {pw}(D)}})\).

Conversely, suppose that \({s} \in {{\mathscr{L}}({{\mathsf {pw}}({{D}})})}\). Then, there exists an accepting sequence

for s in pw(D), where X₀ = I(B₁) and X_i+ 1 = N(B_i+ 1,X_i,{σ_i+ 1}) for each i ∈⟦k⟧. Thus, let \({\mathfrak {p}}_{{k}} \in {X}_{{k}-1}\) and \({\mathfrak {q}}_{{k}} \in {X}_{{k}}\) such that \(({{\mathfrak {p}}_{{k}}, {\sigma }_{{k}}, {\mathfrak {q}}_{{k}}}) \in {T}({B}_{{k}})\). Moreover, for each i ∈ [k − 1], let \({\mathfrak {p}}_{i} \in {X}_{i-1}\) and \({\mathfrak {q}}_{i} \in {X}_{i}\) such that \({\mathfrak {q}}_{i} = {\mathfrak {p}}_{i+1}\) and \(({{\mathfrak {p}}_{i}, {\sigma }_{i}, {\mathfrak {q}}_{i}}) \in {T}({B}_{i})\). We note that for each i ∈⟦k⟧, there exist left states and right states \({\mathfrak {p}}_{i+1}\) and \({\mathfrak {q}}_{i+1}\) as described above, otherwise (Ω(X_i),σ_i+ 1,Ω(X_i+ 1)) would not be a transition in T(pw(B_i+ 1)). Therefore,

is an accepting sequence for s in D, and \(s \in {\mathscr{L}}({D})\). Finally, the fact that \(\mathfrak {det}[{\Sigma },{w}]\) is 2-regular follows from the fact that \(\mathfrak {det}[{\Sigma },{w}] \doteq \mathfrak {mm}[{\mathsf {pw}}[{\Sigma },{w}]]\) is an instantiation of a multimap transduction and that multimap transductions are 2-regular (Proposition 25.(1)). □

6.3 Reachability Transduction

In this subsection, we define the reachability transduction, which intuitively simulates the process of eliminating unreachable states from the frontiers of each layer of an ODD. It is worth noting that unlike the determinization transduction, that can be defined using a map that acts layerwisely, the reachability transduction will require the use of a compatibility transduction. The issue is that reachability of a given state q in a given B belonging to a given ODD D is a property that depends on which layers have been read before B. To circumvent this issue, the action of the reachability transduction on a ODD D can be described in three intuitive steps. First, we use a multimap transduction to expand each layer of the ODD into a set of annotated layers. Each annotation splits states of a layer into two classes: those that are deemed to be useful, and those that should be deleted. Subsequently, we use a compatibility transduction to ensure that only sequences of annotated layers with compatible annotations are considered to be legal. The crucial observation is that each ODD D has a unique annotated version where each two adjacent annotated layers are compatible with each other. Finally, we apply a mapping that sends each annotated layer to the layer obtained by deleting the states that have been marked for deletion. The resulting ODD is then the unique ODD obtained from D by eliminating unreachable states.

Let Σ be an alphabet, \({w} \in {{\mathbb {N}}_+}\) and \({B}\in {\widehat {{\mathscr{B}}}({\Sigma }, {w})}\). A reachability annotation for B is a pair (𝜗,η) of functions \(\vartheta \colon {\ell }({B})\rightarrow \lbrace {0,1}\rbrace \) and \(\eta \colon {r}({B})\rightarrow \lbrace {0,1}\rbrace \) that satisfies the following conditions:

1. 1.

   if ι(B) = 1, then, for each left state \({\mathfrak {p}}\in {\ell }({B})\), \(\vartheta _{}({\mathfrak {p}})=1\) if and only if \(\mathfrak {p}\in I(B)\);

2. 2.

   for each right state \({\mathfrak {q}}\in {r}({B})\), \(\eta _{}({\mathfrak {q}})=1\) if and only if there exists \({\mathfrak {p}}\in {\ell }(B)\) and σ ∈Σ such that \(\vartheta ({\mathfrak {p}})=1\) and \(({\mathfrak {p},\sigma ,\mathfrak {q}})\in T(B)\).

Let Σ be an alphabet, \({w},{k}\in {{\mathbb {N}}_+}\), and let \({{D}} = {B}_{1}\cdots {B}_{{k}}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\). A reachability annotation for D is a sequence 〈(𝜗₁,η₁),…,(𝜗_k,η_k)〉 that satisfies the following conditions:

1. 1.

   for each i ∈ [k], (𝜗_i,η_i) is a reachability annotation for B_i;

2. 2.

   for each i ∈ [k − 1], η_i = 𝜗_i+ 1.

Proposition 28

Let Σ be an alphabet and \({w} \in {{\mathbb {N}}_+}\). Every ODD \({{D}} \in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\) admits a unique reachability annotation.

Proof

First, we observe that for each layer \({B}\in {\widehat {{\mathscr{B}}}({\Sigma }, {w})}\) and each function \(\vartheta \colon {\ell }({B})\rightarrow \lbrace {0,1}\rbrace \), there exists exactly one function \(\eta \colon {r}({B})\rightarrow \lbrace {0,1}\rbrace \) such that (𝜗,η) is a reachability annotation for B.

Let \({k}\in {{\mathbb {N}}_+}\) and \({{D}}={B}_{1}\cdots {B}_{{k}}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\), such that ℓ(B_i+ 1) = r(B_i) for each i ∈ [k − 1], and ι(B₁) = 1 and ι(B_i) = 0 for each i ∈{2,…,k}. Based on the previous observation, we prove by induction on k that the following statement holds: there exists a unique sequence 〈(𝜗₁,η₁),…,(𝜗_k,η_k)〉 such that 𝜗_i = η_i+ 1 for each i ∈ [k − 1], and (𝜗_i,η_i) is a reachability annotation for B_i for each i ∈ [k].

Base case. :

Consider k = 1. Since ι(B_k) = 1, the function \(\vartheta _{{k}}\colon {\ell }({B}_{{k}})\rightarrow \lbrace {0,1}\rbrace \) is uniquely determined. Indeed, by definition, for each left state \({\mathfrak {p}}\in {\ell }({B}_{{k}})\), \(\vartheta _{{k}}({\mathfrak {p}})=1\) if \({\mathfrak {p}}\in {I}({B}_{{k}})\), and \(\vartheta _{{k}}({\mathfrak {p}})=0\) otherwise. Thus, there exists a unique sequence 〈(𝜗_k,η_k)〉 such that (𝜗_k,η_k) is a reachability annotation for B_k.

Inductive step. :

Consider k > 1. Let \({{D}^{\prime }}={B}_{1}\cdots {B}_{{k}-1}\) be the string obtained from D = B₁⋯B_k by removing the layer B_k. It follows from the inductive hypothesis that there exists a unique sequence 〈(𝜗₁,η₁),…,(𝜗_k− 1,η_k− 1)〉 such that 𝜗_i = η_i+ 1 for each i ∈ [k − 2], and (𝜗_i,η_i) is a reachability annotation for B_i for each i ∈ [k − 1]. In particular, we note that the function η_k− 1 is uniquely determined. Furthermore, based on the previous observation, for each function \(\vartheta _{{k}}\colon {\ell }({B}_{{k}})\rightarrow \lbrace {0,1}\rbrace \), there exists a unique function \(\eta _{{k}}\colon {r}({B}_{{k}})\rightarrow \lbrace {0,1}\rbrace \) such that (𝜗_k,η_k) is a reachability annotation for B_k. Therefore, since 𝜗_k must be equal to η_k− 1, there exists a unique sequence 〈(𝜗₁,η₁),…,(𝜗_k,η_k)〉 such that 𝜗_i = η_i+ 1 for each i ∈ [k − 1] and (𝜗_i,η_i) is a reachability annotation for B_i for each i ∈ [k].

□

Let Σ be an alphabet and \({w}\in {{\mathbb {N}}_+}\). We denote by \(\mathcal {R}({\Sigma },{w})\) the set consisting of all triples (B,𝜗,η) such that B is a layer in \({\widehat {{\mathscr{B}}}({\Sigma }, {w})}\) and (𝜗,η) is a reachability annotation for B. Additionally, we denote by \(\xi [{\Sigma },{w}]\colon \mathcal {R}({\Sigma },{w})\rightarrow {\widehat {{\mathscr{B}}}({\Sigma }, {w})}\) the map that sends each triple \(({{B},\vartheta ,\eta })\in \mathcal {R}({\Sigma },{w})\) to the layer \(\xi [{\Sigma },{w}]({B},\vartheta ,\eta )\in {\widehat {{\mathscr{B}}}({\Sigma }, {w})}\) obtained from B by removing the left states \({\mathfrak {p}}\in {\ell }({B})\) with \(\vartheta _{}({\mathfrak {p}})=0\), the right states \({\mathfrak {q}}\in {r}({B})\) with \(\eta _{}({\mathfrak {q}})=0\), and the transitions incident with such left and right states. More formally, for each triple \(({{B},\vartheta ,\eta })\in \mathcal {R}({\Sigma },{w})\), we let \(\xi [{\Sigma },{w}]({B},\vartheta ,\eta ) = {{B}^{\prime }}\), where \({{B}^{\prime }}\) is the layer belonging to \({\widehat {{\mathscr{B}}}({\Sigma }, {w})}\) defined as follows:

• \({\ell }({{B}^{\prime }}) \doteq {\ell }({B})\setminus \lbrace {{\mathfrak {p}} \colon \vartheta _{}({\mathfrak {p}})=0}\rbrace \);

• \({r}({{B}^{\prime }}) \doteq {r}({B})\setminus \lbrace {{\mathfrak {q}} \colon \eta _{}({\mathfrak {q}})=0}\rbrace \);

• \({T}({{B}^{\prime }}) \doteq {T}({B})\setminus \lbrace {({{\mathfrak {p}},{\sigma },{\mathfrak {q}}}) \colon \vartheta _{}({\mathfrak {p}})=0}\rbrace \);

• \({\iota }({{B}^{\prime }}) \doteq {\iota }({B})\); \({\phi }({{B}^{\prime }}) \doteq {\phi }({B})\);

• \({I}({{B}^{\prime }}) \doteq {I}({B})\); \({F}({{B}^{\prime }}) \doteq {r}({{B}^{\prime }}) \cap {F}({B})\).

We let \( {\xi }[{\Sigma },{w}]\colon {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\rightarrow {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\) be the map that for each \({k}\in {{\mathbb {N}}_+}\), sends each ODD \({D} = {B}_{1}\cdots {B}_{{k}}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\) to the ODD

where 〈(𝜗₁,η₁),…,(𝜗_k,η_k)〉 denotes the unique reachability annotation for D (see Proposition 28).

Proposition 29

Let Σ be an alphabet, \({w}\in {{\mathbb {N}}_+}\) and \({D}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\). Then, ξ[Σ,w](D) is a reachable ODD in \({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\) such that \({{\mathscr{L}}( {\xi }[{\Sigma },{w}]({D}))} = {{\mathscr{L}}({D})}\).

Proof

Assume that D = B₁⋯B_k and \( {\xi }[{\Sigma },{w}]({D}) = {{B}^{\prime }}_{1}\cdots {{B}^{\prime }}_{{k}}\), for some \({k}\in {{\mathbb {N}}_+}\), where \({{B}^{\prime }}_{i} = \xi [{\Sigma },{w}]({B}_{i},\vartheta _{i},\eta _{i})\) for each i ∈ [k] and 〈(𝜗₁,η₁),…,(𝜗_k,η_k)〉 is the unique reachability annotation of D. First, we prove that ξ[Σ,w](D) is reachable. Note that for each i ∈ [k] and each \({\mathfrak {q}}\in {r}({B}_{i})\),

This implies that for each i ∈ [k], \({{B}^{\prime }}_{i}\) is a reachable layer since \({r}({{B}^{\prime }}_{i}) \subseteq {r}({B}_{i})\). Therefore, ξ[Σ,w](D) is a reachable ODD. Now, we prove that \({{\mathscr{L}}( {\xi }[{\Sigma },{w}]({D}))} = {{\mathscr{L}}({D})}\). It is immediate from the definition of ξ[Σ,w](D) that \({{\mathscr{L}}( {\xi }[{\Sigma },{w}]({D}))} \subseteq {{\mathscr{L}}({D})}\). On the other hand, it is not hard to check that for each string s ∈Σ^k, every accepting sequence for s in D is also an accepting sequence for s in ξ[Σw](D). Consequently, \({{\mathscr{L}}( {\xi }[{\Sigma },{w}]({D}))} \supseteq {{\mathscr{L}}({D})}\).

To prove that ξ[Σ,w] preserves determinism, it is enough to note that \({T}({{B}^{\prime }}_{i})\subseteq {T}({B}_{i})\) for each i ∈ [k]. As a result, since D is deterministic, so is ξ[Σ,w](D). Finally, since D is complete, by definition, for each i ∈ [k] and each \({\mathfrak {p}} \in {\ell }({B}_{i}) \cap {\ell }({{B}^{\prime }}_{i})\), there exists a symbol σ and a right state \({\mathfrak {q}} \in {r}({B}_{i})\) such that \(({{\mathfrak {p}},{\sigma },{\mathfrak {q}}}) \in {T}({B}_{i})\). This implies that for each i ∈ [k] and each \({\mathfrak {p}} \in {\ell }({{B}^{\prime }}_{i})\), there exists a symbol σ and a right state \({\mathfrak {q}} \in {r}({{B}^{\prime }}_{i})\) such that \(({{\mathfrak {p}},{\sigma },{\mathfrak {q}}}) \in {T}({{B}^{\prime }}_{i})\). Therefore, ξ[Σ,w](D) is also complete. □

For each alphabet Σ and each positive integer \({w}\in {{\mathbb {N}}_+}\), we let \(\text {RR}[{\Sigma },{w}] \subseteq {\widehat {{\mathscr{B}}}({\Sigma }, {w})} \times \mathcal {R}({\Sigma },{w})\) and \(\text {RC}[{\Sigma },{w}] \subseteq \mathcal {R}({\Sigma },{w})\times \mathcal {R}({\Sigma },{w})\) be the relations defined as follows.

Now, for each alphabet Σ and each positive integer \({w} \in {{\mathbb {N}}_+}\), we define \(\mathfrak {rea}[{\Sigma },{w}]\) as the \((\widehat {{\mathscr{B}}}({\Sigma },{w}),\widehat {{\mathscr{B}}}({\Sigma },{w}))\)-transduction

The next lemma states that \(\mathfrak {rea}[{\Sigma },{w}]\) is a transduction that sends each ODD \({{D}}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\) to a reachable ODD \(D^{\prime }\in \widehat {{\mathscr{B}}}({\Sigma },{w})^{\protect \circledast }\) that has the same language as D, and that preserves the determinism and completeness properties.

Lemma 30 (Reachability Transduction)

For each alphabet Σ and each positive integer \({w}\in {{\mathbb {N}}_+}\), the following statements hold.

1. 1.

   \(\mathfrak {rea}[{\Sigma },{w}]\) is functional.

2. 2.

   \(\mathsf {Dom}(\mathfrak {rea}[{\Sigma },{w}]) \supseteq {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\).

3. 3.

   For each pair \(({{{D}},{{D}^{\prime }}})\in \mathfrak {rea}[{\Sigma },{w}]\), \({{\mathscr{L}}({{D}^{\prime }})} = {{\mathscr{L}}({{D}})}\) and \({{D}^{\prime }}\) is reachable.

4. 4.

   \(\mathfrak {rea}[{\Sigma },{w}]\) is \(2^{O(|{\Sigma }|\cdot {w}\cdot \log {w})}\)-regular.

Proof

We note that \(\mathfrak {rea}[{\Sigma },{w}]\) consists of all pairs \(({{{D}},{{D}^{\prime }}})\) of non-empty strings over the alphabet \({\widehat {{\mathscr{B}}}({\Sigma }, {w})}\) satisfying the conditions that \(\lvert {{{D}}}\rvert =\lvert {{{D}^{\prime }}}\rvert \) and that, if D = B₁⋯B_k and \({D^{\prime }}={B^{\prime }}_{1}\cdots {B^{\prime }}_{{k}}\) for some \({k}\in {{\mathbb {N}}_+}\), then there exists a reachability annotation (𝜗_i,η_i) for the layer B_i such that \({{B}^{\prime }}_{i}=\xi [{\Sigma },{w}]({B}_{i},\vartheta _{i},\eta _{i})\) for each i ∈ [k], and r(B_j) = ℓ(B_j+ 1) and η_j = 𝜗_j+ 1 for each j ∈ [k − 1]. Additionally, based on Proposition 28, each (Σ,w)-ODD admits a unique reachability annotation. As a result, we obtain that \(\mathsf {Dom}(\mathfrak {rea}[{\Sigma },{w}]) \supseteq {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\). Moreover, \({{D}^{\prime }} = {\xi }[{\Sigma },{w}]({{D}})\); thus, by the uniqueness of ξ[Σ,w](D), the transduction \(\mathfrak {rea}[{\Sigma },{w}]\) is functional. Finally, it follows from Proposition 29 that for each pair \(({{{D}},{{D}^{\prime }}})\in \mathfrak {rea}[{\Sigma },{w}]\), \({{D}^{\prime }} = {\xi }[{\Sigma },{w}]({{D}})\) is a reachable ODD in \({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\) that has the same language as D.

The fact that \(\mathfrak {rea}[{\Sigma },{w}]\) is \(2^{O(|{\Sigma }|\cdot {w} \cdot \log {w})}\)-regular follows from Proposition 5.(2) together with the fact that the multimap transductions \(\mathfrak {mm}[\text {RR}[{\Sigma },{w}]]\) and \(\mathfrak {mm}[\xi [{\Sigma },\) w]] are 2-regular (Proposition 25.(1)), and that the transduction \(\mathfrak {cp}[\text {RC}[{\Sigma },{w}]]\) is \(2^{O(|{\Sigma }|\cdot {w} \cdot \log {w})}\)-regular (Proposition 25.(2)), given that \(\text {RC}[{\Sigma },{w}]\subseteq \mathcal {R}({\Sigma },{w})\times \mathcal {R}({\Sigma },{w})\) and that \(|\mathcal {R}({\Sigma },{w})| = 2^{O(|{\Sigma }|\cdot {w}\cdot \log {w})}\). □

6.4 Merging Transduction

In this subsection, we define the merging transduction, which intuitively simulates the process of merging equivalent states in the frontiers of each layer of an ODD D. As in the case of the reachability transduction, the merging transduction will be defined as the composition of three elementary transductions. First, we use a multimap transduction to expand each layer of the ODD into a set of annotated layers. Each annotation partitions each frontier of the layer into cells containing states that are deemed to be equivalent. Subsequently, we use a compatibility transduction to ensure that only sequences of annotated layers with compatible annotations are considered to be legal. As in the case of the reachability transduction, it is possible to show that each ODD D has a unique annotated version where each two adjacent annotated layers are compatible with each other. Finally, we apply a mapping that sends each annotated layer to the layer obtained by merging all states in each cell of each partition to the smallest state in the cell. The result is a minimized ODD with same language as D.

Let Σ be an alphabet, \({w} \in {{\mathbb {N}}_+}\), \({B}\in {\widehat {{\mathscr{B}}}({\Sigma }, {w})}\) and ν be a partition of r(B). Two (not necessarily distinct) left states \({\mathfrak {p}},{\mathfrak {p}}^{\prime }\in {\ell }({B})\) are said to be ν-equivalent if, for each symbol σ ∈Σ, there exists a right state \({\mathfrak {q}}\in r({B})\) such that \(({{\mathfrak {p}},{\sigma },{\mathfrak {q}}})\) is a transition in T(B) if and only if there exists a right state \({\mathfrak {q}}^{\prime }\in {r}({B})\) such that \(({{\mathfrak {p}}^{\prime },{\sigma },{\mathfrak {q}}^{\prime }})\) is a transition in T(B), and \({\mathfrak {q}}\) and \({\mathfrak {q}}^{\prime }\) belong to the same cell of ν. We remark that each left state \({\mathfrak {p}}\) is trivially ν-equivalent to itself.

A merging annotation for B is a pair (μ,ν), where μ is a partition of ℓ(B) and ν is a partition of r(B), that satisfies the following two conditions:

1. 1.

   if ϕ(B) = 1, then ν = {r(B) ∖ F(B),F(B)} whenever r(B) ∖ F(B)≠∅ and F(B)≠∅, and ν = {r(B)} whenever r(B) ∖ F(B) = ∅ or F(B) = ∅;

2. 2.

   for each two left states \({\mathfrak {p}},{\mathfrak {p}}^{\prime }\in {\ell }({B})\), \({\mathfrak {p}}\) and \({\mathfrak {p}}^{\prime }\) belong to the same cell of μ if and only if \(\mathfrak {p}\) and \(\mathfrak {p}^{\prime }\) are ν-equivalent.

Let Σ be an alphabet, \({w},{k}\in {{\mathbb {N}}_+}\), and let \({{D}} = {B}_{1}\cdots {B}_{{k}}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\). A merging annotation for D is a sequence 〈(μ₁,ν₁)⋯(μ_k,ν_k)〉 that satisfies the following conditions:

1. 1.

   for each i ∈ [k], (μ_i,ν_i) is a merging annotation for B_i;

2. 2.

   for each i ∈ [k − 1], ν_i = μ_i+ 1.

Proposition 31

Let Σ be an alphabet and \({w} \in {{\mathbb {N}}_+}\). Every deterministic, complete (Σ,w)-ODD admits a unique merging annotation.

Proof

First, we claim that for each layer \({B}\in {\widehat {{\mathscr{B}}}({\Sigma }, {w})}\) and each partition ν of r(B), there exists a unique partition μ of ℓ(B) such that (μ,ν) is a merging annotation for B. Indeed, any two left states \({\mathfrak {p}},{\mathfrak {p}}^{\prime }\in {\ell }({B})\) belong to the same cell of μ if and only if they are ν-equivalent. Thus, the partition μ is uniquely defined as the set of all maximal subsets \({X}\subseteq {\ell }({B})\) of pairwise ν-equivalent left states.

Let \({k}\in {{\mathbb {N}}_+}\) and \({{D}}={B}_{1}\cdots {B}_{{k}}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\), be such that ℓ(B_i+ 1) = r(B_i) for each i ∈ [k − 1], ϕ(B_i) = 0 for each i ∈ [k − 1] and ϕ(B_k) = 1. Based on the previous claim, we prove by induction on j that the following statement holds for each \(j\in \{0,\dots ,{k}-1\}\): there exists a unique sequence 〈(μ_k−j,ν_k−j)⋯(μ_k,ν_k)〉 such that (μ_i,ν_i) is a merging annotation for B_i for each \(i\in \{j,\dots ,{k}\}\), and ν_i = μ_i+ 1 for each \(i\in \{{k}-j,\dots ,{k}-1\}\). In particular, this implies that the ODD D admits a unique merging annotation 〈(μ₁,ν₁)⋯(μ_k,ν_k)〉.

Base case. :

Consider j = 0. Then k − j = k. Since ϕ(B_k) = 1, the partition ν_k is uniquely determined. Indeed, ν_k = {F(B_k),r(B_k) ∖ F(B_k)} if both r(B_k) ∖ F(B_k)≠∅ and F(B_k)≠∅, and ν_k = {r(B_k)} otherwise. Thus, there exists a unique sequence 〈(μ_k,ν_k)〉 such that (μ_k,ν_k) is a merging annotation for B_k.

Inductive step. :

Consider \(j\in \{1,\dots ,{k}-1\}\). We show that there is a unique sequence

$$ \langle{({\mu_{{k}-j},\nu_{{k}-j}})\cdots({\mu_{{k}},\nu_{{k}}})}\rangle $$

such that (μ_i,ν_i) is a merging annotation for B_i for each i ∈{k − j,…,k}, and ν_i = μ_i+ 1 for each i ∈{k − j,…,k − 1}. It follows from the inductive hypothesis that there exists a unique sequence 〈(μ_{k−(j− 1)},ν_{k−(j− 1)})⋯(μ_k,ν_k)〉 such that (μ_i,ν_i) is a merging annotation for B_i for each i ∈{k − (j − 1),…,k}, and ν_i = μ_i+ 1 for each i ∈{k − (j − 1),…,k − 1}. Now, let (μ_k−j,ν_k−j) be the merging annotation of B_k−j with the property that ν_k−j = μ_{k−(j− 1)}. Such a merging annotation exists (since r(B_k−j) = ℓ(B_{k−(j− 1)})) and is unique since μ_k−j is uniquely determined by ν_k−j. This concludes the proof of the inductive step, and therefore of the proposition.

□

Let Σ be an alphabet, \({w},{k}\in {{\mathbb {N}}_+}\) and \({D}={B}_{1}\cdots {B}_{{k}}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\). For each i ∈ [k], we say that a string s = σ₁…σ_k is accepted by D from a left state \({\mathfrak {p}}\in {\ell }({B}_{i})\) if there exists a sequence \(\langle {({{\mathfrak {p}}_{i},{\sigma }_{i},{\mathfrak {q}}_{i}}),\ldots ,({{\mathfrak {p}}_{{k}},{\sigma }_{{k}},{\mathfrak {q}}_{{k}}})}\rangle \) of transitions such that \({\mathfrak {p}}_{i}={\mathfrak {p}}\), \({\mathfrak {q}}_{{k}}\in {F}({B}_{{k}})\) and, for each j ∈{i,…,k}, \(({{\mathfrak {p}}_{j},{\sigma }_{j},{\mathfrak {q}}_{j}})\in {T}({B}_{j})\). For each i ∈ [k] and each left state \({\mathfrak {p}}\in {\ell }({B}_{i})\), we let

Proposition 32

Let Σ be an alphabet, \({w},{k}\in {{\mathbb {N}}_+}\), D = B₁⋯B_k be a deterministic, complete ODD in \({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\), and let 〈(μ₁,ν₁)⋯(μ_k,ν_k)〉 be the unique merging annotation for D. For each i ∈ [k] and each two left states \({\mathfrak {p}},{\mathfrak {p}}^{\prime }\in {\ell }({B}_{i})\), \({\mathfrak {p}}\) and \({\mathfrak {p}}^{\prime }\) belong to the same cell of μ_i if and only if \({{\mathscr{L}}({D},i,{\mathfrak {p}})}={{\mathscr{L}}({D},i,{\mathfrak {p}}^{\prime })}\).

Proof

The proof is by induction on k − i. Base case. Consider k − i = 0. Then i = k. By definition, two left states \({\mathfrak {p}},{\mathfrak {p}}^{\prime }\in {\ell }({B}_{{k}})\) belong to the same cell of μ_k if and only if \({\mathfrak {p}}\) and \({\mathfrak {p}}^{\prime }\) are ν_k-equivalent. In other words, \({\mathfrak {p}}\) and \({\mathfrak {p}}^{\prime }\) belong to the same cell of μ_k if and only if, for each symbol σ ∈Σ, there exists a final state \({\mathfrak {q}}\in {F}({B}_{{k}})\) such that \(({{\mathfrak {p}},{\sigma },{\mathfrak {q}}})\in {T}({B}_{{k}})\) if and only if there exists a final state \({\mathfrak {q}}^{\prime }\in {F}({B}_{{k}})\) (possibly \({\mathfrak {q}}^{\prime }={\mathfrak {q}}\)) such that \(({{\mathfrak {p}}^{\prime },{\sigma },{\mathfrak {q}}^{\prime }})\in {T}({B}_{{k}})\). Consequently, \({\mathfrak {p}}\) and \({\mathfrak {p}}^{\prime }\) belong to the same cell of μ_k if and only if \({{\mathscr{L}}({D},i,{\mathfrak {p}})}={{\mathscr{L}}({D},i,{\mathfrak {p}}^{\prime })}\).

Inductive step. Consider k − i > 0. Since r(B_i) = ℓ(B_i+ 1) and ν_i = μ_i+ 1, it follows from the inductive hypothesis that any two right states \({\mathfrak {q}},{\mathfrak {q}}^{\prime }\in {r}({B}_{i})\) belong to the same cell of ν_i if and only if \({{\mathscr{L}}({D},i+1,{\mathfrak {q}})}={{\mathscr{L}}({D},i+1,{\mathfrak {q}}^{\prime })}\). Moreover, note that for each left state \({\mathfrak {p}}\in {\ell }({B}_{i})\),

Let \({\mathfrak {p}},{\mathfrak {p}}^{\prime }\in {\ell }({B}_{i})\). We will prove that \({\mathfrak {p}},{\mathfrak {p}}^{\prime }\) belong to the same cell of μ_i if and only if \({{\mathscr{L}}({D},i,{\mathfrak {p}})}={{\mathscr{L}}({D},i,{\mathfrak {p}}^{\prime })}\). The proof is split in two parts.

First, suppose that \({\mathfrak {p}}\) and \({\mathfrak {p}}^{\prime }\) belong to the same cell of μ_i. Then \({\mathfrak {p}}\) and \({\mathfrak {p}}^{\prime }\) are ν_i equivalent. In other words, for each symbol σ ∈Σ, there exists \({\mathfrak {q}}\in r({B}_{i})\) such that \(({{\mathfrak {p}},{\sigma },{\mathfrak {q}}})\in {T}({B}_{i})\) if and only if there exists \({\mathfrak {q}}^{\prime }\in {r}({B}_{i})\) such that \(({{\mathfrak {p}}^{\prime },{\sigma },{\mathfrak {q}}^{\prime }})\in {T}({B}_{i})\) and \({\mathfrak {q}}_{i}\) and \({\mathfrak {q}}_{i}^{\prime }\) belong to the same cell of ν_i. Using the induction hypothesis, we have that for each pair \({\mathfrak {q}},{\mathfrak {q}}^{\prime }\) belonging to the same cell of ν_i, \({{\mathscr{L}}({D},i+1,{\mathfrak {q}})}={{\mathscr{L}}({D},i+1,{\mathfrak {q}}^{\prime })}\). Therefore, using (3), that \({{\mathscr{L}}({D},i,{\mathfrak {p}})}={{\mathscr{L}}({D},i,{\mathfrak {p}}^{\prime })}\).

Now, in order to prove the converse, suppose for contradiction that \({\mathfrak {p}}\) and \({\mathfrak {p}}^{\prime }\) do not belong to the same cell of μ_i and that \({{\mathscr{L}}({D},i,{\mathfrak {p}})}={{\mathscr{L}}({D},i,{\mathfrak {p}}^{\prime })}\). Since B_i is a deterministic, complete layer, for each symbol σ ∈Σ, there exists exactly one right state \({\mathfrak {q}}\in {r}({B}_{i})\) such that \(({{\mathfrak {p}},{\sigma },{\mathfrak {q}}})\in {T}({B}_{i})\). Similarly, for each symbol σ ∈Σ, there exists exactly one right state \({\mathfrak {q}}^{\prime }\in {r}({B}_{i})\) such that \(({{\mathfrak {p}}^{\prime },{\sigma },{\mathfrak {q}}^{\prime }})\in {T}({B}_{i})\). Consequently, for some symbol σ ∈Σ, the right states \({\mathfrak {q}}\) and \({\mathfrak {q}}^{\prime }\) associated with σ, and \({\mathfrak {p}}\) and \({\mathfrak {p}}^{\prime }\), respectively, belong to distinct cells of ν_i. Then, it follows from the induction hypothesis that \({{\mathscr{L}}({D},i+1,{\mathfrak {q}})}\neq {{\mathscr{L}}({D},i+1,{\mathfrak {q}}^{\prime })}\). Assume without loss of generality that \({{\mathscr{L}}({D},i+1,{\mathfrak {q}})}\setminus {{\mathscr{L}}({D},i+1,{\mathfrak {q}}^{\prime })}\neq \emptyset \), and let \({u}\in {{\mathscr{L}}({D},i+1,{\mathfrak {q}})}\setminus {{\mathscr{L}}({D},i+1,{\mathfrak {q}}^{\prime })}\). Based on (3), we have that \({\sigma }{u}\in {{\mathscr{L}}({D},i,{\mathfrak {p}})}\) but \({\sigma }{u}\not \in {{\mathscr{L}}({D},i,{\mathfrak {p}}^{\prime })}\). This implies that \({{\mathscr{L}}({D},i,{\mathfrak {p}})}\neq {{\mathscr{L}}({D},i,{\mathfrak {p}}^{\prime })}\), contradicting our initial supposition. □

Let Σ be an alphabet and \({w}\in {{\mathbb {N}}_+}\). We denote by \({\mathscr{M}}({\Sigma },{w})\) the set consisting of all triples (B,μ,ν) such that B is a deterministic, complete layer in \({\widehat {{\mathscr{B}}}({\Sigma }, {w})}\), and (μ,ν) is a merging annotation for B. Additionally, we denote by \(\zeta [{\Sigma },{w}]\colon {\mathscr{M}}({\Sigma },{w})\rightarrow {\widehat {{\mathscr{B}}}({\Sigma }, {w})}\) the map that sends each triple \(({{B},\mu ,\nu })\in {\mathscr{M}}({\Sigma },{w})\) to the layer \(\zeta [{\Sigma },{w}]({B},\mu ,\nu )\in {\widehat {{\mathscr{B}}}({\Sigma }, {w})}\) obtained from B by identifying, for each X ∈ μ ∪ ν, all states belonging to X with the smallest state that belongs to X. More formally, for each triple \(({{B},\mu ,\nu })\in {\mathscr{M}}({\Sigma },{w})\), we let \(\zeta [{\Sigma },{w}]({B},\mu ,\nu ) = {{B}^{\prime }}\), where \({{B}^{\prime }}\) is the deterministic, complete layer belonging to \({\widehat {{\mathscr{B}}}({\Sigma }, {w})}\) defined as follows:

• \({\ell }({{B}^{\prime }}) \doteq \bigcup _{{X} \in \mu }\lbrace {\min \limits {X}}\rbrace \); \({r}({{B}^{\prime }}) \doteq \bigcup _{{X}^{\prime } \in \nu }\lbrace {\min \limits {X}^{\prime }}\rbrace \);

• \({T}({{B}^{\prime }}) \doteq \bigcup _{{X}\in \mu ,{X}^{\prime }\in \nu }\lbrace {({\min \limits {X},{\sigma },\min \limits {X}^{\prime }}) \colon \exists {\mathfrak {p}}\in {X}, \exists \mathfrak {q}\in X^{\prime }, ({\mathfrak {p},\sigma ,\mathfrak {q}})\in T(B)}\rbrace \);

• \({\iota }({{B}^{\prime }}) \doteq {\iota }({B})\); \({\phi }({{B}^{\prime }}) \doteq {\phi }({B})\);

• \({I}({{B}^{\prime }}) \doteq {I}({B})\); \({F}({{B}^{\prime }}) \doteq {r}({{B}^{\prime }}) \cap {F}({B})\).

Let \( {\zeta }[{\Sigma },{w}]\colon {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\rightarrow {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\) be the map that for each \(k\in \mathbb {N}_{+}\), sends each deterministic, complete ODD \(D = B_{1}{\cdots } B_{k}\in \widehat {{\mathscr{B}}}({\Sigma },{w})^{\protect \circ {{k}}}\) to the deterministic, complete ODD

where 〈(μ₁,ν₁),…,(μ_k,ν_k)〉 denotes the unique merging annotation for D (see Proposition 31).

Let Σ be an alphabet, \({w},{k}\in {{\mathbb {N}}_+}\) and \({D}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\). We recall that since D is a deterministic, complete ODD, we have that for each string \({s}={\sigma }_{1}\cdots {\sigma }_{{k}}\in {\Sigma }^{{k}}\), there is a unique valid sequence \(\langle {({{\mathfrak {p}}_{1},{\sigma }_{1},{\mathfrak {q}}_{1}}),\ldots ,({{\mathfrak {p}}_{{k}},{\sigma }_{{k}},{\mathfrak {q}}_{{k}}})}\rangle \) for s in D. Thus, for each string s ∈Σ^k and each i ∈ [k], we let \({\mathfrak {q}}_{[{D},{s},i]}\doteq {\mathfrak {q}}_{i}\) denote the unique right state \({\mathfrak {q}}_{i}\in {r}({B}_{i})\) that belongs to the valid sequence for s in D. Moreover, we let

denote the equivalence class of s with respect to D and i.

Proposition 33

Let Σ be an alphabet, \({w},{k}\in {{\mathbb {N}}_+}\), \({D}={B}_{1}\cdots {B}_{{k}}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\), and let \({\mathfrak {q}}\) be a right state in r(B_i) such that \({\mathfrak {q}}={\mathfrak {q}}_{[{D},{s},i]}\) for some string s ∈Σ^k and some i ∈ [k − 1]. For each string \({s}^{\prime }={\sigma }_{1}^{\prime }\cdots {\sigma }_{{k}}^{\prime }\in [{D},{s},i]\) and each string u ∈Σ^k−i, we have that \({u}\in {{\mathscr{L}}({D},i,{\mathfrak {q}})}\) if and only if \({\sigma }_{1}^{\prime }\cdots {\sigma }_{i}^{\prime }{u}\in {{\mathscr{L}}({D})}\).

Proof

Let \({s}^{\prime }={\sigma }_{1}^{\prime }\cdots {\sigma }_{{k}}^{\prime }\in [{D},{s},i]\) and \({u}={\tau }_{i+1}\cdots {\tau }_{{k}}\in {\Sigma }^{{k}-i}\). Also, let

be the unique valid sequence for \(s^{\prime }\) in D. We note that \(\mathfrak {p}_{1}\in I(B_{1})\) and \(\mathfrak {p}_{i+1}=\mathfrak {q}\). Suppose that \(u\in {\mathscr{L}}({D}{i}{\mathfrak {p}_{i+1}})\). By definition, there is a sequence

of transitions such that \(\mathfrak {p}_{i+1}^{\prime }=\mathfrak {p}_{i+1}\), \(\mathfrak {q}_{k}^{\prime }\in F(B_{k})\) and, for each j ∈{i + 1,…,k}, \(({{\mathfrak {p}}_{j}^{\prime },{\sigma }_{j}^{\prime },{\mathfrak {q}}_{j}^{\prime }})\in {T}({B}_{j})\). Thus, \(\langle ({{\mathfrak {p}}_{1},{\sigma }_{1}^{\prime },{\mathfrak {q}}_{1}}),\ldots ,({{\mathfrak {p}}_{i},{\sigma }_{i}^{\prime },{\mathfrak {q}}_{i}}),({{\mathfrak {p}}_{i+1}^{\prime },{\tau }_{i+1},{\mathfrak {q}}_{i+1}^{\prime }}),\ldots ,\) \(({{\mathfrak {p}}_{{k}}^{\prime },{\tau }_{{k}},{\mathfrak {q}}_{{k}}^{\prime }})\rangle \) is an accepting sequence for the string \({\sigma }_{1}^{\prime }\cdots {\sigma }_{i}^{\prime }{u}\) in D, and therefore \({\sigma }_{1}^{\prime }\cdots {\sigma }_{i}^{\prime }{u}\in {{\mathscr{L}}({D})}\).

Conversely, suppose that \({\sigma }_{1}^{\prime }\cdots {\sigma }_{i}^{\prime }{u}\in {{\mathscr{L}}({D})}\). Then, there exists a unique accepting sequence

for \(\sigma _{1}^{\prime }\cdots \sigma _{i}^{\prime }u\) in D. By the uniqueness of this sequence, we have that \(\mathfrak {p}^{\prime }_{1}=\mathfrak {p}_{1}\) and \({\mathfrak {q}}^{\prime }_{j}={\mathfrak {q}}_{j}\) for each j ∈ [i]. In particular, \({\mathfrak {p}}^{\prime }_{i+1} = {\mathfrak {q}}^{\prime }_{i} = {\mathfrak {q}}\). Therefore, \({u}\in {{\mathscr{L}}({D},i,{\mathfrak {q}})}\). □

Proposition 34

Let Σ be an alphabet, \({w},{k}\in {{\mathbb {N}}_+}\), and let D and \({{D}^{\prime }}\) be two deterministic, complete ODDs in \({\widehat {{\mathscr{B}}}({{\Sigma }},{{w}})^{\protect \circ {{k}}}}\). If \({{\mathscr{L}}( {\zeta }[{\Sigma },{w}]({{D}}))}={{\mathscr{L}}( {\zeta }[{\Sigma },{w}]({{D}^{\prime }}))}\), then \([ {\zeta }[{\Sigma },{w}]({{D}}),{s},i]=[ {\zeta }[{\Sigma },{w}]({{D}^{\prime }}),{s},i]\) for each s ∈Σ^k and each i ∈ [k].

Proof

For the sake of contradiction, suppose that \({{\mathscr{L}}( {\zeta }[{\Sigma },{w}]({{D}}))}={\mathscr{L}}( {\zeta }[{\Sigma },{w}]\) \(({{D}^{\prime }}))\) but, for some string \({s}={\sigma }_{1}\cdots {\sigma }_{{k}}\in {\Sigma }^{{k}}\) and some i ∈ [k], \([ {\zeta }[{\Sigma },{w}]({{D}}),{s},i]\neq [ {\zeta }[{\Sigma },{w}]({{D}^{\prime }}),{s},i]\).

Assume without loss of generality that \([ {\zeta }[{\Sigma },{w}]({{D}}),{s},i]\setminus [ {\zeta }[{\Sigma },{w}]({{D}^{\prime }}),{s},i]\neq \emptyset \). Then, let \({s}^{\prime }={\sigma }_{1}^{\prime }\cdots {\sigma }_{{k}}^{\prime }\in [ {\zeta }[{\Sigma },{w}]({{D}}),{s},i]\setminus [ {\zeta }[{\Sigma },{w}]({{D}^{\prime }}),{s},i]\). Consider \({\mathfrak {p}}_{i+1}^{\prime }={\mathfrak {q}}_{[ {\zeta }[{\Sigma },{w}]({{D}^{\prime }}),{s},i]}\) and \({\mathfrak {p}}_{i+1}^{\prime \prime }={\mathfrak {q}}_{[ {\zeta }[{\Sigma },{w}]({{D}^{\prime }}),{s}^{\prime },i]}\). We note that i < k, otherwise \({{\mathscr{L}}( {\zeta }[{\Sigma },{w}]({{D}}))}\) would be different from \({{\mathscr{L}}( {\zeta }[{\Sigma },{w}]({{D}^{\prime }}))}\). Moreover, since \({\mathfrak {p}}_{i+1}^{\prime }\neq {\mathfrak {p}}_{i+1}^{\prime \prime }\), we obtain by Proposition 32 that

Assume without loss of generality \({{\mathscr{L}}( {\zeta }[{\Sigma }, {w}]({{D}^{\prime }}),i+1,{\mathfrak {p}}_{i+1}^{\prime })}\setminus {\mathscr{L}} ( {\zeta }[{\Sigma },{w}]({{D}^{\prime }}),i+1, {\mathfrak {p}}_{i+1}^{\prime \prime })\neq \emptyset \). Let \({u}\in {{\mathscr{L}}( {\zeta }[{\Sigma },{w}]({{D}^{\prime }}),i+1,{\mathfrak {p}}_{i+1}^{\prime })}\setminus {{\mathscr{L}}( {\zeta }[{\Sigma },{w}]({{D}^{\prime }}),i+1,{\mathfrak {p}}_{i+1}^{\prime \prime })}\). Since \( {\zeta }[{\Sigma },{w}]({{D}^{\prime }})\) is deterministic, there exists a unique valid sequence for the string \({\sigma }_{1}^{\prime }\cdots {\sigma }_{i}^{\prime }{u}\) in \( {\zeta }[{\Sigma },{w}]({{D}^{\prime }})\), and by definition this sequence must contain the left state \({\mathfrak {p}}_{i+1}^{\prime \prime }\). Consequently, it follows from Proposition 33 and from the fact that u is not accepted by \( {\zeta }[{\Sigma },{w}]({{D}^{\prime }})\) from \({\mathfrak {p}}_{i+1}^{\prime \prime }\) that

On the other hand, u is accepted by \( {\zeta }[{\Sigma },{w}]({{D}^{\prime }})\) from \({\mathfrak {p}}_{i+1}^{\prime }\). As a result, we obtain by Proposition 33 that \({\sigma }_{1}\cdots {\sigma }_{i}{u}\in {{\mathscr{L}}( {\zeta }[{\Sigma },{w}]({{D}^{\prime }}))}\). In addition, we have that \({\sigma }_{1}\cdots {\sigma }_{i}{u}\in {{\mathscr{L}}( {\zeta }[{\Sigma },{w}]({{D}}))}\) since \({{\mathscr{L}}( {\zeta }[{\Sigma },{w}]({{D}}))}={{\mathscr{L}}( {\zeta }[{\Sigma },{w}]({{D}^{\prime }}))}\). This further implies that \({u}\in {{\mathscr{L}}( {\zeta }[{\Sigma },{w}]({{D}}),i+1,{\mathfrak {p}}_{i+1})}\), where \({\mathfrak {p}}_{i+1}\) denotes \({\mathfrak {q}}_{[ {\zeta }[{\Sigma },{w}]({{D}}),{s},i]}\). However, since \({s}^{\prime }\in [ {\zeta }[{\Sigma },{w}]({{D}}),{s},i]\), it follows from Proposition 33 that

which, along with (4), implies that \({{\mathscr{L}}( {\zeta }[{\Sigma },{w}]({{D}}))}\neq {{\mathscr{L}}( {\zeta }[{\Sigma },{w}]({{D}^{\prime }}))}\). □

Proposition 35

Let Σ be an alphabet, \({w}\in {{\mathbb {N}}_+}\) and \({D}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\). If D is reachable, then ζ[Σ,w](D) is a minimized ODD such that \({{\mathscr{L}}( {\zeta }[{\Sigma },{w}]({D}))} = {{\mathscr{L}}({D})}\).

Proof

Assume that D = B₁⋯B_k, for some \({k} \in {{\mathbb {N}}_+}\), and let 〈(μ₁,ν₁)⋯(μ_k,ν_k)〉 be the unique merging annotation for D. First, we prove that \({{\mathscr{L}}( {\zeta }[{\Sigma },{w}]({D}))} = {{\mathscr{L}}({D})}\). Let \({s} = {\sigma }_{1}\cdots {\sigma }_{{k}} \in {\Sigma }^{{k}}\). Suppose that \({s} \in {{\mathscr{L}}({D})}\). Then, there exists an accepting sequence \(\langle {({{\mathfrak {p}}_{1},{\sigma }_{1},{\mathfrak {q}}_{1}}),\ldots ,({{\mathfrak {p}}_{{k}},{\sigma }_{{k}},{\mathfrak {q}}_{{k}}})}\rangle \) for s in D. For each i ∈ [k], let X_i be the unique cell of ν_i that contains \({\mathfrak {q}}_{i}\). Then, we have that

is an accepting sequence for s in ζ[Σ,w](D). As a result, we obtain that \({{\mathscr{L}}( {\zeta }[{\Sigma },{w}]({D}))} \subseteq {{\mathscr{L}}({D})}\). Now, suppose that \({s} \in {{\mathscr{L}}( {\zeta }[{\Sigma },{w}]({D}))}\). Then, there exists an accepting sequence \(\langle {({{\mathfrak {p}}^{\prime }_{1},{\sigma }_{1},{\mathfrak {q}}^{\prime }_{1}}),\ldots ,({{\mathfrak {p}}^{\prime }_{{k}},{\sigma }_{{k}},{\mathfrak {q}}^{\prime }_{{k}}})}\rangle \) for s in ζ[Σ,w](D). We note that for each i ∈ [k], there exists a right state \({\mathfrak {q}}_{i}\in {r}({B}_{i})\) such that \({\mathfrak {q}}_{i}\) and \({\mathfrak {q}}^{\prime }_{i}\) belong to a same cell of ν_i and \(({{\mathfrak {p}}_{i},{\sigma }_{i},{\mathfrak {q}}_{i}})\in {T}({B}_{i})\), where \({\mathfrak {p}}_{1} = {\mathfrak {p}}^{\prime }_{1}\) and \({\mathfrak {p}}_{j}={\mathfrak {q}}_{j-1}\) for each j ∈{2,…,k}. Thus, there exists an accepting sequence \(\langle {({{\mathfrak {p}}_{1},{\sigma }_{1},{\mathfrak {q}}_{1}}),\ldots ,({{\mathfrak {p}}_{{k}},{\sigma }_{{k}},{\mathfrak {q}}_{{k}}})}\rangle \) for s in D. Therefore, \({{\mathscr{L}}( {\zeta }[{\Sigma },{w}]({D}))} \supseteq {{\mathscr{L}}({D})}\).

Now, we prove that ζ[Σ,w](D) is minimized if D is reachable. Thus, assume that D is reachable. This implies that ζ[Σ,w](D) is also reachable and thus, for each i ∈ [k] and each \({\mathfrak {q}} \in {r}(\zeta [{\Sigma },{w}]({B}_{i},\mu _{i},\nu _{i}))\), \({\mathfrak {q}} = {\mathfrak {q}}_{[ {\zeta }[{\Sigma },{w}]({D}),{s},i]}\) for some s ∈Σ^k. Then, for each i ∈ [k], let \({w}_{i} = \lvert {{r}(\zeta [{\Sigma },{w}]({B}_{i},\mu _{i},\nu _{i}))}\rvert \) and let \({{s}_{1}^{i}},\ldots ,{s}_{{w}_{i}}^{i}\) be strings such that \([ {\zeta }[{\Sigma },{w}]({D}),{{s}_{j}^{i}},i] \neq [ {\zeta }[{\Sigma },{w}]({D}),{s}_{j^{\prime }}^{i},i]\) for each j ∈ [w_i] and each \(j^{\prime } \in {[{{w}_{i}}]}\) with \(j \neq j^{\prime }\). Also, let \({{D}^{\prime }}={{B}^{\prime }}_{1}\cdots {{B}^{\prime }}_{{k}}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\) be a minimized ODD such that \({{\mathscr{L}}({D^{\prime }})} = {{\mathscr{L}}({D})}\). We note that \({D^{\prime }}\) is reachable. Thus, for each i ∈ [k] and each \({\mathfrak {q}}^{\prime } \in {r}({{B}^{\prime }}_{i})\), \({\mathfrak {q}}^{\prime } = {\mathfrak {q}}_{[{{D}^{\prime }},{s}^{\prime },i]}\) for some \({s}^{\prime } \in {\Sigma }^{{k}}\). Moreover, we have that \( {\zeta }[{{\Sigma }}{{w}}]({D^{\prime }})={D^{\prime }}\), otherwise \({{D}^{\prime }}\) would not be minimized. Then, for each i ∈ [k], we let \(\pi _{i} \colon {r}(\zeta [{\Sigma },{w}]({B}_{i},\mu _{i},\nu _{i})) \rightarrow {r}({{B}^{\prime }}_{i})\) be the mapping such that for each j ∈ [w_i], \(\pi _{i}({\mathfrak {q}}_{[ {\zeta }[{\Sigma },{w}]({D}),{{s}_{j}^{i}},i]}) = {\mathfrak {q}}_{[{{D}^{\prime }},{{s}_{j}^{i}},i]}\). It follows from Proposition 34 that π_i is a bijection. Consequently, we obtain that 〈π₀,…,π_k〉 is a isomorphism between ζ[Σ,w](D) and \({{D}^{\prime }}\), where \(\pi _{0} \colon {\ell }(\zeta [{\Sigma },{w}]({B}_{1},\mu _{1},\nu _{1})) \rightarrow {\ell }({{B}^{\prime }}_{1})\) is the trivial bijection that sends the unique left state in ℓ(ζ[Σ,w](B₁,μ₁,ν₁)) to the unique left state in \({\ell }({B^{\prime }}_{1})\). Therefore, ζ[Σ,w](D) is minimized. □

For each alphabet Σ and each positive integer \({w}\in {{\mathbb {N}}_+}\), we let \(\text {MR}[{\Sigma },{w}]\subseteq {\widehat {{\mathscr{B}}}({\Sigma }, {w})} \times {\mathscr{M}}({\Sigma },{w})\) and \(\text {MC}[{\Sigma },{w}]\subseteq {\mathscr{M}}({\Sigma },{w})\times {\mathscr{M}}({\Sigma },{w})\) be the following relations.

For each alphabet Σ and each positive integer \({w} \in {{\mathbb {N}}_+}\), we define the \(({\widehat {{\mathscr{B}}}({\Sigma }, {w})},\) \(\widehat {{\mathscr{B}}}({\Sigma }, {w}))\)-transduction \(\mathfrak {mer}[{\Sigma },{w}]\) as

The next lemma states that \(\mathfrak {mer}[{\Sigma },{w}]\) is a transduction that sends each deterministic, complete ODD \({D}\in {\widehat {{\mathscr{B}}}({{\Sigma }},{{w}})^{\protect \circledast }}\) to a minimized deterministic, complete ODD \({{D}^{\prime }}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\) that has the same language as D.

Lemma 36 (Merging Transduction)

For each alphabet Σ and each positive integer \({w}\in {{\mathbb {N}}_+}\), the following statements hold.

1. 1.

   \(\mathfrak {mer}[{\Sigma },{w}]\) is functional.

2. 2.

   \(\mathsf {Dom}(\mathfrak {mer}[{\Sigma },{w}]) \supseteq {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\).

3. 3.

   For each pair \(({{D}},{{D}^{\prime }})\in \mathfrak {mer}[{\Sigma },{w}]\), if D is a reachable ODD, then \(D^{\prime }\in \widehat {{\mathscr{B}}}({\Sigma },{w})^{\protect \circledast }\), \({\mathscr{L}}({D^{\prime }}) = {\mathscr{L}}({D})\) and \(D^{\prime }\) is minimized.

4. 4.

   \(\mathfrak {mer}[{\Sigma },{w}]\) is \(2^{O(|{\Sigma }|\cdot {w}\log {w})}\)-regular.

Proof

We note that \(\mathfrak {mer}[{\Sigma },{w}]\) consists of all pairs \(({{{D}},{{D}^{\prime }}})\) of non-empty strings over the alphabet \({\widehat {{\mathscr{B}}}({\Sigma }, {w})}\) satisfying the conditions that \(\lvert {{{D}}}\rvert =\lvert {{{D}^{\prime }}}\rvert \) and that, if D = B₁⋯B_k and \({D^{\prime }}={B^{\prime }}_{1}\cdots {B^{\prime }}_{{k}}\) for some \({k}\in {{\mathbb {N}}_+}\), then there exists a merging annotation (μ_i,ν_i) for the layer B_i such that \({{B}^{\prime }}_{i}=\zeta [{\Sigma },{w}]({B}_{i},\mu _{i},\nu _{i})\) for each i ∈ [k], and r(B_j) = ℓ(B_j+ 1) and ν_j = μ_j+ 1 for each j ∈ [k − 1]. Additionally, based on Proposition 31, each (Σ,w)-ODD admits a unique merging annotation. As a result, we obtain that \(\mathsf {Dom}(\mathfrak {mer}[{\Sigma },{w}]) \supseteq {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\). Moreover, if \(({{{D}},{{D}^{\prime }}})\in \mathfrak {mer}[{\Sigma },{w}]\), then \({{D}^{\prime }} = {\zeta }[{\Sigma },{w}]({{D}})\); thus, by the uniqueness of ζ[Σ,w](D), the transduction \(\mathfrak {mer}[{\Sigma },{w}]\) is functional. Finally, it follows from Proposition 35 that for each pair \(({{{D}},{{D}^{\prime }}})\in \mathfrak {mer}[{\Sigma },{w}]\) such that D is a reachable ODD in \({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\), we have that \({{D}^{\prime }} = {\zeta }[{\Sigma },{w}]({{D}})\) is a minimized ODD in \({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\) that has the same language as D.

The fact that \(\mathfrak {mer}[{\Sigma },{w}]\) is \(2^{O(|{\Sigma }|\cdot {w}\cdot \log {w})}\)-regular follows from Proposition 5.(2) together with the fact that the multimap transductions \(\mathfrak {mm}[\text {MR}[{\Sigma },{w}]]\) and \(\mathfrak {mm}[\zeta [{\Sigma },\) w]] are 2-regular (Proposition 25.(1)), and that the transduction \(\mathfrak {cp}[\text {MC}[{\Sigma },{w}]]\) is \(2^{O(|{\Sigma }|\cdot {w}\cdot \log {w})}\)-regular (Proposition 25.(2)), given that \(\text {MC}[{\Sigma },{w}] \subseteq {\mathscr{M}}({\Sigma },{w})\times {\mathscr{M}}({\Sigma },{w})\), and that \(|{\mathscr{M}}({\Sigma },{w})|=2^{O(|{\Sigma }|\cdot {w}\cdot \log {w})}\). □

6.5 Normalization Transduction.

In this subsection, we define the normalization transduction, which intuitively simulates the process of numbering the states in each frontier of each layer of an ODD D according to their lexicographical order. This transduction can be defined as the composition of three elementary transductions. First, we use a multimap transduction to expand each layer of the ODD into a set of annotated layers. Each annotation relabels the left and right frontier vertices of the layer in such a way that the layer itself is normalized. Subsequently, we use a compatibility transduction that defines two consecutive annotated layers to be compatible if and only if the relabeling of the right-frontier of the first is equal to the relabeling of the left frontier of the second. It is possible to show that each reachable ODD D gives rise to a unique sequence of annotated layers where each two consecutive layers are compatible. Finally, we apply a mapping that sends each annotated layer to the layer obtained sending the numbers in the frontiers to their relabeled versions. The resulting ODD is isomorphic to the original one, and therefore besides preserving the language, it also preserves reachability and minimality.

Let Σ be an alphabet, \({w} \in {{\mathbb {N}}_+}\), and let \({B}\in {\widehat {{\mathscr{B}}}({\Sigma }, {w})}\). For each two bijections \(\pi \colon {\ell }({B})\rightarrow \llbracket {\lvert {{\ell }({B})}\rvert }\rrbracket \) and \(\pi ^{\prime }\colon {r}({B})\rightarrow \llbracket {\lvert {{r}({B})}\rvert }\rrbracket \), we denote by \({\langle {\pi {B}\pi ^{\prime }}\rangle }\) the (Σ,w)-layer obtained from B by applying the bijection π to the left frontier of B and by applying the bijection \(\pi ^{\prime }\) to the right frontier of B. More formally, \({\langle {\pi {B}\pi ^{\prime }}\rangle }={{B}^{\prime }}\) is the (Σ,w)-layer defined as follows:

• \({\ell }({{B}^{\prime }}) \doteq \lbrace {\pi ({\mathfrak {p}}) \colon {\mathfrak {p}} \in {\ell }({B})}\rbrace \); \({r}({{B}^{\prime }}) \doteq \lbrace {\pi ^{\prime }(\mathfrak {q}) \colon \mathfrak {q} \in r(B)}\rbrace \);

• \({I}({{B}^{\prime }}) \doteq \lbrace {\pi ({\mathfrak {p}}) \colon {\mathfrak {p}} \in {I}({B})}\rbrace \); \({F}({{B}^{\prime }}) \doteq \lbrace {\pi ^{\prime }(\mathfrak {q}) \colon \mathfrak {q} \in F(B)}\rbrace \);

• \({T}({{B}^{\prime }}) \doteq \lbrace {({\pi ({\mathfrak {p}}), {\sigma }, \pi ^{\prime }({\mathfrak {q}})}) \colon ({{\mathfrak {p}}, {\sigma }, {\mathfrak {q}}}) \in {T}(B)}\rbrace \);

• \({\iota }({{B}^{\prime }}) \doteq {\iota }({B})\); \({\phi }({{B}^{\prime }}) \doteq {\phi }({B})\).

We note that since \({B}\in {\widehat {{\mathscr{B}}}({\Sigma }, {w})}\), \({\langle {\pi {B}\pi ^{\prime }}\rangle }\) also belongs to \({\widehat {{\mathscr{B}}}({\Sigma }, {w})}\).

Let Σ be an alphabet, \({w} \in {{\mathbb {N}}_+}\). A normalizing isomorphism for a reachable layer \({B}\in {\widehat {{\mathscr{B}}}({\Sigma }, {w})}\) is a pair \(({\pi ,\pi ^{\prime }})\) of bijections \(\pi \colon {\ell }({B})\rightarrow \llbracket {\lvert {{\ell }({B})}\rvert }\rrbracket \) and \(\pi ^{\prime }\colon {r}({B})\rightarrow \llbracket {\lvert {{r}({B})}\rvert }\rrbracket \) such that the layer \({\langle {\pi {B}\pi ^{\prime }}\rangle }\) is normalized. Let \({k}\in {{\mathbb {N}}_+}\) and D = B₁⋯B_k be a reachable ODD in \({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\). A normalizing isomorphism for D is a sequence \(\overline {\pi } = \langle {\pi _{0},\pi _{1},\ldots ,\pi _{{k}}}\rangle \) such that for each i ∈ [k], (π_i− 1,π_i) is a normalizing isomorphism for B_i.

Proposition 37

Let Σ be an alphabet and w. Every reachable ODD in \({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\) admits a unique normalizing isomorphism.

Proof

First, we claim that for each reachable, layer \({B}\in {\widehat {{\mathscr{B}}}({\Sigma }, {w})}\) and each bijection \(\pi \colon {\ell }({B})\rightarrow \llbracket {\lvert {{\ell }({B})}\rvert }\rrbracket \), there exists a unique bijection \(\pi ^{\prime }\colon {r}({B})\rightarrow \llbracket {\lvert {{r}({B})}\rvert }\rrbracket \) such that \({\langle {\pi {B}\pi ^{\prime }}\rangle }\) is normalized. Indeed, consider \({{B}^{\prime }}={\langle {{\pi }{B}{\pi }^{\prime \prime }}\rangle }\), where \({\pi }^{\prime \prime }\colon {r}({B})\rightarrow \llbracket {\lvert {{r}({B})}\rvert }\rrbracket \) denotes the identity function. Then, let \({\pi }^{\prime }\colon {r}({B})\rightarrow \llbracket {\lvert {{r}({B})}\rvert }\rrbracket \) be a bijection such that for each two right states \({\mathfrak {q}},{\mathfrak {q}}^{\prime }\in {r}({B})\), we have that \({\pi }^{\prime }({\mathfrak {q}})\leq {\pi }^{\prime }({\mathfrak {q}}^{\prime })\) if and only if \(\chi _{{{B}^{\prime }}}({\mathfrak {q}}) \leq \chi _{{{B}^{\prime }}}({\mathfrak {q}}^{\prime })\). One can readily verify that \({\langle {\pi {B}\pi ^{\prime }}\rangle }\) is normalized. Furthermore, since \({{B}^{\prime }}\) is deterministic, \(\chi _{{{B}^{\prime }}}\) is an injection from \({r}({{B}^{\prime }})\) to \({\ell }({{B}^{\prime }})\times {\Sigma }\), i.e., for each two distinct right states \({\mathfrak {q}},{\mathfrak {q}}^{\prime }\in {r}({{B}^{\prime }})\), we have that either \(\chi _{{{B}^{\prime }}}({\mathfrak {q}})<\chi _{{{B}^{\prime }}}({\mathfrak {q}}^{\prime })\) or \(\chi _{{{B}^{\prime }}}({\mathfrak {q}}^{\prime })<\chi _{{{B}^{\prime }}}({\mathfrak {q}})\). In other words, \(\chi _{{{B}^{\prime }}}\) describes a total order on \({r}({{B}^{\prime }})\). Therefore, \(\pi ^{\prime }\) is the unique bijection from r(B) to \(\llbracket {\lvert {{r}({B})}\rvert }\rrbracket \) such that \({\langle {\pi {B}\pi ^{\prime }}\rangle }\) is normalized.

Let \({k}\in {{\mathbb {N}}_+}\) and \({{D}}={B}_{1}\cdots {B}_{{k}}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\) be an ODD such that B_i is a reachable layer for each i ∈ [k], ℓ(B_i+ 1) = r(B_i) for each i ∈ [k − 1], ι(B₁) = 1 and ι(B_i) = 0 for each i ∈{2,…,k}. Based on the previous claim, we prove by induction on k that the following statement holds: there exists a unique sequence 〈π₀,π₁,…,π_k〉 such that (1) \(\pi _{0}\colon {\ell }({B}_{1})\rightarrow \llbracket {\lvert {{\ell }({B}_{1})}\rvert }\rrbracket \) is a bijection, (2) \(\pi _{i}\colon {r}({B}_{i})\rightarrow \llbracket {\lvert {{r}({B}_{i})}\rvert }\rrbracket \) is a bijection for each i ∈ [k], and (3) 〈π_i− 1B_iπ_i〉 is a normalized layer for each i ∈ [k].

Base case. :

Consider k = 1. Since B₁ is deterministic, \(\lvert {{\ell }({B}_{1})}\rvert = 1\). Thus, the bijection \(\pi _{0}\colon {\ell }({B}_{1})\rightarrow \llbracket {\lvert {{\ell }({B}_{1})}\rvert }\rrbracket \) is trivially uniquely determined. As a result, there exists a unique sequence 〈π₀,π₁〉 satisfying the required conditions (1)–(3).

Inductive step. :

Consider k > 1. Let \({{D}^{\prime }}={B}_{1}\cdots {B}_{{k}-1}\) be the string obtained from D = B₁⋯B_k by removing the layer B_k. It follows from the inductive hypothesis that there exists a unique sequence 〈π₀,π₁,…,π_k− 1〉 such that \(\pi _{0}\colon {\ell }({B}_{1})\rightarrow \llbracket {\lvert {{\ell }({B}_{1})}\rvert }\rrbracket \) is a bijection, \(\pi _{i}\colon {r}({B}_{i})\rightarrow \llbracket {\lvert {{r}({B}_{i})}\rvert }\rrbracket \) is a bijection for each i ∈ [k − 1], and 〈π_i− 1B_iπ_i〉 is a normalized layer for each i ∈ [k − 1]. In particular, we note that the bijection π_k− 1 is uniquely determined. Furthermore, based on the previous claim, there exists a unique bijection \(\pi _{{k}}\colon {r}({B}_{{k}})\rightarrow \llbracket {\lvert {{r}({B}_{{k}})}\rvert }\rrbracket \) such that 〈π_k− 1B_kπ_k〉 is normalized. Therefore, there exists a unique sequence 〈π₀,π₁,…,π_k〉 satisfying the required conditions (1)–(3).

□

Proposition 38

Let Σ be an alphabet, \({w},{k}\in {{\mathbb {N}}_+}\) and \({{D}}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\). If D is a reachable, deterministic ODD and \(\overline {\pi } = \langle {\pi _{0},\pi _{1},\ldots ,\pi _{{k}}}\rangle \) is the unique normalizing isomorphism for D, then \({{D}^{\prime }} = {\langle {\pi _{0}{B}_{1}\pi _{1}}\rangle }\cdots {\langle {\pi _{{k}-1}{B}_{{k}}\pi _{{k}}}\rangle }\) is a normalized ODD such that \({{\mathscr{L}}({{D}^{\prime }})} = {{\mathscr{L}}({{D}})}\).

Proof

It immediately follows from the definition of normalizing isomorphism that \({{D}^{\prime }}\) is normalized. Finally, we note that \(\overline {\pi }\) is an isomorphism from D to \({{D}^{\prime }}\). Therefore, by Proposition 3, \({{\mathscr{L}}({{D}^{\prime }})} = {{\mathscr{L}}({{D}})}\). □

For each finite set X, we denote by \(\mathbb {S}_{X} \doteq \lbrace {\pi \colon X\rightarrow \llbracket {\lvert {X}\rvert }\rrbracket \colon \pi \text { is a bijection}}\rbrace \) the set of all bijections from X to \(\llbracket {\lvert {X}\rvert }\rrbracket \). For each alphabet Σ and each \({w} \in {{\mathbb {N}}_+}\) we define the following set.

We let \(\eta [{\Sigma },{w}]:\mathcal {S}[{\Sigma },{w}] \rightarrow {\widehat {{\mathscr{B}}}({\Sigma }, {w})}\) be the map that sends each triple \(({\pi ,{B},\pi ^{\prime }}) \in \mathcal {S}[{\Sigma },{w}]\) to the layer \({\langle {\pi {B}\pi ^{\prime }}\rangle }\). Moreover, we let \(\text {NR}[{\Sigma },{w}]\subseteq {\widehat {{\mathscr{B}}}({\Sigma }, {w})}\times \mathcal {S}[{\Sigma },{w}]\) and \(\text {NC}[{\Sigma },{w}]\subseteq \mathcal {S}[{\Sigma },{w}]\times \mathcal {S}[{\Sigma },{w}]\) be the following relations.

Finally, for each alphabet Σ, and each positive integer \({w} \in {{\mathbb {N}}_+}\), we let \(\mathfrak {nor}[{\Sigma },{w}]\) be the \(({\widehat {{\mathscr{B}}}({\Sigma }, {w})},{\widehat {{\mathscr{B}}}({\Sigma }, {w})})\)-transduction

The next lemma states that \(\mathfrak {nor}\) is a transduction that sends each reachable, deterministic, complete ODD \({D}\in {\widehat {{\mathscr{B}}}({{\Sigma }},{{w}})^{\protect \circledast }}\) to as normalized, deterministic, complete ODD \({{D}^{\prime }}\in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\) that has the same language as D.

Lemma 39 (Normalization Transduction)

For each alphabet Σ and each positive integer \({w}\in {{\mathbb {N}}_+}\), the following statements hold.

1. 1.

   \(\mathfrak {nor}[{\Sigma },{w}]\) is functional.

2. 2.

   \(\mathsf {Dom}(\mathfrak {nor}[{\Sigma },{w}]) \supseteq \lbrace {{D} \in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }} \colon {D} \text { is reachable}}\rbrace \).

3. 3.

   For each pair \(({{D}},{{D}^{\prime }})\in \mathfrak {nor}[{\Sigma },{w}]\), if D is reachable then \(D^{\prime }\in \widehat {{\mathscr{B}}}({\Sigma },{w})^{\protect \circledast }\), \({\mathscr{L}}({D^{\prime }}) = {\mathscr{L}}({D})\) and \(D^{\prime }\) is normalized.

Proof

We note that \(\mathfrak {nor}[{\Sigma },{w}]\) consists of all pairs \(({{{D}},{{D}^{\prime }}})\) of non-empty strings over the alphabet \({\widehat {{\mathscr{B}}}({\Sigma }, {w})}\) satisfying the conditions that \(\lvert {{{D}}}\rvert =\lvert {{{D}^{\prime }}}\rvert \) and that, if D = B₁⋯B_k and \({D^{\prime }}={B^{\prime }}_{1}\cdots {B^{\prime }}_{{k}}\) for some \({k}\in {{\mathbb {N}}_+}\), then there exists a sequence of permutations \(\overline {\pi } = \langle {\pi _{0},\pi _{1},\ldots ,\pi _{{k}}}\rangle \) such that for each i ∈ [k], \((\pi _{i-1},{B}_{i},\pi _{i})\in \mathcal {S}[{\Sigma },{w}]\) and \({B}_{i}^{\prime } = {\langle {\pi _{i-1}{B}_{i}\pi _{i}}\rangle }\). Additionally, based on Proposition 37, each reachable, deterministic (Σ,w)-ODD admits a unique normalizing isomorphism. As a result, we obtain that \(\mathsf {Dom}(\mathfrak {nor}[{\Sigma },{w}]) \supseteq \lbrace {{D} \in {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }} \colon {D} \text { is reachable}}\rbrace \). Moreover, if \(({{{D}},{{D}^{\prime }}})\in \mathfrak {d}({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }})\circ \mathfrak {nor}[{\Sigma },{w}]\), then \({{D}^{\prime }} = {\langle {\pi _{0}{B}_{1}\pi _{1}}\rangle }\cdots {\langle {\pi _{{k}-1}{B}_{{k}}\pi _{{k}}}\rangle }\), where \(\overline {\pi } = \langle {\pi _{0},\pi _{1},\ldots ,\pi _{{k}}}\rangle \) denotes the unique normalizing isomorphism of D; thus, by the uniqueness of \(\overline {\pi }\), the transduction \(\mathfrak {d}({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }})\circ \mathfrak {nor}[{\Sigma },{w}]\) is functional. Finally, it follows from Proposition 38 that for each pair \(({{{D}},{{D}^{\prime }}})\in \mathfrak {nor}[{\Sigma },{w}]\) such that D is a reachable ODD in \({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\), we have that \({{D}^{\prime }}\) is a normalized ODD in \({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\) that has the same language as D.

The fact that \(\mathfrak {nor}[{\Sigma },{w}]\) is \(2^{O(|{\Sigma }|\cdot {w}\cdot \log {w})}\)-regular follows from Proposition 5.(2) together with the fact that the multimap transductions \(\mathfrak {mm}[\text {NR}[{\Sigma },{w}]]\) and \(\mathfrak {mm}[\eta [{\Sigma },{w}]]\) are 2-regular (Proposition 25.(1)), and that the transduction \(\mathfrak {cp}[\text {NC}\) [Σ,w]] is \(2^{O(|{\Sigma }|\cdot {w}\cdot \log {w})}\)-regular (Proposition 25.(2)), given that \(\text {NC}[{\Sigma },{w}] \subseteq \mathcal {S}[{\Sigma },{w}]\times \mathcal {S}[{\Sigma },{w}]\), and that \(|\mathcal {S}[{\Sigma },{w}]|=2^{O(|{\Sigma }|\cdot {w}\cdot \log {w})}\). □

6.6 Putting All Steps Together

In this subsection we combine Observation 26 with Lemma 27, Lemma 30, Lemma 36 and Lemma 39 to prove our Canonization as Transduction Theorem (Theorem 9). Consider the transduction

Since each of the four transductions in the composition is at most \(2^{O(|{\Sigma }|\cdot w \cdot \log w)}\)-regular, we have that \(\widehat {\mathfrak {can}}[{\Sigma },{w}]\) is \(2^{O(|{\Sigma }|\cdot {w}\cdot \log {w})}\)-regular. Since each these four transductions is functional, the transduction \(\widehat {\mathfrak {can}}[{\Sigma },{w}]\) is functional. Since \(\mathsf {Dom}(\mathfrak {d}({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }})) = {\widehat {{\mathscr{B}}}({{\Sigma }},{{w}})^{\protect \circledast }}\) and the image of each of the three first transductions is contained in the domain of the next transduction (from left to right), we have that \(\mathsf {Dom}(\widehat {\mathfrak {can}}[{\Sigma },{w}]) = {{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\). Now, let \(({{D}},{{D}}^{\prime })\) be a pair of ODDs in \(\widehat {\mathfrak {can}}[{\Sigma },{w}]\). Then there exist ODDs D₁ and D₂ such that \(({{D}},{{D}}_{1})\in \mathfrak {rea}[{\Sigma },{w}]\), \(({{D}}_{1},{{D}}_{2})\in \mathfrak {mer}[{\Sigma },{w}]\), and \(({{D}}_{2},{{D}}^{\prime })\in \mathfrak {nor}[{\Sigma },{w}]\). Since each of these transductions is language preserving, we have that \({{\mathscr{L}}({{D}})}={{\mathscr{L}}({{D}}_{1})}={{\mathscr{L}}({{D}}_{2})}={{\mathscr{L}}({{D}}^{\prime })}\). Since \({{D}}\in {\widehat {{\mathscr{B}}}({{\Sigma }},{{w}})^{\protect \circledast }}\), we have that D is by definition deterministic and complete. By Lemma 30, D₁ is deterministic, complete and reachable. By Lemma 36, D₂ is deterministic, complete and minimized. Finally, by Lemma 39, \({{D}}^{\prime }\) is deterministic, complete, minimized and normalized. Since for each ODD D, there is a unique deterministic, complete, minimized and normalized ODD \(\mathcal {C}({{D}})\) with the same language as D, we have that \({{D}}^{\prime }=\mathcal {C}({{D}})\). This shows that \(\widehat {\mathfrak {can}}[{\Sigma },{w}] = \{({{D}},\mathcal {C}({{D}})) : {{D}}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\}\).

Now, consider the transduction

Since \(\widehat {\mathfrak {can}}[{\Sigma },{w}]\) is \(2^{O(|{\Sigma }|\cdot {w} \cdot \log {w})}\)-regular, we have that \(\widehat {\mathfrak {can}}[{\Sigma },2^{{w}}]\) is \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\)-regular. This implies that \(\mathfrak {can}[{\Sigma },{w}]\) is also \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\)-regular. Since \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}= \mathsf {Dom}(\mathfrak {det}[{\Sigma },{w}])\) and \(\mathsf {Im}(\mathfrak {det}[{\Sigma },{w}])\) is included in \(\mathsf {Dom}(\widehat {\mathfrak {can}}[{\Sigma },2^{{w}}])\), we have that \(\mathsf {Dom}(\mathfrak {can}[{\Sigma },{w}]) = {{\mathscr{B}}({{\Sigma }},{{w}})^{\protect \circledast }}\). Now, let \(({{D}},{{D}}^{\prime })\) be a pair of ODDs in \(\mathfrak {can}[{\Sigma },{w}]\). Then there is an ODD \({{D}}_{1}\in {\widehat {{\mathscr{B}}}({{\Sigma }},{2^{{w}}})^{\protect \circledast }}\) such that \(({{D}},{{D}}_{1})\in \mathfrak {det}[{\Sigma },{w}]\) and \(({{D}}_{1},{{D}}^{\prime })\in \widehat {\mathfrak {can}}[{\Sigma },2^{{w}}]\). By Lemma 27, we have that D₁ is complete, deterministic and \({{\mathscr{L}}({{D}})}={{\mathscr{L}}({{D}}_{1})}\). Additionally, \({{D}}^{\prime } = \mathcal {C}({{D}}_{1})\). Since \({{\mathscr{L}}({{D}})} = {{\mathscr{L}}({{D}}_{1})} = {{\mathscr{L}}(\mathcal {C}({{D}}_{1}))} = {{\mathscr{L}}({{D}}^{\prime })}\), we have that \({D}^{\prime } = \mathcal {C}({{D}}_{1}) = \mathcal {C}({{D}})\). This shows that \(\mathfrak {can}[{\Sigma },{w}] = \{({{D}},\mathcal {C}({{D}})) : {{D}}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\}\). \(\square \)

In this work, we have introduced the notion of second-order finite automata, a formalism that combines traditional finite automata with ODDs of bounded width in order to represent possibly infinite classes of languages. Our main result (Theorem 10) is a canonical form of canonical forms theorem. It states for each second-order finite automaton \({\mathcal {F}}\), one can construct a canonical form \(\mathcal {C}_{2}({\mathcal {F}})\) whose language \({{{\mathscr{L}}}(\mathcal {C}_{2}({\mathcal {F}}))} = \{\mathcal {C}({{D}}) : {{D}}\in {{{\mathscr{L}}}({\mathcal {F}})}\}\) is precisely the set of canonical forms of ODDs in \({{{\mathscr{L}}}({\mathcal {F}})}\). Here, the canonical form \(\mathcal {C}({{D}})\) of an ODD D is the usual deterministic, complete, normalized ODD with minimum number of states having the same language as D. In this sense, the ODDs in \({{{\mathscr{L}}}(\mathcal {C}_{2}({\mathcal {F}}))}\) carry useful complexity theoretic information about the languages they represent in the class \({{{\mathscr{L}}}_{2}({\mathcal {F}})} = {{{\mathscr{L}}}_{2}(\mathcal {C}_{2}({\mathcal {F}}))}\).

Our canonization result immediately implies that the collection of regular-decisional classes of languages is closed under union, intersection, set difference, and a suitable notion of bounded-width complementation. This result also implies that inclusion and non-emptiness of intersection for regular-decisional classes of languages are decidable. Furthermore, non-emptiness of intersection for the second languages of second-order finite automata \({\mathcal {F}}_{1}\) and \({\mathcal {F}}_{2}\) can be solved in fixed parameter tractable time when the parameter is the maximum width of an ODD accepted by \({\mathcal {F}}_{1}\) or \({\mathcal {F}}_{2}\).

We also provided two algorithmic applications of second-order automata to the theory of ODDs. First, we have shown that several width/size minimization problems for ODDs can be solved in fixed-parameter tractable time when parameterized by the width of the input ODD. This implies corresponding FPT algorithms for width/size minimization of ordered binary decision diagrams (OBDDs) with a fixed ordering. Previous to our work, only exponential algorithms were known. Finally, we have shown that second-order finite automata can be used to count the exact number of distinct functions computable by (Σ,w)-ODDs of a given width w and a given length k in time \(2^{2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}}\cdot {k}^{O(1)}\), and in time \(2^{2^{O(|{\Sigma }|\cdot {w} \cdot \log {w})}}\cdot {k}^{O(1)}\) if only deterministic, complete ODDs are considered. It is worth noting that the naive process of enumerating functions while eliminating repetitions takes time (and space) exponential in both w and in k.

Regular Canonizing Relations

Most results in this work are obtained as a consequence of Theorem 9, which states that the relation \(\mathfrak {can}[{\Sigma },{w}] = \{({{D}},\mathcal {C}({{D}})) : {{D}}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\}\) is a regular relation. It is worth noting that aside from complexity theoretic considerations, Theorem 10 and Theorem 13 have identical proofs if we replace \(\mathfrak {can}[{\Sigma },{w}]\) with any regular canonizing relation R(Σ,w) for \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\) in the sense we will define below. Nevertheless, when taking complexity considerations into account, and also when considering our applications in Section 5, the fact that the transductions \(\mathfrak {can}[{\Sigma },{w}]\) and \(\widehat {\mathfrak {can}}[{\Sigma },{w}]\) are \(2^{O(|{\Sigma }|\cdot {w} \cdot 2^{{w}})}\)-regular and \(2^{O(|{\Sigma }|\cdot {w} \cdot \log {w})}\)-regular respectively play an important role. Additionally, some of our results use explicitly the fact the canonical form \(\mathcal {C}({{D}})\) has minimum number of states among all deterministic, complete ODDs with the same language as D.

Say that a relation \(R({\Sigma },{w}) \subseteq {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\times {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\) is canonizing for \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\) if the following three conditions are verified.

1. 1.

   R(Σ,w) is functional and the domain of R(Σ,w) is equal to \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\).

2. 2.

   For each \(({{D}},{{D}}^{\prime })\in R({\Sigma },{w})\), \({{\mathscr{L}}({{D}})} = {{\mathscr{L}}({{D}}^{\prime })}\).

3. 3.

   \(({{D}},{{D}}^{\prime })\in R({\Sigma },{w})\) implies that \(({{D}}^{\prime \prime },{{D}}^{\prime })\in R({\Sigma },{w})\) for each \({{D}}^{\prime \prime }\in {{\mathscr{B}}({{\Sigma }},{{w}})^{\protect \circledast }}\) with \({\mathscr{L}}({D})={\mathscr{L}}({D^{\prime \prime }})\).

The notion of a relation \(\widehat {R}({\Sigma },{w})\) that is canonizing for \({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\) can be defined analogously. An interesting question is whether there are canonizing relations with significantly better complexity than the ones of \(\mathfrak {can}[{\Sigma },{w}]\) and \(\widehat {\mathfrak {can}}[{\Sigma },{w}]\). More specifically, is there some canonizing relation for \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}\) that is α-regular for \(\alpha = 2^{f(|{\Sigma }|)\cdot 2^{o({w})}}\) where f is a function depending only on the size of the alphabet? Similarly, is there some canonizing relation for \({{\widehat {{\mathscr{B}}}({\Sigma }, {w})}^{\protect \circledast }}\) that is α-regular for some \(\alpha = 2^{o(f(|{\Sigma }|)\cdot {w} \cdot \log {w})}\)? In view of Observation 14, a canonizing relation of complexity α = 2^{O(f(|Σ|)⋅w)} would imply that emptiness of intersection regular-decisional classes of languages can be realized in polynomial time even when w is logarithmic in the size of the input second-order finite automata representing these classes of languages.

Connections with the Theory of Automatic Structures

Finite automata operating with ODDs and tuples of ODDs were first considered in [15] as a formalism to provide a uniform representation of classes of finite relational structures of bounded ODD-width. The technical results from [13] rely on two observations. First, that the relation \(\mathcal {R}_{\in }({\Sigma },{w}) = \{({{D}},s) : {{D}}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}, s\in {{\mathscr{L}}({{D}})}\}\) is regular (Proposition 6.3 of [13]). Second, that the relation \(\mathcal {R}_{\subseteq }({\Sigma },{w}) = \{({{D}},{{D}}^{\prime }) : {{D}},{{D}}^{\prime }\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}, {{\mathscr{L}}({{D}})}\subseteq {{\mathscr{L}}({{D}}^{\prime })}\}\) is regular (Proposition 6.6 of [13]). Similar observations have been used in [32] to study second-order finite automata using the framework of the theory of automatic structures [1, 2, 31]. In particular, some of our decidability and closure results have been rederived in [32] using this framework, and some new applications of second-order finite automata to partial-order theory have been obtained.

As pointed out in [32], the fact that automatic structures are closed under first-order interpretations [8, 23, 31] has also applications in our framework. For instance, one can infer that the relation \(\mathcal {R}_{\subseteq }({\Sigma },{w})\) is automatic from the fact that \(\mathcal {R}_{\in }({\Sigma },{w})\) is automatic, together with the fact that for each two ODDs \({{D}},{{D}}^{\prime }\), the inclusion \({{\mathscr{L}}({{D}})}\subseteq {{\mathscr{L}}({{D}}^{\prime })}\) is defined by the first-order formula \(\forall s, ({{{D}},s}) \in \mathcal {R}_{\in }({\Sigma },{w}) \Rightarrow ({{{D}^{\prime }},s}) \in \mathcal {R}_{\in }({\Sigma },{w})\). Similarly, the relation \(\mathcal {R}_{=}({\Sigma },{w}) = \lbrace {({{{D}},{{D}^{\prime }}}) : {{D}}, {{D}^{\prime }}\in {{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circledast }}, {{\mathscr{L}}({D})} = {{\mathscr{L}}({D^{\prime }})}}\rbrace \) can be inferred to be automatic from the fact the equality \({{\mathscr{L}}({{D}})} = {{\mathscr{L}}({{D}}^{\prime })}\) is defined by the first-order formula \(\forall s, ({{{D}},s}) \in \mathcal {R}_{\in }({\Sigma },{w}) \Leftrightarrow ({{{D}^{\prime }},s}) \in \mathcal {R}_{\in }({\Sigma },{w})\). Since relations definable in this way can be accepted by finite automata of size \(f(\lvert {{\Sigma }}\rvert ,{w})\), for some function f, the interplay between automatic structures and first-order logics may be useful in the development of algorithms that decide properties of ODDs in \({{{\mathscr{B}}({\Sigma }, {w})}^{\protect \circ {{k}}}}\) in time fixed-parameter linear time \(f(\lvert {{\Sigma }}\rvert ,{w})\cdot {k}\), although the functions \(f(\lvert {{\Sigma }}\rvert ,{w})\) obtained by a direct application of this approach may be very large. We refer to [22] for an updated survey on the theory of automatic structures.

Jain, Luo and Stephan have introduced the notion of automatic indexed classes of languages as a tool to address some problems in computational learning theory [29]. An indexed class of languages {L_α : α ∈ I} is said to be automatic if the relation E = {(α,x) : x ∈ L_α,α ∈ I} is automatic. The fact that \(\mathcal {R}_{\in }({\Sigma },{w})\) is regular immediately implies that any regular-decisional class of languages corresponds to an automatic class of languages. Indeed, given a second-order finite automaton \({\mathcal {F}}\), the second language of \({\mathcal {F}}\), \({{{\mathscr{L}}}_{2}({\mathcal {F}})} = \{{{\mathscr{L}}({{D}})} : {{D}} \in {{{\mathscr{L}}}({\mathcal {F}})}\}\), is an automatic class of languages where each \({{D}}\in {{{\mathscr{L}}}({\mathcal {F}})}\) is regarded as an index, and \({{\mathscr{L}}({{D}})}\) is regarded as the language indexed by D. Henning Fernau conjectured that if {L_α : α ∈ I} is an automatic class of languages where each index α ∈ I is a finite string and all strings in L_α have the same length, then this class is regular-decisional (i.e. is equal to the second language of some second-order finite automaton). This conjecture has recently been confirmed by Kuske in [32]. Similar connections can be established with the framework of uniform classes of automatic structures [39], which are defined with basis on the notion of automatic structures with advice. In this context, an ODD D may be regarded as an advice string, while the language \({{\mathscr{L}}({{D}})}\) may be regarded as the set of strings associated with the advice D. This point of view is particularly relevant when ODDs are used to represent relations, as done for instance in [13].

In view of the connections discussed above, our framework provides a suitable parameterization for problems arising in the realm of the theory of automatic classes of languages [29] and in the realm of the theory of uniformly automatic classes of structures [39]. The intuition is that the size of the representation for the whole class of languages/structures (i.e, the size of the second-order finite automaton given at the input) is completely dissociated from the complexity of the languages/structures being represented in the class (i.e. the ODD-width w necessary to represent languages/structures in the class). Since the concepts in [29, 39] have applications in the fields of learning theory [7, 24, 27, 28] and algebra [9, 30, 38, 39], an interesting line of research would be the investigation of potential applications of our fixed-parameter tractable algorithms to problems in these fields.