Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Renaud Vilmart

TL;DR

This work develops a complete rewrite framework for the Sum-Over-Paths (SOP) formalism within the balanced Toffoli-Hadamard fragment and extends completeness to all dyadic fragments of quantum computation by leveraging the ZH-calculus. It establishes translations between SOP and ZH, showing that TH completeness in ZH transfers to SOP, and introduces reversible dyadic level upgrades that connect different dyadic fragments. The paper also provides methods to sum and concatenate SOP-morphisms via controlled morphisms, enabling Hamiltonian-style constructions within SOP. Key findings include termination of the TH rewrite system, its non-confluence, and a complete, scalable approach to dyadic completeness with practical graphical interpretations. This work advances symbolic verification and Hamiltonian-based quantum computation by unifying SOP with ZH and enabling complex term manipulations within dyadic phase regimes.

Abstract

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

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

TL;DR

This work develops a complete rewrite framework for the Sum-Over-Paths (SOP) formalism within the balanced Toffoli-Hadamard fragment and extends completeness to all dyadic fragments of quantum computation by leveraging the ZH-calculus. It establishes translations between SOP and ZH, showing that TH completeness in ZH transfers to SOP, and introduces reversible dyadic level upgrades that connect different dyadic fragments. The paper also provides methods to sum and concatenate SOP-morphisms via controlled morphisms, enabling Hamiltonian-style constructions within SOP. Key findings include termination of the TH rewrite system, its non-confluence, and a complete, scalable approach to dyadic completeness with practical graphical interpretations. This work advances symbolic verification and Hamiltonian-based quantum computation by unifying SOP with ZH and enabling complex term manipulations within dyadic phase regimes.

Abstract

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

This paper contains 22 sections, 32 theorems, 126 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Sums-Over-Paths
  3. The Morphisms
  4. A Rewrite System
  5. Generalising Rules
  6. The $\mathbf{ZH}$-Calculus
  7. The Diagrams and their Interpretation
  8. Equational Theory
  9. Translations between $\mathbf{SOP}$ and $\mathbf{ZH}$
  10. From $\mathbf{SOP}$ to $\mathbf{ZH}$
  11. From $\mathbf{ZH}$ to $\mathbf{SOP}$
  12. Restrictions of $\mathbf{SOP}$
  13. The Rewrite System $\underset{\operatorname{TH}}\longrightarrow$, Graphically
  14. Completeness for Toffoli-Hadamard
  15. Completeness for the Dyadic Fragment
  16. ...and 7 more sections

Key Result

Proposition 2.5

Figures (2)

  • Figure 1: Rewrite system $\xrightarrow[\substack{\text{TH}}]{}$
  • Figure 2: Set of rules $\operatorname{ZH}_{\operatorname{TH}}$backens2021ZHcompleteness.

Theorems & Definitions (80)

  • Definition 2.1: $\mathbf{SOP}$
  • Remark 2.2
  • Example 2.3
  • Example 2.4
  • Proposition 2.5
  • proof
  • Corollary 2.6
  • Proposition 2.7: Soundness
  • proof
  • Example 2.8
  • ...and 70 more