From k+1 to k heads the descriptive trade-off is non-recursive

Christos Kapoutsis

Home/Archive/arXiv

arXiv · 2610.11958

From k+1 to k heads the descriptive trade-off is non-recursive

Christos Kapoutsis

View original source ↗Read source document ↗Export metadata ↓

Abstract

We prove that no recursive function can upper bound the increase in the size of description when a two-way deterministic finite automaton with k+1 heads is replaced by an equivalent two-way deterministic finite automaton with k heads. This is true for all k, and remains true if the automata are unary and/or nondeterministic.

Explore related subjects

cs.FL

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Christos Kapoutsis. 2026-10-08. From k+1 to k heads the descriptive trade-off is non-recursive. https://arxiv.org/abs/2610.11958

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

KEEP EXPLORING

Related papers

arXiv2026

Parameterized Reachability for Register Machines with Data

We investigate the parameterized reachability problem for concurrent register machines over infinite data domains. In this framework, each machine is a program equipped with a set of local registers, the communication across machines is mediated through a set of shared registers. Both local and shared registers can take values from an infinite data domain. The program's primitive operations include copying values between registers, assigning constants, comparing registers for (dis-)equality, and nondeterministic assignments that store an arbitrary domain value into a local register. The parameterized reachability problem considers a program and a target location, asking whether there exists some n in Naturals such that an execution of n identical machines (referred to as instances) results in at least one instance reaching the specified location. We show that this problem is Pspace-complete in the general case and it becomes undecidable if a freshness assumption (i.e., each assignment must produce a unique value distinct from all constants) is applied to nondeterministic assignments. This undecidability persists even for systems restricted to two shared and two local registers. Finally, we establish optimal decidability results for two restricted settings: when each thread is limited to a single local register, or when the system utilizes only one shared register.

cs.FL↗

arXiv2026

An Improved Lower Bound for Separating Words by Permutation Automata

We prove that some pairs of binary words of every sufficiently large prescribed length $n$ require $Ω(\log n\log\log n)$ states to separate by a deterministic finite automaton whose letters act as permutations. We obtain this bound by constructing distinct equal-length positive binary words that form an identity of $\mathfrak{S}_k$ of length $\exp(O(k/\log k))$. This improves the previous lower bound $(3/2-o(1))\log n$ of Bulatov, Karpova, Shur, and Startsev (arXiv:1609.03199). The proof combines a positive-word construction with a cover of permutation orders. Consecutive segments of prime powers reduce the covering problem to enumerating sets of positive integers with bounded sum. The required estimates use the central binomial coefficient and the classical asymptotic formula for partitions into distinct parts. An appendix gives sharper constants and lower-order terms using a greedy cover and a quantitative prime number theorem.

cs.FL↗

arXiv2026

Type-Checking for Pattern-Based Tree Transformations

We introduce and study pattern-based tree transformations. As an illustrating example, consider a source pattern $(x \cdot y) + (x \cdot z)$ and a target pattern $x \cdot (y + z)$ as a pair. This source pattern matches any expression $e$ of the form $(e_1 \cdot e_2) + (e_1 \cdot e_3)$ (by substituting $x$ with $e_1$, $y$ with $e_2$, and $z$ with $e_3$) and the pair transforms it into the expression $e_1 \cdot (e_2 + e_3)$ as dictated by the target pattern. Note that in this example, the set of expressions that match the source pattern is not a regular tree language. We propose a model of tree transformations given by a finite representation of a (possibly infinite) set of such (source pattern, target pattern) pairs. The expressive power of this model comes at the cost of undecidability of checking equivalence. Nevertheless, we show that the type-checking problem is decidable for our model of pattern-based tree transformations. The type-checking problem asks whether applying a given transformation to trees having a given regular property (type) preserves the property. Our decision procedure is by a reduction to the emptiness problem of alternating tree automata.

cs.FL↗