Pith. sign in

REVIEW 3 major objections 4 minor 67 references

Quantum Term Rewrite Systems, a typed extension of term rewriting to superposed quantum terms, characterize exactly the class FBQP of functions computable in quantum polynomial time.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-01 10:35 UTC pith:MJXBO3ZW

load-bearing objection Quantum TRS framework with a plausible FBQP characterization, but the circuit-size bound rests on an unproved merging lemma; deserves review. the 3 major comments →

arxiv 2607.20170 v1 pith:MJXBO3ZW submitted 2026-07-22 cs.LO

Quantum Term Rewrite Systems: Applications to Complexity Analysis

Kostia Chardonnet , Emmanuel Hainry , Romain P\'echoux , Thomas Vinet This is my paper
classification cs.LO
keywords quantum term rewrite systemsterm rewritingquantum circuitsFBQPcomplexity analysisterminationtype inferenceresource analysis
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces Quantum Term Rewrite Systems (QTRS), a version of term rewriting in which terms can be superposed with complex amplitudes and evaluated in parallel, with a type system that guarantees the rewrite system corresponds to physically realizable quantum processes. Its main result is that the fragment QTRS(Poly) — QTRS that are structure-preserving, quantum-controlling, simply recursive, and terminate in polynomial time on qubit lists — compiles to uniform polynomial-size quantum circuit families, and conversely every such function is expressible. In short, the paper establishes that these rewrite systems characterize exactly the class FBQP of functions computable in quantum polynomial time. Along the way, it shows the fragment is universal for uniform quantum circuits, gives circuit-size bounds from runtime bounds, and shows classical termination and complexity analysis techniques (worst-path orderings, polynomial interpretations, dependency pairs) can be reused in the quantum setting. The value for a reader is a high-level, statically analyzable model for quantum programs that connects termination and resource analysis to circuit size.

Core claim

