One-Dimensional Fragment over Words and Trees

TL;DR

This work analyzes the one-dimensional fragment $F_1$ of first-order logic over words and trees, providing a complete complexity classification for satisfiability under various navigational signatures and comparing its expressive power with $FO^2$, $C^2$, and $UNFO$. It establishes that over words and $ ext{ω}$-words, $F_1[{ ightarrow},{ ightarrow^{+}}]$ is expressively equivalent to well-known two-variable and temporal formalisms, while over trees the expressivity depends on the navigational signature, equating $F_1$ with CoreXPath, GF$^2$, FO$^2$, C$^2$, and UNFO for XML-like signatures and yielding distinct hierarchies for unordered trees. The paper develops a refined toolkit—normal forms, types, profiles, and contraction/surgery techniques—to prove small-model properties and derive tight complexity bounds: $N ext{ExpTime}$-complete for word cases; $2 ext{-ExpTime}$-complete with full XML navigations and $ ext{ExpSpace}$-complete in several reduced-signature scenarios for trees. It also maps a robust boundary between decidability and undecidability, showing undecidability for certain extensions such as data words and uninterpreted binary relations. Overall, the results provide a comprehensive landscape of the computational and expressive characteristics of $F_1$ across word and tree domains, with implications for database-like grammars and navigational logics such as CoreXPath.

Abstract

One-dimensional fragment of first-order logic is obtained by restricting quantification to blocks of existential (universal) quantifiers that leave at most one variable free. We investigate this fragment over words and trees, presenting a complete classification of the complexity of its satisfiability problem for various navigational signatures, and comparing its expressive power with other important formalisms. These include the two-variable fragment with counting and the unary negation fragment.

Figures (6)

• Figure 1: The grid-like structure used to show undecidability of $\hbox{\rm F}_1$$[{\rightarrow}, \sim]$. Solid arrows represent ${\rightarrow}$, wavy lines represent $\sim$.
• Figure 2: The grid-like structure used to show undecidability of $\hbox{\rm F}_1$$[{\rightarrow}_1, {\rightarrow}_2]$. Solid arrows represent ${\rightarrow}_1$, dotted arrows represent ${\rightarrow}_2$.
• Figure 3: A visualisation of a tree ordering scheme. Straight arrows represent ${\downarrow}$, wavy arrows represent ${\downarrow_{ +}}$. Connections implied by transitivity are omitted for clarity.
• Figure 4: Positions in a tree with respect to a node $a$.
• Figure 5: Combining type $\pi_1$, $\pi_2$ into a single type $\pi_3$. The dashed and solid connection in $\pi_3$ are present in $\pi_1$ and, resp., $\pi_2$, the wavy connection follows from the definition of profiles.

Theorems & Definitions (63)

• Lemma 2.1
• proof
• Lemma 2.2
• proof
• Theorem 3.1
• Lemma 3.2
• proof
• Lemma 4.1
• proof
• Lemma 4.2