arXiv subjects

James Worrell

Publications and source records attributed to James Worrell.

At least 19 recordsLinked to original sources

arXiv2026

Conjectural Decidability of the Skolem Problem

The Skolem Problem asks to determine whether a given integer linear recurrence sequence (LRS) has a zero term. This problem, whose decidability has been open for many decades, arises across a wide range of topics in computer science, including loop termination, formal languages, automata theory, and probabilistic model checking, amongst many others. In the present paper, we introduce a notion of "large" zeros of (non-degenerate) linear recurrence sequences, i.e., zeros occurring at an index larger than a double exponential of the magnitude of the data defining the given LRS. We establish two main results. First, we define an infinite set of prime numbers, termed "good", having density one amongst all prime numbers, with the following property: for any large zero of a given LRS, there is an interval around the large zero together with an upper bound on the number of good primes possibly present in that interval. The bound in question is much lower than one would expect if good primes were distributed similarly as ordinary prime numbers, as per the Cram\'er model in number theory. We therefore conclude, conditionally on a strengthening of the classical Cram\'er conjecture, that large zeros do not exist, which would entail decidability of the Skolem Problem. Second, we show unconditionally that large zeros are very sparse: the set of positive integers that can possibly arise as large zeros of some LRS has null density. This in turn immediately yields a Universal Skolem Set of density one, answering a question left open in the literature.

cs.DM↗

arXiv2025

Termination Analysis of Linear-Constraint Programs

This paper provides an overview of techniques in termination analysis for programs with numerical variables and transitions defined by linear constraints. This subarea of program analysis is challenging due to the existence of undecidable problems, and this Survey systematically explores approaches that mitigate this inherent difficulty. These include foundational decidability results, the use of ranking functions, and disjunctive well-founded transition invariants. The Survey also discusses non-termination witnesses, used to prove that a program will not halt. We examine the algorithmic and complexity aspects of these methods, showing how different approaches offer a trade-off between expressive power and computational complexity. The Survey does not discuss how termination analysis is performed on real-world programming languages, nor does it consider more expressive abstract models that include non-linear arithmetic, probabilistic choice, or term rewriting systems.

cs.PL↗

arXiv2025

Positivity of Nearly Linearly Recurrent Sequences

Nearly linear recurrences generalise linear recurrences and can be represented as special cases of both linear time-invariant systems in control theory and linear-constraint loops in program analysis. We formulate the Positivity Problem for such recurrences: given a recurrence and initial values, decide whether every sequence satisfying the recurrence is termwise nonnegative. This problem generalises Positivity for linear recurrence sequences and is a special case of halfspace non-reachability for linear time-invariant systems. Our main result is a decision procedure for order-2 recurrences. The termination of the procedure relies on a transcendence theorem of independent interest: we prove that certain convergent series obtained by summing the absolute values of terms of algebraic linear recurrence sequences are transcendental.

math.DS↗

arXiv2025

On the growth of hypergeometric sequences

Hypergeometric sequences obey first-order linear recurrence relations with polynomial coefficients and are commonplace throughout the mathematical and computational sciences. For certain classes of hypergeometric sequences, we prove linear growth estimates on their Weil heights. We give an application of our effective results towards the Membership Problem from Computer Science. Recall that Membership asks to procedurally determine whether a specified target is an element of a given recurrence sequence.

math.NT↗

arXiv2025

On the Complexity of the Skolem Problem at Low Orders

The Skolem Problem asks to determine whether a given linear recurrence sequence (LRS) $\langle u_n \rangle_{n=0}^\infty$ over the integers has a zero term, that is, whether there exists $n$ such that $u_n = 0$. Decidability of the problem is open in general, with the most notable positive result being a decision procedure for LRS of order at most 4. In this paper we consider a bounded version of the Skolem Problem, in which the input consists of an LRS $\langle u_n \rangle_{n=0}^\infty$ and a bound $N \in \mathbb N$ (with all integers written in binary), and the task is to determine whether there exists $n\in\{0,\ldots,N\}$ such that $u_n=0$. We give a randomised algorithm for this problem that, for all $d\in \mathbb N$, runs in polynomial time on the class of LRS of order at most $d$. As a corollary we show that the (unrestricted) Skolem Problem for LRS of order at most 4 lies in $\mathsf{coRP}$, improving the best previous upper bound of $\mathsf{NP}^{\mathsf{RP}}$. The running time of our algorithm is exponential in the order of the LRS -- a dependence that appears necessary in view of the $\mathsf{NP}$-hardness of the Bounded Skolem Problem. However, even for LRS of a fixed order, the problem involves detecting zeros within an exponentially large range. For this, our algorithm relies on results from $p$-adic analysis to isolate polynomially many candidate zeros and then test in randomised polynomial time whether each candidate is an actual zero by reduction to arithmetic-circuit identity testing.

