Schreiber Quantum Certification via Linear Homotopy Types

A project that we are developing at CQTS:

---

The monadic aspect:

• Hisham Sati, $\;$ Urs Schreiber:

  
  

  The Quantum Monadology

  
  

  Abstract. The modern theory of functional programming languages commonly uses monads for encoding computational side-effects and side-contexts beyond bare-bone program logic. Even though quantum computing is intrinsically side-effectful (as in quantum measurement) and context-dependent (as on mixed ancillary states) little of this monadic paradigm has previously been brought to bear on quantum programming languages (the two exceptions being Altenkirch \& Green‘s “Quantum IO monad” and Coecke et al.’s “classical structures” Frobenius monad).

  In this paper, we analyze the system of (co)monads on categories of parameterized spectra – for the present purpose specialized to set-indexed complex vector spaces – which arise from Grothendieck‘s “motivic yoga of operations” given by pushing foward and pulling back over maps. Interpreting an indexed vector space as a collection of alternative possible quantum state spaces parameterized by quantum measurement results, we find that these (co)monads provide a natural and expressive language for functional quantum programming.

  We close by indicating a domain-specific quantum programming language (QS) embeddable into the recently constructed linear homotopy type theory (LHoTT) which naturally expresses these monadic quantum effects in transparent do-notation. Once embedded into LHoTT, this should make for formally verifiable universal quantum programming language with classical control, dynamic lifting and topological effects (discussed in the companion article [TQP]).

On the categorical semantics:

• Hisham Sati, $\;$ Urs Schreiber:

  
  

  Entanglement of Sections

  
  

  arXiv:2309.07245

On the formalization of unitarity and dagger-structure:

• Hisham Sati, $\;$ Urs Schreiber:

  
  

  Quantum and Reality

The full picture, eventually to become a book (unfinished):

• David J. Myers, $\;$ Hisham Sati, $\;$ Urs Schreiber:

  
  

  QS: Quantum Programming via Linear Homotopy Types

  
  

  draft: pdf

  
  

  Abstract. We lay out a language paradigm, QS, for quantum programming and quantum information theory – rooted in the algebraic topology of stable homotopy types – which has the following properties, deemed necessary and probably sufficient for the eventual goal of heavy-duty quantum computation:

  • Application: in its 0-sector, QS is cross-translatable with the established quantum programming scheme Quipper, including support for classical control (dynamic lifting via dependent linear types) such as by quantum measurement outcomes which are handled monadically as in the widely used zxCalculus.

  • Compilation: but QS is embedded in (is just syntactic sugar for) a universal quantum certification language LHoTT, being a novel linear enhancement of the established formal (programming/certification) language scheme of Homotopy Type Theory (HoTT).

  • Certification: as such, QS introduces a previously missing method of formal verification of general classically controlled quantum programs, e.g. it verifies quantum axioms such as the deferred measurement principle.

  • Stabilization: in its higher sector, QS natively models hardware-level topologically stabilized quantum computation such as by realistic anyonic braid gates, verifying their conformal field theoretic properties.

  • Realization: in fact, QS naturally interfaces with the holographic quantum theory of topologically ordered quantum materials that are thought to eventually provide topologically stabilized quantum hardware.

  In developing these results we find a pleasant unification of quantum logic (linear types), epistemic modal logic (possible worlds), quantum interpretations (many worlds), and twisted cohomology (parameterized spectra) & motives (six-operations) – which may be of interest in itself. (“QS” stands both for “Quantum Systems language” and for the sphere spectrum “$Q S^0$”.)

  In companion articles [TQP] [EoS] we further discuss topological quantum gates in and the categorical semantics of LHoTT/QS.

Brief survey:

