arXiv subjects

Renaud Vilmart

Publications and source records attributed to Renaud Vilmart.

At least 19 recordsLinked to original sources

arXiv2026

Minimality of the Pure Qubit ZX Calculus

The ZX calculus is a graphical language for reasoning about quantum processes. In this paper, we develop a minimal pure-qubit ZX calculus based on the work of Vilmart [arXiv:1812.09114], Backens, Perdrix, and Wang [arXiv:1709.08903], and Stoltz [arXiv:2606.12383]. This resolves a problem that has remained open for nearly a decade, since completeness was first proved. Specifically, we show that $(I_r)$ is derivable and establish the necessity of $(B)$ and $(I_g)$, yielding two complete and minimal rulesets.

quant-ph↗

arXiv2026

Intuitionistic Unitary Linear Logic: A Proof-Theoretical Approach to Purely Quantum Higher-Order

Although the circuit model for quantum computation is well established, it is incapable of representing non-causal higher-order quantum processes such as the quantum switch. If several models of non-causal quantum computation have been considered in the literature, the approaches have so far only been focusing on the physicality of such processes, using matrices and other techniques from linear algebra. If these approaches are expressive, they however only provide a static and monolithic understanding of these processes. In this article, we propose a new formalism for non-causal, higher-order quantum processes. Based on a Curry-Howard interpetation, our proposal offers a computational interpretation that is both compositional and modular. In particular, we present Intuitionistic Unitary Linear Logic (IULL), a logic based on linear logic focusing on conservation of unitarity for higher order terms. We prove the coherence of IULLL, its completeness with regard to unitaries, and the admissibility of its cut rules. We finally discuss the validity of our approach by revisiting known non-causal quantum processes with IULL.

cs.LO↗

arXiv2026

A Unique Normal Form for Tensor Trains over Arbitrary Fields

Tensor trains (or Matrix-Product States) are a data structure used in many fields of computer science and physics. They were recently shown to generalise binary decision diagrams when used over the 2-element Galois field, prompting the question of their reducibility in such a context, when the standard approach, over real or complex number, is not amenable to finite fields. We provide here a unique normal form and associated polynomial-time reduction strategy for tensor trains over arbitrary fields. We also show how to directly extract a normal form out of a full tensor, how to get the leading index and value of a normal form, and an upper bound on the size of a fully-reduced tensor train relative to a naive storage of the full tensor. On the one hand, this work strengthens the use of tensor trains as a relevant formal tool. On the other hand, from the perspective of tensor networks, it extends the formalism to more general settings than the well-studied real and complex fields, and crucially provides the first tensor train form with the uniqueness property.

cs.DS↗

arXiv2026

Resource-Efficient Synthesis of Sparse Quantum States

Preparing a quantum circuit that implements a given sparse state is an important building block that is necessary for many different quantum algorithms. In the context of fault-tolerant quantum computing, the so-called non-Clifford gates are much more expensive to perform than the Clifford ones. We hence provide an algorithm for synthesizing sparse quantum states with a special care for quantum resources. The circuit depth, ancilla count, and crucially non-Clifford count of the circuit produced by the algorithm are all linear in the sparsity when access to arbitrary-angled rotations is given. When compiled down to the standard Clifford+T gate set, several constructions can be given for increasingly better T-count and depth at the expense of a larger number of ancillae. The most optimised construction for T-count reaches $\mathcal O\left(\sqrt{s\log_2(1/ε)}+\log_2(1/ε)\right)$ T gates for error $ε$, a result on par with an optimal construction for full state preparation by Gosset et al. The constructions are broken into two parts, one that synthesises a generalized W-state, well studied in the literature; and the second which is a classical reversible circuit implementing a permutation that maps the basis states of the W-state to those of the target sparse quantum state. We reduce this problem to the diagonalization of a binary matrix, using a specific set of elementary matrix operations corresponding to the classical reversible gates. We then solve this problem using a new version of Gauss-Jordan elimination, that minimizes the circuit complexities including circuit depth using parallel elimination steps. When the circuit is applied in one direction, we notice that all occurrences of (the expensive) Toffoli gates can all be replaced by adaptive Clifford circuits, leading to a better non-Clifford count.

quant-ph↗

arXiv2025

The Tensor-Plus Calculus

We propose a graphical language that accommodates two monoidal structures: a multiplicative one for pairing and an additional one for branching. In this colored PROP, whether wires in parallel are linked through the multiplicative structure or the additive structure is implicit and determined contextually rather than explicitly through tapes, world annotations, or other techniques, as is usually the case in the literature. The diagrams are used as parameter elements of a commutative semiring, whose choice is determined by the kind of computation we want to model, such as non-deterministic, probabilistic, or quantum. Given such a semiring, we provide a categorical semantics of diagrams and show the language as universal for it. We also provide an equational theory to identify diagrams that share the same semantics and show that the theory is sound and complete and captures semantical equivalence. In categorical terms, we design an internal language for semiadditive categories (C,+,0) with a symmetric monoidal structure (C,x,1) distributive over it, and such that the homset C(1,1) is isomorphic to a given commutative semiring, e.g., the semiring of non-negative real numbers for the probabilistic case.