cs.CC↗

arXiv2025

Algebraic Closure of Matrix Sets Recognized by 1-VASS

It is known how to compute the Zariski closure of a finitely generated monoid of matrices and, more generally, of a set of matrices specified by a regular language. This result was recently used to give a procedure to compute all polynomial invariants of a given affine program. Decidability of the more general problem of computing all polynomial invariants of affine programs with recursive procedure calls remains open. Mathematically speaking, the core challenge is to compute the Zariski closure of a set of matrices defined by a context-free language. In this paper, we approach the problem from two sides: Towards decidability, we give a procedure to compute the Zariski closure of sets of matrices given by one-counter languages (that is, languages accepted by one-dimensional vector addition systems with states and zero tests), a proper subclass of context-free languages. On the other side, we show that the problem becomes undecidable for indexed languages, a natural extension of context-free languages corresponding to nested pushdown automata. One of our main technical tools is a novel adaptation of Simon's factorization forests to infinite monoids of matrices.

cs.FL↗

arXiv2025

Computing transcendence and linear relations of 1-periods

A 1-period is a complex number given by the integral of a univariate algebraic function, where all data involved -- the integrand and the domain of integration -- are defined over algebraic numbers. We give an algorithm that, given a finite collection of 1-periods, computes the space of all linear relations among them with algebraic coefficients. In particular, the algorithm decides whether a given 1-period is transcendental, and whether two 1-periods are equal. This resolves, in the case of 1-periods, a problem posed by Kontsevich and Zagier, asking for an algorithm to decide equality of periods. The algorithm builds on the work of Huber and W\"ustholz, who showed that all linear relations among 1-periods arise from 1-motives; we make this perspective effective by reducing the problem to divisor arithmetic on curves and providing the theoretical foundations for a practical and fully explicit algorithm. To illustrate the broader applicability of our methods, we also give an algorithmic classification of autonomous first-order (non-linear) differential equations.

math.AG↗

arXiv2025

On the $p$-adic Skolem Problem

The Skolem Problem asks to determine whether a given linear recurrence sequence (LRS) has a zero term. Showing decidability of this problem is equivalent to giving an effective proof of the Skolem-Mahler-Lech Theorem, which asserts that a non-degenerate LRS has finitely many zeros. The latter result was proven over 90 years ago via an ineffective method showing that such an LRS has only finitely many $p$-adic zeros. In this paper we consider the problem of determining whether a given LRS has a $p$-adic zero, as well as the corresponding function problem of computing exact representations of all $p$-adic zeros. We present algorithms for both problems and report on their implementation. The output of the algorithms is unconditionally correct, and termination is guaranteed subject to the $p$-adic Schanuel Conjecture (a standard number-theoretic hypothesis concerning the $p$-adic exponential function). While these algorithms do not solve the Skolem Problem, they can be exploited to find natural-number and rational zeros under additional hypotheses. To illustrate this, we apply our results to show decidability of the Simultaneous Skolem Problem (determine whether two coprime linear recurrences have a common natural-number zero), again subject to the $p$-adic Schanuel Conjecture.

cs.LO↗

arXiv2024

Transcendence of Hecke-Mahler Series

We prove transcendence of the Hecke-Mahler series $\sum_{n=0}^\infty f(\lfloor n\theta+\alpha \rfloor) \beta^{-n}$, where $f(x) \in \mathbb{Z}[x]$ is a non-constant polynomial $\alpha$ is a real number, $\theta$ is an irrational real number, and $\beta$ is an algebraic number such that $|\beta|>1$.

math.NT↗

arXiv2024

A parametric version of the Hilbert Nullstellensatz

Hilbert's Nullstellensatz is a fundamental result in algebraic geometry that gives a necessary and sufficient condition for a finite collection of multivariate polynomials to have a common zero in an algebraically closed field. Associated with this result, there is the computational problem HN of determining whether a system of polynomials with coefficients in the field of rational numbers has a common zero over the field of algebraic numbers. In an influential paper, Koiran showed that HN can be determined in the polynomial hierarchy assuming the Generalised Riemann Hypothesis (GRH). More precisely, he showed that HN lies in the complexity class AM under GRH. In a later work he generalised this result by showing that the problem DIM, which asks to determine the dimension of the set of solutions of a given polynomial system, also lies in AM subject to GRH. In this paper we study the solvability of polynomial equations over arbitrary algebraically closed fields of characteristic zero. Up to isomorphism, every such field is the algebraic closure of a field of rational functions. We thus formulate a parametric version of HN, called HNP, in which the input is a system of polynomials with coefficients in a function field $\mathbb{Q}(\mathbf{x})$ and the task is to determine whether the polynomials have a common zero in the algebraic closure $\overline{\mathbb{Q}(\mathbf{x})}$. We observe that Koiran's proof that DIM lies in AM can be interpreted as a randomised polynomial-time reduction of DIM to HNP, followed by an argument that HNP lies in AM. Our main contribution is a self-contained proof that HNP lies in AM that follows the same basic idea as Koiran's argument -- namely random instantiation of the parameters -- but whose justification is purely algebraic, relying on a parametric version of Hilbert's Nullstellensatz, and avoiding recourse to semi-algebraic geometry.

