arXiv subjects

George Kenison

Publications and source records attributed to George Kenison.

15 recordsLinked to original sources

arXiv2026

On Word Representations and Embeddings in Complex Matrices

Embeddings of word structures into matrix semigroups provide a natural bridge between combinatorics on words and linear algebra. However, low-dimensional matrix semigroups impose strong structural restrictions on possible embeddings. Certain finitely generated groups admit faithful representations in SL(2, C) and other similar matrix groups. On the other hand, it is known that the product of two free semigroups on two generators cannot be embedded into the 2x2 complex matrices. In this paper we study embeddings of word structures into low-dimensional matrix semigroups over the complex numbers and develop new techniques for constructing word representations of the Euclidean Bianchi groups. These representations provide a symbolic framework and a natural first step towards analysing fundamental decision problems in 2x2 matrix semigroups.

cs.FL↗

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↗

arXiv2024

Simple Linear Loops: Algebraic Invariants and Applications

The automatic generation of loop invariants is a fundamental challenge in software verification. While this task is undecidable in general, it is decidable for certain restricted classes of programs. This work focuses on invariant generation for (branching-free) loops with a single linear update. Our primary contribution is a polynomial-space algorithm that computes the strongest algebraic invariant for simple linear loops, generating all polynomial equations that hold among program variables across all reachable states. The key to achieving our complexity bounds lies in mitigating the blowup associated with variable elimination and Gr\"obner basis computation, as seen in prior works. Our procedure runs in polynomial time when the number of program variables is fixed. We examine various applications of our results on invariant generation, focusing on invariant verification and loop synthesis. The invariant verification problem investigates whether a polynomial ideal defining an algebraic set serves as an invariant for a given linear loop. We show that this problem is coNP-complete and lies in PSPACE when the input ideal is given in dense or sparse representations, respectively. In the context of loop synthesis, we aim to construct a loop with an infinite set of reachable states that upholds a specified algebraic property as an invariant. The strong synthesis variant of this problem requires the construction of loops for which the given property is the strongest invariant. In terms of hardness, synthesising loops over integers (or rationals) is as hard as Hilbert's Tenth problem (or its analogue over the rationals). When the constants of the output are constrained to bit-bounded rational numbers, we demonstrate that loop synthesis and its strong variant are both decidable in PSPACE, and in NP when the number of program variables is fixed.

cs.CC↗

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↗

arXiv2023

Linear Loop Synthesis for Quadratic Invariants

Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. Yet, generating invariants is a notorious task already for syntactically restricted classes of loops. Rather than generating invariants for given loops, in this paper we synthesise loops that exhibit a predefined behaviour given by an invariant. From the perspective of formal loop verification, the synthesised loops are thus correct by design and no longer need to be verified. To overcome the hardness of reasoning with arbitrarily strong invariants, in this paper we construct simple (non-nested) while loops with linear updates that exhibit polynomial equality invariants. Rather than solving arbitrary polynomial equations, we consider loop properties defined by a single quadratic invariant in any number of variables. We present a procedure that, given a quadratic equation, decides whether a loop with affine updates satisfying this equation exists. Furthermore, if the answer is positive, the procedure synthesises a loop and ensures its variables achieve infinitely many different values.

cs.LO↗

arXiv2023

(Un)Solvable Loop Analysis

Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem. Whilst the problem is in general undecidable, the goal is settled for restricted classes of loops. For the class of solvable loops, introduced by Kapur and Rodr\'iguez-Carbonell in 2004, one can automatically compute invariants from closed-form solutions of recurrence equations that model the loop behaviour. In this paper we establish a technique for invariant synthesis for loops that are not solvable, termed unsolvable loops. Our approach automatically partitions the program variables and identifies the so-called defective variables that characterise unsolvability. Herein we consider the following two applications. First, we present a novel technique that automatically synthesises polynomials from defective monomials, that admit closed-form solutions and thus lead to polynomial loop invariants. Second, given an unsolvable loop, we synthesise solvable loops with the following property: the invariant polynomials of the solvable loops are all invariants of the given unsolvable loop. Our implementation and experiments demonstrate both the feasibility and applicability of our approach to both deterministic and probabilistic programs.

