A Complete Equational Presentation of Qudit Circuits via Polycontrolled PROPs

TL;DR

This paper introduces the first finite, sound, and complete equational theory for exact unitary qudit circuits, enabling precise reasoning about high-dimensional quantum computations at the circuit level.

Contribution

It provides a novel, finite, and dimension-uniform equational framework for qudit circuits, incorporating primitive value-control for native circuit reasoning.

Findings

The theory is sound and complete for all finite qudit dimensions.

Circuits are built from local gates, composition, and value-controls.

Equality corresponds exactly to having the same unitary semantics.

Abstract

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.