arXiv subjects

Alex Rice

Publications and source records attributed to Alex Rice.

At least 19 recordsLinked to original sources

arXiv2026

A Dynamic Intermediate Representation for Hybrid Quantum-Classical Programs

Quantum compilers typically follow the circuit model, representing programs as fixed sequences of gates. This static view breaks down in hybrid quantum-classical applications, where gate choices depend on runtime data or measurement results. We introduce a new Intermediate Representation (IR) that elevates gates to first-class values, enabling their dynamic creation, composition, and control. This unified representation allows classical computation to steer quantum behaviour, capturing phenomena including stochastic gate selection, adaptive error correction, and measurement-driven computation within a single framework. Case studies in noise modelling, randomised compilation, error correction, and measurement-based quantum computing show that our IR expresses these programs compactly and supports optimisations that were not possible in the circuit model. Evaluation on a benchmark suite of hybrid quantum-classical programs indicates that our IR represents programs compactly and facilitates compiler analysis and transformation.

cs.PL↗

arXiv2026

Quantum Orchestras: a Concrete Semantics for Recursive Hybrid Programs

Many production quantum programming languages represent hybrid quantum computations by extending a classical base language with a quantum effect, where qubits are addressed by reference, and quantum operations are understood to mutate some external quantum state. However, the semantics of this view of quantum computation remains underdeveloped, especially when the language allows mid-circuit measurements and non-termination. In this work, we provide a general method for building denotational semantics for such languages, by defining the quantum orchestra monad, which precisely captures this style of quantum effect. The monad has a concrete presentation, being based on the formalism of quantum instruments, a common tool in quantum information theory for capturing the action of a quantum process along with its classical outcomes. It acts on the category DCPO, and so enables the interpretation of divergent hybrid programs. The quantum orchestra monad serves as a natural extension of both the classical state monad and the probabilistic powerdomain monad. We investigate some of the subtleties present when trying to na\"ively extend these definitions to the quantum non-commutative case.

cs.PL↗

arXiv2026

Composing Quantum Instruments

We study the composition of classically-controlled quantum instruments--the natural quantum analogue of Markov kernels. Classically, Markov kernels compose by integrating one kernel against another. Defining this composition for quantum instruments with continuous outcomes requires an integral of quantum channel-valued functions with respect to a quantum instrument. We construct this integral in the Heisenberg picture using the Okamura-Ozawa normal extension to a von Neumann tensor product. This integral recovers the expected finite formula, preserves normal complete positivity and subunitality, and provides the multiplication for a monad governing the composition of quantum instruments. As an immediate consequence, we identify the category of quantum Markov kernels as the Kleisli category of this monad.

quant-ph↗

arXiv2026

The sum-product problem for small sets II

We establish that every set of $k=10$ natural numbers determines at least $30$ distinct pairwise sums or at least $30$ distinct pairwise products, as well as the analogous result for $k=11$ and at least $34$ sums/products, with sharpness uniquely (up to scaling) exhibited by $\{1, 2, 3, 4, 6, 8, 9, 12, 16, 18\}$ and $\{1, 2, 3, 4, 6, 8, 9, 12, 16, 18, 24\}$, respectively. This extends previous work of the fifth author with Clevenger, Havard, Heard, Lott, and Wilson, which established the corresponding thresholds for $k\leq 9$. Included is a classification result for sets of $10$ real numbers (resp. positive real numbers) determining at most $29$ pairwise sums (resp. pairwise products) that do not contain $8$ elements of any single arithmetic progression (resp. geometric progression), as well as some observations controlling additive quadruples in small subsets of two-dimensional generalized geometric progressions.

math.CO↗

arXiv2025

Notes and computations on forbidden differences

We explore from several perspectives the following question: given $X\subseteq \mathbb{Z}$ and $N\in \mathbb{N}$, what is the maximum size $D(X,N)$ of $A\subseteq \{1,2,\dots,N\}$ before $A$ is forced to contain two distinct elements that differ by an element of $X$? The set of forbidden differences, $X$, is called \textit{intersective} if $D(X,N)=o(N)$, with the most well-studied examples being $X=S=\{n^2: n\in \mathbb{N}\}$ and $X=\mathcal{P}-1=\{p-1: p\text{ prime}\}$. In addition to some new results, including exact formulas and estimates for $D(X,N)$ in some non-intersective cases like $X=\mathcal{P}$ and $X=S+k$, $k\in \mathbb{N}$, we also provide a comprehensive survey of known bounds and extensive computational data. In particular, we utilize an existing algorithm for finding maximum cliques in graphs to determine $D(S,N)$ for $N\leq 300$ and $D(\mathcal{P}-1,N)$ for $N\leq 500$. None of these exact values appear previously in the literature.

