The Alternation Hierarchy of First-Order Logic on Words is Decidable
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866910806781722624 |
|---|---|
| author | Barloy, Corentin Cadilhac, Michaël Paperman, Charles Straubing, Howard |
| author_facet | Barloy, Corentin Cadilhac, Michaël Paperman, Charles Straubing, Howard |
| contents | We show that for any $i > 0$, it is decidable, given a regular language, whether it is expressible in the $Σ_i[<]$ fragment of first-order logic FO[<]. This settles a question open since 1971.
Our main technical result relies on the notion of polynomial closure of a class of languages $\mathcal{V}$, that is, finite unions of languages of the form $L_0a_1L_1\cdots a_nL_n$ where each $a_i$ is a letter and each $L_i$ a language of $\mathcal{V}$. We show that if a class $\mathcal{V}$ of regular languages with some closure properties (namely, a positive variety) has a decidable separation problem, then so does its polynomial closure Pol($\mathcal{V}$). The resulting algorithm for Pol($\mathcal{V}$) has time complexity that is exponential in the time complexity for $\mathcal{V}$ and we propose a natural conjecture that would lead to a polynomial time blowup instead.
Corollaries include the decidability of half levels of the dot-depth hierarchy and the group-based concatenation hierarchy. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_14899 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The Alternation Hierarchy of First-Order Logic on Words is Decidable Barloy, Corentin Cadilhac, Michaël Paperman, Charles Straubing, Howard Formal Languages and Automata Theory Logic in Computer Science Logic We show that for any $i > 0$, it is decidable, given a regular language, whether it is expressible in the $Σ_i[<]$ fragment of first-order logic FO[<]. This settles a question open since 1971. Our main technical result relies on the notion of polynomial closure of a class of languages $\mathcal{V}$, that is, finite unions of languages of the form $L_0a_1L_1\cdots a_nL_n$ where each $a_i$ is a letter and each $L_i$ a language of $\mathcal{V}$. We show that if a class $\mathcal{V}$ of regular languages with some closure properties (namely, a positive variety) has a decidable separation problem, then so does its polynomial closure Pol($\mathcal{V}$). The resulting algorithm for Pol($\mathcal{V}$) has time complexity that is exponential in the time complexity for $\mathcal{V}$ and we propose a natural conjecture that would lead to a polynomial time blowup instead. Corollaries include the decidability of half levels of the dot-depth hierarchy and the group-based concatenation hierarchy. |
| title | The Alternation Hierarchy of First-Order Logic on Words is Decidable |
| topic | Formal Languages and Automata Theory Logic in Computer Science Logic |
| url | https://arxiv.org/abs/2501.14899 |