• David J. Myers, $\;$ Mitchell Riley, $\;$ Hisham Sati, $\;$ Urs Schreiber:

  
  

  Effective Quantum Certification via Linear Homotopy Types

  
  

  extended abstract: pdf

  
  

  Abstract. The intricacies of realistic — namely: of classically controlled and (topologically) error-protected — quantum algorithms arguably make computer-assisted verification a practical necessity; and yet a satisfactory theory of dependent quantum data types had been missing, certainly one that would be aware of topological error-protection.

  To solve this problem we present Linear Homotopy Type Theory (LHoTT) as a programming and certification language for quantum computers with classical control and topologically protected quantum gates, focusing on (1.) its categorical semantics, which is a homotopy-theoretic extension of that of Proto-Quipper and a parameterized extension of Abramsky et al.'s quantum protocols, (2.) its expression of quantum measurement as a computational effect induced from dependent linear type formation and reminiscent of Lee at al.‘s dynamic lifting monad but recovering the interacting systems of Coecke et al.‘s "classical structures" monads.

  Namely, we have recently shown [MSS23] that classical dependent type theory in its novel but mature full-blown form of Homotopy Type Theory (HoTT) is naturally a certification language for realistic topological logic gates. But given that categorical semantics of HoTT is famously provided by parameterized homotopy theory, we had argued earlier [Sc14] for a quantum enhancement LHoTT of classical HoTT, now with semantics in parameterized stable homotopy theory. This linear homotopy type theory LHoTT has meanwhile been formally described [Ri22]; here we explain it as the previously missing certified quantum language with monadic dynamic lifting, as announced in [Sc22].

  Concretely, we observe that besides its support, inherited from HoTT, for topological logic gates, LHoTT intrinsically provides a system of monadic computational effects which realize what in algebraic topology is known as the ambidextrous form of Grothendieck’s “Motivic Yoga”; and we show how this naturally serves to code quantum circuits subject to classical control implemented via computational effects. Logically this emerges as a linearly-typed quantum version of epistemic modal logic inside LHoTT, which besides providing a philosophically satisfactory formulation of quantum measurement, makes the language validate the quantum programming language axioms proposed by Staton [St14]; notably the deferred measurement principle is verified by LHoTT.

  Finally we indicate the syntax of a domain-specific programming language QS (an abbreviation both for “Quantum Systems” and for “$Q S^0$-modules” aka spectra) which sugars LHoTT to a practical quantum programming language with all these features; and we showcase QS-pseudocode for simple forms of key algorithm classes, such as quantum teleportation, quantum error-correction and repeat-until-success quantum gates.

---

Companion articles:

• Mitchell Riley:

  A Linear Dependent Type Theory with Identity Types

  as a Quantum Verification Language

  pdf, pdf

  (translation between LHoTT and the proto-Quipper of Fu, Kishida & Selinger 2020)

• David Jaz Myers, Hisham Sati, Urs Schreiber:

  Topological Quantum Gates in Homotopy Type Theory

  arXiv:2303.02382

  (certification of topological quantum gates in HoTT)

Expository presentations:

• Quantum Data Types via Linear Homotopy Type Theory

  talk at Workshop on Quantum Software @ QTML 2022

  Naples, 12 Nov 2022

  slides: pdf (view on full screen)

  
  

  Abstract. The proper concept of data types in quantum programming languages, hence of their formal verification and categorical semantics, has remained somewhat elusive, as witnessed by the issue of “dynamic lifting” encountered in the Quipper language family. In this talk I explain our claim that a powerful quantum data type-system elegantly solving these problems is naturally provided by the linear homotopy type theory recently realized by M. Riley. Together with our previous claim that homotopy type theory natively knows about the fine detail of $\mathfrak{su}$(2)-anyon braid quantum gates, this shows that linear homotopy type theory is a natural substrate for typed quantum programming languages aware of topological quantum hardware.

  This is joint work, at CQTS, with D. J. Myers, M. Riley and Hisham Sati.

• Effective Quantum Certification via Linear Homotopy Types,

  talk at Colloquium of the Topos Institute

  
  

  Part I: 13 April 2023

  video: YT

  slides: pdf (view full screen)

  
  

  Part II: 24 Aug 2023 [zoom]

  video: YT

  slides: pdf (view full screen)

Related talks:

• 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)

  [video:YT, script:web]

• 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)

  [slides:pdf, video: YT]

• Quantum Data Types via Linear Homotopy Type Theory

  talk at Workshop on Quantum Software @ QTML 2022, Naples, 12 Nov 2022

  [slides: pdf]

Precursor discussion:

• Quantization via Linear Homotopy Types

  [arXiv:1402.7041]

---