# Techniques: The Quantum Effect: A Recipe for QuantumPi

## What the paper contributes (one paragraph)
The paper shows that a computationally universal quantum programming language can be built as a formal combination of two copies of a classical reversible language (Pi, the internal language of rig groupoids), glued by the complementarity equation of classical structures and layered as Hughes' arrows. The result is QuantumPi (qpi), with a categorical semantics in the category of finite-dimensional Hilbert spaces and contractions, fully implemented in Agda. A canonicity theorem proves that any conforming model must be computationally universal (Hadamard plus Toffoli, up to local unitaries). Because quantum behaviour is reduced to classical reasoning plus one complementarity equation, the paper supports equational reasoning about quantum programs: it gives machine-checked proofs of circuit equivalences (for example that X and H are involutive, and CNOT/Z/H rewrites), and shows that measurement can be added as a further "hiding" effect to model end-to-end algorithms such as Simon and Grover.

## Techniques offered
- **Categorical construction of a quantum programming language (the quantum effect / QuantumPi)** - builds a computationally universal quantum language and its Hilbert-space semantics from two complementarity-glued copies of a classical reversible language, supplying a language and semantic framework rather than a hardware-facing routine.
  - guarantee: canonicity theorem; any model of the language in the contraction category satisfying the classical-structure, execution, and complementarity laws is computationally universal (static, proof-level assurance).
  - quote: "This article gives just such a recipe, namely constructing a computationally universal quantum programming language from two copies of a (particlar) universal classical reversible language."
- **Equational reasoning about quantum circuit equivalence (machine-checked in Agda)** - reduces proving that two quantum programs or circuits are equal to classical equational reasoning augmented with the complementarity law, mechanised so the equivalences are machine-checkable.
  - guarantee: machine-checked proofs of exact circuit equivalence; soundness via the categorical laws, with completeness left open (proves programs exactly equal, not up to error).
  - quote: "This section demonstrates that some forms of reasoning about quantum programs in \qpi\ indeed reduces to classical reasoning augmented with the complementarity equation."

## Where it could apply
- Target primitive(s): none specific; reasoning targets gate-level circuits and oracles (for example the Simon and Grover circuits expressed in the language).
- Target application group(s): platforms_tooling

## Caveats
This is a categorical and programming-language-semantics paper; its core contribution is foundational (a universality recipe and a canonicity theorem) rather than a routine that supplies an external vendor result. The canonicity theorem is a guarantee, not a separate technique. The equational reasoning proves only exact equivalence, not approximate or error-bounded equivalence, and a complete equational theory is explicitly left open, so the verification capability is partial. Encoding general rotations (for example for the QFT) from Toffoli and Hadamard is noted as awkward and inefficient.