cs.LO↗

arXiv2025

The decohered ZX-calculus

The discard ZX-calculus is known to be complete and universal for mixed-state quantum mechanics, allowing for both quantum and classical processes. However, if the quantum aspects of ZX-calculus have been explored in depth, little work has been done on the classical side. In this paper, we investigate a fragment of discard ZX-calculus obtained by decohering the usual generators of ZX-calculus. We show that this calculus is universal and complete for affinely supported probability distributions over $\mathbb{F}_{2}^{n}$. To do so, we exhibit a normal form, mixing ideas from the graphical linear algebra program and diagrammatic Fourier transforms. Our results both clarify how to handle hybrid classical-quantum processes in the discard ZX-calculus and pave the way to the picturing of more general random variables and probabilistic processes.

quant-ph↗

arXiv2025

The Many-Worlds Calculus

In this paper, we explore the interaction between two monoidal structures: a multiplicative one, for the encoding of pairing, and an additive one, for the encoding of choice. We propose a colored PROP to model computation in this framework, where the choice is parameterized by an algebraic side effect: the model can support regular tests, probabilistic and non-deterministic branching, as well as quantum branching, i.e. superposition. The graphical language comes equipped with a denotational semantics based on linear applications, and an equational theory. We prove the language to be universal, and the equational theory to be complete with respect to this semantics.

cs.LO↗

arXiv2024

Minimality in Finite-Dimensional ZW-Calculi

The ZW-calculus is a graphical language capable of representing 2-dimensional quantum systems (qubit) through its diagrams, and manipulating them through its equational theory. We extend the formalism to accommodate finite dimensional Hilbert spaces beyond qubit systems. First we define a qu$d$it version of the language, where all systems have the same arbitrary finite dimension $d$, and show that the provided equational theory is both complete -- i.e. semantical equivalence is entirely captured by the equations -- and minimal -- i.e. none of the equations are consequences of the others. We then extend the graphical language further to allow for mixed-dimensional systems. We again show the completeness and minimality of the provided equational theory.

quant-ph↗

arXiv2024

Double-Logarithmic Depth Block-Encodings of Simple Finite Difference Method's Matrices

Solving differential equations is one of the most computationally expensive problems in classical computing, occupying the vast majority of high-performance computing resources devoted towards practical applications in various fields of science and engineering. Despite recent progress made in the field of quantum computing and quantum algorithms, its end-to-end application towards practical realization still remains unattainable. In this article, we tackle one of the primary obstacles towards this ultimate objective, specifically the encoding of matrices derived via finite difference method solving Poisson partial differential equations in simple boundary-value problems. To that end, we propose a novel methodology called block-diagonalization, which provides a common decomposition form for our matrices, and similarly a common procedure for block-encoding these matrices inside a unitary operator of a quantum circuit. The depth of these circuits is double-logarithmic in the matrix size, which is an exponential improvement over existing quantum methods and a superexponential improvement over existing classical methods. These improvements come at the price of a constant multiplicative overhead on the number of qubits and the number of gates. Combined with quantum linear solver algorithms, we can utilize these quantum circuits to produce a quantum state representation of the solution to the Poisson partial differential equations and their boundary-value problems.

quant-ph↗

arXiv2024

Rewriting and Completeness of Sum-Over-Paths in Dyadic Fragments of Quantum Computing

The "Sum-Over-Paths" formalism is a way to symbolically manipulate linear maps that describe quantum systems, and is a tool that is used in formal verification of such systems. We give here a new set of rewrite rules for the formalism, and show that it is complete for "Toffoli-Hadamard", the simplest approximately universal fragment of quantum mechanics. We show that the rewriting is terminating, but not confluent (which is expected from the universality of the fragment). We do so using the connection between Sum-over-Paths and graphical language ZH-calculus, and also show how the axiomatisation translates into the latter. We provide generalisations of the presented rewrite rules, that can prove useful when trying to reduce terms in practice, and we show how to graphically make sense of these new rules. We show how to enrich the rewrite system to reach completeness for the dyadic fragments of quantum computation, used in particular in the Quantum Fourier Transform, and obtained by adding phase gates with dyadic multiples of $π$ to the Toffoli-Hadamard gate-set. Finally, we show how to perform sums and concatenation of arbitrary terms, something which is not native in a system designed for analysing gate-based quantum computation, but necessary when considering Hamiltonian-based quantum computation.

cs.LO↗

arXiv2023

Quantum Circuit Completeness: Extensions and Simplifications

Although quantum circuits have been ubiquitous for decades in quantum computing, the first complete equational theory for quantum circuits has only recently been introduced. Completeness guarantees that any true equation on quantum circuits can be derived from the equational theory. We improve this completeness result in two ways: (i) We simplify the equational theory by proving that several rules can be derived from the remaining ones. In particular, two out of the three most intricate rules are removed, the third one being slightly simplified. (ii) The complete equational theory can be extended to quantum circuits with ancillae or qubit discarding, to represent respectively quantum computations using an additional workspace, and hybrid quantum computations. We show that the remaining intricate rule can be greatly simplified in these more expressive settings, leading to equational theories where all equations act on a bounded number of qubits. The development of simple and complete equational theories for expressive quantum circuit models opens new avenues for reasoning about quantum circuits. It provides strong formal foundations for various compiling tasks such as circuit optimisation, hardware constraint satisfaction and verification.

