PaperlayerView exact revision on arXiv

Source-linked AI summary

Controlled PROP: Theory and Applications to Quantum Circuits

Noé Delorme, Simon Perdrix

arXiv:2610.23192v1quant-phcs.LO

TL;DR

Quantum and reversible computation use control, but standard PROP axiomatizations do not treat it as a constructor. The paper introduces controlled PROPs and applies them to quantum circuits, giving complete axiomatizations with bounded-qubit axioms where standard PROP completeness requires axioms at every arity.

  • Problem

    Standard PROP axiomatizations for quantum circuits require axioms involving n qubits for every n, despite the central role of controlled operations in diagrammatic reasoning.

    Source: §1.2 · p. 2, §5 · p. 16

  • Method

    The paper extends PROPs with control functors and uses controlled and conjugated-controlled PROPs to formalize control in quantum circuits.

    Source: §1.1 · p. 2, §1.2 · p. 2

  • Results

    Controlled-PROP quantum-circuit axiomatizations are complete with bounded-qubit axioms, unlike standard PROP axiomatizations, which require axioms involving arbitrarily many qubits.

    Source: §1.2 · p. 3, §5 · p. 16, §6.3 · p. 22

  • Takeaways & Limitations

    Controlled PROPs provide a framework for diagrammatic reasoning with control as a constructor, which the paper expects may also be useful in other domains such as classical reversible computing.

    Source: Conclusion · p. 28

    Freely generated conjugated controlled PROPs cannot be specified by purely equational axioms because the conjugation law is conditional and must be handled alongside the axioms.

    Source: §3.3 · p. 11

Abstract

from arXiv · show

Control is a fundamental concept in quantum and reversible computational models. It enables the conditional application of a transformation to a system, depending on the state of another system. We introduce a general framework for diagrammatic reasoning featuring control as a constructor. To this end, we provide an elementary axiomatization of control functors, extending the standard formalism of PROPs to controlled PROPs. As an application, we show that controlled PROPs facilitate diagrammatic reasoning for quantum circuits. In particular, they admit a simple and complete axiomatization involving at most three qubits, whereas in the standard PROP setting, completeness necessarily requires axioms involving arbitrarily many qubits.

1. Introduction

The paper makes control a constructor in diagrammatic languages and applies this framework to quantum circuits. Its controlled- and conjugated-controlled- PROP axiomatizations use bounded-qubit axioms, unlike standard PROP completeness, which requires axioms involving arbitrarily many qubits.

1.1. Controlled PROPs.

  • A controlled PROP formalizes control as a constructor: an endomorphism diagram gains one input and one output for its controlled version.Its constructors are sequential composition, parallel composition, and control.Source: §1.1 · p. 2
  • The conjugation law reduces control of a compute/uncompute pattern to control of the operation between a reversible operation and its inverse.Such patterns are used for change of basis, ancilla preparation and release, oracles, and circuit optimization [19].Source: §1.1 · p. 2

1.2. Quantum circuits.

  • For quantum circuits, the paper gives complete axiomatizations both as a conjugated controlled PROP and as a controlled PROP with a few additional conjugation-law relations.The conjugated presentation uses four simple axioms plus the standard Euler decomposition axiom.Source: §1.2 · p. 3
  • Controlled-PROP quantum-circuit axioms involve a bounded number of qubits, whereas complete standard-PROP axiomatizations require an axiom involving n qubits for every n [11].The paper presents its conjugated controlled- PROP axiomatization in Figure 1.Source: §1.2 · p. 3, Figure 1 · p. 3
  • The framework also yields a simple complete axiomatization for controllable circuits with ancillas and illustrates applications to reversible circuits and qudit systems.The ancilla example shows controlled PROPs need not consist only of endomorphisms, even though control applies only to endomorphisms.Source: §1.2 · p. 3

1.3. Related work.

  • Earlier graphical-language work used controlled operations as shorthand or in related constructions, while this paper makes control a constructor in the formalism.Related approaches include ZX-calculus normal forms [26] [27] and a vertically connecting composition for generalized controlled operations.Source: §1.3 · p. 3
  • The paper distinguishes control functors from rig-based approaches, which it describes as currently specific to the binary case [22].It presents controlled PROPs as suited to more general settings.Source: §1.3 · p. 4

2. PROPs

A PROP is a strict symmetric monoidal category with natural-number objects and addition as tensor product. The section explains its compositions, diagrammatic structure, and how generators and equations specify a graphical language.

