APERIODICITY, STAR-FREENESS, AND FIRST-ORDER LOGIC DEFINABILITY OF STRUCTURED CONTEXT-FREE LANGUAGES

A classic result in formal language theory is the equivalence among noncounting, or aperiodic, regular languages, and languages defined through star-free regular expressions, or first-order logic. Past attempts to overcome the finite-state hypothesis have met with difficulties: for instance it is known that star-free tree languages may violate the non-counting property. We extend such classic equivalence results to a significant family of deterministic context-free languages, the operator-precedence languages (OPL), which strictly includes the widely investigated visibly pushdown, alias input-driven, family and other structured context-free languages. The OP model originated in the ’60s for defining programming languages and is still used by high performance compilers; its rich algebraic properties have been investigated initially in connection with grammar learning and recently completed with further closure properties and with monadic second order logic definition. We introduce an extension of regular expressions, the OP-expressions (OPE) which define the OPLs and, under the star-free hypothesis, define first-order definable and noncounting OPLs. Then, we prove, through a fairly articulated grammar transformation, that aperiodic OPLs are first-order definable. Thus, the classic equivalence of star-freeness, aperiodicity, and first-order definability is established for the large and powerful class of OPLs. Since operator precedence languages strictly include other classes of structured languages such as visibly pushdown languages, the same results given in this paper hold as trivial corollary for that family too.

1. Introduction. From a long time much research effort in the field of formal language theory has been devoted to extend as much as possible the nice algebraic and logic properties of regular languages to larger families of languages, typically the context-free (CF) ones or subfamilies thereof. Regular languages in fact are closed w.r.t. all basic algebraic operations and are characterized also in terms of classic monadic second-order (MSO) logic (with the ordering relation between character positions) [9,23,49], but not so for general CF languages.
On the other hand, some important algebraic and logic properties of regular languages are preserved by certain subfamilies of the CF languages, that may be referred to as structured CF languages because the syntax structure is immediately visible in their sentences. Two first and practically equivalent examples of such languages are parenthesis languages and tree languages introduced respectively by McNaughton [36] and Thatcher [46]. More recently, visibly pushdown languages (VPL) [4], originally introduced as input-driven languages (IDL) [50], height-deterministic [39] and synchronized languages [10] have also been shown to share many important properties of regular languages. In particular tree languages and VPLs are closed w.r.t. Boolean operations, concatenation, Kleene * and are characterized in terms of some MSO logic, although such operations and the adopted logic language are not the same in the two cases. For a more complete analysis of structured languages and how they extend algebraic and logic properties of regular languages, see [33].
In this paper we study for structured CF languages three important language features, namely the noncounting (NC) or aperiodicity, the star-freeness (SF), and the first-order (FO) logic definability properties, which for regular languages are known to be equivalent [38].
Intuitively, a language has the aperiodicity property if the recognizing device -a finite state automaton in the case of regular languages-cannot separate two strings that only differ by the count, modulo an integer greater than 1, of the occurrences of some substring. Linguists and computer scientists alike have observed that human languages, both natural and artificial, are NC. SF regular languages are definable through a star-free regular expression (RE), i,e, an expression composed exclusively by means of Boolean operations and concatenation. FO logic defined regular languages are characterized by the first-order (FO) restriction of MSO logic. The above properties, together with other equivalent ones which are not the object of the present investigation [38], have ignited various important practical applications in the realm of regular languages. FO definition, in particular, has a tremendous impact on the success of model-checking algorithms, thanks to the first-order completeness of linear temporal logic 1 : most model-checkers of practical usefulness exploit NC languages.
Moving from regular languages to suitable families of structured CF languages is certainly a well motivated goal: the aperiodicity property, in fact, is perhaps even more important for CF languages than for regular ones: whereas various hardware devices, e.g., count modulo some natural number, it is quite unlikely that a programming, a data description, or a natural language exhibits counting features such as forbidding an even number of nested loops or recursive procedure calls. We could claim that most if not all of CF languages of practical interest have an aperiodic structure.
Noncounting parenthesis languages have been first introduced in [15]. Then, an equivalent definition in terms of tree languages has been given in [47]. Until now, however, very few results are available. In facts, the three equivalent characterizations that hold for NC regular languages could not be confirmed. We mention the negative result for tree languages [47] saying that star-free tree languages may be counting; of course, the notion of star-freeness for tree languages is based on a suitable redefinition of concatenation for trees. The same work and further subsequent studies (e.g., [28,24,29,42]) provided partial results by investigating special subclasses of the various involved families but the original simplicity and beauty of the regular language properties was lost.
In this paper we show that the three equivalent characterizations holding for NC regular languages can be extended to the family of operator precedence languages. It is worthwhile to outline the OPL history and their practical and theoretical development.
Invented by R. Floyd [25] to support fast deterministic parsing, operator precedence grammars (OPG) are still used within modern compilers to parse expressions with operators ranked by priority. The syntax tree of a sentence is determined by three binary precedence relations over the terminal alphabet that are easily pre-computed from the grammar productions. We classify OPLs as "structured but semi-visible" languages since their structure is implicitly assigned by such precedence relations. For readers unacquainted with OPLs, we anticipate an example: the arithmetic sentence a + b * c does not make manifest the natural structure (a + (b * c)), but the latter is implied by the fact that the plus operator yields precedence to the times.
It was soon realized [19] that, thanks to the tree structure assigned to strings by the precedence relations, many closure properties of regular languages and other structured CF ones hold for OPLs too; this despite the fact that, unlike other better known structured languages, OPLs need a simple parsing process to make their syntax trees explicit. This fact accounts for the wider generative capacity that makes OPLs suitable to define programming and data description languages.
After a long intermission, theoretical research [18] proved further algebraic properties of OPLs, thus moving some steps ahead from regular to structured CF languages. At the same time, it was found that the VPLs are a particular case of the OPLs characterized by the precedence relations encoded in the 3-partition of their alphabet; OPLs considerably generalize VPLs while retaining their closure properties. Then in [32] the Operator Precedence automata (OPA) recognizing OPLs where introduced to formalize the efficient parallel parsing algorithm implemented in [6]. We also produced in [32] an MSO logic characterization that naturally extends the classic one for regular languages.
Thus, OPLs' potential for practical applications is broader than other structured CF languages: the following example hints to applications for automatic proof of systems properties. OPLs with their corresponding MSO logic may be used to specify and prove properties of software systems where the typical LIFO policy of procedure calls and returns can be broken by unexpected events such as interrupts or exceptions [32,33], a feature that is not available in VPLs and their MSO logic [3].
In summary, to the best of our knowledge, OPLs are currently the largest language family that retains the main closure and decidability properties of regular languages, including a logical characterization naturally extending the classic one.
We recently realized that a NC subclass of OPLs introduced long ago in the course of grammar-inference studies [20,17] is FO logic definable [31]. This lead us to the present successful search of equivalent characterizations of aperiodic, star-free and FO definable OPLs. Our approach is based on two key ideas: 1. Since the traditional attempt at extending NC regular languages to tree languages had deadlocked, we went back to string languages. Accordingly, we use the operation of string concatenation and not the append operation of tree languages (that is responsible for the counterexample in [47] showing that there are counting star-free tree languages). 2. We kept using the MSO logic of our past work [32,31], which had been inspired by preceding work on CF string languages [30] and on VPLs [4]. Such logics too are defined on strings rather than on trees. We examined its restriction to the FO case. The main results of this paper are: • The introduction (in Section 3) of operator precedence expressions (OPE) which extend regular expressions: they add to the classical operations a new one, called fence, that imposes a matching between two (hidden) parentheses: we show that OPEs define the OPL family. • The proof (in Section 4) that the OPLs defined by star-free OPEs coincide with the ones defined by FO formulas, and (in Section 5) the proof that they have the aperiodicity property. • Finally, (in Section 7) the proof that every NC OPL can be defined by means of an FO formula. The proof, articulated in several lemmas, exploits a regular language control theorem (in Section 6) which, informally, "splits" the logic formulas defining an OPL into a part describing its tree-like structure and another part that imposes a regular control on the strings derived from grammar's nonterminal symbols. After a series of nontrivial transformations of finite automata, we obtain the result that the control language can be made NC if the original OPL is in turn NC. Thanks to the fact that both parts of the logic formulas can be defined in FO logic, we obtain the language family identities: OPLs = OPE-languages = MSO-languages NC-OPLs = SF-OPE-languages = FO-languages which extend the classic equivalences for regular languages and can be immediately transposed to VPLs. Section 2 provides the necessary terminology and background on OPLs, aperiodicity, parenthesis languages, MSO and FO logic characterization. The conclusion mentions new application-oriented developments rooted in the present results, consisting of a suitable, FO-complete, temporal logic and a model-checker to prove properties of aperiodic OPLs. New directions for future research are also suggested.

