A Complete Equational Presentation of Qudit Circuits via Polycontrolled PROPs

Technical Summary: A Complete Equational Presentation of Qudit Circuits via Polycontrolled PROPs

Problem Statement
High-dimensional quantum computation utilizing qudits (quantum systems with dimension $d \geq 2$) lacks a native, finite, schematic equational theory at the circuit level. While graphical calculi (such as ZX/ZW) offer completeness for broader classes of linear maps, they often require a separate reconstruction step to recover standard unitary circuits. Existing circuit-level results for qudits are specialized (e.g., restricted to Clifford fragments or diagonal gates) or rely on unbounded axiom sets where control wires proliferate. The core challenge is to define a circuit presentation where equality is derivable exactly when standard unitary denotations agree, using a finite list of local axiom schemata whose diagrammatic shape is uniform across all dimensions $d$.

Methodology
The paper constructs a polycontrolled PROP (Product and Permutation category), denoted $\mathbf{CQC}_d$, to model qudit circuits. The methodology proceeds through three main stages:

1. Syntax and Semantics:

   • The syntax is built from local gates (scalar phases and adjacent two-level Hadamards), sequential/parallel composition, and primitive value-controls. Unlike previous approaches where control is a derived operation, here a control functor $C_k$ for each basis value $k \in [d]$ is a primitive constructor.
   • The semantics map these circuits to unitary operators on $(\mathbb{C}^d)^{\otimes n}$, denoted $\mathbf{Qudit}_d$.
   • The authors define an equational theory $\mathbf{QC}_d$ generated by a finite set of local axiom schemata (Figures 2 and 3). These schemata involve at most three wires and are uniform in $d$, with dimension dependence restricted to level labels and product-frame ranges.

2. Derivation of Control Algebra:

   • The structural congruence of $\mathbf{CQC}_d$ initially only enforces laws for a single control value. The paper proves that the finite axiom system $\mathbf{QC}_d$ is sufficient to derive the global control-algebra laws: compatibility (swapping nested controls of different values), commutativity (operations on disjoint branches commute), and exhaustivity (the composition of all value-controlled branches equals the identity).
   • This derivation relies on a "factor normalisation" lemma, reducing arbitrary controlled circuits to sequential products of contextual "G-factors" (generators and their controlled versions).

3. Completeness via Transfer to Linear Optics:

   • To prove completeness, the authors employ a transfer argument embedding qudit circuits into single-photon linear optical circuits (LOPP).
   • They utilize a reflected $d$-ary Gray code to map the $d^n$ computational basis states of an $n$-qudit register to $d^n$ optical modes. This ordering ensures that adjacent optical modes correspond to adjacent two-level qudit transitions (possibly under controls).
   • The proof constructs an encoding $E$ from qudit circuits to LOPP circuits and a decoding $D$ in the reverse direction.
   • Leveraging the known completeness of LOPP for single-photon unitaries, the authors show that if two qudit circuits have equal unitary semantics, their encodings are equal in LOPP. The decoding of this optical equality, combined with the derived control algebra and the retraction property ($D(E(C)) = C$), yields the equality in $\mathbf{QC}_d$.

Key Contributions

• First Finite Schematic Theory: The paper provides the first finite, schematic, and bounded-arity equational theory that is sound and complete for exact unitary qudit circuits in every finite dimension $d \geq 2$.
• Primitive Value-Control: By treating value-control as a primitive constructor rather than a derived syntactic sugar, the authors avoid the "blow-up" of control wires often seen in completeness proofs. This allows the axiom set to remain finite and dimension-uniform.
• Dimension-Uniformity: The diagrammatic shape of the axioms does not depend on $d$. The dimensionality is encoded solely in the range of indices and product frames, making the theory scalable and uniform.
• Internal Derivation of Control Laws: The paper demonstrates that compatibility, commutativity, and exhaustivity—properties often assumed as axioms in control-heavy frameworks—are derivable from a local, finite set of rules within the circuit PROP.
• Gray-Ordered Transfer: The use of reflected Gray order to bridge qudit circuits and linear optics is a novel technical contribution that preserves locality and allows the transfer of completeness results from the optical domain to the qudit domain.

Results
The main theorem (Theorem 4.17) establishes that for any $d \geq 2$ and any two $n$-qudit circuits $C_1, C_2$:
$$\llbracket C_1 \rrbracket = \llbracket C_2 \rrbracket \iff \mathbf{QC}_d \vdash C_1 = C_2$$
where $\llbracket \cdot \rrbracket$ is the standard unitary denotation. The theory $\mathbf{QC}_d$ is proven to be sound (axioms preserve semantics) and complete (semantic equality implies derivability).

Significance
The paper claims to provide a foundational tool for circuit-level rewriting in high-dimensional quantum computing. By establishing a native equational theory, it enables compilers and verifiers to reason about local transformations (such as introducing value-controls or adjacent two-level gates) without needing to reconstruct the entire circuit or rely on external graphical calculi. The work addresses the specific difficulty of extending qubit completeness proofs to qudits, where binary shortcuts fail and structured control management is required. The authors position this as a necessary step for exploiting native high-dimensional hardware (e.g., trapped-ion processors) and for optimizing algorithms that utilize qudit workspace to reduce circuit depth or ancilla requirements.