The paper's central claim is Theorem 27: the binary functions computed by the compiled circuits of QTRS(Poly) — the fragment of quantum term rewrite systems that are structure-preserving, quantum-controlling, simply recursive, and terminating in polynomial time on lists of qubits — are exactly the class FBQP. To get there, the paper proves that QTRSCirc is universal for uniform quantum circuit families (any uniform family can be expressed as a QTRS) and, conversely, that every terminating QTRSCirc can be compiled to a uniform family of quantum circuits that approximates its outputs with probability 2/3. For the simply recursive subset, the compiled circuit's size is bounded by O(τ(|v|)^(rk(f

What carries the argument

The load-bearing objects are: (1) the type system enforcing physicality, which types superposed terms only when summands are orthogonal and amplitudes form a normalised complex vector, ensuring function symbols are isometries; (2) the fragment QTRSCirc, defined by structure-preserving and quantum-controlling rewrite rules that leave control qubits untouched, which lets each rewrite rule be compiled as a controlled statement; (3) simple recursion, which forbids mutual recursion and forces all recursive calls to a function on a given structural input to merge into a single call, preventing exponential circuit blow-up; and (4) worst-path orderings, which lift classical rewriting orderings to su

Load-bearing premise

Theorem 25's circuit-size bound rests on an unproved merging lemma, cited from the literature, that in a simply recursive QTRS all recursive calls on the same input can be merged into a single call without exponential blow-up; if that lemma fails, the polynomial size bound underlying the FBQP characterization collapses.

What would settle it

Construct a simply recursive QTRS in QTRS(Poly) whose rewrite rules satisfy the hypotheses of Theorem 25 but contain two recursive branches on the same input; compile it via the paper's inductive procedure and inspect the size of the resulting circuit family. If the size is super-polynomial while the reduction length is polynomial, the merging lemma is false and Theorem 25 fails. A direct counterexample to the cited merging lemma in the literature would also settle it.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Every uniform family of quantum circuits can be expressed as a QTRS of the QTRSCirc fragment (Theorem 21).
  • Every terminating QTRS in QTRSCirc compiles to a uniform family of quantum circuits that approximates outputs with probability 2/3 (Theorem 22).
  • For simply recursive QTRS, compiled circuit size is O(τ(|v|)^(rk(f)+1)) with τ the runtime bound (Theorem 25).
  • QTRS(Poly) — terminating in polynomial time on qubit lists — computes exactly FBQP (Theorem 27).
  • Termination techniques from classical TRS, including polynomial interpretations and dependency pairs, adapt to QTRS and yield complexity bounds (Theorems 32, 37, 41).

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the main theorem holds, resource analysis for quantum programs can be carried out with classical rewriting technology: any termination or runtime bound proved by polynomial interpretations or dependency pairs automatically yields a circuit-size bound, so existing TRS complexity provers become quantum circuit-size certified compilers.
  • The undecidability of full type inference (Π0_2-hard) suggests that practical QTRS tools will restrict to the easily typed fragment, for which type inference is polynomial-time; this mirrors the classical gap between full termination and decidable fragments.
  • The same compilation theorem could characterise other quantum classes by varying the time bound τ — for example, quantum polylogarithmic time — without changing the underlying QTRS machinery.
  • Worst-path orderings could be used directly in termination provers for quantum rewriting, since they only require an ordering on classical terms; this may make QTRS amenable to automated certification with existing classical termination tools.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper introduces Quantum Term Rewrite Systems (QTRS), an extension of term rewriting with superpositions and amplitudes, together with a type system intended to enforce physicality. It establishes basic properties (confluence, subject reduction, unique canonical forms), studies decidability of type inference, and adapts standard TRS termination techniques (polynomial interpretations, dependency pairs) to the quantum setting. The central claimed result is Theorem 27: the fragment QTRS(Poly), consisting of QTRS in QTRSCirc that are simply recursive and terminate in polynomial time on qubit lists, compiles exactly to FBQP. The universality and soundness directions rely on Theorems 21, 22, and 25, with the polynomial circuit-size bound of Theorem 25 as the key technical bridge.

Significance. If the main theorem holds, the paper gives a rewriting-based implicit characterization of quantum polynomial time, a novel contribution that connects static complexity analysis of term rewriting with quantum circuit size. The paper also contributes a typed framework for quantum rewriting, confluence/subject-reduction results, an undecidability boundary for type inference, and reusable adaptations of polynomial interpretations and dependency pairs. These results are interesting beyond the FBQP characterization. The paper is ambitious and the appendices contain substantive proof attempts; the main weakness is that the load-bearing circuit-size bound and parts of the completeness construction are not fully established in the manuscript.

major comments (3)
  1. [§3.3, proof of Theorem 27] The completeness construction for kQRect conflicts with Definition 23 (SRec). In the displayed rules, the auxiliary symbol f has rules f(s1::...::sk::l) -> s1::...::sk::fs...m(l), and when fs... is rec this makes f call rec. The symbol rec has a rule rec(h1::...::ht::l) -> hm(f(pm(h1::...::ht::l))), which makes rec call f. Thus f and rec are distinct function symbols with f≈R rec, directly violating the condition 'f≈R g implies f = g' in Definition 23. Consequently the QTRS constructed for kQRect is not in SRec, and hence not in QTRS(Poly) as defined. This breaks the completeness half of Theorem 27 as written. The construction must be reworked, or SRec must be redefined in a way that still supports Theorem 25 but admits this recursion scheme.
  2. [§3.3, Theorem 25] The polynomial circuit-size bound is the sole bridge from polynomial normalization time to polynomial circuit size in the soundness direction of Theorem 27, but its proof relies on an unstated merge step. The text says 'following the merging process from [36, Theorem 9]' and asserts that because all calls to g are on an identical input, those calls can be compiled as a single call. Definition 23 only guarantees #Callee(f,S)≤1 within a structural set; it does not by itself show how the compiled controlled subcircuit is shared across the exponentially many branches of the structural set without incurring an exponential factor. If that sharing fails, the bound becomes 2^m·τ(|v|)^{rk(f)} rather than polynomial. Since no statement or proof of the merging lemma for QTRS-compiled circuits is included, Theorem 25 is not self-contained and Theorem 27's soundness direction rests on an unverified e
  3. [§3.3, Theorems 22 and 25] The proof of Theorem 22 is not a direct argument: it says to use 'the same compilation process' as in the proof of Theorem 25, but Theorem 25 is stated only for QTRS(τ) = QTRSCirc ∩ SRec ∩ Time(τ), while Theorem 22 claims compilation for arbitrary terminating QTRSCirc. The proof of Theorem 25 itself begins by assuming the compilation construction and then analyzes its size, so the reader never sees an explicit inductive construction for the general case. The relationship between the evaluation strategy, the input structure w, and the generated circuit C_struct(v) should be spelled out before any size bound is claimed.
minor comments (4)
  1. [Appendix A, Lemma 50] The statement says 'Then, t≡t′,' but the proof and the usage in Lemma 10 establish 's′≡t′'. This appears to be a typo and should be corrected.
  2. [§3.2, Theorem 15] The hardness proof is explicitly about 'free typing inference' (no equivalence rule), while the theorem statement concerns full type inference. The transfer from the free variant to the general problem is not explained. If the reduction is intended to show hardness of the general problem, the argument must address the equivalence rule, e.g., by ensuring the constructed term is only typable through the orthogonality check.
  3. [§3.3, proof of Theorem 21] The phrase 'Any n-qubit unitary can be encoded as a QTRS with 2n rules' is inaccurate if it is meant per basis transition: a general n-qubit unitary has 2^n basis states, so one expects up to 2^n rules or controlled operations. This is likely a typo, but the construction of the universal QTRS would benefit from a more precise description of how gates are represented and why the resulting system is terminating and in QTRSCirc.
  4. [§3.3, proof of Theorem 27] The uniformity of the generated circuit family is asserted with the sentence 'this creation is uniform, and is done in polynomial time' but no algorithm or complexity argument is given. Since the circuit family is indexed by structures and generated by reduction of rewrite rules, the proof should explain how a Turing machine computes C_w from w in polytime, especially concerning the representation of the complex amplitudes.

Circularity Check

0 steps flagged

No significant circularity: the FBQP characterization has independent content, though Theorem 25 delegates a key branch-merging step to the authors' prior work [36].

full rationale

The central claim (Theorem 27) is not forced by definition or by a fitted parameter. QTRS(Poly) is defined with a polynomial runtime bound built in, but the equivalence with FBQP still requires a compilation direction (Theorems 22 and 25) and a universality/completeness direction (Theorem 21 together with the encoding of Yamakami's algebra). The universality direction uses external TRS Turing completeness [40], and the completeness direction re-encodes Yamakami's external characterization [63]; neither reduces to the paper's own definitions. The only notable self-citation is in the proof of Theorem 25, where the polynomial circuit-size bound invokes 'the merging process from [36, Theorem 9]' to merge recursive calls and avoid exponential blow-up. This is a load-bearing proof dependency on prior work by three of the four authors, and the lemma is not re-proved in this paper; it is therefore a verification/correctness risk. But it is not circular: it is a cited theorem, not a normalization choice, not a fitted constant, and not a restatement of the target FBQP characterization. The paper does not rename an empirical pattern as a new result; the QTRS model is a distinct formalism with its own semantics, typing, and compilation. Thus no derivation step reduces to its own inputs by construction.

Axiom & Free-Parameter Ledger

1 free parameters · 7 axioms · 0 invented entities

No new physical objects are postulated. QTRS is a mathematical formalism, not an entity with an independent falsifiable handle; amplitude symbols are program syntax. The free parameters listed are proof certificates, not fitted data.

free parameters (1)
  • Monotonic polynomial interpretation coefficients = LfM=X+3Y, LconsM=X+Y+1 in Example 33
    Hand-chosen by the authors to prove termination of the example; a proof certificate, not a parameter of the main theorems. Additive assignments in Definition 40 similarly choose α_c≥1 by hand.
axioms (7)
  • standard math Equality, sum, and product are decidable on algebraic numbers (Halava et al. 2005)
    Used in Theorems 15 and 16 for the decidability status of amplitude checks.
  • domain assumption TRS are Turing complete (Huet and Lankford 1978)
    Used in Theorem 21 to encode arbitrary uniform circuit families into a QTRS.
  • domain assumption Strong normalization of constructor TRS is Π0_2-complete (Simonsen 2009)
    Used in Theorem 15's hardness proof.
  • domain assumption Yamakami's function algebra □QP_1 characterizes FBQP (Yamakami 2020)
    Used in Theorem 27's completeness direction; the proof quotes this external characterization.
  • domain assumption Solovay–Kitaev theorem provides gate approximations with polylog overhead (Kitaev 1997)
    Used to make circuit approximations with probability 2/3 in Theorems 22 and 25.
  • domain assumption Branch sequentialization merging lemma [36, Theorem 9] applies to simply recursive QTRS
    Invoked in Theorem 25 to merge recursive calls and avoid exponential blow-up; not proved in this paper.
  • domain assumption QTRS(Poly) is defined with a semantic polynomial-time termination premise (Definitions 24 and 26)
    The FBQP characterization is conditional on the system already being known to terminate in polynomial time; this is assumed about the class, not derived as a purely syntactic consequence.

pith-pipeline@v1.3.0-alltime-deepseek · 36498 in / 17090 out tokens · 171669 ms · 2026-08-01T10:35:10.210161+00:00 · methodology

0 comments
read the original 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}$.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

67 extracted references · 24 canonical work pages

  1. [1]

    Computational Advantage from Quantum-Controlled Ordering of Gates , author =. Phys. Rev. Lett. , publisher =

  2. [2]

    Science of Computer Programming , publisher =

    On probabilistic term rewriting , author =. Science of Computer Programming , publisher =. doi:10.1016/j.scico.2019.102338 , issn =

    arXiv 2019

  3. [3]

    Journal of Automated Reasoning , publisher =

    Lower Bounds for Runtime Complexity of Term Rewriting , author =. Journal of Automated Reasoning , publisher =. doi:10.1007/s10817-016-9397-x , issn =

    work page doi:10.1007/s10817-016-9397-x

  4. [4]

    Theoretical Computer Science , volume = 236, number = 1, pages =

    Termination of term rewriting using dependency pairs , author =. Theoretical Computer Science , volume = 236, number = 1, pages =. doi:10.1016/S0304-3975(99)00207-8 , issn =

    doi:10.1016/s0304-3975(99)00207-8

  5. [5]

    Dependency

    Avanzini, Martin and Moser, Georg , year = 2009, booktitle =. Dependency. doi:10.1007/978-3-642-02348-4_4 , isbn =

    work page doi:10.1007/978-3-642-02348-4_4 2009

  6. [6]

    Polynomial

    Avanzini, Martin and Moser, Georg , year = 2013, month = nov, journal =. Polynomial. doi:10.2168/LMCS-9(4:9)2013 , issn =

    work page doi:10.2168/lmcs-9(4:9)2013 2013

  7. [7]

    Quantum Expectation Transformers for Cost Analysis , author =

  8. [8]

    Algorithms with polynomial interpretation termination proof , author =. J. Funct. Program. , publisher =. doi:10.1017/S0956796800003877 , issn =

    work page doi:10.1017/s0956796800003877

  9. [9]

    Logical Methods in Computer Science , publisher =

    A Characterization of Basic Feasible Functionals Through Higher-Order Rewriting and Tuple Interpretations , author =. Logical Methods in Computer Science , publisher =. doi:10.46298/lmcs-21(4:19)2025 , issn =

    work page doi:10.46298/lmcs-21(4:19)2025 2025

  10. [10]

    Fundamenta Informaticae , publisher =

    On Complexity Bounds and Confluence of Parallel Term Rewriting* , author =. Fundamenta Informaticae , publisher =. doi:10.3233/fi-242191 , issn =

    work page doi:10.3233/fi-242191

  11. [11]

    Term Rewriting and Applications , publisher =

    Proving Positive Almost-Sure Termination , author =. Term Rewriting and Applications , publisher =. doi:10.1007/978-3-540-32033-3_24 , isbn = 9783540320333, issn =

    work page doi:10.1007/978-3-540-32033-3_24

  12. [12]

    Applications to ELAN , author =

    Probabilistic Rewrite Strategies. Applications to ELAN , author =. Rewriting Techniques and Applications , publisher =. doi:10.1007/3-540-45610-4_18 , isbn = 9783540456100, issn =

    work page doi:10.1007/3-540-45610-4_18

  13. [13]

    Logic for Programming, Artificial Intelligence, and Reasoning , publisher =

    Characterising Space Complexity Classes via Knuth-Bendix Orders , author =. Logic for Programming, Artificial Intelligence, and Reasoning , publisher =. doi:10.1007/978-3-642-16242-8_11 , isbn = 9783642162428, issn =

    work page doi:10.1007/978-3-642-16242-8_11

  14. [14]

    Theoretical Computer Science , volume = 412, number = 25, pages =

    Quasi-Interpretations a Way to Control Resources , author =. Theoretical Computer Science , volume = 412, number = 25, pages =. doi:10.1016/j.tcs.2011.02.007 , issn =

    work page doi:10.1016/j.tcs.2011.02.007 2011

  15. [15]

    Term Rewriting and All That , author =

  16. [16]

    41st Annual Symposium on Logic in Computer Science (LICS 2026) , publisher =

    Barsse, Kathleen and P\'. 41st Annual Symposium on Logic in Computer Science (LICS 2026) , publisher =. doi:10.4230/LIPIcs.LICS.2026.14 , isbn =

    work page doi:10.4230/lipics.lics.2026.14 2026

  17. [17]

    Bernstein, Ethan and Vazirani, Umesh , year = 1997, month = oct, journal =. Quantum. doi:10.1137/S0097539796300921 , issn =

    doi:10.1137/s0097539796300921 1997

  18. [18]

    New Journal of Physics , publisher =

    Interacting quantum observables: categorical algebra and diagrammatics , author =. New Journal of Physics , publisher =. doi:10.1088/1367-2630/13/4/043016 , issn =

    doi:10.1088/1367-2630/13/4/043016

  19. [19]

    Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages , author =. Proc. ACM Program. Lang. , publisher =. doi:10.1145/3704883 , issue_date =

    doi:10.1145/3704883

  20. [20]

    LIPIcs, Volume 378, FSCD 2026 , booktitle =

    Resource-Aware Quantum Programming with General Recursion and Quantum Control , author =. LIPIcs, Volume 378, FSCD 2026 , booktitle =

    2026

  21. [21]

    Proceedings of the ACM on Programming Languages , publisher =

    Hybrid Path-Sums for Hybrid Quantum Programs , author =. Proceedings of the ACM on Programming Languages , publisher =. doi:10.1145/3808314 , issn =

    doi:10.1145/3808314

  22. [22]

    30th Annual Symposium on Foundations of Computer Science , publisher =

    Characterizations of the basic feasible functionals of finite type , author =. 30th Annual Symposium on Foundations of Computer Science , publisher =

  23. [23]

    2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , publisher =

    Realizability in the Unitary Sphere , author =. 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , publisher =

    2019

  24. [24]

    Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model , author =. Log. Methods Comput. Sci. , volume = 18, number = 3, doi =

  25. [25]

    Theoretical computer science , publisher =

    Orderings for term-rewriting systems , author =. Theoretical computer science , publisher =

  26. [26]

    Quantum implicit computational complexity , author =. Theor. Comput. Sci. , volume = 411, number = 2, pages =

  27. [27]

    Foundations of Software Science and Computation Structures, FoSSaCS 2025 , location =

    Combining quantum and classical control: syntax, semantics and adequacy , author =. Foundations of Software Science and Computation Structures, FoSSaCS 2025 , location =. doi:10.1007/978-3-031-90897-2_8 , isbn =

    doi:10.1007/978-3-031-90897-2_8 2025

  28. [28]

    Journal of Automated Reasoning , publisher =

    Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs , author =. Journal of Automated Reasoning , publisher =. doi:10.1007/s10817-013-9277-6 , issn =

    doi:10.1007/s10817-013-9277-6

  29. [29]

    Computer Science Logic , publisher =

    Degrees of Undecidability in Term Rewriting , author =. Computer Science Logic , publisher =. doi:10.1007/978-3-642-04027-6_20 , isbn = 9783642040276, issn =

    work page doi:10.1007/978-3-642-04027-6_20

  30. [30]

    Information Processing Letters , publisher =

    Constant runtime complexity of term rewriting is semi-decidable , author =. Information Processing Letters , publisher =. doi:10.1016/j.ipl.2018.06.012 , issn =

    work page doi:10.1016/j.ipl.2018.06.012 2018

  31. [31]

    Ferrari, Florent and Hainry, Emmanuel and P. Quantum. 50th

  32. [32]

    Feng, Yuan and Ying, Mingsheng , year = 2021, journal =. Quantum

    2021

  33. [33]

    Quipper: a scalable quantum programming language , author =

  34. [34]

    Applied Sciences , publisher =

    Quantum Turing Machines: Computations and Measurements , author =. Applied Sciences , publisher =. doi:10.3390/app10165551 , issn =

    work page doi:10.3390/app10165551

  35. [35]

    Skolem's Problem - On the Border between Decidability and Undecidability , author =

  36. [36]

    On the uniform halting problem for term rewriting systems , author =

  37. [37]

    Automated

    Hirokawa, Nao and Moser, Georg , year = 2008, booktitle =. Automated. doi:10.1007/978-3-540-71070-7_32 , isbn =

    doi:10.1007/978-3-540-71070-7_32 2008

  38. [38]

    Logical Methods in Computer Science , publisher =

    Theory of higher order interpretations and application to Basic Feasible Functions , author =. Logical Methods in Computer Science , publisher =. doi:10.23638/lmcs-16(4:14)2020 , issn =

    work page doi:10.23638/lmcs-16(4:14)2020 2020

  39. [39]

    Hainry, Emmanuel and P. A. Foundations of Software Science and Computation Structures , pages =. doi:10.1007/978-3-031-30829-1_8 , isbn =

    work page doi:10.1007/978-3-031-30829-1_8

  40. [40]

    Formal Structures for Computation and Deduction,

    Branch Sequentialization in Quantum Polytime , author =. Formal Structures for Computation and Deduction,

  41. [41]

    Automated Deduction – CADE 29 , publisher =

    Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs , author =. Automated Deduction – CADE 29 , publisher =. doi:10.1007/978-3-031-38499-8_20 , isbn = 9783031384998, issn =

    work page doi:10.1007/978-3-031-38499-8_20

  42. [42]

    Russian Mathematical Surveys , publisher =

    Quantum computations: algorithms and error correction , author =. Russian Mathematical Surveys , publisher =. doi:10.1070/rm1997v052n06abeh002155 , issn =

    doi:10.1070/rm1997v052n06abeh002155

  43. [43]

    Nature , publisher =

    A scheme for efficient quantum computation with linear optics , author =. Nature , publisher =. doi:10.1038/35051009 , issn =

    doi:10.1038/35051009

  44. [44]

    Logical Methods in Computer Science , publisher =

    Complexity of Conditional Term Rewriting , author =. Logical Methods in Computer Science , publisher =. doi:10.23638/lmcs-13(1:6)2017 , issn =

    work page doi:10.23638/lmcs-13(1:6)2017 2017

  45. [45]

    2409.18420 , archiveprefix =

    Exponential separation in quantum query complexity of the quantum switch with respect to simulations with standard quantum circuits , author =. 2409.18420 , archiveprefix =

    Pith/arXiv arXiv

  46. [46]

    LIPIcs, Volume 260, FSCD 2023 , booktitle =

    Cost-Size Semantics for Call-By-Value Higher-Order Rewriting , author =. LIPIcs, Volume 260, FSCD 2023 , booktitle =

    2023

  47. [47]

    On proving term rewriting systems are Noetherien , author =

  48. [48]

    Journal of Logical and Algebraic Methods in Programming , publisher =

    Dependency pairs for proving termination properties of conditional term rewriting systems , author =. Journal of Logical and Algebraic Methods in Programming , publisher =. doi:10.1016/j.jlamp.2016.03.003 , issn =

    work page doi:10.1016/j.jlamp.2016.03.003 2016

  49. [49]

    Information and Computation , publisher =

    Analysing the implicit complexity of programs , author =. Information and Computation , publisher =. doi:10.1016/s0890-5401(03)00011-7 , issn =

    work page doi:10.1016/s0890-5401(03)00011-7

  50. [50]

    Automated Deduction – CADE 30 , publisher =

    The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting , author =. Automated Deduction – CADE 30 , publisher =. doi:10.1007/978-3-031-99984-0_12 , isbn = 9783031999840, issn =

    work page doi:10.1007/978-3-031-99984-0_12

  51. [51]

    Theoretical Computer Science , volume = 192, number = 1, pages =

    Higher-Order Rewrite Systems and Their Confluence , author =. Theoretical Computer Science , volume = 192, number = 1, pages =. doi:10.1016/S0304-3975(97)00143-6 , issn =

    doi:10.1016/s0304-3975(97)00143-6

  52. [52]

    CoRR , doi =

    Automated Expected Cost Analysis for Quantum Programs , author =. CoRR , doi =

  53. [53]

    Quantum Computation and Quantum Information: 10th Anniversary Edition , author =

  54. [54]

    Nature Communications , publisher =

    Experimental superposition of orders of quantum gates , author =. Nature Communications , publisher =. doi:10.1038/ncomms8913 , issn =

    work page doi:10.1038/ncomms8913

  55. [55]

    Open Quantum Assembly Language , author =

  56. [56]

    Qunity: A Unified Language for Quantum and Classical Computing , author =. Proc. ACM Program. Lang. , publisher =. doi:10.1145/3571225 , issue_date =

    doi:10.1145/3571225

  57. [57]

    SIAM Journal on Computing , volume = 26, number = 5, pages =

    Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer , author =. SIAM Journal on Computing , volume = 26, number = 5, pages =

  58. [58]

    Rewriting Techniques and Applications , publisher =

    The ^0_2 -Completeness of Most of the Properties of Rewriting Systems You Care About (and Productivity) , author =. Rewriting Techniques and Applications , publisher =. doi:10.1007/978-3-642-02348-4_24 , isbn = 9783642023484, issn =

    work page doi:10.1007/978-3-642-02348-4_24

  59. [59]

    Quantum lambda calculus , publisher =

    Semantic Techniques in Quantum Computation , author =. Quantum lambda calculus , publisher =

  60. [60]

    From Symmetric Pattern-Matching to Quantum Control

    Sabry, Amr and Valiron, Beno \^i t and Vizzotto, Juliana Kaizer. From Symmetric Pattern-Matching to Quantum Control. Foundations of Software Science and Computation Structures

  61. [61]

    PRX Quantum , publisher =

    Computational Advantage from the Quantum Superposition of Multiple Temporal Orders of Photonic Gates , author =. PRX Quantum , publisher =

  62. [62]

    Term rewriting systems , author =

  63. [63]

    Confluence and

    Yamada, Toshiyuki , year = 2001, booktitle =. Confluence and. doi:10.1007/3-540-45127-7_25 , isbn =

    work page doi:10.1007/3-540-45127-7_25 2001

  64. [64]

    Yamakami, Tomoyuki , year = 2020, month = dec, journal =. A. doi:10.1017/jsl.2020.45 , issn =

    doi:10.1017/jsl.2020.45 2020

  65. [65]

    Proceedings of 1993

    Quantum Circuit Complexity , author =. Proceedings of 1993

    1993

  66. [66]

    Foundations of quantum programming , author =

  67. [67]

    Proceedings of the ACM on Programming Languages , publisher =

    Quantum Control Machine: The Limits of Control Flow in Quantum Programming , author =. Proceedings of the ACM on Programming Languages , publisher =. doi:10.1145/3649811 , issn =

    doi:10.1145/3649811