Preliminaries.
We assume some familiarity with the classical literature on formal language and automata theory, e.g., [44,27]. Here, we just list and explain our notations for the basic concepts we use from this theory. The terminal alphabet is usually denoted by Σ, and the empty string is ε. For a string, or set, x, |x| denotes the length, or the cardinality, of x. The character #, not present in the terminal alphabet, is used as string delimiter, and we define the alphabet Σ # = Σ ∪ {#}. Other special symbols augmenting Σ will be introduced in the following.
2.1. Regular languages: automata, regular expressions, logic. Finite Automata. A finite automaton (FA) A is defined by a 5-tuple (Q, Σ, δ, I, F ) where Q is the set of states, δ the state-transition relation (or its graph denoted by −→), δ ⊆ Q × Σ × Q; I and F are the nonempty subsets of Q respectively comprising the initial and final states. If the tuple (q, a, q ) is in the relation δ, the edge q a − −→ q is in the graph. The transitive closure of the relation is defined as usual. Thus, for a string x ∈ Σ * such that there is a path from state q to q labeled with x, the notation q x − −→ q is equivalent to (q, x, q ) ∈ δ * ; if q ∈ I and q ∈ F , then the string x is accepted by A. The language of the accepted strings is denoted by L(A); it is called a regular language.
In this paper we make use of two well-known extensions of the previous FA definition, both not impacting on the language family recognized. In the first extension, we permit an edge label to be the empty string; such an edge is called a spontaneous transition or step. In the second one, an edge label may be a string in Σ + . These two classical extensions are formalized by letting δ δ δ ⊆ Q × Σ * × Q, where for clarity, the extended transition relation is written in boldface. An edge (q, x, q ) ∈ δ δ δ is called a macro-transition or macro-step and is denoted by q x −→ −→ −→ δ δ δ q . Whenever there will be no risk on ambiguity we will omit the label δ δ δ in the edge.
Regular expressions and star-free languages. A regular expression (RE) over an alphabet Σ is a well-formed formula made with the characters of Σ, ∅, ε, the Boolean operators ∪, ¬, ∩, the concatenation '·', and the Kleene star operator ' * '. We may also use the operator ' + '. When neither ' * ' nor ' + ' are used, the RE is called star-free (SF). An RE E defines a language over Σ, denoted by L(E).
Monadic second and first order logics to define languages [48]. A monadic second order (MSO) logic on an alphabet Σ is a well-formed formula made with first and second order variables interpreted, respectively, as string positions and sets of string positions, monadic predicates on string positions biunivocally associated to Σ elements, an ordering relation, and the usual logical connectors and quantifiers. When the logic is restricted to first-order variables only, it is named an FO-logic.
Non-counting or aperiodic regular languages. A regular language L over Σ is called noncounting (NC) or aperiodic if there exists an integer n ≥ 1 such that for all x, y, z ∈ Σ * , xy n z ∈ L iff xy n+m z ∈ L, ∀m ≥ 0. PROPOSITION 2.1 ([38]). Finite automata, regular expressions and MSO logic define the family of regular (or rational) languages (REG). The family of aperiodic regular languages coincides with the families of languages defined by star-free REs and by FO-logic.

Grammars.
DEFINITION 2.2 (Grammar and language). A (CF) grammar is a tuple G = (Σ, V N , P, S) where Σ and V N , with Σ ∩ V N = ∅, are resp. the terminal and the nonterminal alphabets, the total alphabet is V = Σ ∪ V N , P ⊆ V N × V * is the rule (or production) set, and S ⊆ V N , S = ∅, is the axiom set. For a generic rule, denoted as A → α, where A and α are resp. called the left/right hand sides (lhs / rhs), the following forms are relevant: axiomatic , at least one terminal is interposed between any two nonterminals occurring in α parenthesized : α = β where β ∈ V * , and , are new terminals.
A grammar is called backward deterministic or a BD- If all rules of a grammar are in operator form, the grammar is called an operator grammar or O-grammar.
A grammar G p = (Σ ∪ { , }, V N , P p , S) is a parenthesis grammar (Par-grammar) if the rhs of every rule is parenthesized. G p is called the parenthesized version of G, if P p consists of all rules A → α such that A → α is in P .
For brevity we give for granted the usual definition of derivation denoted by the symbols = =⇒ , (derivation in m steps); the subscript G will be omitted whenever clear from the context. We give also for granted the notion of syntax tree and that a parenthesized string is an equivalent way to represent a syntax tree of a CF grammar where internal nodes are unlabeled.
The language defined by a grammar starting from a nonterminal A is We call w a sentence if A ∈ S. The union of L G (A) for all A ∈ S is the language L(G) defined by G. The language generated by a Par-grammar is called a parenthesis language, and its sentences are well-parenthesized strings. Two grammars defining the same language are equivalent. Two grammars such that their parenthesized versions are equivalent, are structurally equivalent.
Notation: In the following, unless otherwise explicitly stated, lowercase letters at the beginning of the alphabet will denote terminal symbols, lowercase letters at the end of the alphabet will denote strings of terminals, Greek letters at the beginning of the alphabet will denote strings in V * . Capital letters will be used for nonterminal symbols.
Any grammar can be effectively transformed into an equivalent BD-grammar, and also into an O-grammar [5,27] without renaming rules and without empty rules but possibly a single rule whose lhs is an axiom not otherwise occurring in any other production. From now on, w.l.o.g., we exclusively deal with O-grammars without renaming and empty rules, with the only exception that, if ε is part of the language, there is a unique empty rule whose lhs is an axiom that does not appear in the rhs of any production. DEFINITION 2.3 (Backward deterministic reduced grammar [36,44] A BDR-grammar is both backward deterministic and reduced.
From [36], every parenthesis language is generated by a unique, up to an isomorphism of its nonterminal alphabet, Par-grammar that is BDR.
Intuitively, operator precedence grammars are O-grammars whose parsing is driven by three precedence relations, called equal, yield and take, included in Σ # × Σ # . A character a is equal in precedence to b iff some rhs of the grammar contains as substring ab or aBb, where B is a nonterminal, i.e., a and b are either adjacent in some rhs or are separated by at most one nonterminal; in fact, when evaluating the relations between terminal characters for OPG, the presence or not of -at most one-nonterminal is irrelevant; for this reason we often say that nonterminals are "transparent" for the parsing of OPLs.
A character a yields precedence to b iff during a grammar derivation it occurs immediately to the left of a rhs. Again, whether in the rhs there is a nonterminal character at the left of b or not is inessential. Symmetrically, a takes precedence over b iff a can occur as the rightmost terminal character of a rhs, whether followed or not by a nonterminal, and b is the immediately following terminal character. More precisely the three relations are defined as follows. Subsequently we show how they can drive the bottom-up parsing of sentences. DEFINITION 2.4 ([25]). Let G = (Σ, V N , P, S) be an O-grammar. Let a, b denote elements in Σ, A, B in V N , C either an element of V N or the empty string ε, and α, β range over V * . The left and right terminal sets of nonterminals are respectively: (The grammar name will be omitted unless necessary to prevent confusion.) The operator precedence relations (OPRs) are defined over Σ # × Σ # as follows: • equal in precedence: a . = b ⇐⇒ ∃A → αaCbβ ∈ P • takes precedence: a b ⇐⇒ ∃A → αBbβ ∈ P, a ∈ R(B); a # ⇐⇒ a ∈ R(B), B ∈ S • yields precedence: a b ⇐⇒ ∃A → αaBβ ∈ P, b ∈ L(B); # b ⇐⇒ b ∈ L(B), B ∈ S. The OPRs can be collected into a |Σ # | × |Σ # | array, called the operator precedence matrix of the grammar, OP M (G): for each (ordered) pair (a, b) ∈ Σ # × Σ # , OP M a,b (G) contains the OP relations holding between a and b.
More formally, consider a square matrix: We extend the set inclusion relations and the Boolean operations in the obvious cell by cell way, to any two matrices having the same terminal alphabet. Two matrices are compatible iff their union is conflict-free.
DEFINITION 2.5 (Operator precedence grammar). A grammar G is an operator precedence (or Floyd's) grammar, for short an OPG, iff the matrix OP M (G) is conflict-free, i.e. the three OP relations are disjoint.
An OPG is=-acyclic if OP M (G) is so. An operator precedence language (OPL) is a language generated by an OPG. Remarks. If the relation= is acyclic, then the length of the rhs of any rule of G is bounded by the length of the longest=-chain in OP M (G).
Notice that, unlike the arithmetic relations having similar typography, the OP relations do not enjoy any of the transitive, symmetric, reflexive properties. We kept the original Floyd's notation but we urge the reader not to be confused by the similarity of the two notations.
It is known that the family of OPLs is strictly included within the deterministic and reverse-deterministic CF family, i.e., the languages that can be deterministically parsed both from left to right and from right to left.
The key feature of OPLs is that a conflict-free OPM M defines a universe of strings compatible with M and associates to each of them a unique syntax tree whose internal nodes are unlabeled and whose leaves are elements of Σ, or, equivalently, a unique parenthesization. We illustrate such a feature through a simple example and refer the reader to previous literature for a thorough description of OP parsing [26,33]. # e + e * e + e # each pair , (with no further , in between) includes a possible rhs of a production of any OPG sharing the OPM with G AE , not necessarily a G AE rhs. Thus, as it happens in typical bottom-up parsing, we replace each string included within the pair , with a dummy nonterminal N ; this is because nonterminals are irrelevant for OPMs. The result is the string #N + N * N + N #. Next, we compute again the precedence relation between consecutive terminal characters by ignoring nonterminals: the result is # N + N * N +N #.
This time, there is only one pair , including a potential rhs determined by the OPM (the fact that the external and "look matched" is coincidental as it can be easily verified by repeating the previous procedure with the string e + e * e + e + e). Again, we replace the pattern N * N , with the dummy nonterminal N ; notice that there is no doubt about associating the two N s to the * rather than to one of the adjacent + symbols: if we replaced, say, just the * with an N we would obtain the string N + N N N + N which cannot be derived by an O-grammar. By recomputing the precedence relations we obtain the string # N + N +N #. Finally, There is an obvious one-to-one correspondence between the trees whose internal nodes are unlabeled or labeled by a unique character, and well-parenthesized strings on the enriched alphabet Σ ∪ { , }); e.g., the parenthesized string corresponding to the tree of Figure 2.2 is e + e * e + e .
Obviously, all sentences of L(G AE ) can be given a syntax tree by OP M (G AE ), but there are also strings in Σ * that can be parsed according to the same OPM but are not in L(G AE ). E.g., the string + + + is parsed according to the OP M (G AE ) as the parenthesis string + + + . Notice also that, in general, not every string in Σ * is assigned a syntax tree -or parenthesized string-by an OPM; e.g., in the case of OP M (G AE ) the parsing procedure applied to ee is immediately blocked since there is no precedence relation between e and itself.
The following definition synthesizes the concepts introduced by Example 2.6. DEFINITION 2.7 (OP-alphabet and Maxlanguage).
• A string in Σ * is compatible with an OPM M iff the procedure described in Example 2.6 terminates by producing the pattern #N #. The set of all strings compatible with an OPM M is called the maxlanguage or the universe of M and is simply denoted as L(M ). • Let M be a conflict-free OPM over Σ # × Σ # . We use the same identifier M to denote the -partial-function M : Σ * → (Σ ∪ { , }) * that assigns to strings in Σ * their unique well-parentesization as informally illustrated in Example 2.6. • The pair (Σ, M ) where M is a conflict-free OPM over Σ # × Σ # , is called an OPalphabet. We introduce the concept of OP-alphabet as a pair to emphasize that it defines a universe of strings on the alphabet Σ -not necessarily covering the whole Σ * -and implicitly assigns them a structure univocally determined by the OPM, or, equivalently, by the function M . • Let (Σ, M ) be an OP-alphabet. The class of (Σ, M )-compatible OPGs and OPLs are: Various formal properties of OPGs and OPLs are documented in the literature, chiefly 2 As a side remark, the above procedure that lead to the syntax tree of Figure 2.2 could be easily adapted to become an algorithm that produces a new syntax tree whose internal nodes are labeled by G AE 's nonterminals. Such an algorithm could be made deterministic by transforming G AE into an equivalend BD grammar (sharing the same OPM). This aspect, however, belongs to the realm of efficient parsing which is not a major concern in this paper.
in [19,18,33]. For convenience, we just recall and collect the ones that are relevant for this article in the next proposition. Remark. Thanks to the fact that a conflict-free OPM assigns to each string at most one parenthesization -and exactly one if the OPM is complete-the above closure properties of OPLs w.r.t. Boolean operations automatically extend to their parenthesized versions 3 . In particular, any complete, conflict-free,=-acyclic OPM defines a universal parenthesized language L pU such that its image under the homomorphism that erases parentheses is Σ * and the result of applying Boolean operations to the parenthesized versions of some OPLs is the same as the result of parenthesizing the result of applying the same operations to the unparenthesized languages.
In the following we will assume that an OPM is=-acyclic unless we explicitly point out the opposite. Such a hypothesis is stated for simplicity despite the fact that, rigorously speaking, it affects the expressive power of OPLs: it guarantees the closure w.r.t. Kleene star and therefore the possibility of generating Σ * ; this limitation however, is not necessary if we define OPLs by means of automata or MSO logic [32]; in the case of OPGs a=-cyclic OPM could require rhs of unbounded length; thus, the assumption could be avoided by adopting OPGs extended by the possibility of including regular expressions in production rhs [21], which however would require a much heavier notation. More comments about avoiding this hypothesis are given in the conclusion.

Logic characterization of operator precedence languages.
In [32] the traditional monadic second order logic (MSO) characterization of regular languages by Büchi, Elgot, and Trakhtenbrot [9,23,49] is extended to the case of OPL. Historically, a first attempt to extend the MSO logic for regular languages to deal with the typical tree structure of CF languages was proposed in [30] and then resumed by [4]. In essence, the approach consists in adding to the normal syntax of the original logic a new binary relation symbol, named matching relation, which joins the positions of two characters that somewhat extend the use of parentheses of [37]; e.g., in VPLs the alphabet is partitioned into three disjoint sets, two of them, named call and return, playing the role of open and closed parentheses so that their matching relation pairs a call with a return according to the traditional LIFO policy of pushdown automata.
Such a matching relation, however, is typically one-to-one -with an exception of minor relevance-but cannot be extended to languages whose structure is not made immediately visible by explicit parentheses. Thus, in [32] we introduced a new binary relation between # e + e * e + e # 0 1 2 3 4 5 6 7 8 string positions which, instead of joining the extreme positions of subtrees of the syntax trees, joins their contexts, i.e., the positions of the terminal characters immediately at the left and at the right of every subtree, i.e., respectively, of the character that yields precedence to the subtree's leftmost leaf, and of the one over which the subtree's rightmost leaf takes precedence. The new relation is denoted by the symbol and we write x y to state that it holds between position x and position y.
Unlike the similar but simpler matching relation adopted in [30] and [4], the relation is not one-to-one. For instance, Figure 2.3 displays the relation holding for the sentence e + e * e + e generated by grammar G AE : we have 0 2, 2 4, 4 6, 6 8, 2 6, 0 6, and 0 8. Such pairs correspond to contexts where a reduce operation is executed during the left-to-right, bottom-up parsing of the string (they are listed according to their execution order). By comparing Figure 2.3 with Figure 2.1 it is immediate to realize that every "embraces" a subtree of the syntax tree of the string e + e * e + e. Formally, we define a countable infinite set of first-order variables x, y, . . . and a countable infinite set of monadic second-order (set) variables X, Y, . . . . We adopt the convention to denote first and second-order variables in boldface font. DEFINITION 2.9 (Monadic Second-Order Logic for OPLs). Let (Σ, M ) be an OP-alphabet, V 1 a set of first-order variables, and V 2 a set of second-order (or set) variables. The MSO (Σ,M ) (monadic second-order logic over (Σ, M )) is defined by the following syntax (the OP-alphabet will be omitted unless necessary to prevent confusion): where c ∈ Σ # , x, y ∈ V 1 , and X ∈ V 2 . 4 A MSO formula is interpreted over a (Σ, M ) string w compatible with M , with respect to assignments ν 1 : V 1 → {0, 1, . . . , |w| + 1} and ν 2 : V 2 → ℘ ({0, 1, . . . , |w| + 1}), in this way: • #w#, M, ν 1 , ν 2 |= c(x) iff #w# = w 1 cw 2 and |w 1 | = ν 1 (x).
, and w 2 is the frontier of a subtree of the syntax tree of w.
for all Y ∈ V 2 − {X}. To improve readability, we will drop M , ν 1 , ν 2 and the delimiters # from the notation whenever there is no risk of ambiguity; furthermore we use some standard abbreviations in formulas, e.g., ∧, ∀, ⊕ (the exclusive or), x + 1, x − 1, x = y, x ≤ y.
Whenever we will deal with logic definition of languages we will implicitly exclude from such languages the empty string, according with the traditional convention adopted in the literature 5 (see, e.g., [38]); thus, when talking about MSO or FO definable languages we will exclude empty rules from their grammars.
Example 2.10. Consider the OP-alphabet with Σ = {a, b} and M any complete OPM containing, among other precedence relations that are not relevant in this example, a a, a . = b, b b. Thus, the universe L(M ) is the whole Σ * . We want to build an MSO formula that defines the sublanguage consisting of an odd number of as followed by the same number of bs. We build such a formula as the conjunction of several clauses.
The first clause imposes that after a b there are no more as: Thus, the original Σ * is restricted to the nonempty strings of the language {a * b * }. A second clause imposes that the first character be an a and is paired with the last character which is a b: This further restricts the language to {a n b n | n > 0} because the relations a a . = b b imply the reduction of ab, possibly with an N in between. Hence, if the first a and the last b of the string are the context of such a reduction, the number of as in the string must be equal to the number of bs.
Finally, to impose that the number of as -and therefore of bs too-is odd, we introduce two second-order variables O -which stands for odd-and E -which stands for even-and impose that i) all positions belong to either one of them, ii) the elements of O and E storing the as alternate -and therefore those storing the bs too-, iii) the position of the first and last a belongs to O. Such conditions are formalized below 6 .
Remark. The reader could verify that the same language can be defined by using a partial OPM, precisely an OPM consisting exclusively of the relations # a, a a, a . = b, b b, b #, and restricting the MSO formula to the above clause referring only to second-order variables. Using partial OPMs, however, does not increase the expressive power of our logic formalism -and of the equivalent formalisms OPGs and OPAs-: we will show, in Section 3, that any "hole" in the OPM can be replaced by suitable (FO) subformulas.
We also anticipate that, as a consequence of our major result, defining languages such as the one of this example, necessarily requires a second-order formula.
In [32] it is proved that the above MSO logic describes exactly the OPL family. As usual, we denote the restriction of the MSO logic to the first-order as FO.

