Pith. sign in

REVIEW 3 major objections 5 minor 2 cited by

Automating Equational Proofs in Dirac Notation

T0 review · 3 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash

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

Pith's one-line read Dirac notation's first-order theory is decidable, and equations reduce to unique normal forms.

desk verdict A useful, honestly-scoped rewriting tool for Dirac notation whose abstract oversells the decision procedure: completeness is still a conjecture, and the paper itself supplies a valid identity the §7 algorithm cannot decide. read the letter →

arxiv 2411.11617 v1 pith:YYT2YVHI submitted 2024-11-18 cs.PL

Yingte Xu , Gilles Barthe , Li Zhou This is my paper · ORCID
classification cs.PL MSC 03B2503C1068Q4281P68
keywords Diracnotationbra-kettermrewritingequationalreasoningdecidabilityrealclosedfieldsquantumprogramverificationsymboliccomputation
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Dirac notation is the everyday language of quantum states, but until now equational reasoning in it has been largely manual. This paper treats bra-ket notation as a typed algebraic theory and asks what can be decided automatically. It proves that, for fixed finite-dimensional Hilbert spaces, the first-order theory of Dirac notation is decidable: every formula reduces to one about complex numbers, where Tarski's theorem on real closed fields applies. For the common problem of deciding whether two expressions are equal, it constructs an associative-commutative term-rewriting system that is sound, terminating, and locally confluent, so equality can be established by comparing unique normal forms. The authors report that a prototype based on the system solves most of the Dirac-notation equations extracted from an existing quantum-program verification library in under a second each, while flagging the converse completeness direction as a conjecture for the core system and unproved for the extended big-sum language.

What carries the argument

The load-bearing object is the many-sorted first-order theory DN with types S for scalars, K(sigma) and B(sigma) for kets and bras over a classical basis type sigma, and O(sigma,tau) for linear operators, together with the AC term-rewriting system R_DN. The theory's decidability rests on the basis-expansion identity that decomposes every ket, bra, and operator into complex combinations of basis elements; the rewrite system's work is to orient the linear-algebra equalities into rules that sort multiplications to the right, distribute tensor products, reduce inner products of basis kets to Kronecker deltas, and propagate adjoints and conjugates until a unique normal form modulo AC is reached. For the extended language DNE with big sums, the machinery adds sum-elimination by delta symbols, pushing symbols into sums, swapping and splitting index sets, and a final alpha-equivalence check by constrained AC-unification.

What would settle it

Find well-typed core-language terms e1 and e2 that are semantically equal but whose R_DN normal forms differ; the tool would report them unequal, disproving relative completeness. For the extended language, a concrete non-joinable pair or an infinite rewriting sequence in R_DNE would falsify the assumption that the stated algorithm is a decision procedure.

Watch

Extended reading notes

Core claim

The central claim is that Dirac notation has a decidable first-order theory and a practical equational proof procedure. The decidability argument embeds the many-sorted theory of kets, bras, operators, tensor products, inner and outer products, adjoints, scalars, and Kronecker deltas into the first-order theory of complex numbers: over a fixed finite basis, every state and operator is uniquely determined by complex coefficients, and quantifiers over them become quantifiers over complex numbers; decidability then follows from Tarski's theorem. The equational procedure is a term-rewriting system modulo associativity and commutativity with more than 150 rules, which the paper proves sound, terminating, locally confluent, and hence normalizing to a unique normal form, aided by automated termination and critical-pair tools and a mechanized soundness proof. The paper's Theorem 7.4 gives the one-way direction: same normal form implies semantic equality. The converse, relative completeness of the rewriter, is stated as Conjecture 7.5, with only a weaker completeness result relying on expansion over bases; for the extended language with big sums, termination and confluence of the rewriting rules are not proved.

Load-bearing premise

The load-bearing premise is that the rewrite system's normal forms are complete enough that every semantically valid equation of the core language reduces to the same normal form; the authors state this general direction as Conjecture 7.5, having proved only a weaker basis-expanded version.

Editorial extensions