cs.PL↗

arXiv2023

The Membership Problem for Hypergeometric Sequences with Quadratic Parameters

Hypergeometric sequences are rational-valued sequences that satisfy first-order linear recurrence relations with polynomial coefficients; that is, a hypergeometric sequence $\langle u_n \rangle_{n=0}^{\infty}$ is one that satisfies a recurrence of the form $f(n)u_n = g(n)u_{n-1}$ where $f,g \in \mathbb{Z}[x]$. In this paper, we consider the Membership Problem for hypergeometric sequences: given a hypergeometric sequence $\langle u_n \rangle_{n=0}^{\infty}$ and a target value $t\in \mathbb{Q}$, determine whether $u_n=t$ for some index $n$. We establish decidability of the Membership Problem under the assumption that either (i) $f$ and $g$ have distinct splitting fields or (ii) $f$ and $g$ are monic polynomials that both split over a quadratic extension of $\mathbb{Q}$. Our results are based on an analysis of the prime divisors of polynomial sequences $\langle f(n) \rangle_{n=1}^\infty$ and $\langle g(n) \rangle_{n=1}^\infty$ appearing in the recurrence relation.

cs.LO↗

arXiv2023

From Polynomial Invariants to Linear Loops

Loop invariants are software properties that hold before and after every iteration of a loop. As such, invariants provide inductive arguments that are key in automating the verification of program loops. The problem of generating loop invariants; in particular, invariants described by polynomial relations (so called polynomial invariants), is therefore one of the hardest problems in software verification. In this paper we advocate an alternative solution to invariant generation. Rather than inferring invariants from loops, we synthesise loops from invariants. As such, we generate loops that satisfy a given set of polynomials; in other words, our synthesised loops are correct by construction. Our work turns the problem of loop synthesis into a symbolic computation challenge. We employ techniques from algebraic geometry to synthesise loops whose polynomial invariants are described by pure difference binomials. We show that such complex polynomial invariants need ``only'' linear loops, opening up new venues in program optimisation. We prove the existence of non-trivial loops with linear updates for polynomial invariants generated by pure difference binomials. Importantly, we introduce an algorithmic approach that constructs linear loops from such polynomial invariants, by generating linear recurrence sequences that have specified algebraic relations among their terms.

cs.LO↗

arXiv2022

The Threshold Problem for Hypergeometric Sequences with Quadratic Parameters

Hypergeometric sequences are rational-valued sequences that satisfy first-order linear recurrence relations with polynomial coefficients; that is, $\langle u_n \rangle_{n=0}^\infty$ is hypergeometric if it satisfies a first-order linear recurrence of the form $p(n)u_{n+1} = q(n)u_{n}$ with polynomial coefficients $p,q\in\mathbb{Z}[x]$ and $u_0\in\mathbb{Q}$. In this paper, we consider the Threshold Problem for hypergeometric sequences: given a hypergeometric sequence $\langle u_n\rangle_{n=0}^\infty$ and a threshold $t\in\mathbb{Q}$, determine whether $u_n \ge t$ for each $n\in\mathbb{N}_0$. We establish decidability for the Threshold Problem under the assumption that the coefficients $p$ and $q$ are monic polynomials whose roots lie in an imaginary quadratic extension of $\mathbb{Q}$. We also establish conditional decidability results; for example, under the assumption that the coefficients $p$ and $q$ are monic polynomials whose roots lie in any number of quadratic extensions of $\mathbb{Q}$, the Threshold Problem is decidable subject to the truth of Schanuel's conjecture. Finally, we show how our approach both recovers and extends some of the recent decidability results on the Membership Problem for hypergeometric sequences with quadratic parameters.

cs.LO↗

arXiv2022

