A brief note that we are finalizing:
Hisham Sati$\;\;$and$\;\;$ Urs Schreiber:
Quantum and Reality
download:
Abstract. Formalizations of quantum information theory in category theory and type theory, for the design of verifiable quantum programming languages, need to express its two fundamental characteristics: (1) parameterized linearity and (2) metricity. The first is naturally addressed by dependent-linearly typed languages such as Proto-Quipper or, following our recent observations [Mon, EoS]: Linear Homotopy Type Theory (
LHoTT
). The second point has received much attention (only) in the form of semantics in “dagger-categories”, where operator adjoints are axiomatized but their specification to Hermitian adjoints still needs to be imposed by hand.In this brief note we describe a natural emergence of Hermiticity which is rooted in principles of equivariant homotopy theory, lends itself to homotopically-typed languages and naturally connects to topological quantum states classified by twisted equivariant KR-theory. Namely, we observe that when the complex numbers are considered as a monoid internal to $\mathbb{Z}/2$-equivariant real linear types, via complex conjugation (the “Real numbers”), then (finite-dimensional) Hilbert spaces do become self-dual objects among internally-complex Real modules. This move absorbs the dagger-structure into the type structure; for instance a complex linear map is unitary iff seen internally to Real modules it is orthogonal.
The point is that this construction of Hermitian forms requires of the ambient linear type theory nothing further than a negative unit term of tensor unit type. We observe that just such a term is constructible in plain LHoTT, where it interprets as the non-trivial degree=0 element of the $\infty$-group of units of the sphere spectrum, interestingly tying the foundations of quantum theory to homotopy theory. We close by indicating how this observation allows to encode (and verify) unitarity of quantum gates and of quantum channels in quantum languages embedded into LHoTT, as described in [Mon].
This is part of the CQTS-project:
Related articles:
Related presentations:
Topological Quantum Programming via Linear Homotopy Types,
talk at Quantum Physics and Logic 2024, Buenes Aires, 15-19 July 2024
Towards Certified Topological Quantum Programming via Linear Homotopy Types,
talk at Quantum Information and Quantum Matter 2024,
NYU Abu Dhabi, 27-31 May 2024
Towards Quantum Programming via Linear Homotopy Types,
talk at Homotopy Type Theory and Computing – Classical and Quantum,
CQTS @ New York University Abu Dhabi, 19-21 April 2024
Topological Quantum Programming via Linear Homotopy Types
talk at: Homotopy Type Theory Electronic Seminar (01 Feb 2024)
Effective Quantum Certification via Linear Homotopy Types,
talk at Colloquium of the Topos Institute
Part I: 13 April 2023 [video: YT, slides:pdf]
Part II: 24 Aug 2023 [video:YT, slides:pdf]
Towards verified topological hardware-aware quantum programming
talk at CQTS & TII Workshop 2023, CQTS @ NYU Abu Dhabi, 24 Feb 2023
[slides:pdf]
Topological Quantum Programming in TED-K
talk at PlanQC 2022 33 (15 Sep 2022)
Quantum Data Types via Linear Homotopy Type Theory
talk at Workshop on Quantum Software @ QTML 2022, Naples, 12 Nov 2022
[slides: pdf]
Last revised on May 25, 2024 at 10:08:18. See the history of this page for a list of all contributions to it.