Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Polycontrolled PROPs for Qudit Circuits: A Uniform Complete Equational Theory For Arbitrary Finite Dimension

Colin Blake

TL;DR

This work delivers a dimension-uniform, finitary equational theory for unitary qudit circuits by introducing a polycontrolled circuit PROP $\textbf{CQC}_d$ with a primitive control constructor. It constructs a finite axiom system $\mathrm{QC}_d$, uniform in dimension, and proves it sound and complete for the standard unitary semantics via a modular reduction to the linear-optical calculus $\textbf{LOPP}$ using a Gray-code embedding. The core idea is to treat control as a primitive, enabling bounded-arity schemata and a clean completeness proof that generalizes known qubit results to arbitrary finite $d$. The completeness result relies on a robust encoding/decoding pipeline (Gray-code based) and a mimicking argument that transfers all $\textbf{LOPP}$ derivations back into $\mathrm{QC}_d$, yielding a practical, circuit-level rewriting framework for native qudit hardware with resource-efficient compilation and verification potential.

Abstract

We present a finite schematic axiomatisation of quantum circuits over d-level systems (qudits), uniform in every finite dimension d >= 2. For each d we define a PROP equipped with a family of control functors, treating control as a primitive categorical constructor. Using a translation between qudit circuits and the LOPP calculus for linear optics based on d-ary Gray codes, we obtain for each d a finite set of local axiom schemata that is sound and complete for unitary d-level circuits: two circuits denote the same unitary if and only if they are inter-derivable using axioms involving at most three wires. The generators are compatible with standard universal qudit gate families, yielding a sound equational basis for circuit rewriting and optimisation-by-rewriting. Conceptually, this extends the qubit circuit completeness results of Clément et al.\ to arbitrary finite dimension, and instantiates the control-as-constructor approach of Delorme and Perdrix in this setting, while keeping the axiom shapes uniform in d.

Polycontrolled PROPs for Qudit Circuits: A Uniform Complete Equational Theory For Arbitrary Finite Dimension

TL;DR

This work delivers a dimension-uniform, finitary equational theory for unitary qudit circuits by introducing a polycontrolled circuit PROP with a primitive control constructor. It constructs a finite axiom system , uniform in dimension, and proves it sound and complete for the standard unitary semantics via a modular reduction to the linear-optical calculus using a Gray-code embedding. The core idea is to treat control as a primitive, enabling bounded-arity schemata and a clean completeness proof that generalizes known qubit results to arbitrary finite . The completeness result relies on a robust encoding/decoding pipeline (Gray-code based) and a mimicking argument that transfers all derivations back into , yielding a practical, circuit-level rewriting framework for native qudit hardware with resource-efficient compilation and verification potential.

Abstract

We present a finite schematic axiomatisation of quantum circuits over d-level systems (qudits), uniform in every finite dimension d >= 2. For each d we define a PROP equipped with a family of control functors, treating control as a primitive categorical constructor. Using a translation between qudit circuits and the LOPP calculus for linear optics based on d-ary Gray codes, we obtain for each d a finite set of local axiom schemata that is sound and complete for unitary d-level circuits: two circuits denote the same unitary if and only if they are inter-derivable using axioms involving at most three wires. The generators are compatible with standard universal qudit gate families, yielding a sound equational basis for circuit rewriting and optimisation-by-rewriting. Conceptually, this extends the qubit circuit completeness results of Clément et al.\ to arbitrary finite dimension, and instantiates the control-as-constructor approach of Delorme and Perdrix in this setting, while keeping the axiom shapes uniform in d.
Paper Structure (45 sections, 39 theorems, 311 equations, 9 figures, 1 algorithm)

This paper contains 45 sections, 39 theorems, 311 equations, 9 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Qudit circuits as a polycontrolled PROP
  3. PROPs and (poly)controlled PROPs
  4. Raw circuits and the PROP CQC
  5. Qudit semantics
  6. Universality
  7. Equational theories on CQC_d
  8. A Finite Axiom System for Qudit Circuits
  9. Derived gates used in the axiom schemata
  10. The axiom schemata and how to read them
  11. Derived control-algebra laws
  12. Embedding Qudit Circuits into LOPP Circuits
  13. The LOPP calculus as a semantic model
  14. Gray codes for mode ordering
  15. Contextual encoding of quantum circuits
  16. ...and 30 more sections

Key Result

Proposition 2.10

The interpretation $\left\llbracket \cdot \right\rrbracket:\textbf{CQC}^{\textup{raw}}_d(n,n)\to\textbf{Qudit}_d(n,n)$ respects the structural congruence $\equiv$ of Definition def:structural-congruence-CQC_d. Hence it factors uniquely through the quotient to a well-defined strict symmetric monoidal satisfying $\left\llbracket [C]_{\equiv} \right\rrbracket=\left\llbracket C \right\rrbracket$ for e

Figures (9)

  • Figure 1: Core axiom schemata for $\mathrm{QC}_{d}$. In \ref{['eulerH']}, \ref{['3Rx']} and \ref{['3CRx']} the right-hand-side angles are determined by the explicit relations recorded in Appendix \ref{['appendix:relations_angles']}. Rules \ref{['XH']}, \ref{['Hphasecomm']}, and \ref{['Hcnot']} apply when the indices $i,j,k$ are pairwise distinct. In \ref{['HHcomm']} the indices $i,j,k,\ell$ are pairwise distinct.
  • Figure 2: Auxiliary axiom schemata for $\mathrm{QC}_{d}$. (1) "Totalisation" rules \ref{['axiom-total-phase']} and \ref{['axiom-total-hadamard']}, used to recover exhaustivity of control by a structural induction on circuits. If one takes exhaustivity as an admissible rule schema, then (TP) and (TH) are immediate instances and can be omitted. (2) Local commutation/conjugation schemata for differently-controlled operations: \ref{['cp-cp']}, \ref{['cp-cnot']}, \ref{['cnot-cnot']}, \ref{['cnot-cnot-diff']}, \ref{['ch-ccp']}, \ref{['ch-ccnot']}, \ref{['ch-ch']} require $k\neq \ell$. These patterns are redundant once one is allowed to use distinct-control commutativity as a derived rule. (3) The mixed-control swap schemata \ref{['axiom-compat']} and \ref{['axiom-compat-pi']}. If compatibility were assumed as an ambient (structural) principle of $\textbf{CQC}_d$, then \ref{['axiom-compat']} and \ref{['axiom-compat-pi']} would be derivable and could be omitted.
  • Figure 3: Derived rules in $\mathrm{QC}_d$ (batch 1).
  • Figure 4: Derived rules in $\mathrm{QC}_d$ (batch 2).
  • Figure 5: Derived rules in $\mathrm{QC}_d$ (batch 3).
  • ...and 4 more figures

Theorems & Definitions (148)

  • Definition 2.1: Saunders
  • Definition 2.2: delorme-perdrix-control
  • Definition 2.3: delorme-perdrix-control
  • Definition 2.4
  • Definition 2.5
  • Definition 2.6
  • Definition 2.7
  • Definition 2.8
  • Definition 2.9
  • Proposition 2.10
  • ...and 138 more