Schreiber Towards Quantum Programming via Linear Homotopy Types

a talk that I have given:




Abstract. Remarkably, among the \infty -toposes into which HoTT interprets are “tangent \infty -toposes” of parameterized module spectra, which behave like semantics for an enhancement of HoTT by dependent *linear* homotopy types, neatly combining the linear aspect of typed quantum programming languages (like Proto-Quipper) with homotopy-theoretic aspects needed for future *topological quantum* languages. The talk surveys this HoTT-perspective on (topological) quantum systems, developed jointly with Hisham Sati (“Topological Quantum Gates in HoTTarXiv:2303.02382, “Entanglement of SectionsarXiv:2309.07245, “The Quantum MonadologyarXiv:2310.15735, “Quantum and RealityarXiv:2311.11035).


Contents


Script

  1. Quantum Systems via Linear Homotopy Types

  2. Modal Quantum Circuit Logic via Dependent Linear Types

  3. Topological Quantum Gates via Linear Type Transport


(1) Quantum Systems via Linear Homotopy Types


Following Awodey 2009, it is now well-understood [Cisinski 2012, 2014; Shulman 2015, 2019] that

univalent\;HoTT\;finds its categorical semantics

[(Γ,x:A,y:B(x))] [Γ,x:AB(x):Type] [Γ] [Γa:A] [(Γ,x:A)] id [ΓA:Type] [Γ] \array{ &&&& \big[ (\Gamma, x \colon A, y \colon B(x)) \big] \\ &&&& \Big\downarrow \mathrlap{ {}^{ \big[ \Gamma, x \colon A \,\vdash\, B(x) \colon Type \big] } } \\ [\Gamma] && \overset{ [\Gamma \vdash a \colon A] } {\longrightarrow} && \big[ (\Gamma, x \colon A) \big] \\ & {}_{id}\searrow && \swarrow_{\mathrlap{[\Gamma \vdash A \colon Type]}} \\ && [\Gamma] }

in \infty -toposes presented by well-behaved (type-theoretic) model categories.


Remarkably [Biedermann 2007; Joyal 2008; Hoyois 2019],

among these \infty -toposes are

tangent \infty -toposesT RGrpd \;T^R Grpd_\infty

of parameterized R R -module spectra

over varying \infty -groupoids (cf. the talk by Finster).


This can be surprising, because these are amalgamations

T RGrpd 𝒳Grpd RMod 𝒳 T^R Grpd_\infty \;\;\;\; \simeq \;\;\;\; \int_{\mathcal{X} \in Grpd_\infty} \, R Mod^{\mathcal{X}}

of stable \infty -categories RMod 𝒳R Mod^{\mathcal{X}}

of parameterized R R -module spectra over fixed bases 𝒳\mathcal{X}

which as such are far from being \infty -toposes themselves.


This fact can indeed be so surprising that

when I first highlighted it to a HoTT-audience in 2014 (slide 6)

it was ferociously doubted.


Specifically [Robinson 1987; Shipley 2007],

when RHR \equiv H\mathbb{C} is the Eilenberg-MacLane spectrum of the complex numbers, say, then


More concretely [Sati and S. 2023, Prop. 3.23 p. 40]:

a model category-presentation for T HGrpd T^{H\mathbb{R}} Grpd_\infty

is given by the integral model structure for

the projective model structures of simplicial functor categories

from simplicial groupoids to the model structure on simplicial chain complexes

Loc = XsGrpdsCh X. \mathbf{Loc}_{\mathbb{C}} \;=\; \int_{\mathbf{X} \in sGrpd} \mathbf{sCh}_{\mathbb{C}}^{\mathbf{X}} \,.


Alongside its Cartesian product, this category carries

(“external”) symmetric monoidal tensor product-structure \boxtimes:

(𝒱 1:X 1sCh )(𝒱 2:X 2sCh ) (pr 1 *𝒱 1pr 2 *𝒱 2X 1×X 2sCh ). \begin{array}{l} \big( \mathscr{V}_1 \,\colon\, \mathbf{X}_1 \longrightarrow \mathbf{sCh}_{\mathbb{C}} \big) \boxtimes \big( \mathscr{V}_2 \,\colon\, \mathbf{X}_2 \longrightarrow \mathbf{sCh}_{\mathbb{C}} \big) \\ \;\coloneqq \;\; \Big( \mathrm{pr}_1^\ast \mathscr{V}_1 \otimes \mathrm{pr}_2^\ast \mathscr{V}_2 \;\;\coloneqq\;\; \mathbf{X}_1 \times \mathbf{X}_2 \longrightarrow \mathbf{sCh}_{\mathbb{C}} \Big) \,. \end{array}


It turns out [Sati and S. 2023, Thm. 3.42 p. 53, Rem. 344 p. 54],

that this is rather well-behaved

as far as model categories for parameterized spectra go [cf. Malkiewich 2023]

but it is not quite a \boxtimes-monoidal model category-structure.


However [Sati and S. 2023, Thm. 3.46 p. 56]

it becomes monoidal model

when restricted to 1-truncated classical base types,

Loc Grpd= 𝒳GrpdsCh 𝒳. Loc^{Grpd}_{\mathbb{C}} \;=\; \int_{\mathcal{X} \in Grpd} sCh_{\mathbb{C}}^{\mathcal{X}} \,.

So this is a well-behaved extension by symmetric monoidal chain complexes

of the original groupoid model for 1-truncated HoTT [Hofmann & Streicher 1994].


To get a sense of the nature of this extension,

focus on the “hearts” of these fiber-wise stable symmetric monoidal \infty -categories, which form


It is clear but maybe underappreciated [Pratt 1993; Valiron & Zdancewic 2014; cf. Sati and S. 2023b pp. 53]

