Game Semantics for Higher-Order Unitary Quantum Computation
Samson Abramsky, Radha Jagadeesan
TL;DR
The paper develops a game-semantics framework for higher-order quantum computation by constructing deterministic IMALL-based games ${\mathcal G}$ and extending to ${\cal V}$ and ${\cal U}$ to model all unitary morphisms on $n$-qubit tensors while remaining compatible with base types. It demonstrates universality for unitaries in the reversible and unitary subcategories, and shows how additive/distributive structures interact with tensorial flow through trace-based composition and GOI-inspired reasoning. A key contribution is the realization that Schwinger-basis unitary operations can be encoded as reversible strategies within ${\mathcal G}$, enabling a semantic route to universal quantum computation at higher types; the work also relates to existing GOI formalisms and to a first-order fragment of a broader universality result in the literature. Overall, the framework provides a type-safe, reversible, and unitary semantics for higher-order quantum control, with potential implications for formalizing quantum programming languages and compiler backends.
Abstract
We develop a symmetric monoidal closed category of games, incorporating sums and products, to model quantum computation at higher types. This model is expressive, capable of representing all unitary operators at base types. It is compatible with base types and realizable by unitary operators.