Search arXiv⌕ Search

arXiv · 2610.16473

Some complete $ω$-powers of a one-counter language in the difference hierarchy

Abstract

Fix a finite alphabet $Σ$ having at least two letters, and natural numbers $n,k\geq 1$. We denote by $D_n(\mathbfΠ^0_k)$ the class of differences of $n$ subsets of the Cantor space $Σ^ω$ in $\mathbfΠ^0_k$, and by $\checked{D}_n(\mathbfΠ^0_k)$ the class of complements of sets in $D_n(\mathbfΠ^0_k)$. We prove, for any natural numbers $n,k\geq 1$, the existence of a finite alphabet $Σ$ having at least two letters and a finitary language $U_{n,k}$ over $Σ$ accepted by a one-counter automaton such that the $ω$-power $$U_{n,k}^\infty:=\{ w_0w_1\cdots\inΣ^ω\mid\forall i\inω~~w_i\in U_{n,k}\}$$ is $D_{2n-1}(\mathbfΠ^0_k)$-complete. We also prove a conditional result for the dual classes $\checked{D}\_{2n}(\mathbfΠ^0\_k)$: under the assumption that there exists a finitary language $V_{n,3}$ accepted by a one-counter automaton, such that its $ω$-power $V_{n,3}^\infty$ is $\checked{D}_{2n}(\mathbfΠ^0_3)$-complete, there would also exist, for any integer $k>3$, a finitary language $V_{n,k}$ accepted by a one-counter automaton, such that its $ω$-power $V_{n,k}^\infty$ is $\checked{D}_{2n}(\mathbfΠ^0_k)$-complete. Finally we add another conditionnal result about Wadge degrees of rational $\mathbfΔ^0_2$ omega powers, which completes the recent results of [FGL26].

Explore related subjects

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Jacques Duparc, Olivier Finkel, Dominique Lecomte. 2026-10-12. Some complete $ω$-powers of a one-counter language in the difference hierarchy. https://arxiv.org/abs/2610.16473

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

Algorithmic Unverifiability of Safety for Fixed and Recursively Self-Improving Systems

Existing impossibility results for AI verification concern a fixed system. Self-modifying systems (agents that rewrite their own code, recursive self-improvement loops) raise a different question: can a safety property that holds now be certified, in advance, to keep holding after the system rewrites itself? We model one step of self-modification as a total computable transformation of code, and preservation as 'safe now and safe after the step'. If the transformation depends only on behaviour, preservation is Rice's theorem one level up; if it reads the code, as self-modification does, preservation is no longer semantic, yet at least as hard as the halting problem, by the same s-m-n reduction carried out inside a class of behaviourally identical programs. One step is never harder than the property; persistence along the whole trajectory can be one arithmetical level higher. No tower of supervisors lowers the problem; every total supervisor errs on a set of systems it cannot locate. Every faithful scheme certifying on finite behavioural evidence admits, for properties not settled by any finite set of inputs, an evolution trace it certifies at every stage while the property is violated. Statically, we record the classical limits (Rice, Goedel, Trakhtenbrot) and add the resource face: over succinctly described finite environments, verifying a policy against an adversary is coNP-complete and synthesising one PSPACE-complete. These limits do not say self-modifying systems are unsafe; they locate where algorithmic guarantees break, at the expressivity a general system needs: Turing-completeness and unrestricted self-modification. What survives is exact: a monitor detects the first violation of a safety property, and no sound procedure certifies all safe systems; certification requires restricting rewrites by design; and a frozen reference keeps the question well posed.

cs.LO↗

Cover Semantics for Intuitionistic Modalities

Intuitionistic modal logic (IML) has inspired several developments in programming languages including modal type systems for staging, computational effects and language-based security. IMLs are typically studied using Kripke-style relational semantics, which simplifies proofs of meta-theoretic properties, such as completeness and consistency, by making it easy to construct models. Kripke-style relational semantics, however, relies upon classical reasoning principles, which makes it unappealing from a computational perspective and unsuitable for formalization in a constructive type theory. Goldblatt provides an alternative semantics for IMLs by extending Beth-Kripke-Joyal-style "cover" semantics for intuitionistic propositional logic with relations to support modalities. Goldblatt's "relational cover" semantics overcomes classical reasoning but introduces a new limitation: it relies upon a "modal localization" condition that restricts the class of models and complicates model construction. Goldblatt bypasses this restriction by using intricate order-theoretic completion arguments to prove completeness. In this article, we present a conservative extension of relational cover semantics that alleviates this restriction and is amenable to simpler and standard model construction techniques. We formalize our semantics in Agda and prove completeness constructively in the style of Normalization by Evaluation for a variety of IMLs featuring independent box and diamond modalities.

cs.LO↗

Formalizing Flag Algebras in Lean

Razborov's flag algebra method is one of the most successful tools for proving asymptotic density inequalities in extremal graph theory. It reduces an inequality about all large graphs avoiding a forbidden pattern to finitely many algebraic conditions, and a certificate satisfying them can be found by semidefinite programming. We formalize the method for finite simple graphs in Lean 4, building on Mathlib. The formalization covers flags and their densities, the flag algebra as a quotient vector space, positive homomorphisms as limits of graph sequences, Razborov's random extensions, and the downward operator that averages out labels. On top of this theory, we build verified computation of flag densities and a tactic that turns certificates found by semidefinite programming into Lean proofs. The certificate serves only as candidate data; Lean checks every fact the proof uses. With this development we verify seven Turán-type upper bounds. Adding lower-bound constructions proved in Lean yields the asymptotic form of Mantel's theorem and the asymptotic Erdős pentagon theorem $π(C_5;K_3)=24/625$; to our knowledge, the latter has not previously been formalized in a proof assistant. We also prove two inequalities of Goodman. All density theorems reported here depend only on the standard axioms of Lean's logic. Formalization also led us to treat forbidden subgraphs with a different semantics. Instead of building a separate flag algebra for each forbidden family, we keep a single algebra of all graphs and impose the constraint only when interpreting an inequality, through randomly labeled limits of graphs satisfying it. We prove that this ensemble semantics yields the intended density bounds, and that a condition we call root-plantability characterizes when it agrees with the standard semantics.

cs.LO↗