2. PROPs

  • A PROP has natural-number objects, with addition as tensor product, and is a strict symmetric monoidal category.Its morphisms compose sequentially and in parallel, with identities and swaps as structural morphisms.Source: §2 · p. 4
  • String diagrams depict morphisms as boxes with input and output wires; sequential and parallel compositions, identities, and swaps have corresponding graphical forms.The PROP coherence laws governing these structures are depicted in Figure 2.Source: §2 · p. 4, Figure 2 · p. 5
  • A PROP can be freely generated from typed generators and equations, with morphisms given by terms quotiented by coherence laws and the axioms.The axioms can be applied locally inside any compatible context.Source: §2 · p. 6
  • A graphical language is sound when derivable equations hold semantically, complete when semantic equalities are derivable, and universal when every semantic morphism has a diagram representation.Together, these properties give an exact equational presentation of the represented semantics.Source: §2 · p. 7

3. Controlled PROPs

The section formalizes control as a functor on endomorphisms, then extends PROPs with control and with a conjugation law. These structures let diagrammatic reasoning express controlled equations and relate control to reversible operations.

3.1. Control functors.

  • Control functors map each endomorphism f:n→n to ctrl(f):(n+1)→(n+1), subject to additional coherence laws.They are defined only on endomorphisms and are not generally monoidal; control of a parallel composition differs from parallel composition of controlled morphisms.Source: §3.1 · pp. 7–8
  • Control functors need not be unique: in dimension 2, ctrl|0⟩ and ctrl|−⟩ are also control functors; for d>2, the map U ↦ P k |k⟩⟨k| ⊗Uk fails functoriality in general.Source: §3.1 · p. 9

3.2. Controlled PROPs.

  • A controlled PROP equips a PROP with a distinguished control functor, allowing derivable equations to be controlled directly.Any PROP admits two degenerate control functors, corresponding to always applying or never applying the operation; points can distinguish nondegenerate control behavior.Source: §3.2 · pp. 9–10
  • Controlled PROPs can be freely generated by controlled terms modulo the PROP coherence laws and chosen axioms, with control preserved on equivalence classes.Their functors preserve both PROP structure and control.Source: §3.2 · pp. 9–10

3.3. Conjugated controlled PROPs.

  • A conjugated controlled PROP satisfies a law that moves reversible operations outside control when they conjugate an operation.This connects controlled compute/uncompute patterns to preparing and releasing ancillas, implementing oracles, and adjusting control scope during compilation.Source: §3.3 · p. 11
  • Free conjugated controlled PROPs require conditional reasoning alongside axioms, because quotienting can create new left-invertible morphisms and new instances of the conjugation law.Thus, the axioms and the inference rule for conjugation must be handled simultaneously.Source: §3.3 · p. 11

4. Conjugation in unitary controlled PROPs

For unitary controlled PROPs, conjugation can be characterized by an equation involving a morphism and its dagger. Under reducibility, checking a restricted set of overlapping generator pairs suffices to establish the full property.

