Existential Definability over the Subword Ordering

DOI10.46298/LMCS-19(4:35)2023MaRDI QIDQ6178718zbMATH OpenOpenAlexFDO

Authors Pascal Baumann, Moses Ganardi, Ramanathan S. Thinniyam, Georg Zetzsche

Publication date 16 January 2024

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2210.15642

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Abstract: We study first-order logic (FO) over the structure consisting of finite words over some alphabet $A$, together with the (non-contiguous) subword ordering. In terms of decidability of quantifier alternation fragments, this logic is well-understood: If every word is available as a constant, then even the $Sigm{a}_1$ (i.e., existential) fragment is undecidable, already for binary alphabets $A$. However, up to now, little is known about the expressiveness of the quantifier alternation fragments: For example, the undecidability proof for the existential fragment relies on Diophantine equations and only shows that recursively enumerable languages over a singleton alphabet (and some auxiliary predicates) are definable. We show that if $|A|ge3$, then a relation is definable in the existential fragment over $A$ with constants if and only if it is recursively enumerable. This implies characterizations for all fragments $Sigm{a}_i$: If $|A|ge3$, then a relation is definable in $Sigm{a}_i$ if and only if it belongs to the $i$-th level of the arithmetical hierarchy. In addition, our result yields an analogous complete description of the $Sigm{a}_i$-fragments for $ige2$ of the pure logic, where the words of $A^{\ast }$ are not available as constants.

Cites work

• Algorithms for subsequence combinatorics
• An approach to computing downward closures
• Complexity of counting first-order logic for the subword order
• Computing downward closures for stacked counter automata
• Context-bounded analysis for concurrent programs with dynamic creation of threads
• Decidability in the logic of subsequences and supersequences
• Definability in the Subword Order
• General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
• scientific article; zbMATH DE number 3660804 (Why is no real title available?)
• scientific article; zbMATH DE number 545277 (Why is no real title available?)
• scientific article; zbMATH DE number 7204383 (Why is no real title available?)
• scientific article; zbMATH DE number 7297889 (Why is no real title available?)
• scientific article; zbMATH DE number 7056230 (Why is no real title available?)
• Languages ordered by the subword order
• Logically defined subsets of \(\mathbb{N}{}^ k\)
• Multivariate fine-grained complexity of longest common subsequence
• On Arch Factorization and Subword Universality for Words and Compressed Words
• On the index of Simon's congruence for piecewise testability
• Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable
• Scattered Factor-Universality of Words
• Searching subsequences
• Separability by piecewise testable languages and downward closures beyond subwords
• Testing Simon's congruence
• The complexity of downward closure comparisons
• The complexity of regular abstractions of one-counter languages
• The Complexity of Some Problems on Subsequences and Supersequences
• The diagonal problem for higher-order recursion schemes is decidable
• The downward-closure of Petri net languages
• The ideal approach to computing closed subsets in well-quasi-orderings
• Theories of orders on the set of words
• Unboundedness and downward closures of higher-order pushdown automata
• Verifying programs with unreliable channels
• What makes some language theory problems undecidable

Cited in

(2)

• Jumbled scattered factors
• Scattered factor universality -- a survey

This page was built for publication: Existential Definability over the Subword Ordering

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6178718)