Schreiber Towards Certified Topological Quantum Programming via Linear Homotopy Types

A talk that I have given:


Talk Script

Motivation and Overview

In the current

Noisy Intermediate Quantum (NISQ) era

we see that quantum computing works

in principle — namely in small-scale examples

(cf. quotes here)

Towards the anticipated

Quantum Supremacy era

the remaining problem is:

To get it under control,

to scale up to heavy-duty usefulness.

(cf. quote here)

If we allow ourselves to step back and re-examine

the long-term perspective of heavy-duty quantum

we see that the following

basic problems have remained unsolved:

  • verification

    of the resulting (topological) quantum protocols at compile-time

    by formal proof — since de-bugging ceases to be an option

    (cf. quotes here)

where all of this must be subject to

We may observe that these are largely

issues of theory, of formal language:

We may also observe that

solving this looks like a hard problem

for a reason:

Quantum certification language is Formal quantum theory.

To properly verify a (topological) quantum program,

the verification language needs to accurately

reflect key aspects of actual quantum physics

thus effectively being a formal theory of quantum systems

(which is how we originally arrived here: S. 2014a, S. 2014b).

It may seem a tall order to formalize all this.

And yet:

Our claim is that a miracle occurs (explained below):

any extension of “homotopically typed” languages

by linear homotopy type which satisfy

an axiom scheme called the Motivic Yoga

as anticipated in: arXiv:1402.7041 pp. 39

prototyped on paper in: doi:10.14418/wes01.3.139

provides a formal context in which

such topological quantum language

may admissibly be embedded

as laid out in:

Topological Quantum Gates in HoTTarXiv:2303.02382,

Entanglement of SectionsarXiv:2309.07245

The Quantum MonadologyarXiv:2310.15735

Quantum and RealityarXiv:2311.11035.

Next to explain a little what this means.

Data Types and Spaces

The simple but profound idea of program verification is

to always declare the data type DD of any datum dd

d:D"dis of typeD" \underset{ \text{"}d\;\text{is of type}\;D\text{"} }{ \underbrace{ d \,\colon\, D } }

specifying what the data may be

and how it may be be used.

For example, in modeling the quantum Hall effect

one needs to specify the numerical datum “FillingFactorFillingFactor”.

If one declares this to be a real number

FillingFactor: FillingFactor \;\colon\; \mathbb{R}

then an irrational value like

FillingFactor=π FillingFactor = \pi

would conform to the data type specification while

violating the intended meaning of the program.

But if one instead declared the datum to be a rational number

FillingFactor: FillingFactor \;\colon\; \mathbb{Q}

as befits discussion of the fractional quantum Hall effect,

then an ill-identification like FillingFactor=πFillingFactor = \pi

can be recognized as an error at compile-time.

In this vein, if one declared even more restrictively

the data to be an integer number

FillingFactor: FillingFactor \;\colon\; \mathbb{N}

then the code would be verified (“type checked”)

when appropriate for the integer quantum Hall effect.

Simple as it is, carrying this

idea of thorough data typing

to all its logical implications

yields remarkably expressive languages.

This is the topic of type theory.

In particular a program is what maps

data of specified input type to

data of specified output type

The goal then is

to form data types AA

such that a datum is f(d):Af(d) \colon A iff

it conforms to its intended specification

so that a program is verified iff it can be

guaranteed to produce data of type AA.

For example, given data types X 1,X 2X_1, X_2, we may

form the new type of pairs (x 1,x 2)(x_1, x_2) of data

with x 1:X 1x_1 \colon X_1 and x 2:X 2x_2 \colon X_2,

which is defined by the following inference rules

prescribing how to form valid data from given data

(shown here just to give an impression):

What this means is that a program which

outputs data of such pair type X 1×X 2X_1 \times X_2

is guaranteed to produce valid data,

obeying the logical rule that there is

an X 1X_1-datum and an X 2X_2-datum.

By further such elementary type formation rules

one may specify and verify any logical constraint on data

a fact known by the slogan “propositions are types”.

This has a remarkable analogy with topology:

The defining properties of the above pair types

are just those of topological product spaces.

More precisely and yet more generally, this has

a remarkable analogy with algebraic topology:

The defining properties of such pair types

are just the universal properties

of category theoretic product objects.

This confluence of concepts between

has been called the computational trilogy.

Our basic observation [Sati S. 2022] may be summarized as:

there is a natural quantum enhancement of the trilogy to

a topological quantum computational trilogy between

which reveals a natural solution to the above

problem of topological quantum certification.

To this end, consider next the situation

where the type of a datum actually depends

on given data

γ:Γd γ:D γgivenγof typeΓthend γis of typeD γ \underset{ \text{given}\;\gamma\;\text{of type}\;\Gamma\;\text{then}\;d_\gamma\;\text{is of type}\;D_\gamma }{ \underbrace{ \gamma \colon \Gamma \;\;\;\; \vdash \;\;\;\; d_\gamma \,\colon\, D_\gamma } }

For example the dimension of a Hilbert space

which serves as the data type of a quantum state ψ\psi

may depend on previous computations:


taking the principle of data typing fully seriously,

it should be applied also to identifications of data:

Suppose a program is to compute certificates that

pairs of data x 1,x 2:Xx_1, x_2 \colon X may be identified (“are equal”).