cs.CC↗

arXiv2024

Reachability for Multi-Priced Timed Automata with Positive and Negative Rates

Multi-priced timed automata (MPTA) are timed automata with observer variables whose derivatives can change from one location to another. Observers are write-only variables, that is, they do not affect the control flow of the automaton; thus MPTA lie between timed and hybrid automata in expressiveness. Previous work considered observers with non-negative slope in every location. In this paper we treat observers that have both positive and negative rates. Our main result is an algorithm to decide a gap version of the reachability problem for this variant of MPTA. We translate the gap reachability problem into a gap satisfiability problem for mixed integer-real systems of nonlinear constraints. Our main technical contribution -- a result of independent interest -- is a procedure to solve such contraints via a combination of branch-and-bound and relaxation-and-rounding.

cs.FL↗

arXiv2024

Differential Tree Automata

A rationally dynamically algebraic (RDA) power series is one that arises as (a component of) the solution of a system of differential equations of the form $\boldsymbol{y}' = F(\boldsymbol{y})$, where $F$ is a vector of rational functions that is defined at $\boldsymbol{y}(0)$. RDA power series subsume algebraic power series and are a proper subclass of differentially algebraic power series (those that satisfy a univariate polynomial-differential equation). We give a combinatorial characterisation of RDA power series in terms of exponential generating functions of regular languages of labelled trees. Motivated by this connection, we define the notion of a differential tree automaton. Differential tree automata generalise weighted tree automata by allowing the transition weights to be rational functions of the tree size. Our main result is that the ordinary generating functions of the formal tree series recognised by differential tree automata are exactly the differentially algebraic power series. The proof of this result establishes a general form of recurrence satisfied by the sequence of coefficients of a differentially algebraic power series, generalising Reutenauer's matrix representation of polynomially recursive sequences. As a corollary we obtain a procedure for determining equality of differential tree automata.

cs.FL↗

arXiv2024

On the Decidability of Presburger Arithmetic Expanded with Powers

We prove that for any integers $\alpha, \beta > 1$, the existential fragment of the first-order theory of the structure $\langle \mathbb{Z}; 0,1,<, +, \alpha^{\mathbb{N}}, \beta^{\mathbb{N}}\rangle$ is decidable (where $\alpha^{\mathbb{N}}$ is the set of positive integer powers of $\alpha$, and likewise for $\beta^{\mathbb{N}}$). On the other hand, we show by way of hardness that decidability of the existential fragment of the theory of $\langle \mathbb{N}; 0,1, <, +, x\mapsto \alpha^x, x \mapsto \beta^x\rangle$ for any multiplicatively independent $\alpha,\beta > 1$ would lead to mathematical breakthroughs regarding base-$\alpha$ and base-$\beta$ expansions of certain transcendental numbers.

cs.LO↗

arXiv2024

Determination Problems for Orbit Closures and Matrix Groups

Computational problems concerning the orbit of a point under the action of a matrix group occur throughout computer science, including in program analysis, complexity theory, quantum computation, and automata theory. In many cases the focus extends beyond orbits proper to orbit closures under a suitable topology. Typically one starts from a group and a set of points and asks questions about the orbit closure of the set under the action of the group, e.g., whether two given orbit closures intersect. In this paper we consider a collection of what we call determination problems concerning matrix groups and orbit closures. These problems begin with a given variety and seek to understand whether and how it arises either as an algebraic matrix group or as an orbit closure. The how question asks whether the underlying group is $s$-generated, meaning it is topologically generated by $s$ matrices for a given number $s$. Among other applications, problems of this type have recently been studied in the context of synthesising loops subject to certain specified invariants on program variables. Our main result is a polynomial-space procedure that inputs a variety and a number $s$ and determines whether the given variety arises as an orbit closure of a point under an $s$-generated commutative algebraic matrix group. The main tools in our approach are structural properties of commutative algebraic matrix groups and module theory. We leave open the question of determining whether a variety is an orbit closure of a point under an $s$-generated algebraic matrix group (without the requirement of commutativity).