Solving Invariant Generation for Unsolvable Loops

Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem. Whilst the problem is in general undecidable, the goal is settled for restricted classes of loops. For the class of solvable loops, introduced by Kapur and Rodr\'iguez-Carbonell in 2004, one can automatically compute invariants from closed-form solutions of recurrence equations that model the loop behaviour. In this paper we establish a technique for invariant synthesis for loops that are not solvable, termed unsolvable loops. Our approach automatically partitions the program variables and identifies the so-called defective variables that characterise unsolvability. We further present a novel technique that automatically synthesises polynomials, in the defective variables, that admit closed-form solutions and thus lead to polynomial loop invariants. Our implementation and experiments demonstrate both the feasibility and applicability of our approach to both deterministic and probabilistic programs.

cs.PL↗

arXiv2022

On the Skolem Problem for Reversible Sequences

Given an integer linear recurrence sequence $\langle X_n \rangle_n$, the Skolem Problem asks to determine whether there is a natural number $n$ such that $X_n = 0$. Recent work by Lipton, Luca, Nieuwveld, Ouaknine, Purser, and Worrell proved that the Skolem Problem is decidable for a class of reversible sequences of order at most seven. Here we give an alternative proof of their result. Our novel approach employs a powerful result for Galois conjugates that lie on two concentric circles due to Dubickas and Smyth.

math.NT↗

arXiv2020

On Positivity and Minimality for Second-Order Holonomic Sequences

An infinite sequence $\langle{u_n}\rangle_{n\in\mathbb{N}}$ of real numbers is holonomic (also known as P-recursive or P-finite) if it satisfies a linear recurrence relation with polynomial coefficients. Such a sequence is said to be positive if each $u_n \geq 0$, and minimal if, given any other linearly independent sequence $\langle{v_n}\rangle_{n \in\mathbb{N}}$ satisfying the same recurrence relation, the ratio $u_n/v_n$ converges to $0$. In this paper, we focus on holonomic sequences satisfying a second-order recurrence $g_3(n)u_n = g_2(n)u_{n-1} + g_1(n)u_{n-2}$, where each coefficient $g_3, g_2,g_1 \in \mathbb{Q}[n]$ is a polynomial of degree at most $1$. We establish two main results. First, we show that deciding positivity for such sequences reduces to deciding minimality. And second, we prove that deciding minimality is equivalent to determining whether certain numerical expressions (known as periods, exponential periods, and period-like integrals) are equal to zero. Periods and related expressions are classical objects of study in algebraic geometry and number theory, and several established conjectures (notably those of Kontsevich and Zagier) imply that they have a decidable equality problem, which in turn would entail decidability of Positivity and Minimality for a large class of second-order holonomic sequences.

math.NT↗

arXiv2020

On the Skolem Problem and Prime Powers

The Skolem Problem asks, given a linear recurrence sequence $(u_n)$, whether there exists $n\in\mathbb{N}$ such that $u_n=0$. In this paper we consider the following specialisation of the problem: given in addition $c\in\mathbb{N}$, determine whether there exists $n\in\mathbb{N}$ of the form $n=lp^k$, with $k,l\leq c$ and $p$ any prime number, such that $u_n=0$.

math.NT↗

arXiv2018

Statistics in conjugacy classes in free groups

In this paper, we establish statistical results for a convex co-compact action of a free group on a CAT($-1$) space where we restrict to a non-trivial conjugacy class in the group. In particular, we obtain a central limit theorem where the variance is twice the variance that appears when we do not make this restriction.

math.DS↗

arXiv2016

Orbit counting in conjugacy classes for free groups acting on trees

In this paper we study the action of the fundamental group of a finite metric graph on its universal covering tree. We assume the graph is finite, connected and the degree of each vertex is at least three. Further, we assume an irrationality condition on the edge lengths. We obtain an asymptotic for the number of elements in a fixed conjugacy class for which the associated displacement of a given base vertex in the universal covering tree is at most $T$. Under a mild extra assumption we also obtain a polynomial error term.

math.DS↗