Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

arXiv:2607.20170

Quantum Term Rewrite Systems: Applications to Complexity Analysis

Kostia Chardonnet, Emmanuel Hainry F, Romain Péchoux, Thomas Vinet

Published Jul 22, 2026• 0 citations
arXivHTMLPDF

Abstract

Term Rewrite Systems (TRS) is a computational model offering a level of abstraction well-suited towards static analysis, e.g., termination or complexity analyses. In this paper, we introduce Quantum Term Rewrite Systems (QTRS), an extension of TRS to quantum computing, thus allowing to benefit from quantum advantage while being able to certify the complexity. We ensure that QTRS correspond to physically realizable processes and adapt techniques to obtain termination certificates or generic bounds on the reduction length. We delineate a class of terminating QTRS that can be compiled to uniform families of quantum circuits of size bounded by the reduction length. Conversely, this class is universal for quantum circuits. In particular, we show a characterization of the class of functions computable in quantum polynomial time, known as $\mathtt{FBQP}$.

DOI
10.48550/arxiv.2607.20170

Related papers

A Programming Language Characterizing Quantum Polynomial Time

Emmanuel Hainry F, Romain Péchoux, Mário Silva

Abstract We introduce a first-order quantum programming language, named foq , whose terminating programs are reversible. We restrict foq to a strict and tractable subset, named pfoq , of terminating programs with bounded width, that provides a first programming language-based characterization of the quantum complexity class fbqp . We finally present a tractable semantics-preserving algorithm compiling a pfoq program to a quantum circuit of size polynomial in the number of input qubits.

Lecture notes in computer science•Jan 1, 2023•6 citations

A programming language characterizing quantum polynomial time

Emmanuel Hainry F, Romain Péchoux, Mário Silva

We introduce a first-order quantum programming language, named FOQ, whose terminating programs are reversible. We restrict FOQ to a strict and tractable subset, named PFOQ, of terminating programs with bounded width, that provides a first programming language-based characterization of the quantum complexity class FBQP. Finally, we present a tractable semantics-preserving algorithm compiling a PFOQ program to a quantum circuit of size polynomial in the number of input qubits.

arXiv:2212.06656•Dec 13, 2022•0 citations

Quantum Programming in Polylogarithmic Time

Ferrari, Florent, Emmanuel Hainry F, Romain Péchoux +1 more

Polylogarithmic time delineates a relevant notion of feasibility on several classical computational models such as Boolean circuits or parallel random access machines. As far as the quantum paradigm is concerned, this notion yields the complexity class FBQPOLYLOG of functions approximable in polylogarithmic time with a quantum random-access Turing machine. We introduce a quantum programming language with first-order recursive procedures, which provides the first programming-language-based characterization of FBQPOLYLOG. Each program computes a function in FBQPOLYLOG (soundness) and, conversely, each function of this complexity class is computed by a program (completeness). We also provide a compilation strategy from programs to uniform families of quantum circuits of polylogarithmic depth and polynomial size, whose set of computed functions is known as QNC, and recover the well-known separation result FBQPOLYLOG $\subsetneq$ QNC.

arXiv:2507.15415•Jan 1, 2025•0 citations

Quantum Turing Machines and Quantum Prover-Verifier Interactions

Abel Molina

We present results on quantum Turing machines and on prover-verifier interactions. \n \n \nIn our work on quantum Turing machines, we continue the line of research opened by Yao (1993), who proved that quantum Turing machines and quantum circuits are polynomially equivalent computational models: t ≥ n steps of a quantum Turing machine running on an input of length n can be simulated by a uniformly generated family of quantum circuits with size quadratic in t, and a polynomial-time uniformly generated family of quantum circuits can be simulated by a quantum Turing machine running in polynomial time. We then first revisit the simulation of quantum Turing machines with uniformly generated quantum circuits, and present a variation on the simulation method employed by Yao together with an analysis of it. This analysis reveals that the simulation of quantum Turing machines can be performed by quantum circuits having depth linear in t, rather than quadratic depth, and can be extended easily to many variants of quantum Turing machines, such as ones having multi-dimensional tapes. Our analysis is based on an extension of a method of Arrighi, Nesme, and Werner (2011) that allows for the localization of causal unitary evolutions, involving abstract lemmas that might be of independent interest. \n \n \nWe also consider the more complex extension of our variant to the circuit simulation of multi-tape quantum Turing machines, where our variant provides a circuit with O(t^k) size and O(t^{k-1}) depth for the simulation of t steps of a machine with k tapes. This can be contrasted with the O(t^{k}) depth corresponding to the generalization of Yao's simulation by Nishimura and Ozawa (2002). Our usage of abstract techniques regarding the localization of causal unitary evolutions allows again for a simplification of the algebraic manipulation aspects of the construction. We also discuss the further extension to the case of oracle quantum Turing machines. \n \n \nIn our work on prover-verifier interactions, we first consider a protocol under the name of perfect/conclusive quantum state exclusion. This means to be able to discard with certainty at least one out of n possible quantum state preparations by performing a measurement of the resulting state. When all the preparations correspond to pure states and there are no more of them than their common dimension, it is an open problem whether POVMs give any additional power for this task with respect to projective measurements. This is the case even for the simple case of three states in three dimensions, which is discussed by Caves, Fuchs and Schack (2002) as unsuccessfully tackled. In our work, we give an analytical proof that in this case POVMs do indeed not give any additional power with respect to projective measurements. We also discuss possible generalizations of our work, including an application of Quadratically Constrained Quadratic Programming that might be of special interest. \n \n \nWe additionally consider the problem of quantum hedging, a particular kind of quantum correlation that arises between parallel instances of prover-verifier interactions. M. and Watrous (2012) studied a protocol that exhibited a perfect form of quantum hedging, where the risk for the prover of losing a first game can completely offset the corresponding risk for a second game. We take a step towards a better understanding of this hedging phenomenon by giving a characterization of the prover's optimal behavior for a natural generalization of this protocol. Furthermore, we discuss how the usage of the logarithmic utility principle to analyze prover-verifier interactions could justify further study of quantum hedging.