If this is right

  • Quantum program verifiers can replace long manual Dirac-notation proof snippets by calls to a normal-form checker, as demonstrated on the stepwise proof of the HHL algorithm.
  • Equations with free variables, such as the maximally-entangled-state law (M tensor I)|Phi> = (I tensor M^T)|Phi> for arbitrary M, can be checked symbolically, which numerical matrix methods cannot do.
  • A certificate of semantic equality is produced whenever two expressions have the same R_DN normal form, because every rewriting rule is sound for finite-dimensional Hilbert-space semantics.
  • Widespread identities in linear algebra and super-operator theory, including traces, partial traces, Choi states, and adjoints, collapse to near-instant normal-form checks.
  • Big-sum expressions such as entangled states over index sets and quantum while-loop approximations are handled by an extension with sum-index swapping and alpha-equivalence checking.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If Conjecture 7.5 is settled positively, the core rewrite system becomes a genuine decision procedure for equality, upgrading its current sound-only status to complete.
  • The decidability theorem is dimension-fixed: it concerns finite-dimensional Hilbert spaces of known dimension, so first-order reasoning about dimension-parametric or infinite-dimensional spaces remains out of scope for the decision procedure as stated.
  • For the extended big-sum language, the absence of termination and confluence proofs means the algorithm should be read as a sound simplifier plus heuristic equality checker; a divergence sample would show it is not a decision procedure.
  • The symbolic, variable-level nature of the equations makes the approach complementary to fast numerical circuit-verification tools, which cannot handle free variables and which the paper reports remain about three orders of magnitude faster on concrete quantum circuits.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. The paper develops a many-sorted first-order theory DN for Dirac notation—bras, kets, operators, scalars, tensor products, adjoints, and Kronecker deltas—and an extension DNE with finitely indexed sums. Its first main result is a proof that the first-order theory of DN is decidable for fixed finite-dimensional Hilbert spaces by reduction to the theory of complex numbers and Tarski's theorem (Theorem 6.2). Its second claimed result is an efficient decision procedure for equations based on an AC term-rewriting system R_DN, with soundness proved in Coq and termination/local confluence checked with AProVE and CiME2. The paper also defines an extended algorithm for DNE, implements the approach in a Mathematica package called DiracDec, and evaluates it on CoqQ lemmas, Palsberg-Yu examples, and parameterized quantum circuits. The body is honest about the main limitation: completeness of R_DN is left as Conjecture 7.5, and termination/confluence of R_DNE are explicitly not proved.

Significance. If the completeness conjecture and the DNE termination/confluence issues were resolved, this would be a substantial and useful contribution to automated reasoning for quantum programs. The strongest, most reliable parts of the paper are the machine-checked soundness proof for the rewrite rules, the decidability theorem under the fixed finite-dimensional restriction, the explicit identification of the delta-product obstruction to completeness, and the extensive empirical evaluation. As it stands, however, the advertised 'efficient decision' claim is conditional: the paper establishes a sound simplification engine and a decidability result, but not a proven decision procedure for the full language presented in the abstract.

major comments (3)
  1. [§7.2, Theorem 7.4 and Conjecture 7.5] The second headline claim of the paper is not a theorem. Theorem 7.4 proves only the soundness direction: identical R_DN normal forms imply semantic equality. The converse—semantic equality implies identical normal forms—is explicitly left open in Conjecture 7.5, and the paper itself observes that δ_{i,j}×δ_{i,k} and δ_{i,j}×δ_{j,k} have identical denotations but are both irreducible and not AC-equivalent under R_DN. Thus the §7 normal-form test cannot decide this valid equation unless an additional oracle for δ-product equivalence is supplied. The abstract's statement that 'validity of equations can be decided efficiently' is therefore unsupported by the present theorems. The claims should be reframed as a sound simplifier or heuristic, or the completeness theorem must be proved for a precisely delimited fragment.
  2. [§8, Definition 8.3 and text after Lemma 8.4] The extended-language algorithm is also not established as a decision procedure. Definition 8.3 prescribes rewriting to R_DNE normal forms, applying Sum-Expand once, rewriting again, and checking alpha-equivalence, but the paper explicitly says that termination and confluence of R_DNE are not proved. The algorithm additionally relies on the axioms (Sum-Swap) and (Alpha-Eq) outside the rewrite system, and no invariant is given to show that the one-pass expansion reaches a unique normal form. The evaluation in §10 demonstrates practical usefulness, but it does not compensate for the absence of a termination or completeness proof. The extended procedure should be presented as a heuristic, with the open termination and confluence conditions stated prominently.
  3. [Abstract and §6, Theorem 6.2] The decidability claim as stated in the abstract is overbroad. Theorem 6.2 is explicitly restricted to fixed finite-dimensional Hilbert spaces, and its proof relies on the basis-decomposition axioms of Definition 6.1 to reduce quantification over kets, bras, and operators to quantification over finitely many complex coefficients. The abstract instead says that 'the first-order theory of Dirac notation is decidable' without this restriction. Either the abstract should include the fixed finite-dimensional qualification, or the theorem should be extended to genuinely variable or infinite-dimensional spaces, which the paper does not do.
minor comments (5)
  1. [Figure 6, Ax-Adjoint] The displayed rule for the adjoint of addition is garbled: '(D1+D2)† = D† 1+D† 2' should be typeset as (D1+D2)† = D1† + D2†.
  2. [Appendices C and D] The same symbol R'_DN is used for two different systems: the untyped erasure of R_DN in Definition C.3 and the extended system with basis unification and expansion in Definition D.2. These should be renamed to avoid confusion.
  3. [Lemma D.8] In the scalar case of Lemma D.8, the proof writes 'J a1+a2 K > 0 = J e K', which is not meaningful for complex scalars. This should be replaced by a statement about nonzeroness or norm, especially because this lemma is part of the only attempted weak completeness proof.
  4. [Abstract and §10] The counts of examples are inconsistent: the abstract says 'more than 100 examples', Section 1 says 'more than 200 examples', and Section 10.1 reports 243 CoqQ examples. These numbers should be reconciled.
  5. [§7.2] The phrase 'syntactically complete' is used to mean the existence of unique normal forms, which is likely to be confused with the later 'relative completeness' conjecture. A different term, such as 'confluent and terminating', would be clearer.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the derivation chain is self-contained; the identified gaps are completeness overclaims, not circular derivations.

full rationale