For example

  • x 1x_1 may be the computed output of a quantum circuit

    and x 2x_2 the intended output

    then certifying x 1=x 2x_1 = x_2 is to verify

    the correct implementation of the protocol.

    (cf. Riley 2022)

  • x 1x_1 may be the output of a noisy channel followed by error correction

    while x 2x_2 is the output of the undisturbed channel, then

    verifying the correctness of the error-correction protocol

    is to produce a certificate that x 1=x 2x_1 = x_2

    shown here for the bit flip code:

But then also these id-certificates need to have a data type

called identification type (or “identity type”)

By a most remarkable development in computer science

the foundational insight of homotopy type theory is

that the semantics of such identification types

is that of path space fibrations in topology.

Indeed, their inference rules correspond to

(“parallel”) transport in (Serre-)fibrations

Hence in homotopy-typed programming languages like Cubical Agda

the seemingly sophisticated notion of parallel transport in fibrations

is a native expression in the programming language.

(code snippets from Myers & Riley 2023)

Quantum and Topology

The key point for us now is, as we may observe, that:

quantum adiabatic evolution is an example of such transport

A simple special case is quantum annealing

where there is an essentially unique parameter path:

A more profound special case is holonomic quantum computation

where there are non-contractible paths in parameter space

In particular anyon braid gates

for topological quantum computation

are of such a form:

This suggests that

thoroughly data-typed (namely: homotopically typed) programming languages

may natively know about

(the algebraic topology underlying) topological quantum computation.

In fact, we may observe that fundamentally

not only topological quantum gates but

all real quantum gates are continuous paths in parameter space:

Therefore having

path lifting as a native expression of a language

goes a long way in quantum computation.

The theorem: Anyon language

Still, the expected physics of anyon braid gates is rich:

For 𝔰𝔲 ( 2 ) \mathfrak{su}(2) -anyons (Majorana-, Fibonacci-…)

the Laughlin wavefunctions of ground states of topologically ordered quantum materials

are identified with the conformal blocks of 𝔰𝔲 ( 2 ) \mathfrak{su}(2) -current algebra 2d conformal quantum field theory

and their braiding is described by the Knizhnik-Zamolodchikov equation on

the vector bundle of conformal blocks over the configuration space of anyon defect positions.

Can a homotopically typed language really natively speak about —

and hence verify — the actual specification of such gates?


That this is indeed the case is the main theorem of

based on the K-theoretic re-analysis of anyons in

Schematically the proof procedes as follows:

braiding of

Laughlin wavefunctions of \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;Quantum Field Theory

anyonic topological order

(KZ-connection on 𝔰𝔲 ( 2 ) \mathfrak{su}(2) -conformal blocks)

\;\;\;\;\; \Bigg\updownarrow [Sati and S. 2023a, 2023b]

Gauss-Manin connection on

twisted cohomology of \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;Algebraic Topology

configuration space of anyons

(hypergeometric WZW construction)

\;\;\;\;\; \Bigg\updownarrow [Myers, Sati and S. 2024]

type transport of

0-truncated function types into \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;Homotopy Type Theory

braid-dependent EM-types

Side remark on solid state physics:

Here the first equivalence was found [Sati S. 2023] in the process of

generalizing the K-theory classification of topological phases of matter

from free to interacting topological phases

by passing

from K-theory of the Brillouin torus-orbifold \;\;\;\;\;\;\;— classifying single-electron states

to K-theory of its configuration space of points \;\;\; — classifying multi-electron Slater-det states.

Namely the twisted de Rham cohomology in the above theorem

is secretly the Chern character on this equivariant K-theory

In conclusion, this suggests that there ought to be a natural encoding

of topological braid quantum gates into homotopy typed languages.

And indeed there is –

it fits on one line [Myers, Sati and S. 2024, Thm. 6.8]:

This is currently being implemented in Cubical Agda by D. J. Myers et al. @ CQTS.

Quantum Data and Linear Spaces

The only aspect missing up to this point

is the specification of these types of (topological) quantum states

as linear spaces (Hilbert spaces) hence as linear types

equipped with a tensor product modelling their quantum entanglement

Formally, the “quantum-ness” of the tensor product of quantum state spaces

rests in the fact that it is not cartesian.

Namely the cartesian product of classical state spaces

(by its defining universal property)

comes with natural projection and with diagonal maps

corresponding to deletion and copying of classical data

reflected syntactically in structural rules called

the weakening rule and contraction rule:

Famously (known as the no-cloning theorem and no-deleting theorem)

these operations do not naturally exist on quantum state spaces.

Hence for quantum data types these structural inference rules

are to be omitted. The resulting substructural types are known as linear types:

That there ought to be an extension

of homotopy typed languages

by dependent linear types

we anticipated in Quantization via Linear Homotopy Types [arXiv:1402.7041]

motivated by high energy quantum physics [FormalMath@IHP 2014].

A proto-type was produced by Riley 2022.

What makes this work, semantically,

is a deep surprising theorem in modern algebraic topology

which roughly says – echoing Bohr’s famous standpoint:

[highlighted in FormalMath@IHP 2014, Prop. 2.5, p. 6]

This embeds the above encoding of anyon braid gates

into a fully-fledged quantum certification environment

which can naturally verify basic quantum principles

such as the deferred measurement principle

for controlled quantum gates:

Outlook. We have established an approach to the

general problem of topological quantum certification languages

of the following form

which seems practically promising and theoretically intriguing.

Much work remains to further flesh this out

and eventually implement it on computers.

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