math.NT↗

arXiv2025

Quantum Circuits Are Just a Phase

Quantum programs today are written at a low level of abstraction - quantum circuits akin to assembly languages - and the unitary parts of even advanced quantum programming languages essentially function as circuit description languages. This state of affairs impedes scalability, clarity, and support for higher-level reasoning. More abstract and expressive quantum programming constructs are needed. To this end, we introduce a simple syntax for generating unitaries from "just a phase"; we combine a (global) phase operation that captures phase shifts with a quantum analogue of the "if let" construct that captures subspace selection via pattern matching. This minimal language lifts the focus from gates to eigendecomposition, conjugation, and controlled unitaries; common building blocks in quantum algorithm design. We demonstrate several aspects of the expressive power of our language in several ways. Firstly, we establish that our representation is universal by deriving a universal quantum gate set. Secondly, we show that important quantum algorithms can be expressed naturally and concisely, including Grover's search algorithm, Hamiltonian simulation, Quantum Fourier Transform, Quantum Signal Processing, and the Quantum Eigenvalue Transformation. Furthermore, we give clean denotational semantics grounded in categorical quantum mechanics. Finally, we implement a prototype compiler that efficiently translates terms of our language to quantum circuits, and prove that it is sound with respect to these semantics. Collectively, these contributions show that this construct offers a principled and practical step toward more abstract and structured quantum programming.

cs.PL↗

arXiv2025

A type-theoretic approach to semistrict higher categories

Weak $\infty$-categories are known to be more expressive than their strict counterparts, but are more difficult to work with, as constructions in such a category involve the manipulation of explicit coherence data. This motivates the search for definitions of semistrict $\infty$-categories, where some, but not all, of the operations have been strictified. We introduce a general framework for adding definitional equality to the type theory $\mathsf{Catt}$, a type theory whose models correspond to globular weak $\infty$-categories, which was introduced by Finster and Mimram. Adding equality to this theory causes the models to exhibit semistrict behaviour, trivialising some operations while leaving others weak. The framework consists of a generalisation of $\mathsf{Catt}$ extended with an equality relation generated by an arbitrary set of equality rules $\mathcal{R}$, which we name $\mathsf{Catt}_{\mathcal{R}}$. We study this framework in detail, formalising much of its metatheory in the proof assistant Agda, and studying how certain operations of $\mathsf{Catt}$ behave in the presence of definitional equality. We use this framework to introduce two type theories, $\mathsf{Catt}_{\mathsf{su}}$ and $\mathsf{Catt}_{\mathsf{sua}}$, which are instances of this general framework. Further, we provide terminating and confluent reduction systems that generate the equality of both systems. We therefore prove that the equality, and hence typechecking, of both theories is decidable. This is used to give an implementation of these type theories, which uses an approach inspired by normalisation by evaluation to efficiently find normal forms for terms. We further introduce a bidirectional typechecking algorithm used by the implementation which allows for terms to be defined in a convenient syntax where many arguments can be left implicit.

cs.LO↗

arXiv2024

Determinants of Seidel Tournament Matrices

The Seidel matrix of a tournament on $n$ players is an $n\times n$ skew-symmetric matrix with entries in $\{0, 1, -1\}$ that encapsulates the outcomes of the games in the given tournament. It is known that the determinant of an $n\times n$ Seidel matrix is $0$ if $n$ is odd, and is an odd perfect square if $n$ is even. This leads to the study of the set \[ \mathcal{D}(n)= \{ \sqrt{\det S}: \mbox{ $S$ is an $n\times n$ Seidel matrix}\}. \] This paper studies various questions about $\mathcal{D}(n)$. It is shown that $\mathcal{D}(n)$ is a proper subset of $\mathcal{D}(n+2)$ for every positive even integer, and every odd integer in the interval $[1, 1+n^2/2]$ is in $\mathcal{D}(n)$ for $n$ even. The expected value and variance of $\det S$ over the $n\times n$ Seidel matrices chosen uniformly at random is determined, and upper bounds on $\max \mathcal{D}(n)$ are given, and related to the Hadamard conjecture. Finally, it is shown that for infinitely many $n$, $\mathcal{D}(n)$ contains a gap (that is, there are odd integers $k<\ell <m$ such that $k, m \in \mathcal{D}(n)$ but $\ell \notin \mathcal{D}(n)$) and several properties of the characteristic polynomials of Seidel matrices are established.

math.CO↗

arXiv2024

