Schreiber Towards Certified Topological Quantum Programming via Linear Homotopy Types

A talk that I have given:

Urs Schreiber:

Towards

Certified Topological Quantum Programming

via Linear Homotopy Types

talk at:

Quantum Information and Quantum Matter 2024,

NYU Abu Dhabi, 27-31 May 2024

Abstract. Beyond the present NISQ era, useful heavy-duty quantum programs will arguably necessitate (1.) topological quantum circuits for error-protection and (2.) (classical-)computer-verified certificates of correctness — hence essentially a formal verification logic of the underlying topological quantum processes — which may seem a tall order. But we have recently shown that the (conservative) extension of the (programming & certification-)language of “Homotopy Type Theory” (HoTT) by “linear homotopy types” (LHoTT, for which prototypes exist on paper) namely: by classically-controlled topological quantum data types, naturally lends itself to just this purpose. In this talk I will give an introduction to and survey of this approach to Topological Quantum Programming Certification via Linear Homotopy Types, developed at CQTS @ NYUAD (“Topological Quantum Gates in HoTT” arXiv:2303.02382, “Entanglement of Sections” arXiv:2309.07245, “The Quantum Monadology” arXiv:2310.15735, “Quantum and Reality” arXiv:2311.11035).

Talk Script

Motivation and Overview
Data Types and Spaces
Quantum and Topology
The theorem: Anyon language
Quantum Data and Linear Spaces

Related presentations

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:

stabilization

of the quantum hardware by topological quantum error protection

(cf. quotes here)
compilation

of qbit quantum circuits into the available topological quantum gates

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

parameterization

of the quantum system by classical control

including dynamic lifting of quantum measurement

notably for quantum error correction

(cf. quotes here)

We may observe that these are largely

issues of theory, of formal language:

theory of topological phases of quantum matter

has arguably remained shaky

(cf. the experimentally elusive MZMs)
nature of topological quantum gates

had not been reflected in existing quantum programming languages

(e.g. anyon braiding has not)
formal methods for verifying classical code

had not been thoroughly adapted to quantum

(in particular because quantum identity types had been missing – but see below)
theory of classically dependent quantum data types

had not been satisfactorily developed

(cf. quote here)

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

coherence:

no-cloning/deleting & entanglement
decoherence:

quantum measurement & state collapse
parameterization:

adiabatic evolution & topological protection

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 types 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 HoTT” arXiv:2303.02382,

“Entanglement of Sections” arXiv:2309.07245

“The Quantum Monadology” arXiv:2310.15735

“Quantum and Reality” arXiv: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 $D$ of any datum $d$

\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 “ $FillingFactor$ ”.

If one declares this to be a real number

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

then an irrational value like

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 \;\colon\; \mathbb{Q}

as befits discussion of the fractional quantum Hall effect,

then an ill-identification like $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 \;\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 $A$

such that a datum is $f(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 $A$ .

For example, given data types $X_1, X_2$ , we may

form the new type of pairs $(x_1, x_2)$ of data

with $x_1 \colon X_1$ and $x_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 \times X_2$

is guaranteed to produce valid data,

obeying the logical rule that there is

an $X_1$ -datum and an $X_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

$\;\;\;$ topological $\;\;\;\;\;$ quantum $\;\;\;$ computation
$\;\;\;$ dependent $\;\;\;\;\;\;\;\;$ linear $\;\;\;\;\;\;$ type theory
parameterized $\;\;\;\;\;$ stable $\;\;\;\;\;\;$ alg. topology

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

\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:

Now,

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 \colon X$ may be identified (“are equal”).

For example

$x_1$ may be the computed output of a quantum circuit

and $x_2$ the intended output

then certifying $x_1 = x_2$ is to verify

the correct implementation of the protocol.

(cf. Riley 2022)
$x_1$ may be the output of a noisy channel followed by error correction

while $x_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_2$

shown here for the bit flip code: