Efficient methods for the simulation of quantum circuits on classical computers are crucial for their analysis due to the exponential growth of the problem size with the number of qubits. Here we study lumping methods based on bisimulation, an established class of techniques that has been proven successful for (classic) stochastic and deterministic systems such as Markov chains and ordinary differential equations. Forward constrained bisimulation yields a lower-dimensional model which exactly preserves quantum measurements projected on a linear subspace of interest. Backward constrained bisimulation gives a reduction that is valid on a subspace containing the circuit input, from which the circuit result can be fully recovered. We provide an algorithm to compute the constraint bisimulations yielding coarsest reductions in both cases, using a duality result relating the two notions. As applications, we provide theoretical bounds on the size of the reduced state space for well-known quantum algorithms for search, optimization, and factorization. Using a prototype implementation, we report significant reductions on a set of benchmarks. In particular, we show that constrained bisimulation can boost decision-diagram-based quantum circuit simulation by several orders of magnitude, allowing thus for substantial synergy effects.

The Factorial Basis method, initially designed for quasi-triangular, shift-compatible factorial bases, provides solutions to linear recurrence equations in the form of definite-sums. This paper extends the Factorial Basis method to its q-analog, enabling its application in q-calculus. We demonstrate the adaptation of the method to q-sequences and its utility in the realm of q-combinatorics. The extended technique is employed to automatically prove established identities and unveil novel ones, particularly some associated with the Rogers-Ramanujan identities.

Abstract Efficient methods for the simulation of quantum circuits on classic computers are crucial for their analysis due to the exponential growth of the problem size with the number of qubits. Here we study lumping methods based on bisimulation, an established class of techniques that has been proven successful for (classic) stochastic and deterministic systems such as Markov chains and ordinary differential equations. Forward constrained bisimulation yields a lower-dimensional model which exactly preserves quantum measurements projected on a linear subspace of interest. Backward constrained bisimulation gives a reduction that is valid on a subspace containing the circuit input, from which the circuit result can be fully recovered. We provide an algorithm to compute the constraint bisimulations yielding coarsest reductions in both cases, using a duality result relating the two notions. As applications, we provide theoretical bounds on the size of the reduced state space for well-known quantum algorithms for search, optimization, and factorization. Using a prototype implementation, we report significant reductions on a set of benchmarks. Furthermore, we show that constraint bisimulation complements state-of-the-art methods for the simulation of quantum circuits based on decision diagrams.

D-finite functions satisfy linear differential equations with polynomial coefficients. The solutions to this type of equations may have singularities determined by the zeros of their leading coefficient. There are algorithms to desingularize the equations, i.e., remove singularities from the equation that do not appear in its solutions. However, classical computations of closure properties (such as addition, multiplication, etc.) with D-finite functions return equations with extra zeros in the leading coefficient. In this paper we present theory and algorithms based on linear algebra to control the leading coefficients when computing these closure properties and we also extend this theory to the more general class of differentially definable functions.

Holonomic sequences are widely studied as many objects interesting to mathematicians and computer scientists are in this class. In the univariate case, these are the sequences satisfying linear recurrences with polynomial coefficients and also referred to as D-finite sequences. A subclass are C-finite sequences satisfying a linear recurrence with constant coefficients.

Many special functions as well as generating functions of combinatorial sequences that arise in applications are D-finite, i.e., they satisfy a linear differential equation with polynomial coefficients. These functions have been studied for centuries and over the past decades various computer algebra methods have been developed and implemented for D-finite functions. Recently, we have extended this notion to DD-finite functions (functions satisfying linear differential equations with D-finite functions coefficients). Numerous identities for D-finite functions can be proven automatically using closure properties. These closure properties can be shown to hold for DD-finite functions as well. In this paper, we present the algorithmic aspect of these closure properties, discuss issues related to implementation and give several examples.