The Furstenberg-S\'ark\"ozy theorem for polynomials in one or more prime variables

We establish upper bounds on the size of the largest subset of $\{1,2,\dots,N\}$ lacking nonzero differences of the form $h(p_1,\dots,p_{\ell})$, where $h\in \mathbb{Z}[x_1,\dots,x_{\ell}]$ is a fixed polynomial satisfying appropriate conditions and $p_1,\dots,p_{\ell}$ are prime. The bounds are of the same type as the best-known analogs for unrestricted integer inputs, due to Bloom-Maynard and Arala for $\ell=1$, and to the authors for $\ell \geq 2$.

math.NT↗

arXiv2023

The sum-product problem for small sets

For $A\subseteq \mathbb{R}$, let $A+A=\{a+b: a,b\in A\}$ and $AA=\{ab: a,b\in A\}$. For $k\in \mathbb{N}$, let $SP(k)$ denote the minimum value of $\max\{|A+A|, |AA|\}$ over all $A\subseteq \mathbb{N}$ with $|A|=k$. Here we establish $SP(k)=3k-3$ for $2\leq k \leq 7$, the $k=7$ case achieved for example by $\{1,2,3,4,6,8,12\}$, while $SP(k)=3k-2$ for $k=8,9$, the $k=9$ case achieved for example by $\{1,2,3,4,6,8,9,12,16\}$. For $4\leq k \leq 7$, we provide two proofs using different applications of Freiman's $3k-4$ theorem; one of the proofs includes extensive case analysis on the product sets of $k$-element subsets of $(2k-3)$-term arithmetic progressions. For $k=8,9$, we apply Freiman's $3k-3$ theorem for product sets, and investigate the sumset of the union of two geometric progressions with the same common ratio $r>1$, with separate treatments of the overlapping cases $r\neq 2$ and $r\geq 2$.

math.CO↗

arXiv2023

A Syntax for Strictly Associative and Unital $\infty$-Categories

We present the first definition of strictly associative and unital $\infty$-category. Our proposal takes the form of a type theory whose terms describe the operations of such structures, and whose definitional equality relation enforces desired strictness conditions. The key technical device is a new computation rule in the definitional equality of the theory, which we call insertion, defined in terms of a universal property. On terms for which it is defined, this operation "inserts" one of the arguments of a substituted coherence into the coherence itself, appropriately modifying the pasting diagram and result type, and simplifying the syntax in the process. We generate an equational theory from this reduction relation and we study its properties in detail, showing that it yields a decision procedure for equality. Expressed as a type theory, our model is well-adapted for generating and verifying efficient proofs of higher categorical statements. We illustrate this via an OCaml implementation, and give a number of examples, including a short encoding of the syllepsis, a 5-dimensional homotopy that plays an important role in the homotopy groups of spheres.

math.CT↗

arXiv2022

Computations and observations on congruence covering systems

A $\textit{covering system}$ is a collection of integer congruences such that every integer satisfies at least one congruence in the collection. A covering system is called $\textit{distinct}$ if all of its moduli are distinct. An expansive literature has developed on covering systems since their introduction by Erd\H{o}s. Here we provide a full classification of distinct covering systems with at most ten moduli, which we group together based on two forms of equivalence. As a consequence, we determine the minimum cardinality of a distinct covering system with all moduli exceeding $2$, which is $11$.

math.NT↗

arXiv2021

Schur's theorem in integer lattices

A standard proof of Schur's Theorem yields that any $r$-coloring of $\{1,2,\dots,R_r-1\}$ yields a monochromatic solution to $x+y=z$, where $R_r$ is the classical $r$-color Ramsey number, the minimum $N$ such that any $r$-coloring of a complete graph on $N$ vertices yields a monochromatic triangle. We explore generalizations and modifications of this result in higher dimensional integer lattices, showing in particular that if $k\geq d+1$, then any $r$-coloring of $\{1,2,\dots,R_r(k)^d-1\}^d$ yields a monochromatic solution to $x_1+\cdots+x_{k-1}=x_k$ with $\{x_1,\dots,x_d\}$ linearly independent, where $R_r(k)$ is the analogous Ramsey number in which triangles are replaced by complete graphs on $k$ vertices. We also obtain computational results and examples in the case $d=2$, $k=3$, and $r\in\{2,3,4\}$.

math.CO↗

arXiv2021

Enumerating Independent Linear Inferences