The paper's mathematical results are not circular. The decidability reduction (Theorem 6.2) takes an arbitrary DN formula and reduces it to a formula in the first-order theory of complex numbers, whose decidability is imported from Tarski's theorem as an external benchmark; the reduction is a direct semantic argument using the basis decomposition axioms, not an encoding of the target claim. The rewrite system R_DN is proved sound in Coq against an explicit denotational semantics (Lemma 7.1), and termination and local confluence are established by the external tools AProVE and CiME2 (Lemmas 7.2-7.3); none of these steps assumes the equality problem it is meant to decide. The only substantial limitation is that completeness of the rewrite decision procedure is left open (Conjecture 7.5: 'we failed to prove the general theorem because it is difficult to express the normal form using an inductive language'), and the extended-language algorithm is explicitly not proved terminating or confluent ('we do not prove the confluence or termination of R_DNE'), so the abstract's claim that 'validity of equations can be decided efficiently' is stronger than what is proven. These are correctness/completeness caveats, not circular derivations: no parameter is fitted to data and then renamed as a prediction, and no load-bearing premise is justified solely by the authors' own prior work; CoqQ [75] is used as a formalization library whose soundness theorems are machine-checked, which counts as independent evidence under the review rules.

Assumptions & free parameters 0 free parameters · 7 assumptions · 0 invented entities

The central results rest on standard mathematical facts (Tarski, Newman) and on the paper's own semantic model for DN. The main unproven assumptions are the completeness conjecture for R_DN and the termination/confluence of the extended big-sum algorithm, both of which are acknowledged by the authors. No new physical entities are postulated; the invented 'dynamic typing' operator is a technical device in the formalization, not an empirical entity.

assumptions (7)
  • domain assumption Finite-dimensional Hilbert spaces are isomorphic to C^n; the theory DN is restricted to such spaces and the decidability proof fixes the dimensions.
    The decidability result Theorem 6.2 and the whole semantic model are built on finite-dimensional Hilbert spaces. The abstract omits the 'fixed finite dimension' caveat, which is a real limitation.
  • standard math Tarski's theorem: the first-order theory of real closed fields is decidable.
    Used in the proof of Theorem 6.2 to conclude decidability after reducing DN to the theory of complex numbers.
  • standard math Newman's lemma: for a terminating abstract rewrite system, local confluence implies confluence.
    Invoked in Section 4.1 and used to derive unique normal forms from the AProVE/CiME2 results.
  • domain assumption The outputs of the automated tools AProVE (termination) and CiME2 (local confluence) are correct.
    The paper states the tools confirmed termination and that all 1501 critical pairs are joinable, but the correctness of these tool runs is not machine-checked inside the paper's own formal development.
  • ad hoc to paper Relative completeness of R_DN, stated as Conjecture 7.5.
    The paper's claim to decide equalities efficiently depends on this conjecture for the core language. The authors prove only a weaker completeness result (Appendix D) and explicitly state they failed to prove the general theorem.
  • ad hoc to paper The extended rewrite system R_DNE is terminating and confluent enough for the algorithm of Definition 8.3 to produce a decision procedure.
    The paper explicitly does not prove termination or confluence for R_DNE, so the extended algorithm is a heuristic. Its correctness as a decision procedure is therefore an unproven assumption.
  • domain assumption The atomic basis signature is finite, avoiding problems of infinite-dimensional Hilbert spaces.
    Used throughout to justify the basis decomposition axioms and to make index sets for big sums finite.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Automating Equational Proofs in Dirac Notation." pith.science (2026). https://pith.science/paper/YYT2YVHI

@misc{pith2026241111617,
  author       = {Pith},
  title        = {Pith review of: Automating Equational Proofs in Dirac Notation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YYT2YVHI}},
  note         = {Machine review of arXiv:2411.11617}
}
read the original abstract

Dirac notation is widely used in quantum physics and quantum programming languages to define, compute and reason about quantum states. This paper considers Dirac notation from the perspective of automated reasoning. We prove two main results: first, the first-order theory of Dirac notation is decidable, by a reduction to the theory of real closed fields and Tarski's theorem. Then, we prove that validity of equations can be decided efficiently, using term-rewriting techniques. We implement our equivalence checking algorithm in Mathematica, and showcase its efficiency across more than 100 examples from the literature.

Figures

Figures reproduced from arXiv: 2411.11617 by the authors.