that these tensor categories happen to be models of

(the multiplicative fragment of) linear type theory:


Similarly clear but long underappreciated [Pratt 1992; Selinger & Valiron 2005; Abramsky & Duncan 2006]:

Where type theory is about computing,

linear type theory may be understood as being about quantum computation:


Accordingly, over sets (0-truncated objects), the above categories serve

as categorical semantics for quantum programming languages such as:

I’ll expand on this further below:


Moreover [Myers, Sati and S. 2024] (cf. the talk by Myers),

over homotopy 1-types, Loc Loc_{\mathbb{C}} serves as

categorical semantics for topological quantum gates

via “braiding of anyons

Remarkably [Myers, Sati and S. 2024, Thm. 6.8]

here we have a correspondence between

  1. type transport in homotopy type theory

  2. adiabatic transport of quantum states.


This “quantum reflection” of \infty -toposes goes even beyond quantum computation

to capture the “hardware” quantum physics of quantum systems:


E.g. when RR \equiv KU then in T KUGrpd T^{KU} Grpd_\infty:

which serves to describe


Even this “works formally” [S. 2014 pp. 48, 53, 65]:

T RGrpd T^R Grpd_\infty behaves like one would expect for

a categorical semantics of an extension of homotopy type theory by

some kind of dependent linear (stable) homotopy types.


This motivates to ask for a formalization of

Quantization via Linear Homotopy Types [arXiv:1402.7041]

and ask for an extension of HoTT by language features

whose categorical semantics single out tangent \infty -toposes among all \infty -toposes

which may serve as a natural quantum programming/certification.


Concretely [S. 2013, Prop. 4.1.9, p. 446],

tangent \infty -toposesTH\;T \mathbf{H} are infinitesimally cohesive over their base topos H\mathbf{H}.


Hence a would-be “Linear Homotopy Type Theory” should

first of all be a modal extension of HoTT

by an ambidextrous modality expressing the bireflective subcategory

of classical types

into more general classical+quantum types

(\simBohr‘s quantum/classical divide).


Such a classically-modal LHoTT was then

given by [Riley, Finster & Licata 2021] (cf. the talk by Finster) and

a syntax for the (“external”) tensor product was given by [Riley 2022] (see talk by Riley)


Getting to the bottom of how T RGrpd T^R Grpd_\infty knows about the nature of quantum systems

one finds [Schreiber 2014; Sati and S. 2023a pp. 43; Sati and S. 2023b pp. 62]

that the base change adjoint triples on the system of dependent linear type universes T 𝒳 RGrpd RMod 𝒳T^R_{\mathcal{X}} Grpd_\infty \;\simeq\; R Mod^{\mathcal{X}}

together with the linear tensor product and its internal hom

constitutes the Wirthmüller form of Grothendieck‘s yoga of six operations in motivic homotopy theory

— which for short we refer to as the Motivic Yoga.


Therefore a good quantum programming language should be

one that expresses and verifies the Motivic Yoga.

This is the case for LHoTT [Riley 2022, §2.4]


And hence we want to see how to go about formulating

a Quantum Systems Language

with operational semantics in tangent \infty -toposes

naturally embeddable into LHoTT.


(2) Modal Quantum Circuit Logic via Dependent Linear Types

\to The Quantum Monadology [Sati and S. 2023]


The theory of computational effects in functional programming languages suggests that

quantum effects such as

should have a formal reflection in terms of suitable

(co-)monads/modal operators on a linear data type system.



Our fundamental observation is that

in a dependent linear type theory which satisfies the Motivic Yoga (e.g. LHoTT)

suitale such (co-)monads are definable (i.e., by admissible inference rules)

induced from the base change adjoint triple restricted to dependent linear types:

\;\;\; dependent pair type \;\;\dashv\;\; context extension \;\;\dashv\;\; dependent product type


Remarkably [Sati and S. 2023b §2 pp. 53]

this automatically implements

a quantum version of epistemic modal logic (S5)

which accurately reflects

  1. the quantum state collapse upon quantum measurement

  2. the Gell-Mann principle of quantum compulsion:


By ambidexterity/quantum compulsion one finds that [Prop. 2.34 p. 75]

the quantum indefiniteness/randomness modalities unify into a Frobenius monad:


satisfying the Frobenius normal form/Spider theorem:


This recovers (and hence may serve to certify)

the typing of quantum measurement used in the ZX-calculus [Coecke and Pavlović 2008; Coecke and Duncan 2008]

(cf. the talk by Rand).



Next, it is noteworthy that

dependent linear types are monadic over plain linear types:

This provides the following

natural typing of quantum gates/quantum circuits (\to quantum circuits via dependent linear types)


(1) typing of controlled quantum gates:


(2) typing of quantum measurement:


Hence the deferred measurement principle is verifiable in LHoTT

as an instance of the Kleisli equivalence for the quantum necessity modality.


(3) typing of dynamic lifting by passage through the unit/return operation of the indefiniteness modality:


(4) typing of incremental quantum measurement:


(5) typing of quantum measurement on mixed states and the Born rule

by monoidality of quantum indefiniteness [Prop. 2.36 p. 77]


In summary,

we find comprehensive expression

of quantum information/computing structures

in the internal language (LHoTT)

of tangent \infty -toposes.


But in fact, up to this point in this presentation we have

only referred to the 0-truncated/heart-sector of the linear homotopy type system.

The remaining higher (linear) homotopy types turn out to reflect

fine-structure of topological quantum computation:


(3) Topological Quantum Gates via Linear Type Transport

\to Topological Quantum Gates in HoTT

[Myers, Sati and S. 2024]

(cf. following talk by Myers)








Last revised on May 31, 2024 at 10:39:53. See the history of this page for a list of all contributions to it.