cs.CC↗

arXiv2024

On the Decidability of Monadic Theories of Arithmetic Predicates

We investigate the decidability of the monadic second-order (MSO) theory of the structure $\langle \mathbb{N};<,P_1, \ldots,P_d \rangle$, for various unary predicates $P_1,\ldots,P_d \subseteq \mathbb{N}$. We focus in particular on 'arithmetic' predicates arising in the study of linear recurrence sequences, such as fixed-base powers $k^{\mathbf{N}} = \{k^n : n \in \mathbb{N}\}$, $k$-th powers $\mathbf{N}^k = \{n^k : n \in \mathbb{N}\}$, and the set of terms of the Fibonacci sequence $\mathsf{Fib} = \{0,1,2,3,5,8,13,\ldots\}$ (and similarly for other linear recurrence sequences having a single, non-repeated, dominant characteristic root). We obtain several new unconditional and conditional decidability results, a select sample of which are the following: $\bullet$ The MSO theory of $\langle \mathbb{N};<, 2^{\mathbf{N}}, \mathsf{Fib} \rangle$ is decidable; $\bullet$ The MSO theory of $\langle \mathbb{N};<, 2^{\mathbf{N}}, 3^{\mathbf{N}}, 6^{\mathbf{N}} \rangle$ is decidable; $\bullet$ The MSO theory of $\langle \mathbb{N};<, 2^{\mathbf{N}}, 3^{\mathbf{N}}, 5^{\mathbf{N}} \rangle$ is decidable assuming Schanuel's conjecture; $\bullet$ The MSO theory of $\langle \mathbb{N};<, 4^{\mathbf{N}}, \mathbf{N}^2 \rangle$ is decidable; $\bullet$ The MSO theory of $\langle \mathbb{N};<, 2^{\mathbf{N}}, \mathbf{N}^2 \rangle$ is Turing-equivalent to the MSO theory of $\langle \mathbb{N};<,S \rangle$, where $S$ is the predicate corresponding to the binary expansion of $\sqrt{2}$. (As the binary expansion of $\sqrt{2}$ is widely believed to be normal, the corresponding MSO theory is in turn expected to be decidable.) These results are obtained by exploiting and combining techniques from dynamical systems, number theory, and automata theory.

cs.LO↗

arXiv2024

Transcendence for Pisot Morphic Words over an Algebraic Base

It is known that for a uniform morphic sequence $\boldsymbol u = \langle u_n\rangle_{n=0}^\infty$ and an algebraic number $\beta$ such that $|\beta|>1$, the number $[\![\boldsymbol{u} ]\!]_\beta:=\sum_{n=0}^\infty \frac{u_n}{\beta^n}$ either lies in $\mathbb Q(\beta)$ or is transcendental. In this paper we show a similar rational-transcendental dichotomy for sequences defined by irreducible Pisot morphisms. Subject to the Pisot conjecture (an irreducible Pisot morphism has pure discrete spectrum), we generalise the latter result to arbitrary finite alphabets. In certain cases we are able to show transcendence of $[\![\boldsymbol{u}]\!]_{\beta}$ outright. In particular, for $k\geq 2$, if $\boldsymbol u$ is the $k$-bonacci word then $[\![\boldsymbol{u}]\!]_{\beta}$ is transcendental.

math.NT↗

arXiv2024

On Rational Recursion for Holonomic Sequences

It was recently conjectured that every component of a discrete-time rational dynamical system is a solution to an algebraic difference equation that is linear in its highest-shift term (a quasi-linear equation). We prove that the conjecture holds in the special case of holonomic sequences, which can straightforwardly be represented by rational dynamical systems. We propose two algorithms for converting holonomic recurrence equations into such quasi-linear equations. The two algorithms differ in their efficiency and the minimality of orders in their outputs.

cs.SC↗

arXiv2024

The 2-Dimensional Constraint Loop Problem is Decidable

A linear constraint loop is specified by a system of linear inequalities that define the relation between the values of the program variables before and after a single execution of the loop body. In this paper we consider the problem of determining whether such a loop terminates, i.e., whether all maximal executions are finite, regardless of how the loop is initialised and how the non-determinism in the loop body is resolved. We focus on the variant of the termination problem in which the loop variables range over $\mathbb{R}$. Our main result is that the termination problem is decidable over the reals in dimension~2. A more abstract formulation of our main result is that it is decidable whether a binary relation on $\mathbb{R}^2$ that is given as a conjunction of linear constraints is well-founded.

cs.LO↗