Aperiodicity, Star-freeness, and First-order Logic Definability of Operator Precedence Languages

TL;DR

This work advances the theory of formal languages by generalizing the classical equivalence among aperiodicity, star-freeness, and FO definability from regular languages to operator precedence languages (OPLs). It introduces Operator Precedence Expressions (OPEs) and proves that star-free OPEs exactly capture FO-definable, non-counting OPLs, thereby extending NC/SF/FO equivalence to a rich class that includes visibly pushdown languages. A central methodological contribution is the grammar-to-logic translation via a control graph, which partitions grammar structure from string-derived control, enabling MSO formulations that reduce to FO when NC holds. The paper then develops techniques to ensure NC control languages, notably through linearization and counter-based graph transformations that yield FO-definable NC-OPLs. Collectively, the results open avenues for FO-based model checking and temporal-logical frameworks for OPLs and point toward analogous extensions for VPLs and related structured CF languages.

Abstract

A classic result in formal language theory is the equivalence among non-counting, or aperiodic, regular languages, and languages defined through star-free regular expressions, or first-order logic. Past attempts to extend this result beyond the realm of regular languages have met with difficulties: for instance it is known that star-free tree languages may violate the non-counting property and there are aperiodic tree languages that cannot be defined through first-order logic. 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 non-counting 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. We argue that the same approach can be exploited to obtain analogous results for visibly pushdown languages too.

Figures (20)

• Figure 1: $G_{AE}$ (left), its OPM (center), and the syntax tree of $e + e * e + e$ according to the OPM (right).
• Figure 2: The string $e + e * e + e$, with relation $\curvearrowright$.
• Figure 3: The partial OPM defining $L_{\text{Dyck}}$ (left) and a possible completion $M_\text{complete}$ (right).
• Figure 4: The partial OPM $M_\text{int}$ for the OPE describing an interrupt policy.
• Figure 5: An example of paired derivations combined by the concatenation construction. In this case the last character of $u$ is in $\doteq$ relation with the first character of $v$.

Theorems & Definitions (79)

• Proposition 2.1
• Definition 2.2: Grammar and language
• Definition 2.3: Backward deterministic reduced grammar McNaughton67Salomaa73
• Definition 2.4: Floyd1963
• Definition 2.5: Operator precedence grammar
• Example 2.6
• Definition 2.7: OP-alphabet and Maxlanguage
• Proposition 2.8: Algebraic properties of OPGs and OPLs
• Definition 2.9: Monadic Second-Order Logic for OPLs
• Example 2.10