# Techniques: Hadamard-Pi: Equational Quantum Programming

## What the paper contributes (one paragraph)
The paper characterises the computational behaviours obtained when a single Hadamard primitive is added to the universal classical reversible language Pi. It defines a small, discrete, universal quantum programming language (HPi, with an auxiliary QPi) equipped with a categorical denotational semantics and a sound and complete equational theory governed by a finite set of equations. Completeness rests on a new finite presentation, by finitely many generators and relations, of the groups O_n(Z[1/sqrt(2)]) of orthogonal matrices over the ring Z[1/sqrt(2)]. The authors also give an exact synthesis algorithm that decomposes any such orthogonal matrix into a sequence of generator words forming a unique normal form. Together these results enable purely syntactic, finitely axiomatised reasoning about when two reversible quantum programs implement the same unitary, and term rewriting for transforming and optimising those programs.

## Techniques offered
- **Exact synthesis (orthogonal matrices over Z[1/sqrt(2)])** - an algorithm that decomposes any orthogonal matrix over Z[1/sqrt(2)] into a sequence of words over a finite generator set, yielding a unique normal form for circuit synthesis.
  - guarantee: static proof - correctness theorem that each output strictly decreases the matrix level, terminating at a unique deterministic normal form.
  - quote: "We provide an exact synthesis algorithm that turns an orthogonal matrix in $O_n(\ZZ\sbra{\tfrac{1}{\sqrt{2}}})$ into a sequence of words over $\mathcal{G}_n$ as a unique normal form."
- **Complete equational theory for program equivalence (term rewriting)** - a sound and complete, finitely axiomatised equational theory that decides when two reversible quantum programs implement the same computation, enabling mechanised rewriting, transformation, and optimisation.
  - guarantee: static proof - soundness and completeness, so semantic equality holds if and only if one program rewrites to the other via a finite string of equations from a finite set.
  - quote: "Our results enable a complete mechanisation of reversible quantum program rewriting: two programs in \HPiLang implement the same quantum computation if and only if one can be rewritten into the other by a finite string of equations chosen from a finite set of equations."
- **Finite presentation of O_n(Z[1/sqrt(2)])** - a finite set of generators and relations presenting the orthogonal groups over Z[1/sqrt(2)], supplying a complete rewriting basis for words over those generators.
  - guarantee: static proof - soundness and completeness of the relation, so two generator words denote the same matrix if and only if they are related by the finite presentation.
  - quote: "we provide a presentation of the groups $O_n(\ZZ[\tfrac{1}{\sqrt{2}}])$ of orthogonal matrices with entries in the ring $\ZZ[\tfrac{1}{\sqrt{2}}]$ with finitely many generators $\mathcal{G}_n$ and relations."

## Where it could apply
- Target primitive(s): none (gate-level circuit synthesis and program equivalence checking for reversible quantum circuits, not a specific algorithmic primitive such as VQE or QPE)
- Target application group(s): platforms_tooling
- Code family / hardware assumptions: none (gate-set / hardware agnostic; restricted to circuits exactly representable over Z[1/sqrt(2)], i.e. the Hadamard-plus-classical-reversible fragment with discrete gates)

## Caveats
This is a programming-languages and categorical-semantics theory paper; its suppliable artefacts (exact synthesis, complete equational theory, finite group presentation) are formal and syntactic rather than empirical. They apply only to unitaries exactly representable over the ring Z[1/sqrt(2)] (the Hadamard-extended classical reversible fragment), not to arbitrary unitaries or continuously parametrised gates. The synthesis algorithm targets a unique normal form rather than efficiency, and the completeness proofs depend on a cancellativity property baked into the languages whose necessity is left open. No implementation is provided; the authors flag this as future work.