•Jul 31, 2020•0 citations

Perfect Computational Equivalence between Quantum Turing Machines and Finitely Generated Uniform Quantum Circuit Families

Harumichi Nishimura, Masanao Ozawa

In order to establish the computational equivalence between quantum Turing machines (QTMs) and quantum circuit families (QCFs) using Yao's quantum circuit simulation of QTMs, we previously introduced the class of uniform QCFs based on an infinite set of elementary gates, which has been shown to be computationally equivalent to polynomial-time QTMs (with appropriate restriction of amplitudes) up to bounded error simulation. This result implies that the complexity class BQP introduced by Bernstein and Vazirani for QTMs equal their counterparts for uniform QCFs. However, the complexity classes ZQP and EQP for QTMs do not appear to equal their counterparts for uniform QCFs. In this paper, we introduce a subclass of uniform QCFs, finitely generated uniform QCFs, based on finite number of elementary gates and show that the finitely generated uniform QCF is perfectly equivalent to the polynomial-time QTM; they can exactly simulate each other. This naturally implies that BQP as well as ZQP and EQP equal the corresponding complexity classes of the finitely generated uniform QCF.

•Nov 12, 2005•27 citations

Quasilinear Equivalence Checking for Detector Error Models

Mathys Rennela

A Detector Error Model (DEM) is a structured representation of error mechanisms in quantum circuits, which has gained popularity in quantum compilation pipelines for its ability to capture fault-tolerance at a circuit level. It lists error mechanisms as instructions targeting detectors and observables, specifying for each physical fault channel the probability that the fault fires, the detectors it triggers, and the observables it flips. In this paper, we develop an equational theory for DEMs, with its associated categorical semantics. We present a sound, terminating, confluent rewriting system for DEM terms, formulating it as a symmetric monoidal theory (a PROP) over the Giry monad. We prove that every DEM term has a unique normal form, which can be computed efficiently in quasilinear time $O(k|E|\log|E|)$, where $|E|$ is the number of instructions and $k$ bounds the size of a target set. This provides a complete set of invariants (via Tanner graphs) for structural DEM equivalence. We provide the first static decision procedure for DEM equivalence, with rigorous correctness guarantees. It is complete (decides full decoder-equivalence exactly) for non-adaptive quantum error correction (QEC) pipelines, and scales to a sound and applicable decision procedure for partially-adaptive circuits (lattice surgery, distributed QEC, ...) without suffering exponential overhead. We discuss its application to the verification and optimisation of quantum compilers.