The noncounting property for parenthesis and operator precedence languages.
In this section we resume the original definitions and properties of noncounting (NC) CF languages [15] based on parenthesis grammars [36] and show their relations with the OPL family.
In the following all Par-grammars will be assumed to be BDR, unless the opposite is explicitly stated. DEFINITION 2.11 (Noncounting parenthesis language and grammar [15]). A parenthesis language L is noncounting (NC) or aperiodic iff there exists an integer n > 1 such that, for all strings x, u, z, v, y in (Σ ∪ { , }) * where z and uzv are well-parenthesized, xu n zv n y ∈ L iff xu n+m zv n+m y ∈ L, ∀m ≥ 0. A derivation of a Par-grammar is counting iff it has the form A A Par-grammar is noncounting iff none of its derivations is counting. THEOREM 2.12 (NC language and grammar (Th. 1 of [15])). A parenthesis language is NC iff its BDR grammar has no counting derivation. THEOREM 2.13 (Decidability of the NC property (Th. 2 of [15])). It is decidable whether a parenthesis language is NC or not.

DEFINITION 2.14 (NC OP languages and grammars). For a given OPL L on an OP
A derivation of an OPG G is counting iff the corresponding derivation of the associated Par-grammar G p is counting.
Thus, an OPL is NC iff its BDR OPG (unique up to an isomorphim of nonterminal alphabets) has no counting derivations.
Its parenthesized version generates the language {( a) 2n+1 (b ) 2n+1 | n ≥ 0} which is counting; thus so is L(G C ) which is the same language as that of Example 2.10. On the contrary, the grammar G N C , with S = {A}, generates a NC language, despite the fact that the number of a in L(G N C )'s sentences is odd, because substrings aa are not paired with repeated substrings 7 . Notice however, that, if we parenthesize the grammar G N oOP , with S = {A}, which is equivalent to G C , we obtain a NC language according to Definition 2.11. This should be no surprise, since G C and G N oOP are not structurally equivalent and G N oOP is not an OPG, having a non-conflict-free OPM.
The following important corollary immediately derives from Definition 2.14 and Theorem 2.13. COROLLARY 2.16 (Decidability of the NC property for OPLs.). It is decidable whether an OPL is NC or not.
In the following, unless parentheses are explicitly needed, we will refer to unparenthesized strings rather than to parenthesis ones, thanks to the one-to-one correspondence.
It is also worth recalling [16] the following peculiar property of OPLs: such languages are NC or not independently on their OPM, in other words, although the NC property is defined for structured languages (parenthesis or tree languages [36,46]), in the case of OPLs this property does not depend on the structure given to the sentences by the OPM.
It is important to stress, however, that, despite the above peculiarity of OPLs, aperiodicity remains a property that makes sense only with reference to the structured version of languages. Consider, in fact, the following OPLs, with the same OPM consisting of {c c, c . = a, c . = b, a b, b a} besides the implicit relations w.r.t. #: They are both clearly NC and so is their concatenation L 1 ·L 2 according to Definition 2.14, which in its parenthesized version is , (see also Theorem 5.3); however, if we applied Definition 2.11 to L 1 ·L 2 without considering parentheses, we would obtain that, for every n, c 2n (ab) 2n ∈ L 1 · L 2 but not so for c 2n+1 (ab) 2n+1 .
We mention that the subfamily of OPLs which in [17] was proved NC and in [31] was proved FO logic definable, includes, as maximal elements, the maxlanguages of all OPMs.
3. Expressions for operator precedence languages. Next we introduce Operator Precedence Expressions (OPE) as another formalism to define OPLs, equivalent to OPGs and MSO logic. An OPE uses the same operations on strings and languages as Kleene's REs, and just one additional operation, called fence, that selects from a language the strings that correspond to a well-parenthesized string. In the past, regular expressions of different kinds have been proposed for string languages more general than the finite-state ones (e.g. the cap expressions for CF languages [52]) or for languages made of structures instead of strings, e.g., the tree languages or the picture languages. Our OPEs have little in common with any of them and, unlike regular expressions for tree languages [47], enjoy in the context of OPLs the same properties as regular expressions in the context of regular languages.
We recall that an OPM M defines a function from unparenthesized strings to their parenthesized counterparts; such a function is exploited in the following definition. For convenience, we define the homomorphism (projection) η : Σ # → Σ as: η(a) = a, for a ∈ Σ, and η(#) = ε. DEFINITION 3.1 (OPE). Given an OP-alphabet (Σ, M ) whose OPM is complete, an OPE E and its language L(E) ⊆ Σ * are defined as follows. The meta-alphabet of OPE uses the same symbols as regular expressions, together with the two symbols '[', and ']'. Let E 1 and E 2 be OPE: The incomplete OPM defining L Dyck (left), and a possible completion M complete (right).
Among the operations defining OPEs, concatenation has the maximum precedence; settheoretic operations have the usual precedences, the fence operation is dealt with as a normal parenthesis pair.
Similarly to the case of regular expressions, a star-free (SF) OPE is one that does not use the * and + operators.
The conditions on # are due to the peculiarities of OPLs closure w.r.t. concatenation (see also Theorem 5.3). In point 5. the # is not permitted within, say, the left factor E 1 because delimiters are necessarily positioned at the two ends of a string.
Besides the usual abbreviations for set operations (e.g., ∩ and −), we will also use the following derived operators: The fact that in Definition 3.1 matrix M is complete is without loss of generality: to obtain the same effect as M a,b = ∅ for two terminals a and b, (i.e. that there should be a "hole" in the OPM for them), we can use the short notations and intersect them with the OPE.
The following examples illustrate the meaning of the fence operation, the expressiveness of OPLs w.r.t. less powerful classes of CF languages, and how OPEs naturally extend regular expressions to the OPL family.
In fact the fence operation imposes that any string x ∈ a * b * embedded within the context a, b be well-parenthesized according to M .
The OPEs a[a * b * ]# and a + a[a * b * ]b ∪ {a + }, instead, both define the language {a n b m | n > m ≥ 0} since the matrix M allows for, e.g., the string aaabb parenthesized as a a ab b .
It is also easy to define Dyck languages with OPEs, as their parenthesis structure is naturally encoded by the OPM. Consider L Dyck the Dyck language with two pairs of parentheses denoted by a, a and b, b . This language can be described simply through an incomplete OPM, reported in open a must have a matching a .
The following OPE defines L Dyck by suitably restricting the "universe" L(G max,Mcomplete ): For a more application-oriented case, consider the classical LIFO policy managing procedure calls and returns but assume also that interrupts may occur: in such a case the stack of pending calls is emptied and computation is resumed from scratch.
This policy is already formalized by the incomplete OPM of Figure 3.2, with Σ = {call, ret, int} with the obvious meaning of symbols. For example, the string call call ret call call int represents a run where only the second call returns, while the other ones are interrupted. On the contrary, call call int ret is forbidden, because a return is not allowed when the stack is empty.
If we further want to say that there must be at least one procedure terminating regularly, we can use the OPE: Another example is the following, were we state that the run must contain at least one sub-run where no procedures are interrupted: Σ * · hole(call, int) · Σ * .
Notice that the language defined by the above OPE is not a VPL since VPLs allow for unmatched returns and calls only at the beginning or at the end of a string, respectively. Proof. By induction on E's structure. The operations ∪, ¬, ·, and * come from the closures of OPLs. The only new case is a[E]b which is given by the following grammar.
If, by induction, G defines the same language as E, then, for every axiom S E of G we add to G the following rules, where S is a new axiom replacing S E , and S, S are nonterminals not used in G: Let us call this new grammar G . The grammar for a[E]b is then the one obtained by applying the construction for intersection between G and the maxgrammar for M . This intersection is to check that a L(S E ) and R(S E ) b; if it is not the case, according to the semantics of a[E]b, the resulting language is empty.
Next we show that OPEs can express any language that is definable through an MSO formula as defined in Section 2.3. Thanks to the fact that the same MSO logic can express exactly OPLs [32] and to Theorem 3.4 we will obtain our first major result, i.e., the equivalence of MSO, OPG, OP automata (see e.g., [33]), and OPE.
In order to construct an OPE from a given MSO formula we follow the traditional path adopted for regular languages (as explained, e.g., in [40]) and augment it to deal with the new x x x i x x x j relation. For a MSO formula ϕ, let x x x 1 , x x x 2 , . . . , x x x r be the set of first order variables occurring in ϕ, and X X X 1 , X X X 2 , . . . , X X X s be the set of second order variables. We use the new alphabet B p,q = Σ × {0, 1} p × {0, 1} q , where p ≥ r and q ≥ s. The main idea is that the {0, 1} p part of the alphabet is used to encode the value of the first order variables (e.g. for p = r = 4, (1, 0, 1, 0) stands for both the positions x x x 1 and x x x 3 ), while the {0, 1} q part of the alphabet is used for the second order variables. Hence, we are interested in the language K p,q formed by all strings where the components encoding the first order variables contain exactly one occurrence of 1. We also use this definition Proof. By induction on ϕ's structure; the construction is standard for regular operations, the only difference is x x x i x x x j . Following Büchi's theorem, we use the alphabet B p,q to encode interpretations of free variables. The set K p,q of strings where each component encoding a first-order variable is such that there exists only one 1 is given by the following regular expression: Disjunction and negation are naturally translated into ∪ and ¬. Like in Büchi's theorem, the expression E for ∃x x x i ψ (resp. ∃X X X j ψ) is obtained from expression E ψ for ψ, on an alphabet B p,q , by erasing by projection the component i (resp. j) from the alphabet B p,q . The order relation Star-free OPEs are equivalent to FO logic. After having complemented the characterization of OPLs in terms of OPEs, we now enter the analysis of the critical subclass of aperiodic OPLs: in this section we show that the languages defined by star-free OPEs coincide with the FO-definable OPLs; in Section 5 that NC OPLs are closed w.r.t. Boolean operations and concatenation and therefore SF OPEs define NC OPLs; in Section 6 we provide a new characterization of OPLs in terms of MSO formulas by exploiting a control graph associated with a BDR OPG; finally, in Section 7 we show that such MSO formulas can be made FO when the OPL is NC. LEMMA 4.1 (Flat Normal Form). Any star-free OPE can be written in the following form, called flat normal form: Proof. The lemma is a consequence of the distributive and De Morgan properties, together with the following identities, where • 1 , • 2 ∈ {∆, ∇}, and L k are star-free regular expressions, The first two identities are immediate, while the last two are based on the idea that the only non-regular constraints of the left-hand negations are respectively a 1 ∇a 2 or a 1 ∆a 2 , that represent strings that are not in the set only because of their structure.
Proof. Consider the ϕ formula, and its set of first order variables: like in Section 3, B p = Σ × {0, 1} p (the q components are absent, being ϕ a first order formula), and the set K p of strings where each component encoding a variable is such that there exists only one 1.
First, K p is star-free: Disjunction and negation are naturally translated into ∪ and ¬; For the existential quantification, the problem is that star-free (OP and regular) languages are not closed under projections. Like in the regular case, the idea is to leverage the encoding of the evaluation of first-order variables, because there is only one position in which the component is 1 (see K p ). Hence, we can use the two bijective renamings , where the last component is the one encoding the quantified variable. Notice that the bijective renaming does not change the Σ component of the symbol, thus maintaining all the OP precedence relations.
Let E ϕ be the star-free OPE on the alphabet B p for the formula ϕ, with x x x a free variable in it. Let us assume w.l.o.g. that the evaluation of x x x is encoded by the last component of The OPE for ∃x x xϕ is obtained from the OPE for ϕ through the bijective renaming π, and considering all the cases in which the symbol from A can occur.
First, let E be a OPE in flat normal form, equivalent to E ϕ (Lemma 4.1). The FO semantics is such that In the intersection between E and B * AB * , all the possible cases in which the symbol in A can occur in E 's terms must be considered: e.g. in L i,j a i,j ∆b i,j R i,j it could occur in the L i,j prefix, or in a i,j ∆b i,j , or in R i,j . More precisely, The cases in which the symbol from A occurs in L i,j or R i,j are easy, because they are by construction regular star-free languages, hence we can use one of the standard regular approaches found in the literature (e.g. by using the splitting lemma in [22]). The only differences are in the factors a i,j ∆b i,j , or a i,j ∇b i,j .
Let us consider the case a i,j ∆b i,j ∩ B * AB * . The cases a i,j ∈ A or b i,j ∈ A are like (L i,j ∩ B * AB * ) and (R i,j ∩ B * AB * ), respectively, because L i,j a i,j and b i,j R i,j are also regular star-free (∇ is analogous).
The remaining cases are a i,j ∆b i,j ∩ B + AB + and a i, Proof. The proof is by induction on E's structure. Of course, singletons are easily first-order definable; for negation and union we use ¬ and ∨ as natural.
Like in the case of star-free regular languages, concatenation is less immediate, and it is based on formula relativization. Consider two FO formulae ϕ and ψ, and assume w.l.o.g. that their variables are disjunct, and let x x x be a variable not used in neither of them. To construct a relativized variant of ϕ, called ϕ <x x x , proceed from the outermost quantifier, going inward, and replace every subformula ∃y y yλ with ∃y y y((y y y < x x x) ∧ λ). Variants ϕ ≥x x x and ϕ >x x x are analogous. We also call ϕ(x x x, y y y) the relativization where quantifications ∃z z zλ are replaced by ∃z z z((x x x < z z z < y y y) ∧ λ). The language L(ϕ) · L(ψ) is defined by the following formulas: The last part we need to consider is the fence operation, i.e. a[E]b. Let ϕ be a FO formula such that L(ϕ) = L M (E), for a star-free OPE E. Let x x x and y y y be two variables unused in ϕ. Then the language L(a[E]b) is the one defined by ∃x x x∃y y y(a(x x x) ∧ b(y y y) ∧ x x x y y y ∧ ϕ(x x x, y y y)).

