Colin Blake

Colin Blake

High-dimensional quantum computation needs a native circuit-level equational theory for qudits. We give the first finite schematic equational theory that is sound and complete for exact unitary qudit circuits in every finite dimension at least two. The result is entirely circuit-level: circuits are built from local gates, sequential and parallel composition, and value-controls, and equality is derivable exactly when two circuits have the same standard unitary semantics. For each dimension, the theory is presented by a finite family of local bounded-arity axiom schemata whose diagrammatic shapes are uniform in the dimension. The key syntactic ingredient is primitive value-control, which builds control on a chosen basis value directly into the language. This gives the language a useful internal algebra of controlled operations from local rules while keeping the presentation native to qudit circuits. The result provides a finite, dimension-uniform foundation for exact equational reasoning about qudit circuits.

Colin Blake

Equational reasoning is central to quantum circuit optimisation and verification: one replaces subcircuits by provably equivalent ones using a fixed set of rewrite rules viewed as equations. A finite rule set is most informative when it separates the genuine algebra of a circuit fragment from the structural treatment of wires. This paper gives six near-Clifford fragments a common PROP treatment, where wire permutations are structural: qubit Clifford, real Clifford, Clifford+T (up to two qubits), Clifford+CS (up to three qubits), CNOT-dihedral, and qutrit Clifford. Starting from prior completeness theorems, we transfer completeness into this setting and remove redundant non-structural rules, then check minimality by separating interpretations tailored to individual axioms; the resulting presentations are minimal in all arities for qubit Clifford, real Clifford, and CNOT-dihedral, minimal in bounded ranges for the remaining fragments, and comparable by one transfer-and-separation pattern.