4. Conjugation in unitary controlled PROPs

  • For a unitary CPROP, being a CCPROP is equivalent to satisfying ctrl(g # f # g†) = (id1 ⊗g) # ctrl(f) #(id1 ⊗g†) for all f and g.Unitarity lets the conjugation law use g† in place of a separate inverse witness.Source: §4 · pp. 11–12
  • M-reducibility means morphisms can be built from M by sequential and parallel composition, enabling the restricted conjugation check to extend to all morphisms.The proof decomposes morphisms into layers with one M morphism between identities and uses induction on the number of layers.Source: §4 · pp. 12–13
  • An M-reducible unitary CPROP is a CCPROP if the stated conjugation equation holds for pairs of M morphisms acting on overlapping wires.The condition covers placements up to wire permutation; disjoint actions commute trivially, and no check is needed when either operation has zero wires.Source: §4 · p. 12

5. Vanilla quantum circuits

Vanilla quantum circuits are presented as a PROP generated by standard quantum gates and axiomatized by Av. The axiomatization is sound, and the resulting language is universal and complete, but completeness in the PROP setting requires axioms of unbounded arity.

5. Vanilla quantum circuits

  • QC is universal: global phases and one-qubit rotations implement arbitrary one-qubit unitaries, and an entangling gate such as CNOT extends universality to n qubits.The passage attributes this to Euler decomposition and the universality of an entangling two-qubit gate together with arbitrary one-qubit unitaries.Source: §5 · p. 15
  • Av is sound, and its gate generators represent global phases, Z-rotations, Hadamard, and CNOT.Av contains axioms for these gates and an instance of (zn) for each n≥2.Source: §5 · pp. 15–16, Figure 5 · p. 16
  • QC is complete, but any complete axiomatization of unitary circuits as a PROP requires an axiom involving n qubits for every n.The axiomatization Av includes necessary instances of (zn) for every n≥2.Source: §5 · p. 16

6. Controllable quantum circuits

Controllable quantum circuits are presented as a CPROP, and the paper proves the conjugation law and completeness for this setting. The resulting axiomatizations use bounded-size axioms, with a smaller set available when circuits are defined as a CCPROP.

6.1. Controllable quantum circuits.

  • Global phases and Hadamard gates generate universal controllable quantum circuits, whose axiomatization combines adapted standard axioms with new instances of the conjugation law.Some axioms of the standard quantum-circuit axiomatization become trivial in the CPROP formalism.Source: §6.1 · p. 17

6.2. The conjugation law.

  • CQC is proved to be a conjugated CPROP by establishing unitarity and reducibility, then verifying the sufficient condition for the conjugation law.The proof handles the remaining cases by equations summarized in Figure 8.Source: §6.1 · p. 17, §6.2 · pp. 17–20
  • A terminating reduction procedure transforms CQC morphisms into the M+-reducible form, then reduces identities and swaps to establish M-reducibility.The procedure decreases a lexicographic measure of nested controls.Source: §6.2 · pp. 18–19

6.3. Completeness.

  • CQC completeness follows by reducing circuits, encoding them into vanilla quantum circuits, applying their completeness, and decoding the resulting equality.The proof uses the correspondence between decoding a Z-rotation and a nested controlled phase.Source: §6.3 · pp. 20–22
  • The complete CQC axiomatization uses axioms involving at most three qubits; defining circuits as a CCPROP removes four conjugation-law axioms, leaving five axioms involving at most two qubits.The five-axiom set is also identified as complete for CCQC in Figure 6.Source: Figure 6 · p. 18, §6.3 · p. 23

7. Controllable quantum circuits with ancillas

The paper extends controlled quantum circuits to ancillas by defining ACQC as a CPROP restricted to isometries. It proves ACQC universal and complete, and gives a complete axiomatization for controllable circuits with ancillas using at most two-qubit axioms in its CCPROP formulation.

ACQC: controllable circuits with ancillas

  • Ancillas can be embedded into controllable quantum circuits, extending the treatment beyond circuits consisting solely of endomorphisms.The completeness proof follows the PROP approach using an improved proof of a cosine-sine decomposition variant.Source: §7 · pp. 23, 25
  • ACQC is defined as a restriction of freely generated PCQC, whose generators include qubit initialization and post-selection.The construction accounts for the requirement that qubits can be released only when they are in |0⟩ so other qubits are not disturbed.Source: §7 · p. 23
  • The axiomatization Aa is sound, and its isometry restriction ACCQC is complete under the smaller Aca axiomatization.Aca contains eight axioms involving at most two qubits.Source: §7 · pp. 24, 26, Figure 9 · p. 24
  • ACQC is complete, and its isometry restriction is universal for isometries between the permitted input and output sizes.ACQC(n, m) is empty when m < n because isometries cannot lose information.Source: §7 · pp. 24–25
  • Aa retains (ca), an axiom involving an arbitrary number of qubits, although the authors suggest it may be replaceable by more local axioms.They remove (ch1)–(ch4) and (ca) in the freely generated CCPROP formulation to obtain Aca.Source: §7 · pp. 25–26

8. Polycontrolled PROPs

Polycontrolled PROPs extend the framework to PROPs with multiple control functors. The paper illustrates how multiple controls can express unitaries and defines properties that describe how control functors relate to one another.

Polycontrolled PROPs

  • A polycontrolled PROP is a PROP equipped with multiple control functors.The paper presents this as a possible simplification for diagrammatic reasoning.Source: §8 · p. 26
  • Global phases with ctrlZ and ctrlX can express any two-qubit unitary in the illustrated language.The controls correspond intuitively to Z- and X-rotations, respectively.Source: §8 · pp. 26–27
  • The framework defines compatibility, commutativity, conversion, and exhaustivity as distinct properties of multiple control functors.For example, in Lin2, X converts ctrl|1⟩ into ctrl|0⟩ and vice versa.Source: §8 · p. 27
  • The control structure from [22] is captured by two commuting exhaustive control functors converted into one another by an involution.The involution is the morphism x described in that example.Source: §8 · p. 28

9. Controlled SMCs

Control functors extend from PROPs to arbitrary symmetric monoidal categories, where each control functor is specific to an object. The conclusion also identifies broader structural generalizations and leaves physical implementation and circuit-optimization questions open.

9. Controlled SMCs

  • Control structures in arbitrary symmetric monoidal categories are families of object-indexed functors that add the control object to inputs and outputs and obey coherence laws.The generalized definition recovers the PROP definition when instantiated in a PROP.Source: §9 · p. 28

Conclusion

  • The conclusion presents controlled PROPs as a framework for diagrammatic reasoning with control and notes that control functors generalize to arbitrary symmetric monoidal and braided monoidal categories.The paper also expects applications beyond quantum computing, including classical reversible computing.Source: Conclusion · p. 28
  • The framework treats control independently of physical implementation, and its no-go discussion does not apply in the white-box setting where the unitary circuit implementation is known.A full development of the physical-implementation question is left for future investigation.Source: Conclusion · p. 28
  • The conclusion identifies controllable quantum circuits for circuit optimization as future work, citing their simpler rewriting rules than vanilla quantum circuits.Source: Conclusion · p. 29

Appendix A. Proof of the equations of Figure 7

Appendix A provides proofs for the equations of Figure 7 in CQC.

Appendix A. Proof of the equations of Figure 7

Appendix B. Proof of the equations of Figure 10

Appendix B provides proofs for equations (32) through (40) in ACQC.

Appendix B. Proof of the equations of Figure 10

Appendix C. Generalized cosine-sine decomposition

Appendix C presents a self-contained proof of the generalized cosine-sine decomposition, a generalization of the cosine-sine decomposition. Its proof constructs the decomposition using matrix factorizations and unitarity constraints.

Appendix C. Generalized cosine-sine decomposition

  • The generalized cosine-sine decomposition (GCSD) is presented as a generalization of the cosine-sine decomposition (CSD).The appendix provides a self-contained proof of GCSD.Source: Appendix C · pp. 38–39
  • The proof begins by adjoining an identity block to the unitary matrix, taking an SVD of a block, and applying RQD and QLD.Source: Appendix C · pp. 39–40
  • Unitarity constrains the SVD diagonal elements to [0, 1], and the proof separates the elements equal to 1 from those strictly below 1.Source: Appendix C · p. 40
  • The proof uses the resulting unitarity constraints to show triangular submatrices are diagonal and to obtain the cosine and sine diagonal components.Source: Appendix C · pp. 39–41

Appendix D. Proof of Theorem 7.7

The appendix proves Theorem 7.7 by reducing equality of controlled-circuit interpretations to completeness for ordinary quantum circuits. Its intermediate lemma is proved inductively, using a GCSD-based matrix decomposition in the induction step.

Lemma D.1

  • Lemma D.1 is presented as a generalization of axioms (ic) and (icc), and its proof proceeds by induction on n.The n = 0 case is trivial by CQC completeness; for n = 1, the condition yields a circuit C′ with JCKc = Jctrl(C′)Kc, concluded using completeness and Lemma 7.6.Source: Appendix D · p. 41
  • For the induction step, the proof invokes GCSD to decompose a unitary into blocks A0, B0, A1, and B1 with cosine and sine diagonal matrices.Dc = diag(cos(α1), . . . , cos(αN−K)) and Ds = diag(sin(α1), . . . , sin(αN−K)).Source: Appendix D · p. 41
  • The proof defines ctrlb(Ry(α)) with the first qubit as target and control polarity determined by the corresponding bits of b.A bit equal to 1 gives a positive control; a bit equal to 0 gives a negative control.Source: Appendix D · p. 42

Proof of Theorem 7.7

  • The derivation removes each controlled rotation whose control bitstring has a 1 among its first n digits, applying Lemma 7.6 to the positive control before initialization.Every bitstring bin(i) for K ≤ i < N has at least one such 1.Source: Appendix D · p. 42
  • Theorem 7.7’s proof applies Lemma 7.5 to the circuits, then uses completeness of CQC to establish the desired equality.The proof assumes without loss of generality that m1 ≥ m2; its four wire groups represent m1 − m2, m2, n, and k wires.Source: Appendix D · pp. 42–43
Loading 2610.23192v1…