Figure 1
Figure 1. Proof snippet of HHL algorithm in Quantum Hoare Logic. The snippet is taken from [ [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Screenshot from [14] (left) and [75] (right). The left one is the formalization of the no-cloning theorem in Isabelle, while the right one contains Hoare triples for the correctness of programs in Coq. These shortcomings are overcome by Dirac notation [23], which provides an expressive syntax for quantum states and operators. The syntax of Dirac critically exploits the algebraic structure of quantum states and linea… view at source ↗
Figure 3
Figure 3. The inference rules of equational logic. [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figures from the paper (11 more)
Figure 4
Figure 4. Figure 4: Typing rules for DN. of operators can be understood as the conjugate transpose in the matrix view, which swaps the domain and codomain. 5.3 Denotational Semantics Types and expressions of DN can be given denotational semantics using Hilbert spaces. Definition 5.4 (Inte…
Figure 5
Figure 5. Figure 5: Denotational semantics of DN expressions. Symbol [PITH_FULL_IMAGE:figures/full_fig_p012_5.png]
Figure 6
Figure 6. Figure 6: Axiomatic semantics of DN. Associativity is marked in blue, and commutativity is marked in red. [PITH_FULL_IMAGE:figures/full_fig_p013_6.png]
Figure 7
Figure 7. Figure 7: A selection of representative rules from [PITH_FULL_IMAGE:figures/full_fig_p016_7.png]
Figure 8
Figure 8. Figure 8: Extra typing rules for DNE. The denotational semantics of DNE is defined in [PITH_FULL_IMAGE:figures/full_fig_p018_8.png]
Figure 9
Figure 9. Figure 9: Denotational semantics of DNE symbols. 8.1 Equivalence Checking Algorithm Checking the equivalence of expressions with big operators requires more advanced techniques. The equivalence checking algorithm of DNE is a combination of conditional rewriting rules, one￾pass e…
Figure 10
Figure 10. Figure 10: A selection of representative rules from [PITH_FULL_IMAGE:figures/full_fig_p020_10.png]
Figure 11
Figure 11. Figure 11: Axioms beyong 𝑅DNE. 𝑋 represents terms from scalar, ket, bra, or operator sorts. All bind variables 𝑖, 𝑗 are different. Finally, the overall algorithm for deciding the equivalence of extended language expressions is described below. Definition 8.3. Let 𝑒1 and 𝑒2 be tw…
Figure 12
Figure 12. Figure 12: The code for Example 3.1 is given on the left. Variables are marked in blue, symbols introduced in DiracDec are marked in brown, and definitions in the field are marked in purple. The explanations for each command are given on the right. corresponding to 𝐴 𝑇 ≜ Í 𝑖 Í 𝑗…
Figure 13
Figure 13. Figure 13: An example of two equivalent parametrised quantum circuits and their Dirac notation representations. [PITH_FULL_IMAGE:figures/full_fig_p026_13.png]
Figure 14
Figure 14. Figure 14: An illustration of Theorem C.9 proof. Solid, dashed and dotted lines represent rewritings in 𝑅DN, 𝑅 ′ DN and the type erasure respectively. Blue, red, yellow and green surfaces represent the application of Lemma C.5, Lemma C.6, Lemma C.4 and Lemma C.7 respectively. Pr…

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. An Effective Quantum Hoare Logic for Hybrid Quantum Programs with Unbounded Loops

    quant-ph 2026-07 conditional novelty 6.5 of 10

    Integer hybrid path-sums plus a sound Hoare logic enable semi-automated functional verification and expected-cost analysis of hybrid quantum programs with unbounded while loops.

  2. Certified Misty-State Rewriting (A Question-and-Answer Guide)

    physics.pop-ph 2026-08 conditional novelty 3.0 of 10

    Misty-state terms are assigned an unnormalized-amplitude semantics with scoped normalization, canonical normal forms, and branch-based measurement, so the notation's rewrites become exactly checkable.

Reference graph

Works this paper leans on

79 extracted references · 29 canonical work pages · cited by 2 Pith papers

  1. [1]

    Samson Abramsky and Bob Coecke. 2004. A Categorical Semantics of Quantum Protocols. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings . IEEE Computer Society, 415–425. https://doi.org/10.1109/LICS.2004.1319636

    arXiv 2004

  2. [2]

    Matthew Amy. 2019. Towards Large-scale Functional Verification of Universal Quantum Circuits.Electronic Proceedings in Theoretical Computer Science 287 (Jan. 2019), 1–21. https://doi.org/10.4204/eptcs.287.1

    doi:10.4204/eptcs.287.1 2019

  3. [3]

    Matthew Amy. 2023. Complete Equational Theories for the Sum-Over-Paths with Unbalanced Amplitudes. Electronic Proceedings in Theoretical Computer Science 384 (Aug. 2023), 127–141. https://doi.org/10.4204/eptcs.384.8

    doi:10.4204/eptcs.384.8 2023

  4. [4]

    Pablo Arrighi and Gilles Dowek. 2005. A Computational Definition of the Notion of Vectorial Space. Electronic Notes in Theoretical Computer Science 117 (1 2005), 249–261. Issue SPEC. ISS.. https://doi.org/10.1016/J.ENTCS.2004.06.013

    work page doi:10.1016/j.entcs.2004.06.013 2005

  5. [5]

    Pablo Arrighi and Gilles Dowek. 2017. Lineal: A linear-algebraic Lambda-calculus. Logical Methods in Computer Science Volume 13, Issue 1 (3 2017), 1–33. Issue 1. https://doi.org/10.23638/LMCS-13(1:8)2017

    doi:10.23638/lmcs-13(1:8)2017 2017

  6. [6]

    Thomas Arts and Jürgen Giesl. 2000. Termination of term rewriting using dependency pairs. Theoretical Computer Science 236 (4 2000), 133–178. Issue 1-2. https://doi.org/10.1016/S0304-3975(99)00207-8

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

  7. [7]

    Miriam Backens and Aleks Kissinger. 2018. ZH: A Complete Graphical Calculus for Quantum Computations Involving Classical Non-linearity. In Proceedings 15th International Conference on Quantum Physics and Logic, QPL 2018, Halifax, Canada, 3-7th June 2018 (EPTCS, Vol. 287) , Peter Selinger and Giulio Chiribella (Eds.). 23–42. https://doi.org/10.4204/ EPTCS.287.2

    work page 2018

  8. [8]

    Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou. 2019. Relational Proofs for Quantum Programs. Proc. ACM Program. Lang. 4, POPL, Article 21 (December 2019), 29 pages. https://doi.org/10.1145/3371089

    doi:10.1145/3371089 2019

Show all 79 references
  1. [9]

    Fabian Bauer-Marquart, Stefan Leue, and Christian Schilling. 2023. symQV: Automated Symbolic Verification of Quan- tum Programs. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 14000 LNCS (202...

    2023 doi

  2. [10]

    Dan Benanav, Deepak Kapur, and Paliath Narendran. 1987. Complexity of matching problems. Journal of Symbolic Computation 3, 1 (1987), 203–216. https://doi.org/10.1016/S0747-7171(87)80027-5

    1987 doi

  3. [11]

    Yves Bertot, Georges Gonthier, Sidi Ould Biha, and Ioana Pasca. 2008. Canonical big operators. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 5170 LNCS (2008), 86–101. https://doi.org/10.1007...

    2008 doi

  4. [12]

    Frédéric Blanqui and Adam Koprowski. 2011. CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci. 21, 4 (2011), 827–859. https://doi.org/10.1017/S0960129511000120

    2011 doi

  5. [13]

    Anthony Bordg, Hanna Lachnitt, and Yijun He. 2020. Isabelle marries dirac: A library for quantum computation and quantum information. Archive of Formal Proofs (2020)

    2020

  6. [14]

    Anthony Bordg, Hanna Lachnitt, and Yijun He. 2021. Certified quantum computation in Isabelle/HOL. Journal of Automated Reasoning 65, 5 (2021), 691–709. https://doi.org/10.1007/s10817-020-09584-7

    2021 doi

  7. [16]

    Christophe Chareton, Sébastien Bardin, François Bobot, Valentin Perrelle, and Benoît Valiron. 2021. An Automated Deductive Verification Framework for Circuit-building Quantum Programs. In Programming Languages and Systems: 30th European Symposium on Programming, ESOP 2021, Hel...

    2021

  8. [17]

    Christophe Chareton, Sébastien Bardin, Dong Ho Lee, Benoît Valiron, Renaud Vilmart, and Zhaowei Xu. 2023. Formal Methods for Quantum Algorithms. In Handbook of Formal Analysis and Verification in Cryptography . CRC Press, 319–422. https://cea.hal.science/cea-04479879

    2023

  9. [18]

    Bob Coecke and Ross Duncan. 2008. Interacting Quantum Observables. In Automata, Languages and Programming, Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 298...

    2008 doi

  10. [19]

    George E. Collins. 1976. Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition: a synopsis. SIGSAM Bull. 10, 1 (Feb. 1976), 10–12. https://doi.org/10.1145/1093390.1093393

    1976

  11. [20]

    Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. 2011. Automated certified proofs with CiME3. Leibniz International Proceedings in Informatics, LIPIcs 10 (2011), 21–30. https://doi.org/10.4230/LIPICS. RTA.2011.21/-/STATS

    2011 doi

  12. [21]

    Henzinger, and Andrey Kupriyanov

    Przemyslaw Daca, Thomas A. Henzinger, and Andrey Kupriyanov. 2016. Array Folds Logic. In Computer Aided Verification - 28th International Conference, CA V 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II (Lecture Notes in Computer Science, Vol. 9780) , Swarat ...

    2016 doi

  13. [22]

    Alejandro Díaz-Caro and Gilles Dowek. 2017. Typing Quantum Superpositions and Measurement. In Theory and Practice of Natural Computing , Carlos Martín-Vide, Roman Neruda, and Miguel A. Vega-Rodríguez (Eds.). Springer International Publishing, Cham, 281–293. https://doi.org/10....

    2017 doi

  14. [23]

    Paul Adrien Maurice Dirac. 1939. A new notation for quantum mechanics. InMathematical proceedings of the Cambridge philosophical society, Vol. 35. Cambridge University Press, 416–418. https://doi.org/10.1017/S0305004100021162

    1939 doi

  15. [24]

    Ross Duncan, Aleks Kissinger, Simon Perdrix, and John van de Wetering. 2020. Graph-theoretic Simplification of Quantum Circuits with the ZX-calculus. Quantum 4 (June 2020), 279. https://doi.org/10.22331/q-2020-06-04-279

    2020 doi

  16. [25]

    Alejandro Díaz-Caro, Gilles Dowek, and Juan Pablo Rinaldi. 2019. Two linearities for quantum computing in the lambda calculus. Biosystems 186 (2019), 104012. https://doi.org/10.1016/j.biosystems.2019.104012 Selected papers from the International Conference on the Theory and Pr...

    2019

  17. [26]

    Alejandro Díaz-Caro, Mauricio Guillermo, Alexandre Miquel, and Benoît Valiron. 2019. Realizability in the Unitary Sphere. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) . 1–13. https://doi.org/10.1109/ LICS.2019.8785834

    2019

  18. [27]

    ELLIE D’HONDT and PRAKASH PANANGADEN. 2006. Quantum weakest preconditions. Mathematical Structures in Computer Science 16, 3 (2006), 429–451. https://doi.org/10.1017/S0960129506005251

    2006 doi

  19. [28]

    Mnacho Echenim and Mehdi Mhalla. 2024. A Formalization of the CHSH Inequality and Tsirelson’s Upper-bound in Isabelle/HOL. Journal of Automated Reasoning 68, 1 (2024), 2. https://doi.org/10.1007/s10817-023-09689-9

    2024 doi

  20. [29]

    Yuan Feng and Sanjiang Li. 2023. Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs. Information and Computation 294 (2023), 105077. https://doi.org/10.1016/j.ic.2023.105077

    2023

  21. [30]

    Yuan Feng and Mingsheng Ying. 2021. Quantum Hoare Logic with Classical Variables. ACM Transactions on Quantum Computing 2, 4, Article 16 (Dec. 2021), 43 pages. https://doi.org/10.1145/3456877

    2021 doi

  22. [31]

    Jürgen Giesl, Peter Schneider-Kamp, and René Thiemann. 2006. AProVE 1.2: Automatic termination proofs in the dependency pair framework. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 4130 LNA...

    2006 doi

  23. [32]

    Nicolas Granger. 1999. Stability, Simplicity and the Model Theory of Bilinear Forms . Ph. D. Dissertation. University of Manchester

    1999

  24. [33]

    Alexander S Green, Peter LeFanu Lumsdaine, Neil J Ross, DalCa Peter Selinger, and Beno^ıtBeno^ıt Valiron. [n. d.]. Quipper: a scalable quantum programming language. dl.acm.org ([n. d.]). https://dl.acm.org/doi/abs/10.1145/2491956. 2462177

    doi

  25. [34]

    Harrow, Avinatan Hassidim, and Seth Lloyd

    Aram W. Harrow, Avinatan Hassidim, and Seth Lloyd. 2009. Quantum Algorithm for Linear Systems of Equations. Phys. Rev. Lett. 103 (Oct 2009), 150502. Issue 15. https://doi.org/10.1103/PhysRevLett.103.150502

    2009 doi

  26. [35]

    Masahito Hasegawa, Martin Hofmann, and Gordon D. Plotkin. 2008. Finite Dimensional Vector Spaces Are Complete for Traced Symmetric Monoidal Categories. In Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday (Lecture N...

    2008 doi

  27. [36]

    Kesha Hietala, Sarah Marshall, Robert Rand, and Nikhil Swamy. [n. d.]. Q*: Implementing Quantum Separation Logic in F. ([n. d.])

  28. [37]

    Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, and Michael Hicks. 2021. Proving Quantum Programs Correct. In 12th International Conference on Interactive Theorem Proving (ITP 2021) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 193), Liron Cohen and Ceza...

    2021 doi

  29. [39]

    Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. 2021. A verified optimizer for Quantum circuits. 5, POPL, Article 37 (jan 2021), 29 pages. https://doi.org/10.1145/3434318

    2021 doi

  30. [40]

    Xin Hong, Wei-Jia Huang, Wei-Chen Chien, Yuan Feng, Min-Hsiu Hsieh, Sanjiang Li, and Mingsheng Ying. 2024. Equivalence Checking of Parameterised Quantum Circuits. (2024). arXiv:2404.18456 [quant-ph] https://arxiv.org/abs/ 2404.18456

    2024 arXiv

  31. [41]

    Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu. 2019. Quantitative robustness analysis of quantum programs. 3, POPL, Article 31 (jan 2019), 29 pages. https://doi.org/10.1145/3290344

    2019 doi

  32. [42]

    Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. 2018. A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Oxford, United Kingdom) (LICS ’18). Association for Comp...

    2018

  33. [43]

    Aleks Kissinger and John van de Wetering. 2020. PyZX: Large Scale Automated Diagrammatic Reasoning. Electronic Proceedings in Theoretical Computer Science 318 (May 2020), 229–241. https://doi.org/10.4204/eptcs.318.14 Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 42. Publ...

    2020 doi

  34. [44]

    Ugo Dal Lago, Andrea Masini, and Margherita Zorzi. 2009. Confluence Results for a Quantum Lambda Calculus with Measurements. In Proceedings of the 6th International Workshop on Quantum Physics and Logic, QPL@MFPS 2009, Oxford, UK, April 8-9, 2009 (Electronic Notes in Theoretic...

    2009 doi

  35. [45]

    Ugo Dal Lago, Andrea Masini, and Margherita Zorzi. 2009. On a measurement-free quantum lambda calculus with classical control. Math. Struct. Comput. Sci. 19, 2 (2009), 297–335. https://doi.org/10.1017/S096012950800741X

    2009 doi

  36. [46]

    Xuan-Bach Le, Shang-Wei Lin, Jun Sun, and David Sanan. 2022. A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic. Proc. ACM Program. Lang. 6, POPL, Article 36 (jan 2022), 27 pages. https://doi.org/10.1145/3498697

    2022 doi

  37. [47]

    Adrian Lehmann, Ben Caldwell, and Robert Rand. 2022. VyZX : A Vision for Verifying the ZX Calculus. (2022). arXiv:2205.05781 [quant-ph] https://arxiv.org/abs/2205.05781

    2022 arXiv

  38. [49]

    Marco Lewis, Sadegh Soudjani, and Paolo Zuliani. 2023. Formal Verification of Quantum Programs: Theory, Tools, and Challenges. 5, 1, Article 1 (dec 2023), 35 pages. https://doi.org/10.1145/3624483

    2023 doi

  39. [50]

    Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, and Xiaodi Wu. 2024. Qafny: A Quantum-Program Verifier. (2024). arXiv:2211.06411 [quant-ph] https://arxiv.org/abs/2211.06411

    2024 arXiv

  40. [51]

    Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. 2019. Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. InComputer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer International Pu...

    2019 doi

  41. [52]

    Angus Macintyre and Alex J. Wilkie. 1996. On the Decidability of the Real Exponential Field. In Kreiseliana: About and Around Georg Kreisel, Piergiorgio Odifreddi (Ed.). A K Peters, 441–467

    1996

  42. [53]

    Equivalence

    M. H. A. Newman. 1942. On Theories with a Combinatorial Definition of "Equivalence". Annals of Mathematics 43, 2 (1942), 223–243. https://doi.org/10.2307/1968867

    1942 doi

  43. [54]

    Nielsen and Isaac L

    Michael A. Nielsen and Isaac L. Chuang. 2010. Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press. https://doi.org/10.1017/CBO9780511976667

    2010 doi

  44. [55]

    Enno Ohlebusch. 2002. Advanced topics in term rewriting . Springer Science & Business Media. https://doi.org/10.1007/ 978-1-4757-3661-8

    2002

  45. [56]

    Jens Palsberg and Nengkun Yu. 2024. Optimal implementation of quantum gates with two controls. Linear Algebra Appl. 694 (2024), 206–261. https://doi.org/10.1016/j.laa.2024.03.039

    2024 doi

  46. [57]

    Jennifer Paykin, Robert Rand, and Steve Zdancewic. 2017. QWIRE: a core language for quantum circuits. ACM SIGPLAN Notices 52 (5 2017), 846–858. Issue 1. https://doi.org/10.1145/3093333.3009894

    2017

  47. [58]

    Shaikh, Lia Yeh, Richie Yeung, and Bob Coecke

    Boldizsár Poór, Quanlong Wang, Razin A. Shaikh, Lia Yeh, Richie Yeung, and Bob Coecke. 2023. Completeness for arbitrary finite dimensions of ZXW-calculus, a unifying calculus. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) . 1–14. https://doi.org/10...

    2023

  48. [59]

    Robert Rand, Jennifer Paykin, and Steve Zdancewic. 2017. QWIRE Practice: Formal Verification of Quantum Circuits in Coq. In Proceedings 14th International Conference on Quantum Physics and Logic, QPL 2017, Nijmegen, The Netherlands, 3-7 July 2017. (EPTCS, Vol. 266) , Bob Coeck...

    2017 doi

  49. [60]

    Rodrigo Raya and Viktor Kuncak. 2024. On algebraic array theories. J. Log. Algebraic Methods Program. 136 (2024), 100906. https://doi.org/10.1016/J.JLAMP.2023.100906

    2024

  50. [61]

    Peter Selinger. 2008. Finite Dimensional Hilbert Spaces are Complete for Dagger Compact Closed Categories (Extended Abstract). In Proceedings of the Joint 5th International Workshop on Quantum Physics and Logic and 4th Workshop on Developments in Computational Models, QPL/DCM@...

    2008

  51. [62]

    Kartik Singhal, ROBERT Rand, and MATTHEW Amy. 2022. Beyond separation: Toward a specification language for modular reasoning about quantum programs. Programming Languages for Quantum Computing (PLanQC) 2022 Poster Abstract (2022)

    2022

  52. [63]

    Robert Solovay, R. D. Arthan, and John Harrison. 2012. Some new results on decidability for elementary algebra and geometry. Ann. Pure Appl. Log. 163, 12 (2012), 1765–1802. https://doi.org/10.1016/J.APAL.2012.04.003

    2012 doi

  53. [65]

    Alfred Tarski. 1998. A Decision Method for Elementary Algebra and Geometry. In Quantifier Elimination and Cylindrical Algebraic Decomposition, Bob F. Caviness and Jeremy R. Johnson (Eds.). Springer Vienna, Vienna, 24–84. https://doi.org/10.1007/978-3-7091-9459-1_3 Proc. ACM Pr...

    1998 doi

  54. [66]

    The MathComp Analysis Development Team. 2022. MathComp-Analysis: Mathematical Components compliant Analysis Library. https://github.com/math-comp/analysis. Since 2017. Version 0.5.1

    2022

  55. [67]

    Dominique Unruh. 2019. Quantum Hoare Logic with Ghost Variables. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) . 1–13. https://doi.org/10.1109/LICS.2019.8785779

    2019

  56. [68]

    Dominique Unruh. 2019. Quantum Relational Hoare Logic. Proc. ACM Program. Lang. 3, POPL, Article 33 (jan 2019), 31 pages. https://doi.org/10.1145/3290346

    2019 doi

  57. [69]

    John van de Wetering. 2020. ZX-calculus for the working quantum computer scientist. arXiv:2012.13966 [quant-ph] https://arxiv.org/abs/2012.13966

    2020 arXiv

  58. [70]

    Renaud Vilmart. 2023. Completeness of Sum-Over-Paths for Toffoli-Hadamard and the Dyadic Fragments of Quantum Computation. In 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, February 13-16, 2023, Warsaw, Poland (LIPIcs, Vol. 252) , Bartek Klin and Elaine Pime...

    2023 doi

  59. [71]

    Mingsheng Ying. 2012. Floyd–hoare logic for quantum programs. ACM Trans. Program. Lang. Syst. 33, 6, Article 19 (Jan. 2012), 49 pages. https://doi.org/10.1145/2049706.2049708

    2012

  60. [72]

    Mingsheng Ying. 2016. Foundations of quantum programming . Morgan Kaufmann

    2016

  61. [73]

    Nengkun Yu and Jens Palsberg. 2021. Quantum Abstract Interpretation. In Proceedings of the 42nd ACM SIGPLAN Inter- national Conference on Programming Language Design and Implementation (Virtual, Canada) (PLDI 2021). Association for Computing Machinery, New York, NY, USA, 542–5...

    2021

  62. [74]

    Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, and Nengkun Yu. 2021. A Quantum Interpretation of Bunched Logic & Quantum Separation Logic. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) . 1–14. https://doi.org/10.1109/LICS52264.2021.9470673

    2021

  63. [75]

    Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying. 2023. CoqQ: Foundational Verification of Quantum Programs. Proc. ACM Program. Lang. 7, POPL, Article 29 (jan 2023), 33 pages. https://doi.org/10.1145/3571222

    2023 doi

  64. [76]

    Li Zhou, Nengkun Yu, and Mingsheng Ying. 2019. An applied quantum Hoare logic. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (Phoenix, AZ, USA) (PLDI 2019). Association for Computing Machinery, New York, NY, USA, 1149–1162....

    2019

  65. [77]

    These two properties suggest the syntactical completeness of our language, meaning that all terms will be rewritten into the unique normal form after finite steps by𝑅DN

    ⊲ (𝑂1·𝑂′ 1)⊗( 𝑂2·𝑂′ 2) (𝑂1⊗𝑂2)·(( 𝑂′ 1⊗𝑂′ 2)· 𝑂3) ⊲ ((𝑂1·𝑂′ 1)⊗( 𝑂2·𝑂′ 2))· 𝑂3 C Confluence and Termination of 𝑅DN In this section, we prove the confluence and termination of𝑅DN. These two properties suggest the syntactical completeness of our language, meaning that all terms ...

    2025

  66. [78]

    Then, by Lemma C.7,𝑍1 =𝑍2, which finishes the confluence proof

    Since the rewritings of𝑅DN preserve the types,𝑍1 and𝑍2 will have the same type as𝑋 . Then, by Lemma C.7,𝑍1 =𝑍2, which finishes the confluence proof. □ D Completeness of 𝑅DN Completeness of the rewriting system means that terms with equivalent denotational semantics will have t...

    2025

  67. [79]

    Otherwise𝑛𝑓(𝑎1) is a summation, and we apply the propagation rules of conjugate on𝑎+𝑏 and𝑎×𝑏, so that we only need to consider whether∀𝑎∈ 𝑎×,𝑛𝑓(𝑎∗)∈ 𝑎×

    If𝑛𝑓(𝑎1) = 0, we have the 0∗ ⊲ 0 rule. Otherwise𝑛𝑓(𝑎1) is a summation, and we apply the propagation rules of conjugate on𝑎+𝑏 and𝑎×𝑏, so that we only need to consider whether∀𝑎∈ 𝑎×,𝑛𝑓(𝑎∗)∈ 𝑎×. This is true by the following rules: (𝑎∗)∗ ⊲ 𝑎,𝛿∗ 𝑠,𝑡 ⊲ 𝛿𝑠,𝑡 , (𝐵·𝐾)∗ ⊲ 𝐾†·𝐵† and pro...

    2025

  68. [80]

    They are semantically different because𝑎+ 1 = 1 will never be valid. Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 42. Publication date: January 2025. 42:46 Yingte Xu, Gilles Barthe, and Li Zhou • 1+𝑎+ 1 and 1+𝑎+

    2025

  69. [81]

    • 1+𝑎+ 1 and𝑎+ 1+𝑎+

    Reduced to the Lemma D.7 case. • 1+𝑎+ 1 and𝑎+ 1+𝑎+

  70. [82]

    • 1+𝑎+ 1 and𝑎+ 2+𝑎+

    Also because𝑎+ 2 = 1 will never be valid. • 1+𝑎+ 1 and𝑎+ 2+𝑎+

  71. [83]

    scalar rewrite system

    By further case analysis on𝑎1,𝑎2 and𝑎3. • Other cases are similar. (b)𝑚 ≠𝑛, the analysis is similar. □ Concluding the results above, we have the weak completeness theorem. Theorem D.9. The extended term-rewriting system 𝑅DN is semantically complete. Proof. Combining Lemma D.5 ...

    2025

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.