A linear inference is a valid inequality of Boolean algebra in which each variable occurs at most once on each side. In this work we leverage recently developed graphical representations of linear formulae to build an implementation that is capable of more efficiently searching for switch-medial-independent inferences. We use it to find four `minimal' 8-variable independent inferences and also prove that no smaller ones exist; in contrast, a previous approach based directly on formulae reached computational limits already at 7 variables. Two of these new inferences derive some previously found independent linear inferences. The other two (which are dual) exhibit structure seemingly beyond the scope of previous approaches we are aware of; in particular, their existence contradicts a conjecture of Das and Strassburger. We were also able to identify 10 minimal 9-variable linear inferences independent of all the aforementioned inferences, comprising 5 dual pairs, and present applications of our implementation to recent `graph logics'.

cs.LO↗

arXiv2021

A Type Theory for Strictly Associative Infinity Categories

Many definitions of weak and strict $\infty$-categories have been proposed. In this paper we present a definition for $\infty$-categories with strict associators, but which is otherwise fully weak. Our approach is based on the existing type theory Catt, whose models are known to correspond to weak $\infty$-categories. We add a definitional equality relation to this theory which identifies terms with the same associativity structure, yielding a new type theory Catt$_{sa}$, for strictly associative $\infty$-categories. We also provide a reduction relation which generates definitional equality, and show it is confluent and terminating, giving an algorithm for deciding equality of terms, and making typechecking decidable. Our key contribution, on which our reduction is based, is an operation on terms which we call insertion. This has a direct geometrical interpretation, allowing a subterm to be inserted into the head of the term, flatting its syntactic structure. We describe this operation combinatorially in terms of pasting diagrams, and also show can be characterized as a pushout of contexts. This allows reasoning about insertion using just its universal property.

math.CT↗

arXiv2021

The pigenhole principle and multicolor Ramsey numbers

For integers $k,r\geq 2$, the diagonal Ramsey number $R_r(k)$ is the minimum $N\in\mathbb{N}$ such that every $r$-coloring of the edges of a complete graph on $N$ vertices yields on a monochromatic subgraph on $k$ vertices. Here we make a careful effort of extracting explicit upper bounds for $R_r(k)$ from the pigeonhole principle alone. Our main term improves on previously documented explicit bounds for $r\geq 3$, and we also consider an often ignored secondary term, which allows us to subtract a uniformly bounded below positive proportion of the main term. Asymptotically, we give a self-contained proof that $R_r(k)\leq \left(\frac{3+e}{2}\right)\frac{(r(k-2))!}{((k-2)!)^r}(1+o_{r\to \infty}(1)),$ and we conclude by noting that our methods combine with previous estimates on $R_r(3)$ to improve the constant $\frac{3+e}{2}$ to $\frac{3+e}{2}-\frac{d}{48}$, where $d=66-R_4(3)\geq 4$. We also compare our formulas, and previously documented formulas, to some collected numerical data.

math.CO↗

arXiv2020

Coinductive Invertibility in Higher Categories

Invertibility is an important concept in category theory. In higher category theory, it becomes less obvious what the correct notion of invertibility is, as extra coherence conditions can become necessary for invertible structures to have desirable properties. We define some properties we expect to hold in any reasonable definition of a weak $\omega$-category. With these properties we define three notions of invertibility inspired by homotopy type theory. These are quasi-invertibility, where a two sided inverse is required, bi-invertibility, where a separate left and right inverse is given, and half-adjoint inverse, which is a quasi-inverse with an extra coherence condition. These definitions take the form of coinductive data structures. Using coinductive proofs we are able to show that these three notions are all equivalent in that given any one of these invertibility structures, the others can be obtained. The methods used to do this are generic and it is expected that the results should be applicable to any reasonable model of higher category theory. Many of the results of the paper have been formalised in Agda using coinductive records and the machinery of sized types.

math.CT↗

arXiv2020

A Type Theory for Strictly Unital $\infty$-Categories

We use type-theoretic techniques to present an algebraic theory of $\infty$-categories with strict units. Starting with a known type-theoretic presentation of fully weak $\infty$-categories, in which terms denote valid operations, we extend the theory with a non-trivial definitional equality. This forces some operations to coincide strictly in any model, yielding the strict unit behaviour. We make a detailed investigation of the meta-theoretic properties of this theory. We give a reduction relation that generates definitional equality, and prove that it is confluent and terminating, thus yielding the first decision procedure for equality in a strictly-unital setting. Moreover, we show that our definitional equality relation identifies all terms in a disc context, providing a point comparison with a previously proposed definition of strictly unital $\infty$-category. We also prove a conservativity result, showing that every operation of the strictly unital theory indeed arises from a valid operation in the fully weak theory. From this, we infer that strict unitality is a property of an $\infty$-category rather than additional structure.

cs.LO↗