quant-ph↗

arXiv2023

Complete Graphical Language for Hermiticity-Preserving Superoperators

Universal and complete graphical languages have been successfully designed for pure state quantum mechanics, corresponding to linear maps between Hilbert spaces, and mixed states quantum mechanics, corresponding to completely positive superoperators. In this paper, we go one step further and present a universal and complete graphical language for Hermiticity-preserving superoperators. Such a language opens the possibility of diagrammatic compositional investigations of antilinear transformations featured in various physical situations, such as the Choi-Jamiołkowski isomorphism, spin-flip, or entanglement witnesses. Our construction relies on an extension of the ZW-calculus exhibiting a normal form for Hermitian matrices.

quant-ph↗

arXiv2023

Compositionality of planar perfect matchings

We exhibit a strong connection between the matchgate formalism introduced by Valiant and the ZW-calculus of Coecke and Kissinger. This connection provides a natural compositional framework for matchgate theory as well as a direct combinatorial interpretation of the diagrams of ZW-calculus through the perfect matchings of their underlying graphs. We identify a precise fragment of ZW-calculus, the planar W-calculus, that we prove to be complete and universal for matchgates, that are linear maps satisfying the matchgate identities. Computing scalars of the planar W-calculus corresponds to counting perfect matchings of planar graphs, and so can be carried in polynomial time using the FKT algorithm, making the planar W-calculus an efficiently simulable fragment of the ZW-calculus, in a similar way that the Clifford fragment is for ZX-calculus. This work opens new directions for the investigation of the combinatorial properties of ZW-calculus as well as the study of perfect matching counting through compositional diagrammatical technics.

quant-ph↗

arXiv2022

Completeness of Sum-Over-Paths for Toffoli-Hadamard and the Dyadic Fragments of Quantum Computation

quant-ph↗

arXiv2022

Geometry of Interaction for ZX-Diagrams

ZX-Calculus is a versatile graphical language for quantum computation equipped with an equational theory. Getting inspiration from Geometry of Interaction, in this paper we propose a token-machine-based asynchronous model of both pure ZX-Calculus and its extension to mixed processes. We also show how to connect this new semantics to the usual standard interpretation of ZX-diagrams. This model allows us to have a new look at what ZX-diagrams compute, and give a more local, operational view of the semantics of ZX-diagrams.

cs.LO↗

arXiv2022

Formal Methods for Quantum Programs: A Survey

While recent progress in quantum hardware open the door for significant speedup in certain key areas (cryptography, biology, chemistry, optimization, machine learning, etc), quantum algorithms are still hard to implement right, and the validation of such quantum programs is achallenge. Moreover, importing the testing and debugging practices at use in classical programming is extremely difficult in the quantum case, due to the destructive aspect of quantum measurement. As an alternative strategy, formal methods are prone to play a decisive role in the emerging field of quantum software. Recent works initiate solutions for problems occurring at every stage of the development process: high-level program design, implementation, compilation, etc. We review the induced challenges for an efficient use of formal methods in quantum computing and the current most promising research directions.

cs.PL↗

arXiv2022

Classical simulation of quantum circuits with partial and graphical stabiliser decompositions

Recent developments in classical simulation of quantum circuits make use of clever decompositions of chunks of magic states into sums of efficiently simulable stabiliser states. We show here how, by considering certain non-stabiliser entangled states which have more favourable decompositions, we can speed up these simulations. This is made possible by using the ZX-calculus, which allows us to easily find instances of these entangled states in the simplified diagram representing the quantum circuit to be simulated. We additionally find a new technique of partial stabiliser decompositions that allow us to trade magic states for stabiliser terms. With this technique we require only $2^{αt}$ stabiliser terms, where $α\approx 0.396$, to simulate a circuit with T-count $t$. This matches the $α$ found by Qassim et al., but whereas they only get this scaling in the asymptotic limit, ours applies for a circuit of any size. Our method builds upon a recently proposed scheme for simulation combining stabiliser decompositions and optimisation strategies implemented in the software QuiZX. With our techniques we manage to reliably simulate 50-qubit 1400 T-count hidden shift circuits in a couple of minutes on a consumer laptop.

quant-ph↗

arXiv2021

Quantum Multiple-Valued Decision Diagrams in Graphical Calculi

Graphical calculi such as the ZH-calculus are powerful tools in the study and analysis of quantum processes, with links to other models of quantum computation such as quantum circuits, measurement-based computing, etc. A somewhat compact but systematic way to describe a quantum process is through the use of quantum multiple-valued decision diagrams (QMDDs), which have already been used for the synthesis of quantum circuits as well as for verification. We show in this paper how to turn a QMDD into an equivalent ZH-diagram, and vice-versa, and show how reducing a QMDD translates in the ZH-Calculus, hence allowing tools from one formalism to be used into the other.

quant-ph↗