quant-pharXiv:2606.14677•Jun 15, 2026•0 citations
Term Rewrite Systems (TRS) is a computational model offering a level of abstraction well-suited towards static analysis, e.g., termination or complexity analyses. In this paper, we introduce Quantum Term Rewrite Systems (QTRS), an extension of TRS to quantum computing, thus allowing to benefit from quantum advantage while being able to certify the complexity. We ensure that QTRS correspond to physically realizable processes and adapt techniques to obtain termination certificates or generic bounds on the reduction length. We delineate a class of terminating QTRS that can be compiled to uniform families of quantum circuits of size bounded by the reduction length. Conversely, this class is universal for quantum circuits. In particular, we show a characterization of the class of functions computable in quantum polynomial time, known as FBQP\mathtt{FBQP}FBQP.
Polylogarithmic time delineates a relevant notion of feasibility on several classical computational models such as Boolean circuits or parallel random access machines. As far as the quantum paradigm is concerned, this notion yields the complexity class FBQPOLYLOG of functions approximable in polylogarithmic time with a quantum random-access Turing machine. We introduce a quantum programming language with first-order recursive procedures, which provides the first programming-language-based characterization of FBQPOLYLOG. Each program computes a function in FBQPOLYLOG (soundness) and, conversely, each function of this complexity class is computed by a program (completeness). We also provide a compilation strategy from programs to uniform families of quantum circuits of polylogarithmic depth and polynomial size, whose set of computed functions is known as QNC, and recover the well-known separation result FBQPOLYLOG ⊊\subsetneq⊊ QNC.
We present results on quantum Turing machines and on prover-verifier interactions. \n \n \nIn our work on quantum Turing machines, we continue the line of research opened by Yao (1993), who proved that quantum Turing machines and quantum circuits are polynomially equivalent computational models: t ≥ n steps of a quantum Turing machine running on an input of length n can be simulated by a uniformly generated family of quantum circuits with size quadratic in t, and a polynomial-time uniformly generated family of quantum circuits can be simulated by a quantum Turing machine running in polynomial time. We then first revisit the simulation of quantum Turing machines with uniformly generated quantum circuits, and present a variation on the simulation method employed by Yao together with an analysis of it. This analysis reveals that the simulation of quantum Turing machines can be performed by quantum circuits having depth linear in t, rather than quadratic depth, and can be extended easily to many variants of quantum Turing machines, such as ones having multi-dimensional tapes. Our analysis is based on an extension of a method of Arrighi, Nesme, and Werner (2011) that allows for the localization of causal unitary evolutions, involving abstract lemmas that might be of independent interest. \n \n \nWe also consider the more complex extension of our variant to the circuit simulation of multi-tape quantum Turing machines, where our variant provides a circuit with O(t^k) size and O(t^{k-1}) depth for the simulation of t steps of a machine with k tapes. This can be contrasted with the O(t^{k}) depth corresponding to the generalization of Yao's simulation by Nishimura and Ozawa (2002). Our usage of abstract techniques regarding the localization of causal unitary evolutions allows again for a simplification of the algebraic manipulation aspects of the construction. We also discuss the further extension to the case of oracle quantum Turing machines. \n \n \nIn our work on prover-verifier interactions, we first consider a protocol under the name of perfect/conclusive quantum state exclusion. This means to be able to discard with certainty at least one out of n possible quantum state preparations by performing a measurement of the resulting state. When all the preparations correspond to pure states and there are no more of them than their common dimension, it is an open problem whether POVMs give any additional power for this task with respect to projective measurements. This is the case even for the simple case of three states in three dimensions, which is discussed by Caves, Fuchs and Schack (2002) as unsuccessfully tackled. In our work, we give an analytical proof that in this case POVMs do indeed not give any additional power with respect to projective measurements. We also discuss possible generalizations of our work, including an application of Quadratically Constrained Quadratic Programming that might be of special interest. \n \n \nWe additionally consider the problem of quantum hedging, a particular kind of quantum correlation that arises between parallel instances of prover-verifier interactions. M. and Watrous (2012) studied a protocol that exhibited a perfect form of quantum hedging, where the risk for the prover of losing a first game can completely offset the corresponding risk for a second game. We take a step towards a better understanding of this hedging phenomenon by giving a characterization of the prover's optimal behavior for a natural generalization of this protocol. Furthermore, we discuss how the usage of the logarithmic utility principle to analyze prover-verifier interactions could justify further study of quantum hedging.
In order to establish the computational equivalence between quantum Turing machines (QTMs) and quantum circuit families (QCFs) using Yao's quantum circuit simulation of QTMs, we previously introduced the class of uniform QCFs based on an infinite set of elementary gates, which has been shown to be computationally equivalent to polynomial-time QTMs (with appropriate restriction of amplitudes) up to bounded error simulation. This result implies that the complexity class BQP introduced by Bernstein and Vazirani for QTMs equal their counterparts for uniform QCFs. However, the complexity classes ZQP and EQP for QTMs do not appear to equal their counterparts for uniform QCFs. In this paper, we introduce a subclass of uniform QCFs, finitely generated uniform QCFs, based on finite number of elementary gates and show that the finitely generated uniform QCF is perfectly equivalent to the polynomial-time QTM; they can exactly simulate each other. This naturally implies that BQP as well as ZQP and EQP equal the corresponding complexity classes of the finitely generated uniform QCF.
A Detector Error Model (DEM) is a structured representation of error mechanisms in quantum circuits, which has gained popularity in quantum compilation pipelines for its ability to capture fault-tolerance at a circuit level. It lists error mechanisms as instructions targeting detectors and observables, specifying for each physical fault channel the probability that the fault fires, the detectors it triggers, and the observables it flips. In this paper, we develop an equational theory for DEMs, with its associated categorical semantics. We present a sound, terminating, confluent rewriting system for DEM terms, formulating it as a symmetric monoidal theory (a PROP) over the Giry monad. We prove that every DEM term has a unique normal form, which can be computed efficiently in quasilinear time O(k∣E∣log⁡∣E∣)O(k|E|\log|E|)O(k∣E∣log∣E∣), where ∣E∣|E|∣E∣ is the number of instructions and kkk bounds the size of a target set. This provides a complete set of invariants (via Tanner graphs) for structural DEM equivalence. We provide the first static decision procedure for DEM equivalence, with rigorous correctness guarantees. It is complete (decides full decoder-equivalence exactly) for non-adaptive quantum error correction (QEC) pipelines, and scales to a sound and applicable decision procedure for partially-adaptive circuits (lattice surgery, distributed QEC, ...) without suffering exponential overhead. We discuss its application to the verification and optimisation of quantum compilers.