nLab quantum set

Idea

According to Kornell 2020, and in mild paraphrase (following the discussion at dependent linear type and quantum circuits via dependent linear types):

• quantum sets are indexed sets of finite-dimensional Hilbert spaces — hence finite-rank Hilbert-vector bundles over discrete topological spaces regarded as a sets — and regarded as equipped with the external tensor product $\boxtimes$ of vector bundles;

• a quantum relation between quantum sets $(x \colon X) \times \mathscr{H}_x$ and $(x' \colon X') \times \mathscr{H}'_x$ is a monomorphism from a quantum set $\big((x,x') \colon X \times X'\big) \times \mathscr{R}_{(x,x')}$ to $\mathscr{H}^\ast_\bullet \boxtimes \mathscr{H}'_\bullet$:

  $$(x,x') \colon X \times X' \;\;\; \vdash \;\;\; \mathscr{R}_{(x,y)} \hookrightarrow \mathscr{H}^\ast_{(x,y)} \otimes \mathscr{H}^'_{(x,y)}$$

With composition the evident matrix multiplication (Kornell 2020 (5)), quantum relations between quantum sets form a category $qRel$, which is a dagger-compact category.

As such, this serves as categorical semantics for quantum programming languages like Quipper equipped with term recursion, via quantum CPOs (Kornell, Lindenhovius & Mislove 2021).

Related concepts

• quantum CPO

References

• Andre Kornell, Quantum Sets, J. Math. Phys. 61 102202 (2020) [doi:10.1063/1.5054128]

• Andre Kornell, Bert Lindenhovius, Michael Mislove, §2 in: Quantum CPOs, EPTCS 340 (2021) 174-187 [arXiv:2109.02196, doi:10.4204/EPTCS.340.9]

  (in the context of quantum CPOs)