5.
Closure properties of noncounting OPLs and star-free OPEs. Thanks to the fact that an OPM implicitly defines the structure of an OPL, i.e., its parenthesization, aperiodic OPLs inherit from the general class the same closure properties w.r.t. the basic algebraic operations. Such closure properties are proved in this subsection under the same assumption as in the general case (see Proposition 2.8), i.e., that the involved languages share the same complete OPM or have compatible OPMs. Proof. We give the proof for counting languages which also implies the closure of noncounting ones.
By definition of counting parenthesis language and from Theorem 1 of [15], if L p is counting there exist strings x, u, v, z, y and integers n, m with n > 1, m > 1 such that xu n+r zv n+r y ∈ L for all r = km > 0 but not for all r > 0. Thus, the complement of L p contains infinitely many strings xu n+i zv n+i y ∈ L p but not all of them since for some i, i = km. Thus, for ¬L p too there is no n such that xu n zv n y ∈ L iff xu n+r zv n+r y ∈ L for all r ≥ 0.
The same holds for the unparenthesized version of L p if it is an OPL.
THEOREM 5.2. Non-counting parenthesis languages and non-counting OPLs are closed w.r.t. union and therefore w.r.t. intersection.
Proof. Let L p1 , L p2 be two NC parenthesis languages/OPLs. Assume by contradiction that L p = L p1 ∪ L p2 be counting. Thus, there exist strings x, u, v, z, y such that for infinitely many n, xu n zv n y ∈ L p but for no n xu n zv n y ∈ L p iff xu n+r zuv n+r y ∈ L p for all r ≥ 0. Hence, the same property must hold for at least one of L p1 and L p2 which therefore would be counting.
Notice that, unlike the case of complement, counting languages are not closed w.r.t. union and intersection, whether they are regular or parenthesis or OP languages. Proof. Recall from [18] that OPLs with compatible OPM are closed w.r.t. concatenation. Thus, let L 1 , L 2 be NC OPLs, and G 1 = (Σ, V N 1 , P 1 , S 1 ), G 2 = (Σ, V N 2 , P 2 , S 2 ) their respective BDR OPGs. Let also L p1 , L p2 , be their respective parenthesized languages and G p1 , G p2 , their respective parenthesized grammars. We also recall that in general the parenthesized version L p of L = L 1 · L 2 is not the parenthesized concatenation of the parenthesized versions of L 1 and L 2 , i.e., L p may differ from L p1 · L p2 , where L p1 = L p1 and L p2 = L p2 , because the OP concatenation may cause the syntax trees of L 1 and L 2 to coalesce.
The construction given in [18] builds a grammar G whose nonterminal alphabet includes Notice that some substrings of x · w 1 , resp. w 2 · y, may be derived from nonterminals belonging to V N 1 , resp. V N 2 , as the consequence of rules of type [A 1 , could be missing; also, any string γ derivable in G contains at most one nonterminal of type [A 1 , A 2 ] (see Figure 5.1). Suppose, by contradiction, that G has a counting derivation 9 [X 1 , would be counting in G 1 and G 2 since they would involve the same nonterminals in the pairs If instead the counting derivation of G were derived from nonterminals belonging to V N 1 , (resp. V N 2 ) that derivation would exist identical for G 1 (resp. G 2 ).
Thanks to the above closure properties we deduce the following important property of OPEs. 6. From grammar to logic through control graph. In this cornerstone section we show how any OPL can be expressed as a combination of a "skeleton language" -the max-language associated with the OPM-with a "regular control". Such a regular control, defined through a graph derived from the OPG, can be translated in the traditional way into MSO formulas, which become FO if the language defined by the graph is noncounting [38]. These formulas, suitably complemented by the relation, express the language generated by the source OPG. The following definition of control graph associates a regular language with every nonterminal symbol of the grammar. DEFINITION 6.1 (control graph). Let G = (Σ, V N , P, S) be an OPG. The control graph of G, denoted by C(G) = (Q, Σ, δ δ δ), is the graph having vertices or states Q and relation δ δ δ (see Section 2.1) defined as follows: • Let W be the set: The macro-edges of δ δ δ are associated with the productions according to the following table, where w ∈ W : Note that the G produced by the construction is BD if so are G 1 and G 2 , but it could be not necessarily BDR; however, if a BDR OPG has a counting derivation, any equivalent BD grammar too has a counting derivation. The adoption of macro-steps to define a control graph allows us to state an immediate correspondence between the terminal parts of grammar rules and graph macro-edges, without introducing useless intermediate steps.
Intuitively, a state of type A denotes that a path of the control graph visiting the syntax tree of a string generated by G is touching the nonterminal A while following a top-down direction; conversely, it visits A while following a bottom-up direction. We thus call those states, descending and ascending states respectively.
We will see (Theorem 6.4) that the frontier of a syntax tree rooted in nonterminal A is a path of the control graph, going from A to A (of course, being such paths regular languages, they also include strings that are not in L G (A)). A → aBcA | aBcB | ac, B → bAcA | bAcB | bc Its control graph C(G N L ) is given in Figure 6.1.
6.1. Deriving MSO formulas from the control graph. We already know that the MSO logic defined in Section 2.3 as an extension of the traditional logic for regular languages defines exactly the family of OPLs. In this section we show a way to obtain an MSO formula equivalent to an OPG directly from its control graph: the final goal is to obtain from such a construction an FO formula instead of an MSO one in the case that the OPL is aperiodic.
Intuitively the relation, which is the only new element w.r.t. the traditional MSO logic for regular languages, "embraces" the string x generated by some grammar nonterminal A, thus it must be A generated by that rule: The following key formula ψ A states that for every pair of positions x y, if z is the string included in between and A z −→ −→ −→ A , then there must exist a rule of G with A as lhs, and a rhs such that for all of its nonterminals B j , if any, formula ϕ Bj holds.
where the disjunction is considered over the rules of G and B j are either ε or are the nonterminals occurring in the rhs of the production. Finally formula χ states that the strings included between #s must be derived by some axiom: Example 6.3. Consider again the OPG G N L of Example 6.2. Let ϕ A and ϕ B be the MSO formulas defining the regular languages R A and R B , and ϕ A (x, y) and ϕ B (x, y) their respective relativized versions. Then the ψ A formula for nonterminal A of G N L is: We purposely avoided some obvious simplifications to emphasize the general structure of the ψ formula. Vice versa, it is #x# ϕ A (0, |x| + 1) ∧ ψ A , with x = # c 1 . = c 2 . = . . . c n #. Therefore: (i) x ∈ R A , (ii) #x# 0 |x| + 1, and (iii) #x# c i (i) for every i = 1 . . . n. (ii) and (iii) imply that there exists a production B → x, but being G BDR, B must be A.
Hence, x ∈ L(A). Induction: m > 1. Let us consider any A → B 0 c 1 B 1 . . . c n B n ∈ P , c i ∈ Σ, where some B i could be absent -we assume for simplicity that they are all present; the case where some of them is missing can be promptly adapted.
; also, #x# ϕ B0 (0, x 1 ) and #x# ϕ Bn (x n , |x| + 1). Hence, #x# TreeC(0, x 1 . . . x n , |x| + 1). Therefore, let ψ A be ∀x, y ψ A (x, y). By induction hypothesis, ψ A holds in all the substrings w i . The only new case for the values of x, y that make the left hand side of the implication of ψ A true is x = 0 and y = |x| + 1: in this case we proved that #x# ψ A (0, |x| + 1). Hence, The hypothesis #x# ϕ A (0, |x| + 1) ∧ ψ A guarantees that for at least one rule of G, A → B 0 c 1 B 1 c 2 . . . c n B n among x's positions there exist x 1 . . . x n such that #x# TreeC(0, x 1 . . . x n , |x| + 1) and c(x i ) = c i | i = 1 . . . n. Thus x = w 0 c 1 . . . c n w n and, by the induction hypothesis, for each i = 0 . . . n, there exist unique B i such that From Theorem 6.4 we immediately derive the following main COROLLARY 6.5. For any BDR (Σ, M )-compatible OPG G, L(G) is the set of strings satisfying the corresponding formula χ.
In a sense, the above formula ψ A "separates" the formalization of the language structure defined by the OPM from that of the strings generated by the single nonterminals: the former part -i.e., the relation and the T reeC subformula-are first-order; it is well-known from the classic literature on regular languages that the latter part, based on subformulas ϕ A , can be made FO if the regular control languages R A are NC. Thus, we obtain a first important result: COROLLARY 6.6. If the control graph of an OPG G defines languages R A , A denoting any nonterminal character of G, that are all NC, then, L(G) can be defined through an FO formula.
The above separation, however, also hints at a much more attractive result: if a NC OPL is associated with NC control languages, then it can be defined through an FO formula. Unfortunately, we will soon see that there are NC OPLs such that the control graph of their (unique up to a nonterminal isomophism) BDR OPG defines counting regular languages R A . Thus, the following -rather technical-section is devoted to transform the original BDR grammar of a NC OPL and its control graph into equivalent ones where the controlling regular languages involved in the above formulas are NC and therefore FO definable.
7. NC regular languages to control NC OPLs. The previous section showed that, if an OPL is controlled by a control graph whose path labels from descending to corresponding ascending states are NC regular languages, then the OPL can be defined through an FO formula; by adding the intuition that, if languages R A , where A denotes any nonterminal of the original grammar, are NC, then the original OPL is NC as well, we would obtain a sufficient condition for FO-expressibility of NC OPLs. This is not our goal, however: we want to show that any NC OPL can be expressed by means of an FO formula. Unfortunately, it is immediate to realize that there are NC OPLs whose languages R A of the control graph of their BDR grammar are counting, as shown by the following simple example: Example 7.1. Consider the grammar below: A → aBc | d; B → aAb the regular control language R A is (aa) * d(bc) * . However, Theorem 6.4 still holds if we replace R A by the NC language a * d(bc) * : intuitively, it is the OPM, and therefore the relation, which imposes that each b and each c are paired with a single a, so that for each sequence belonging to (bc) * we implicitly count an even number of a.
Generalizing this natural intuition into a rigorous replacement of the original control graph of any OPG with a different NC one which preserves Theorem 6.4 is the target of this section. To achieve it, we need a rather articulated path which is outlined below: 1. First, in the same way as in [15] we build a linear grammar G L associated with the original OPG G (which is always assumed to be BDR) such that L(G L ) is NC iff so is L(G). 2. Then, we derive from the control graph of G L another control graph C(G L ) whose regular languages are NC. This will require a rather sophisticated transformation of the original C(G L ). 3. The original grammar G is transformed into an equivalent one G (no more BDR) whose nonterminals are pairs of states of the transformed control graph C(G L ) where one or more of them are homomorphically mapped into single nonterminals A of G, and such that its control graph C(G ) exhibits only NC control languages. 4. Finally, the original Theorem 6.4 is extended to the case of the transformed grammar G and its new control graph. At this point, the MSO formalization of any OPL provided in Section 6.1 automatically becomes an FO one thanks to the fact that each subformula ϕ A defines a NC regular language.
7.1. Linearized OPG and its control graph.

DEFINITION 7.2 (Bilateral linear grammar).
A linear production of the form A → uBv such that B ∈ V N , and u, v ∈ Σ + is called bilateral. A linear grammar is bilateral if it contains only bilateral productions and terminal productions.
Thus, a bilateral grammar may not contain productions that are null, renaming, left-linear or right-linear.
The following definition slightly modifies a similar one given in [15].
Example 7.4. Consider the grammar G N L of Example 6.2. Its associated linearized grammar G L N L , with Σ L = {a, b, c, A, B, ε R }, 10 and the same axioms as G N L , has the following productions: Thus, the set W of G L N L 's control graph is {a, b, c, bAc, aBc, cA, cB, ac, bc, ε R } A linearized grammar is evidently bilateral and BDR (after some obvious clean-up). It has a different terminal alphabet -and therefore OPM-than the original grammar from which it is derived but it is still an OPG since its new OPM is clearly conflict-free (the two separate "dummy ε" have been introduced just to avoid the risk of conflicts). It is not guaranteed, however, that an OPG with=-acyclic OPM has an associated linearized grammar enjoying the same property. Such a hypothesis, however, is not necessary to guarantee the following results (indeed, it is only necessary to guarantee the existence of a maxgrammar generating the universal language Σ * ; see also further comments in the conclusions.) The following lemma is a trivial adaptation of the analogous Lemma 1 of [15] to Definition 7.3. LEMMA 7.5. Let G be a BDR OPG and G L its associated linearized grammar. L(G L ) is NC iff so is L(G).
This simple but fundamental lemma formalizes the fact that the aperiodicity property can be checked by looking only at the paths traversing the syntax trees from the root to the leaves neglecting their ramifications.
The next definition and property are taken from [11] with a minor adaptation 11 . DEFINITION 7.6 (Counter). For a given FA (without ε-moves) a counter is a pair (X, u), where X is a sequence of different states q 1 q 2 . . . q k , with k > 1 and u is a nonempty string such that for 1 ≤ i ≤ k, q i u −→ −→ −→ δ q (i+1) mod k ; k is said the order of the counter. For a counter C = (X, u), the sequence X is said the counter sequence of C and u the string of C. PROPOSITION 7.7. If an FA A is counter-free, i.e., has no counters, then L(A) is noncounting.
Notice that the converse of this statement only holds in the case of minimized deterministic FA [38].
Thus, for a linearized grammar G L , every path of its control graph belonging to some R A is articulated into a sequence of macro-steps whose states belong to V N followed by a sequence which traverses the corresponding nodes of V N in the reverse order -in between there is a single macro-step from some B to B -. Accordingly, a counter sequence may only contain nodes that either all belong to V N , or all belong to V N ; thus, their corresponding counters will be said descending or ascending.
Let C = (X, u) be a counter with Let also u = z 1 z 2 . . . z j , j ≥ 1 be the factorization into strings z i of the set W corresponding to the macro-steps of the path A i u −→ −→ −→ A (i+1) mod k : notice that such a factorization is the same for all i since the OPM imposes the same parenthesization of u in any path.
The following lemma allows us to reason about the NC property of linear OPLs without considering explicitly the parenthesis versions of their grammars. LEMMA 7.8. Let G L be a bilateral linear OPG, C(G L ) its control graph, G L p the parenthesized version of G L , and C(G L p ) its control graph. Then, for any nonterminal A of G L the control language R pA is NC iff so is R A .
Proof. If R pA is counting, then obviously so is R A . Vice versa, suppose by contradiction that for all k R A contains a string xy k z but not xy k+m z for all m ≥ 0. Notice that for k sufficiently large the parenthesized version y k p of y k must contain either only open or only closed parentheses.
Let us assume w.l.o.g. that y k p begins with an open (resp. ends with a closed) parenthesis; otherwise consider a suitable permutation thereof. If all occurrences of y p itself begin with an open parenthesis (resp. end with a closed one), then R pA is counting too; otherwise for some r with 1 < r ≤ k there must exist an u p = y r p without a parenthesis between two consecutive occurrences of y p ; but this would imply a conflict in the OPM. DEFINITION 7.9 (Counter table). We use an array with the following scheme, called a counter table T , to orderly and completely represent the macro-transitions which may occur within a counter C = (X = T 1 T 2 . . . T k , u = z 1 z 2 . . . z j ): where the 0-th column is conventionally bound to the above counter C.
With reference to the above Table (7.1) the sequence of macro-steps looping from T 0 1 to T 0 1 is called the path of the counter table. Thus, a counter table defines a "matrix of counters" consisting of its columns: in the case of Table (7.1) the first column T 0 1 , T 0 2 , . . . , T 0 k together with the string u will be used as the reference counter of the table. Each cyclic permutation of each column is another counter with the same string, whereas each column is the counter sequence of another counter whose string is a cyclic permutation of u, e.g.
For any counter of a counter table, its associated path is the sequence of macro-steps looping from its first state to itself. The above remarks lead to the following formal definition: If we apply cyclic permutations to the whole path producing a counter C = (X = T 1 T 2 . . . T k , u = z 1 z 2 . . . z j ), and therefore a complete counter table, we obtain a family of counter tables associated with the original Table 7.1. We decide, therefore, to choose arbitrarily an "entry point" of any path producing a counter. Such an entry point uniquely determines a counter table T and therefore a unique reference counter. Furthermore, for convenience, if the same path T l u −→ −→ −→ T (l+1) mod k , for 1 ≤ l ≤ k can also be read as T l u −→ −→ −→ T (l+1) mod k , with u = u r , k = k · r we represent the unique associated T by choosing the minimum of such u (and the maximum of the k). All elements of the table -states, transitions, counter sequences-will be referred through this unique T , ignoring the other tables of its "family". Whenever needed we will identify a counter table, its counter sequences, and any element thereof, through a unique index, as Notice that a counter table uniquely defines a collection of counters (among them the first column being chosen as its reference counter), but the same counter may be a counter, whether a reference counter or not, of different tables. This case arises, for instance, when the linearized grammar contains two productions such as A 1 → z 1 B 1 1 v and A 1 → z 1 C 1 1 w. Then the same counter C = (X = A 1 A 2 . . . A k , u = z 1 z 2 . . . z j ) may occur in two different counter tables that necessarily differ in at least one of the intermediate states B i h . Notice also that the various counters of a counter table are not necessarily disjoint. Consider, for instance, the following sequence of transitions −→ −→ −→ A 1 , called, respectively, descending and ascending, are paired (by such a derivation).
Two counter tables are paired iff their paths, or cyclic permutations thereof, are paired; two counters are paired iff their associated paths T 1 are paired -therefore so are the counter tables they belong to.

7.2.
Transforming G L control graph. If the control graph of a linearized grammar G L is counter free, then L(G L ) is NC. Notice, in fact, that 1. C(G L ) has no ε-moves, thus the Definition 7.6 of counter-free is well-posed for it; 2. If, by contradiction, G L , which is BDR, admitted a counting derivation, such a derivation would imply two paired counters of C(G L ). Unfortunately such a condition is only sufficient but not necessary to guarantee that L(G L ) is NC, as shown by Example 7.1. Thus, according to the path outlined at the beginning of Section 7, our next goal is to transform C(G L ) into a control graph, denoted as C(G L ), whose regular languages are NC and which will drive the construction of a grammar G , equivalent to the original G, such that its control graph defines NC R A for its nonterminals. The construction of C(G L ) will exploit the following lemmas, which make use of the notion of paired counters: LEMMA 7.12. If G L is NC, then C(G L ) either has no paired counters or, for any two paired counters, the orders of the descending and ascending counter are coprime numbers.
Proof. Assume, by contradiction, that the counters C 1 = (X , u), C 2 = (Y , v) are paired by the derivation A 1 * =⇒ u k A 1 v h and that for some j, r, s > 1, k = j · r, h = j · s.
A j and A (r−1)j , A 2j and A (r−2)j . . . refer to the same nonterminal in the derivation A 1 * =⇒ u k A 1 v h , are two paired counters as well which correspond to a counting derivation of G L .
Example 7.13. The productions A → aBb and B → aAb generate the two paired counters of order 2 of the control graph: (A B , a) paired with (B A , b). Instead, the productions A 1 → aA 2 f , A 2 → bA 3 g, A 3 → aA 4 h, A 4 → bA 5 f , A 5 → aA 6 g, A 6 → bA 1 h generate the following sequence of descending counters of order 3 paired with ascending counters of order 2: By looking at the second case of Example 7.13 we notice that for each couple of paired counter sequences there is just one nonterminal that belongs to both of them. This remark is easily generalized to the following lemma: LEMMA 7.14. Let L(G L ) be NC. If in C(G L ) there are two paired counters C 1 = (X , u), Proof. Let |X | = k, and |Y | = h, with h and k coprime, thanks to Lemma 7.12. The two paired counters correspond to a NC derivation of The total length of the derivation is h · k and each A t belongs to a set, marked , of cardinality k in the table T [i] of C 1 and to a set, marked , of cardinality h in the table T [f ] of C 2 . Thus, for any couple (X , Y ) paired by the two counter tables, there exists exactly one A, such that A ∈ X , A ∈ Y by virtue of the Chinese remainder theorem.
On the basis of the above lemmas the construction of C(G L ) aims at replacing any ascending and descending counter with a loop X u −→ −→ −→ δ δ δ X where X is a suitable new state in C(G L ) representing a whole counter sequence of C(G L ); thanks to Lemma 7.12, the new loop will be paired with a path that is not a counter or with another loop which in turn replaces a counter whose order is coprime w.r.t. the order of the former one. By virtue of Lemma 7.14, in turn, this will allow to disambiguate which element of the counter sequence corresponds to the G L 's nonterminal deriving the various instances of string u.
This basic idea, however, cannot be implemented in a trivial way such as replacing all states belonging to a counter sequence by a single state representing the whole sequence. Consider, for instance, a grammar containing the following productions: ; if we further collapse AB C into ABC we reduce the descending part of the control graph to a single state with two self-loops labeled a, b: at this point, once a path reaches the state A and reads the symbol d it is impossible to decide whether such an "ascending d" should be paired with a previous descending b or a since both are labeling a self-loop on the unique state ABC .
The construction we devised for such a C(G L ) is therefore more complex: it is articulated into two steps: first aĈ(G L ) "equivalent" to C(G L ), in a sense that will be made precise in Lemma 7.16, is built.Ĉ(G L ) splits some states belonging to counters in such a way that each new instance thereof belongs to exactly one counter table; then the further construction C(G L ) collapses all counter sequences into single states that allow repeating the "basic counter string u" any number of times, instead of k times. Thus, each path of the original control graph that realizes a counter (X , u) of order k will be replaced by k paths X u −→ −→ −→ X (apart from a transient that will be explained later). Thanks to Lemma 7.12, if G L is NC, it will not be paired with another counter (Y , v), or, if so happens, the order of the other counter will be an h coprime of k; thus, thanks to Lemma 7.14, it will be possible to associate each couple of paired counters of the control graph of G L with a unique derivation of the grammar.
Construction ofĈ(G L ).. Intuitively, the aim ofĈ(G L ) is to produce "non-intersecting counter tables", i.e., counter tables such that T The construction below applies as well to states of type A and to states of type A , according to Definition 6.1. Notice that macro-transitions of the type A z −→ −→ −→ A , which correspond to G L 's productions A → z, z ∈ W , cannot belong to any counter table of C(G L ), but A and/or A can belong to some descending or ascending counter.
The construction ofĈ(G L ) = (Q, Σ,δ δ δ) starts from C(G L ) = (Q, Σ, δ δ δ), i.e., it is a process whereQ andδ δ δ are initialized as Q and δ δ δ, and modifies them in the following way. When the transformations below apply identically to descending and ascending paths we omit labeling the states of the control graph as or : First, we label all counter tables T with unique and different indexes i. will see, however, that, despite the increased number of paths, none of them will generate a counting path after the further transformation fromĈ(G L ) to C(G L ).   Construction of C(G L ).. As anticipated, the core of C(G L )'s construction moves from C(G L ) and, roughly speaking, consists in collapsing all states labeled by the index of the same counter table and belonging to a counter sequence of a given counter into a single new state named as the counter sequence itself and labeled by the index of the table it belongs to.
The behavior of C(G L ) is such that it is exactly likeĈ(G L ) (and as C(G L )) until it reaches a state of some -unique-counter  Then, C(G L ) loops along the horizontal cyclic permutations of the counter -a new counter sequence state is built for every column of the counter table-, therefore without counting the repetitions of the counter string u; in other words it "forgets the vertical cyclic permutations" of the counter table. When C(G L ) exits from the loop it nondeterministically reaches any node that can be reached by any state belonging to the counter sequence state it is leaving. Notice that exit from the loop occurs only as a consequence of a transition that in C(G L ) was not part of the counter table; such a transition may lead either to a state that does not belong to the table, such as L h −→ −→ −→ R in Figure 7.2, or to a state that is still part of the table, such as A c −→ −→ −→ L in the same figure. In the latter case the same table can be re-entered, i.e., the original counting path may be resumed, but this must happen only by going into an entry point of the table, not directly into the counter sequence state containing it (the reason of this choice will be clear later); for instance in the case of Figure 7.2, the transition that reads c (from the counter sequence state containing A) leads to instances of L, not to the counter sequence state(s) containing it. Notice also that the transition A c −→ −→ −→ L may also occur in C(G L ) during the "transient" before entering the counter sequence state: this means that the counting path is interrupted before being completed for the first time and possibly resumed from scratch (with a different entry point).
Obviously, C(G L ) will exhibit all behaviors of C(G L ) plus more; we will see however, that pairing such, say, descending behaviors with the ascending ones will allow us to discard those that are not compatible with G L 's derivations.
We now describe in detail the construction of C(G L ).
To simplify the notation we will avoid the index identifying the single tables whenever not necessary.
Points 1 through 6 of the construction below are identical whether they are applied to states belonging to descending or ascending paths; thus we will not mark those states with or . Notation. To distinguish the k · j replicas of the sequences that, for each pipeline lead to the counter sequence states, we add a second index to the one denoting the counter table, ranging from 0 to k · j − 1; the 0-th copy, e.g., H[2, 0], will denote the entry point of each pipeline. Let us now build C(G L )'s (macro)transitions δ δ δ. 2. All transitions that do not involve states belonging to counter tables are replicated identically fromδ δ δ and therefore from δ δ δ.
of the pipeline (r = 0) or any other element thereof. • If instead A does not belong to any counter but there is some r = 0 is set, however: this is due to our convention that counters can only be entered through the single states that are entry points of a pipeline, whereas, once they entered the counter sequence state they must be exited only therefrom.
A belongs both to a descending counter X and to an ascending one X of C(G L ), then  To illustrate the main features of the above construction, as a first example, consider again the fragment of Example 7.15: the corresponding fragment of C(G L ) is depicted in Figure 7.4; see also the further Example 7.18.
The following example, instead, explains why we introduced the pipelines as an input for counter sequence states.
Example 7.17. The control graph of Figure 7.1 has shown that simply collapsing the states of a counter sequence into a single state produces undesired side effects, such as spurious counters. A first repair could consist in keeping the original states (ofĈ(G L )) and using them as an entry for the compound states, in some sense, a pipeline of length 1.
This solution too, however, is not enough. Consider, for instance, the fragment of control graph in Figure 7.5, no matter whether representing a descending or an ascending fraction of the whole graph; it contains just one counter table with counters (AC, ab) and (BD, ba); thus, the corresponding fraction ofĈ(G L )) is isomorphic to the original graph. A possible version of C(G L )) making use of single states to enter the counter sequence states is given in Figure 7.6 which shows a new counter table with counters (AP, ac) and ((BD)Q, ca) which do not correspond to the behavior of the original control graph.
The source of the problem abides in the fact that the path cac reentering state A after leaving BD "forgot" that its source was D, not B; thus, it can go on in a way that does not separate the two cases. The construction of C(G L )) making use of the full pipelines, on the contrary, "compels" to reenter the counter from scratch, i.e., from the "real" A, from which it would not be possible to bypass the path aba to reach again the state BD. This is why counters may be entered only through their entry points.
Finally the example below points out that in some cases the same transition can be used to follow the path of a counter table, but also to exit it, depending on the context within which it occurs.
Proof. The original "pure counters" ofĈ(G L ) have been "broken" by replacing the arrows that would complete the string u k with transitions that enter a loop accepting u * . Thus, any pipeline associated with a counter whose string is u accepts sequences u m , with m ≥ k. All paths of C(G L ) that do not touch counter sequence states existed in C(G L ) too up to the homomorphism that erases the indexes of the duplicated states.
The only transitions that are not replicas of transitions existing inĈ(G L ) (and in C(G L )) are those exiting the counter sequence states since they are derived from transitions originating by some of the states belonging to the counter sequence, say X. If such transitions originate paths that do not lead to any pipeline, i.e., that do not correspond to C(G L )'s paths leading to some counter table, then such paths cannot contain any counter since they simply replicate C(G L )'s paths with no counters. Suppose, instead, that such a path, after reading a string z, reaches the entry point of a pipeline which, through a string v j leads to a new counter: thus, the reading of z is only a finite prefix of a path that leads from a counter sequence to another one (if instead the path of the pipeline reading v j is abandoned before reaching the counter sequence state, it continues by replicating a path that existed already in C(G L ) without counters, up to a renaming of some states). Notice that, as a particular case the new counter string v could be u again but referring to a different counter table, therefore with disjoint states.
As a further special case, however, it could even happen that z is u s (it cannot be u = z s because by convention, u is the minimal string that can be associated with the counter table -see Definition 7.9) and, by reading z, C(G L ) re-enters a pipeline of the same table so that after going through the whole pipeline we reach again state X. In this case we would have closed a loop from X to X by reading the string u s+k , thus, C(G L ) would not be counter free. Nevertheless, it is aperiodic since, together with u s+k we would also find all strings u s+k+n for any n ≥ 0 because from X we can read any string in u * .
At this point it would be possible to prove again Theorem 6.4 and its Corollary 6.5 for any G L by suitably replacing formulas ϕ A with formulas referring to C(G L ) instead of C(G L ). We would thus obtain FO definability of linear NC OPLs. This result however, has already been obtained with much less effort in [34]. Here we want to achieve the general result for any NC OPL.
7.3. NC control graph for general NC OPGs. Let now G be a BDR OPG, G L its associated linearized OPG, C(G L ) the original control graph of G L andĈ(G L ), C(G L ) its respective transformations obtained through their constructions (remember that C(G L ) has been built starting fromĈ(G L )). A new OPG G = (Σ, V N , P , S ) structurally equivalent to G is built according to the following procedure.
Construction of G .. Notice that, if the counter tables are not paired, Lemmas 7.12 and 7.14 do not apply; thus, it might happen that X A and X A share more that one nonterminal of G. • For convenience, in the following construction we use the notation [X A ] (resp., [X A ] ) to denote either the singleton state A (resp. A ) or any counter sequence state X A containing A, or any element of the corresponding pipelines. • For every production A → B 0 x 1 B 1 . . . x n B n of G (with x i ∈ W ), where, as usual, B 0 and B n may be missing, consider the following cases: 1. A does not belong to any counter, either descending or ascending. Then the following productions are in P : Then the following productions are in P :    (2) and (3), keeping in mind Lemma 7.14.
Notice that, if the derivation involving the two paired counter tables is long enough -precisely, more than 2 · k i · j i = 2 · k f · j f , where k i , j i , resp. k f , j f , are the order and the number of W 's elements of the descending, resp. ascending table-then a number of consecutive nonterminals of G associated with G's nonterminal A will be of type (X A , X A ); the same will happen for the horizontal permutations of the counter which A belongs to. 5. A belongs to a descending counter table T [i] and to an ascending one T [f ] that are not paired. In this case only one of the two tables can be followed by the derivation. In other words, a derivation A * = =⇒ u k Av is interrupted to move to another "semicounting derivation" A * = =⇒ zAw h . In this case both possibilities are applied: all elements [X A ] of the ascending pipeline, including the counter sequence state, are paired with singleton elements of the descending pipeline excluding the counter sequence state, and conversely, in all compatible ways. The elements of the rhs are built in the same way as in points 2. and 3. above, respectively. For instance, if A belongs to a descending counter (AB [1], a) and to an ascending one (AC [2], b) a production A → aBb becomes the following ) stands for any element of the descending (resp. ascending) pipeline, includingAB [1] (resp. AC [2]) and [X A ] (resp. [X A ] ) stands for any element of the descending (resp. ascending) pipeline, excluding AB [1] (resp. AC [2]) 12 See also Example 7.21.
• The axioms of G are: the pairs (A , A ) where A is an axiom of G that does not occur in any counter Intuitively, G splits all of G's nonterminals into pairs representing elements of C(G L )'s descending and ascending paths involving the same nonterminal of G. If one of C(G L )'s states belongs to a counter sequence this is recorded in the name of the new nonterminal symbol which can be an element of the corresponding pipeline of C(G L ). If a derivation is following a descending or an ascending path of the syntax tree that is part of a counter table, say the i-th, then that part of the path must obey the constraints given by the i-th pipeline. Such constraints are given by C(G L ) since all paths root-to-leaves and back of G are the same as those of G L . Notice that, whereas G is BDR, G is not; it may also contain useless nonterminals.
The following examples illustrate the whole grammar transformation procedure. any counter, in the general case). If instead we are following a specific counter marked by its index f , the sequence of the states (in this case the ascending component of G 's nonterminal) must follow the sequence imposed by the f -th pipeline, whereas the other nonterminals, which correspond to the B terminals of G L N L , may be of any type. The remaining rules of G should now be easily inferred by analogy.
The following example instead highlights the ambiguity of G as a consequence of introducing repeated rhs and the case of a grammar nonterminal belonging to both an ascending and a descending counter, but not paired.
Example 7.21. Consider the following grammar G cross , with S = {A, B}: It is easy to realize that C(G cross ) has a descending counter C 1 = (A B , a) and an ascending one C 2 = (B C , b). Notice that nonterminal B occurs in both counter tables. Without providing explicitly the whole grammar G cross we display C(G cross ) in Figure 7 h, instead, could be used elsewhere as part of a longer G cross derivation. The fact that in the lhs of G cross rule occur the labels of two different counter tables denotes the possibility that it belongs to two different counters. Imagine now that h occurs in the context d − b. This means that dhb has been derived in G cross by C however, could be a further step of the ascending counter C 2 or could interrupt the ascending counter and become an exit step from the descending counter C 1 . Thus, we have two possible groups of lhs for a(C , C Proof. Base of the induction.    By taking into account how G axioms are derived from those of G we immediately obtain the main theorem: THEOREM 7.23. The OPG G and the OPG G built from it on the basis of the above construction are structurally equivalent.
The structural equivalence is an obvious consequence of the fact that the two grammars share the same OPM.
The control graph of grammar G , C(G ), is defined through a natural modification of the original Definition 6.1: precisely, V N is the set of the left elements of V N , and V N the set of right elements thereof. Figure 7.11 displays a fragment of C(G ) for the grammar of Example 7.20. Whereas the transitions from descending states are complete, for brevity only the entry points of the ascending part of the graph are displayed.
The following theorem extends Theorem 6.4 to the grammars such as G derived from BDR OPGs. Proof. The proof is almost identical to that of Theorem 6.4, the only difference coming from the fact that G is not BDR. Thus the of formula (6.3) must be extended to all G productions having any ([X A ] , [X A ] ) as lhs. E.g., in the base of the induction, instead of just one production A → x we may have several ones of type ([X A ] , [X A ] ) → x, each one of them satisfying ψ ([X A ] ,[X A ] ) with the corresponding lhs.
The following theorem is the last step to achieve FO definability of aperiodic OPLs. Proof. The fact that the set of paths is a regular language follows immediately from the definition of the automaton as in Definition 6.1.   Figure 8.1 summarizes the results presented in this paper together with previous related ones. The outer boxes represent equivalent ways to express general OPLs, whereas the inner ones represent equivalent ways to express aperiodic OPLs. The figure immediately suggests a first further research step, i.e., making the inner triangle a square, as well as the outer one: we conjecture that once the concept of NC OPLs has been put in the appropriate framework, a further characterization thereof in terms of a suitable subclass of Legend All boxes denote classes of OPLs with a common OPM: • MSO denotes languages defined through MSO formulas • FO denotes languages defined through FO formulas • OPA denotes languages defined through OP automata [32] • OPESF denotes languages defined through star-free OPEs • OPGNC denotes aperiodic OPLs, i.e., languages defined through NC OPGs Arrows between boxes denote language family inclusion; they are labeled by the reference pointing to the section where the property has been proved, and the asterisk stands for [32]. OPAs should be possible but so far we did not pursue such an option. A further benefit coming from such an extension would be avoiding the hypothesis of . =-acyclic OPMs: this restriction is necessary only to guarantee that an OPG can generate the whole Σ * but is not necessary for OPAs which indeed have a slightly more expressive power than traditional OPGs 13 .
Another natural extension of the results reported in this paper is their generalization to the case of ω-OPLs [32], complementing, once again, previous studies on aperiodic ω-regular languages (see, e.g., [45,51]).
We also hope that the articulated path that we used to prove that NC OPLs are FO definable can be made shorter and more direct, although we cannot forget that even in the case of regular languages such proof paths are rather complex (see, e.g., [38]).
There are other subclasses of regular languages related to the aperiodic ones; among them we mention locally testable languages: intuitively, the distinguishing feature of these languages is that one can decide whether a string belongs to a given language or not by examining only substrings of bounded length. It is known [38] that aperiodic regular languages are the closure of the locally testable ones under concatenation. In [15] we proposed a first definition of locally testable parenthesis languages and showed that they are strictly included in the NC ones. More recently local testability has been investigated for tree-languages and its potential application on data-managing systems has been advocated. [7,41]. It could be worth investigating the relation of this property too with aperiodicity and FO definability for OPLs.
The most exciting goal that some researchers are pursuing, however, is the completion of the great historical path that, for regular languages, lead from the first characterization in terms of MSO logic to the restricted case of FO characterization of NC regular languages, to the temporal logic one which in turn is FO-complete, thanks to Kamp's theorem [43], and, ultimately, to the striking success of model checking techniques.
Some proposals of temporal logic extension of the classic linear or branching time ones to cope with the typical nesting structure of CF languages have been already offered in the literature. E.g., [35] presents an FO-complete temporal logic to specify properties of paths in tree-languages; [1,2,8] present different cases of temporal logics extended to deal with VPLs; they also prove FO-completeness of such logics but do not afford the relation between FO and MSO versions of their logics, neither do they deal with aperiodicity for VPLs 14 . 13 Alternatively, OPGs could be extended with productions allowing for rhs that include regular expressions [18,21] but, since we are not aware of any practical case of OPG with . =-cyclic OPM, we avoided this option to keep the notation not too cumbersome.
14 As a corollary of our result, one can also obtain an FO logic characterization of NC VPLs.
We too have designed a first example of temporal logic for OPLs [12] which recently evolved into a new FO-complete and more user-friendly one [13]. We also built an algorithm that derives an OPA from a formula of this logic of exponential size in the length of the formula and implemented a satisfiability and model checker which has been experimentally tested on a realistic benchmark [14].
Thanks to the result of this paper, and to the fact that most, if not all, of the CF languages for practical applications are aperiodic, the final goal of building model checkers that cover a much wider application field than that of regular languages -and of various structured CF languages, such as VPLs, too-with comparable computational complexity does not seem unreachable.
There are many jewels to extract from the old, but still rich, mine of OPLs.