Formally Verified Quantum Programming
Formally Verified Quantum Programming
PROGRAMMING
Robert Rand
A DISSERTATION
in
2018
Supervisor of Dissertation
Steve Zdancewic
Professor of Computer and Information Science
Rajeev Alur
Professor of Computer and Information Science
Dissertation Committee
Stephanie Weirich, Professor of Computer and Information Science, Chair
Val Tannen, Professor of Computer and Information Science
Benjamin Pierce, Professor of Computer and Information Science
Prakash Panangaden, Professor of Computer Science, McGill University
Acknowledgments
A lot of people helped me on the road to this dissertation, none more than my advisor,
Steve Zdancewic. From the moment I wandered into his office and asked if we could do
research on probability and logic (his response: “Sure!”), to the moment he emailed me
and Jennifer Paykin asking if we wanted to work on a quantum computing project
(“Sure!”), to the moment I submitted this dissertation, Steve has been endlessly
enthusiastic, generous with his time, and willing to explore entirely new horizons.
In a similar vein, I have to thank my friend and collaborator Jennifer Paykin,
who jumped into the new and exciting world of quantum programming languages
with me. Doing research is an entirely different, and better, experience with a close
collaborator, especially one as talented and tireless as Jennifer. Qwire, and therefore
this thesis, could not possibly have existed without her.
Thanks to Mike Mislove and the other members of the “Semantics, Formal Rea-
soning, and Tools for Quantum Programming” research initiative for introducing me
to quantum computing and helping me acclimate to the field. Relatedly, thanks to
the MFPS and QPL communities, which taught me a great deal and always made
me feel welcome. Thanks especially to Peter Selinger, who blazed the path that I
tried to follow and happily helped me along it, and Prakash Panangaden, who lent
me his knowledge of quantum mechanics and graciously agreed to serve on my thesis
committee.
Thanks to Andy Gordon, who hosted me for a summer at Microsoft Research
Cambridge. Thanks to my collaborators there: Neil Toronto, Cecily Morrison, Claudio
Russo, Simon Peyton-Jones, Abigail Sellen, Felienne Hermans, Advait Sarkar and
Rupert Horlick. Also, thanks to Tony Hoare, Cédric Fournet and Georges Gonthier for
intellectually stimulating lunch meetings that often segued into extensive discussions
of formal verification.
Thanks to PLClub. The Penn Programming Languages group is not just a research
group: it is a meeting place for people who love programming languages and are deeply
invested in one another’s success. Thanks especially to Stephanie Weirich, Benjamin
Pierce, Rajeev Alur, Mayur Naik and Val Tannen for their criticism, encouragement
and advice. And thanks to Antal Spector-Zabusky, Leonidas Lampropoulos, Arthur
Azevedo de Amorim, Peter-Michael Osera, Vilhelm Sjöberg, Richard Eisenberg, Brent
Yorgey, Justin Hsu, Kenny Foner, Dmitri Garbuzov, Yannick Zakowski, Christine
Rizkallah, Joachim Breitner, William Mansky, Maxime Dénès, Cǎtǎlin Hriţcu, Emilio
ii
Jesús Gallego Arias and Benoît Valiron for their generous help and camaraderie.
Everyone who read this thesis, in part or in full, has my lasting gratitude. That’s
Steve and Jennifer again, and my committee, Stephanie, Benjamin, Val and Prakash,
as well Julien Ross, Yannick Zakowski, Alex Burka and Rivka Cohen. You are all my
heroes.
I’d like to end with a tribute to my first advisor and mentor at Penn, the late
Dr. Ben Taskar. I can vividly remember receiving a text message from out of the
blue saying Ben had passed away. In a daze, I searched the internet for confirmation,
coming upon a lone tweet from Ben’s own mentor, the legendary Andrew Ng:
“RIP Ben Taskar. Machine learning just lost a star.” The night sky may be full
of lost stars but we still benefit from their light.
iii
ABSTRACT
FORMALLY VERIFIED QUANTUM PROGRAMMING
Robert Rand
Steve Zdancewic
The field of quantum mechanics predates computer science by at least ten years,
the time between the publication of the Schrödinger equation and the Church-Turing
thesis. It took another fifty years for Feynman to recognize that harnessing quantum
mechanics is necessary to efficiently simulate physics and for David Deutsch to propose
the quantum Turing machine. After thirty more years, we are finally getting close to
the first general-purpose quantum computers based upon prototypes by IBM, Intel,
Google and others.
While physicists and engineers have worked on building scalable quantum comput-
ers, theoretical computer scientists have made their own advances. Complexity theo-
rists introduced quantum complexity classes like BQP and QMA; Shor and Grover de-
veloped their famous algorithms for factoring and unstructured search. Programming
languages researchers pursued two main research directions: Small-scale languages
like QPL and the quantum λ-calculi for reasoning about quantum computation and
large-scale languages like Quipper and Q# for industrial-scale quantum software de-
velopment. This thesis aims to unify these two threads while adding a third one:
formal verification.
We argue that quantum programs demand machine-checkable proofs of correct-
ness. We justify this on the basis of the complexity of programs manipulating quan-
tum states, the expense of running quantum programs, and the inapplicability of
traditional debugging techniques to programs whose states cannot be examined. We
further argue that the existing mathematical models of quantum computation make
this an easier task than one could reasonably expect. In light of these observations
we introduce Qwire, a tool for writing verifiable, large scale quantum programs.
Qwire is not merely a language for writing and verifying quantum circuits: it is a
verified circuit description language. This means that the semantics of Qwire circuits
are verified in the Coq proof assistant. We also implement verified abstractions, like
ancilla management and reversible circuit compilation. Finally, we turn Qwire and
Coq’s abilities outwards, towards verifying popular quantum algorithms like quantum
teleportation. We argue that this tool provides a solid foundation for research into
quantum programming languages and formal verification going forward.
iv
Contents
List of Figures ix
List of Tables x
3 History 21
3.1 Circuits, QRAM and Classical Control . . . . . . . . . . . . . . . . . . . 21
3.2 QCL: A General Purpose Quantum Language . . . . . . . . . . . . . . 22
3.3 QPL: Semantics for Quantum Programming . . . . . . . . . . . . . . . 23
3.4 Linearity and the Quantum Lambda Calculi . . . . . . . . . . . . . . . 25
3.5 The Quantum IO Monad . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3.6 Quipper and the Proto-Quippers . . . . . . . . . . . . . . . . . . . . . . 27
3.7 Liquid, Revs and Q# . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3.8 The World of Quantum Programming . . . . . . . . . . . . . . . . . . . 30
3.9 Models of Quantum Computation . . . . . . . . . . . . . . . . . . . . . . 30
3.10 Formal Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3.10.1 Quantum Logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3.10.2 Mechanized Verification . . . . . . . . . . . . . . . . . . . . . . . 32
v
4 Qwire in Theory 34
4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
4.1.1 The Best of Both Worlds: Qwire . . . . . . . . . . . . . . . . . 35
4.1.2 Chapter Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
4.2 Qwire by Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4.3 The Qwire Circuit Language . . . . . . . . . . . . . . . . . . . . . . . . 40
4.3.1 Circuit Language . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
4.3.2 Host Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
4.3.3 Static Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
4.4 Operational Semantics: Circuit Normalization . . . . . . . . . . . . . . 45
4.4.1 Type Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
4.5 Denotational Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
4.5.1 Operational Behavior of run . . . . . . . . . . . . . . . . . . . . 53
4.6 A Categorical Semantics for Qwire . . . . . . . . . . . . . . . . . . . . 53
4.7 Dependent Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
4.8 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
5 Qwire in Practice 57
5.1 Circuits in Coq . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
5.2 Typing Qwire . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
5.3 De Bruijin Circuits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
5.4 Matrices and Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
5.4.1 Complex Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . 63
5.4.2 The Matrix Library . . . . . . . . . . . . . . . . . . . . . . . . . . 64
5.4.3 Density Matrices . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
5.5 Denotation of Qwire . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
5.6 Functional Notations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
6 Verifying Qwire 73
6.1 Predicates and Preservation . . . . . . . . . . . . . . . . . . . . . . . . . 73
6.1.1 Well-Formed Matrices . . . . . . . . . . . . . . . . . . . . . . . . 73
6.1.2 Unitarity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
6.1.3 Pure and Mixed States . . . . . . . . . . . . . . . . . . . . . . . . 75
6.1.4 Superoperator Correctness . . . . . . . . . . . . . . . . . . . . . . 76
6.2 Towards Compositionality . . . . . . . . . . . . . . . . . . . . . . . . . . 77
6.3 Future Work on Qwire’s Metatheory . . . . . . . . . . . . . . . . . . . 78
vi
7.2.1 Many Coins . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
7.3 Algebraic Reasoning about Circuits . . . . . . . . . . . . . . . . . . . . . 84
7.3.1 A Unitary and Its Adjoint . . . . . . . . . . . . . . . . . . . . . . 84
7.4 Equational Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
8 Reversibility 87
8.1 Ancillae and Assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
8.2 Safe and Unsafe Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 90
8.3 Syntactically Valid Ancillae . . . . . . . . . . . . . . . . . . . . . . . . . 92
8.4 Compiling Oracles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
8.5 Quantum Arithmetic in Qwire . . . . . . . . . . . . . . . . . . . . . . . 97
8.6 Next Steps for Reversible Computation . . . . . . . . . . . . . . . . . . 98
9 Automation 100
9.1 Typechecking Circuits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
9.1.1 Monoid . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104
9.1.2 Validate . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
9.2 Arithmetic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
9.3 Linear Algebra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
9.3.1 Matrix Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
9.3.2 Solving Matrix Equalities . . . . . . . . . . . . . . . . . . . . . . 108
9.4 Denoting Circuits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
9.5 Tactics Reference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110
vii
C Qwire Documentation 137
C.1 Prelim.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137
C.2 Monad.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137
C.3 Monoid.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137
C.4 Matrix.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137
C.5 Quantum.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137
C.6 Contexts.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137
C.7 HOASCircuits.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138
C.8 DBCircuits.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138
C.9 Denotation.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138
C.10 HOASLib.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138
C.11 SemanticLib.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138
C.12 HOASExamples.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138
C.13 HOASProofs.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138
C.14 Equations.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138
C.15 Composition.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138
C.16 Ancilla.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139
C.17 Symmetric.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139
C.18 Oracles.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139
Bibliography 140
viii
List of Figures
ix
List of Tables
x
Chapter 1
1.1 Motivation
In 1936, Alonzo Church wrote a programming language for a machine that didn’t
exist. His lambda calculus (Church, 1936a) influenced many of the programming lan-
guages that would emerge with the advent of the programmable computer in the
1940s. This, of course, wasn’t Church’s goal: He had in his sights Hilbert’s Entschei-
dungsproblem, which asked whether one could write an algorithm to prove arbitrary
statements in first-order logic. Church (1936b) and Turing (1937) both answered this
problem in the negative and, in doing so, proposed “universal” models of computation
that fundamentally ignored the scientific revolution of ten years prior.
While Church and Turing’s models of computation were able to express which
problems were computable in theory, they were woefully ill-equipped to describe which
problems were solvable in practice, even using the language of complexity theory.
Richard Feynman first recognized this in 1982 (Feynman, 1982), pointing out that a
Turing machine was seemingly incapable of efficiently simulating physics, since physics
obeys the mathematically complex laws of quantum mechanics. This shortcoming was
both surprising and disappointing: You would expect that we could simulate basic
physical processes on our so-called universal computers.
David Deutsch (1985) addressed this problem three years later. He proposed a
“Quantum Turing Machine” that could serve as the basis for quantum complexity the-
ory. Complexity theorists ran with this idea, introducing the classes BQP (Bounded-
Error Quantum Polynomial-Time) (Bernstein and Vazirani, 1997) and QMA (Quan-
tum Merlin-Arthur) (Watrous, 2000), and studying their relationships to the classical
and probabilistic complexity classes. These studies led to breakthrough quantum al-
gorithms, including Shor’s algorithm (1994) for computing prime factors and discrete
logarithms, and Grover’s algorithm (1996) for unstructured search. While Grover’s
algorithm led only to a quadratic speedup, Shor’s algorithm factored numbers in
polynomial time, suggesting that BQP (the quantum analogue of polynomial time,
or P) is strictly larger than P. This suggestion was reinforced by subsequent results,
1
such as Raz and Avishay’s (2018) proof of an oracle separation between BQP and the
polynomial hierarchy. By now, Quantum Complexity Theory is featured in standard
complexity theory textbooks (for example, Arora and Barak (2009)) and even books
aimed at a popular audience (Aaronson, 2013).
While the complexity theorists and algorithms designers have done an impres-
sive job of telling future quantum programmers what to program, programming lan-
guages researchers have lagged behind in telling them how to program. This presents
a dilemma. When general-purpose quantum computers see the light of day (soon,
judging by recent efforts at technology giants Google1 , IBM2 , Intel3 , Microsoft4 and
Alibaba5 , as well as the start-up Rigetti Computing6 ), people will program them.
And if they are forced to invent ad-hoc programming languages to address the chal-
lenges of the moment, we risk introducing design flaws that will plague generations
of quantum programmers.
Reassuringly, programming languages research has a head start on actual quan-
tum computers. Several important paradigms have gained traction within the quan-
tum programming languages community, including the QRAM model (Knill, 1996),
in which a quantum computer is used as a sort of oracle by a connected classical
computer, and Selinger’s (2004a) refinement called quantum data, classical control,
in which data may be quantum, but a program’s control flow is always classical. A
special case of Selinger’s approach is the quantum circuit model, in which a classical
computer constructs quantum circuits and sends them to a quantum computer for
execution.
The twenty-two years since Knill wrote his “Conventions for Quantum Pseu-
docode” (Knill, 1996) have seen the proliferation of quantum programming languages,
which we can loosely classify into two groups:
In the first category we have languages like QPL (Selinger, 2004a), λq (van Ton-
der, 2004), and the Quantum Lambda Calculus (Selinger and Valiron, 2009). QPL
1
https://www.technologyreview.com/s/604242/googles-new-chip-is-a-stepping-
stone-to-quantum-computing-supremacy
2
https://www.technologyreview.com/s/607887/ibm-nudges-ahead-in-the-race-for-
quantum-supremacy
3
https://www.technologyreview.com/s/603165/intel-bets-it-can-turn-everyday-
silicon-into-quantum-computings-wonder-material
4
http://www.nature.com/news/inside-microsoft-s-quest-for-a-topological-quantum-
computer-1.20774
5
https://medium.com/syncedreview/alibaba-launches-11-qubit-quantum-computing-
cloud-service-ad7f8e02cc8
6
https://www.forbes.com/sites/alexknapp/2018/09/07/rigetti-computing-takes-
small-step-toward-cloud-services-in-big-leap-for-quantum-computing
2
was one of the first proposed quantum programming languages, with a denotational
semantics given in terms of string diagrams and density matrices. This language was
used as a model language in a number of subsequent works, such as Kakutani’s (2009)
Hoare-like logic QHL and D’Hondt and Panangaden’s (2006) Quantum Weakest Pre-
conditions. Van Tonder’s λq and Selinger and Valiron’s Quantum Lambda Calculus
are both adaptations of Church’s lambda calculus to a quantum setting. λq focuses
on expressivity and sketches a proof of equivalence to Yao’s (1993) quantum circuit
model and thereby to the quantum Turing machine. Selinger and Valiron’s calcu-
lus, by contrast, focuses on the language’s linear type system, which enforces the
no-cloning theorem of quantum mechanics by guaranteeing that each qubit is used
exactly once. None of these languages are designed for practical quantum computing,
however.
By contrast, quantum circuit languages like QCL (Ömer, 2000, 2003), Quip-
per (Green et al., 2013a,b), Liquid (Wecker and Svore, 2014), and Q# (Svore et al.,
2018) are designed for efficient, general-purpose quantum computing. QCL is a C-like
language with support for both classical and quantum computing, where Quipper
and Liquid are embedded in Haskell and F#, respectively, and are capable of us-
ing these languages’ features and libraries to construct complex families of quantum
circuits. Q# (Svore et al., 2018) is a recent standalone successor to Liquid, meant
to reduce reliance on F# and provide a programming environment targeted exclu-
sively at quantum computing. All of these languages provide optimized compilation
to low-level circuits and can simulate quantum computation. Unfortunately, they lack
important features of QPL and the Quantum Lambda Calculus, such as denotational
semantics and type systems that guarantee circuits are well-formed.
Given the cost and expressive power of quantum computing, we need a program-
ming language that fits in both of these categories. It should take advantage of existing
programming languages research, which strongly suggests using the quantum circuit
model adopted by Quipper and Liquid, as well as their abstractions and optimizations.
It must ensure that any quantum program sent to the quantum computer represents
a valid quantum mechanical operation, as guaranteed by the Quantum Lambda Cal-
culus’ linear type system. And finally, it must be provably safe and easy to reason
about, in the style of QPL.
This last requirement is partly born of necessity: Quantum programs are tremen-
dously difficult to understand and implement, almost guaranteeing that they will
have bugs. And traditional approaches to debugging will not help us: We cannot
set breakpoints and look at our qubits without collapsing the quantum state. Even
techniques like unit tests and random testing will be impossible to run on classical
machines and too expensive to run on quantum computers – and failed tests are
unlikely to be informative. But this requirement is also born of opportunity: The
underlying mathematics of quantum computing is well understood, and it is easier
to model mathematically than classical programs with probabilistic operations. This
lowers the cost of formal verification, and it can make the most powerful form of
3
program specification into the most convenient as well.
The overarching goal of this thesis is to write and verify quantum programs to-
gether. Towards that end, we introduce a quantum programming language called
Qwire and embed it inside the Coq proof assistant. We give it a linear type system
to ensure that it obeys the laws of quantum mechanics and a denotational seman-
tics to prove that programs behave as desired. We also formalize the metatheory of
Qwire to ensure that the language itself is well-behaved and only supports physically
realizable computation. We use Qwire’s rich type theory and semantic guarantees
to implement features that could not be safely implemented in other languages, from
circuit families to assertive terminations. And, naturally, we use Qwire to verify
existing algorithms from the quantum computing literature.
1.3 Outline
We begin by introducing the basics of quantum computing (Chapter 2). We then take
a look at the history of quantum programming languages, from van Tonder’s (2003)
quantum lambda calculus to powerful modern languages like Quipper (Green et al.,
2013a) and Q# (Svore et al., 2018). That brings us to the core of the thesis, the
quantum circuit language Qwire.
Qwire is an embedded circuit generation language for quantum computing. In
Chapter 4, we give Qwire a denotational semantics in terms of density matrices,
a linear type system that guarantees circuits are well formed, and a dynamic lifting
operation for communication between a classical and a quantum computer.
We embed Qwire inside the Coq proof assistant (Chapter 5), tying its variables
to those of Coq’s programming language Gallina, and implementing a typechecking
algorithm as a Coq tactic. We also provide a direct translation to Qwire’s semantics
in terms of density matrices, allowing us to prove properties of generated circuits.
These density matrices rely on our own libraries for linear algebra and quantum
information theory, together with Coquelicot’s (Boldo et al., 2015) complex num-
ber library. We explore Qwire’s metatheory in Chapter 6, showing that well-typed
circuits correspond to quantum-mechanically sound functions on quantum states. In
chapter Chapter 7, we use the resulting semantics to prove the properties of a number
of quantum programs, including quantum teleportation, Deutsch’s algorithm (1985),
and a variety of coin flipping protocols.
While these chapters assume familiarity with the Coq proof assistant, we hope
that they will be accessible to most readers with some knowledge of functional pro-
4
gramming and formal verification. For the reader who would like to understand the
Coq programming language better, we recommend our online tutorial (Rand and
de Amorim, 2016) or the more comprehensive “Software Foundations,” which also
delves deeply into programming languages and type theory, both of which will aid
the reader in digesting this work.
With Qwire in hand, we can begin to explore a type-safe approach to high-level
quantum programming (Chapter 8, based on Rand et al. (2018a)). We begin by imple-
menting some of the core features of Green et al.’s Quipper language using dependent
types. Quipper makes heavy use of ancillas, temporary qubits that are initialized in
some state and discarded in the same state, at least according to the assertions that
accompany the discard operation. Unfortunately, Quipper has no way of ensuring that
these assertions are true. Worse, the compiler relies upon these assertions, so when an
assertion is false, the compiled program is likely to misbehave. We include assertions
in the Coq implementation of Qwire and require the programmer to prove them
correct before the program will compile. We also provide an assertion-using compiler
from boolean expressions to Qwire circuits, and we prove that the generated circuits
compute the same functions as the provided expressions.
All of this work requires a significant amount of reasoning, from proving that cir-
cuits are well typed to showing that they compute the desired function. As we built
Qwire, we noticed which tasks demanded a lot of our own time and attempted to
automate them, for our benefit and that of future users. Chapter 9 discusses the vari-
ous forms of automation present in Qwire, from the monoidal solver and disjointness
checker used by our linear typechecker to the range of tactics used in proving matrix
equalities.
Given that most of this dissertation discusses the ideas that underlie Qwire, in
Chapter 10 we pause the high-level exposition and delve into the Coq development
itself. There we discuss the assumptions that we use in Qwire and attempt to justify
them. We also include every proof and assumption in this thesis in Appendix C, which
we urge the reader to consult, especially if an English-language description proves
ambiguous. We also encourage the reader to step through the Coq development itself,
available at https://github.com/inQWIRE/QWIRE.
Some of this work appears in two prior papers by Paykin, Rand, and Zdancewic:
Paykin et al. (2017) and Rand et al. (2017). The first paper, which introduces the
Qwire language and its type system and denotational semantics, forms the basis
for Chapter 4. The second paper contains early details of Qwire’s implementation,
along with proofs of some basic circuit equalities. Many of the more interesting Qwire
proofs, particularly those about its metatheory, have yet to be published.
We developed Qwire together with Jennifer Paykin, Steve Zdancewic, and Dong-
Ho Lee at the University of Pennsylvania. Though every collaborator was involved in
multiple aspects of Qwire’s development, we can briefly describe the focuses of each
author. This author’s main contributions were towards the semantics of Qwire, its
implementation, and its applications towards formal verification, as explored in this
5
thesis. Paykin designed the language itself and its linear type system, as part of a
line of investigation into linear types, including the linear/producer/consumer model
of classical linear logic (Paykin and Zdancewic, 2016), the linearity monad (Paykin
and Zdancewic, 2017), and her dissertation (Paykin, 2018). Zdancewic, our advisor,
helped flesh out most of the ideas underlying Qwire, primarily when they consisted of
sketches on whiteboards. Finally, Lee contributed to the study of reversible computing
in Qwire (Rand et al., 2018a), providing the quantum adder discussed in Chapter 8,
as well as a compiler from Qwire to lower level “quantum assembly” languages that
we discuss in Chapter 11. That chapter also discusses future directions for Qwire,
from verified optimizations to quantum error correction.
6
Chapter 2
An Introduction to Quantum
Computing
In this chapter, we introduce the basics of quantum computation, starting with sim-
ple qubits and proceeding to concepts like superposition, entanglement, and unitary
transformations. We only assume knowledge of basic linear algebra and try to elide
any concepts not directly relevant to this dissertation, particularly those related to the
physics of quantum computation. To assist the unfamiliar reader, we have included
a number of exercises, which should help them internalize ideas as we present them.
Solutions to these exercises are provided in Appendix A.
2.1 Qubits
Qubits, a pun on the ancient unit of measure, “cubit,” are the quantum analogue
of bits. While qubits can take on a variety of configurations, called states, the two
simplest correspond to the binary 0 and 1 and are written ∣0⟩ and ∣1⟩. We call these
the basis states. They may represent different amounts of charge on a wire, or base
particles rotating clockwise versus counterclockwise—as in classical computing, the
physical implementation of qubits does not concern us.
Conveniently, when describing operations on qubits, we can describe their behavior
on basis states and then lift this behavior to more complicated quantum states. One
common “classical” operation on qubits is Wolfgang Pauli’s X (or NOT ) operator,
which behaves like classical negation:
X ∣0⟩ = ∣1⟩
X ∣1⟩ = ∣0⟩
We concatenate qubits using the tensor operator ⊗. For instance, a ∣1⟩ qubit next
to a ∣0⟩ qubit can be written as ∣1⟩ ⊗ ∣0⟩, or ∣10⟩ for short. Note that these qubits
are ordered: There is a first qubit (the ∣1⟩) and a second qubit (the ∣0⟩). We can now
7
define the controlled-not (or CNOT ) operator on two qubit states:
When the first qubit is ∣1⟩, the second qubit is negated; otherwise, both qubits are
unchanged. The meaning of “controlled-not” should therefore be apparent: The first
qubit controls whether the second is negated or not. This notion of control can be
generalized as follows: For any operator f on k qubits, a “controlled” f is an operator
on k + 1 qubits that applies f if the first qubit is ∣1⟩ and otherwise applies the identity
function. Note that if we iterate the “control” operation, the function will be applied
only if all of the controlling qubits (or “controls”) are ∣1⟩. The controls themselves are
never altered by this operation.
1 1
H ∣0⟩ = √ ∣0⟩ + √ ∣1⟩
2 2
1 1
H ∣1⟩ = √ ∣0⟩ + − √ ∣1⟩
2 2
The scaling factors to the left of ∣0⟩ and ∣1⟩ are complex numbers called amplitudes,
and the expression α ∣0⟩ + β ∣1⟩ represents a superposition, a weighted combination of
∣0⟩ and ∣1⟩. This has no analogue in classical physics, but for our purposes “a weighted
combination” will suffice. The + symbol here behaves like addition: It is commutative
and associative and obeys distributive laws, with both scaling and tensor being a
form of multiplication. Additionally, ∣ψ⟩ and − ∣ψ⟩ cancel each other out, as we will
see in the following example.
Applying an operator to a qubit in a superposition of ∣0⟩ and ∣1⟩ is the same as
applying it to each of the basis qubits, as in the following example:
8
1 1 1 1
H ( √ ∣0⟩ + √ ∣1⟩) = √ H ∣0⟩ + √ H ∣1⟩
2 2 2 2
1 1 1 1 1 1
= √ ( √ ∣0⟩ + √ ∣1⟩) + √ ( √ ∣0⟩ − √ ∣1⟩)
2 2 2 2 2 2
1 1 1 1
= ∣0⟩ + ∣1⟩ + ∣0⟩ − ∣1⟩
2 2 2 2
1 1
= ∣0⟩ + ∣0⟩
2 2
= ∣0⟩
We see that the Hadamard operator can take a non-basis state to a basis state
(this will be true of all our operators).
1 1 1 1
CNOT [( √ ∣0⟩ + √ ∣1⟩) ⊗ ∣0⟩] = CNOT ( √ ∣00⟩ + √ ∣10⟩)
2 2 2 2
1 1
= √ (CNOT ∣00⟩) + √ (CNOT ∣10⟩)
2 2
1 1
= √ ∣00⟩ + √ ∣11⟩
2 2
In this new state, the two qubits are intertwined with one another: It is no longer
possible to express this state as the tensor product of two distinct one-qubit states.
We call this state of affairs entanglement, and it is closely related to the dependence
of two random variables in probability theory.
Measurement To see where probability enters the picture, we have to introduce the
measurement operator, meas, which, unlike X, H and CNOT , can only be expressed
as a function on the whole qubit, not its components:
⎧
⎪ 2
⎪∣0⟩
with probability ∣α∣
meas(α ∣0⟩ + β ∣1⟩) = ⎨
⎪ 2
⎩∣1⟩
⎪ with probability ∣β∣
√
The modulus of a complex number ∣a + bi∣ is a2 + b2 , so whenever the imaginary
component is zero, taking the modulus squared is the same as squaring the number.
9
2 2
Note that in any single qubit state α ∣0⟩ + β ∣1⟩, we have ∣α∣ + ∣β∣ = 1, allowing us to
translate amplitudes into probabilities.
We can see that measuring ∣0⟩ always yields ∣0⟩ and similarly for ∣1⟩, since the
basis state ∣0⟩ is really 1 ∣0⟩ + 0 ∣1⟩. Measuring H ∣0⟩ or H ∣1⟩ will yield each basis state
2
with one-half probability, since √12 = (− √12 )2 = 12 . Measurement is idempotent: Once
we have measured a qubit, it enters the basis state ∣0⟩ or ∣1⟩, so measuring it a second
time has no impact.
We can easily extend this notion of measurement to a multi-qubit system. If we
have the state ∑i αi ∣i⟩ , where ∣i⟩ ranges over the basis states ∣0 . . . 0⟩ through ∣1 . . . 1⟩,
2
the probability that measurement returns ∣i⟩ is ∣αi ∣ .
What if we want to measure one qubit in a multiple qubit system? Let ∑i αi ∣i⟩
represent the part of the state in which the qubit to be measured is ∣0⟩ and ∑j βj ∣j⟩
represent the part in which the qubit is ∣1⟩. Then the probability p0 of measuring our
2
qubit as ∣0⟩ is ∑i ∣αi ∣ , yielding the state
1
√ ∑ αi ∣i⟩
p0 i
and similarly for p1 and ∣1⟩. The scaling factor √1pi renormalizes the quantum state
so that the squares of the amplitudes still add up to 1.
For example, suppose we want to measure the first qubit in the state
1 2+i 1
∣00⟩ + ∣01⟩ + √ ∣11⟩ .
3 3 3
Exercise 2. Now try measuring the second qubit in both of these cases. Verify that
the distribution of results is the same as if we had measured the whole system at
once.
10
Exercise 3. Verify that after measuring a qubit, the norm of the quantum state is
still one.
Z ∣0⟩ = ∣0⟩
Z ∣1⟩ = − ∣1⟩
The setup for quantum teleportation is as follows: Alice and Bob share a Bell
pair, a pair of qubits in the entangled state √12 ∣00⟩ + √12 ∣11⟩, with Alice holding the
first qubit (a) and Bob the second (b). We will annotate these qubits with a and b
for readability. Though they may be separated by some distance, they are entangled,
and hence we use a single quantum state to represent them. Alice wants to send the
state of some third qubit q in the state α ∣0⟩ + β ∣1⟩ to Bob but she has no quantum
channel, only classical channels that can transmit non-quantum bits.
Hence, we begin with the state
1 1
(α ∣0⟩ + β ∣1⟩)q ( √ ∣0a 0b ⟩ + √ ∣1a 1b ⟩)
2 2
which we can expand to
1
√ (α ∣0q 0a 0b ⟩ + α ∣0q 1a 1b ⟩ + β ∣1q 0a 0b ⟩ + β ∣1q 1a 1b ⟩).
2
Alice first applies a CNOT from q (the controlling qubit) to a, obtaining the
following state:
1
√ (α ∣0q 0a 0b ⟩ + α ∣0q 1a 1b ⟩ + β ∣1q 1a 0b ⟩ + β ∣1q 0a 1b ⟩)
2
She then applies a Hadamard to q, obtaining
1 1
√ ∗ √ ((α ∣0q 0a 0b ⟩ + α ∣1q 0a 0b ⟩) + (α ∣0q 1a 1b ⟩ + α ∣1q 1a 1b ⟩)+
2 2
Alice’s final step is to measure her qubits and then send the results of the mea-
11
surements, which can each be encoded using a classical bit, to Bob. Let’s rearrange
some terms to simplify our calculations:
1
( ∣0q 0a ⟩ (α ∣0⟩ + β ∣1⟩)b + ∣0q 1a ⟩ (α ∣1⟩ + β ∣0⟩)b +
2
2 2
Case 1: Alice measured ∣0q 0a ⟩. This case occurs with probability ∣ 12 α∣ + ∣ 12 β∣ .
2 2
Since ∣α∣ + ∣β∣ = 1, this is equal to 14 , and we rescale by the square root of that
probability, or 12 . Hence we arrive at the state:
Bob’s qubit is in precisely the state of Alice’s original qubit, and the teleportation
is complete.
Case 2: Alice measured ∣0q 1a ⟩. This also occurs with probability 41 . Bob obtains
the state
∣0q 1a ⟩ (α ∣1⟩ + β ∣0⟩)b
He applies an X to his qubit and obtains the desired state.
Bob first applies an X to obtain the state of case 3, and then applies a Z to obtain
Alice’s original quantum state.
12
alice bob
∣ϕ⟩ H meas
bell00
0 H meas
0 X Z ∣ϕ⟩
α
( )
β
.
For the more general quantum state α0 ∣00 . . . 0⟩ + α1 ∣00 . . . 1⟩ + ⋅ ⋅ ⋅ + αn−1 ∣11 . . . 1⟩
we have the following vector:
⎛ α0 ⎞
⎜ α1 ⎟
⎜ ⎟
⎜ ⋮ ⎟
⎝αn−1 ⎠
13
.
Note that the k th element in the matrix is the coefficient of ∣kb ⟩, where kb is the
binary representation of k. This makes it easy to switch between representations.
What is the meaning of ∣ϕ⟩ ⊗ ∣ψ⟩ in vector notation? The tensor, or Kronecker
product, takes an m × n matrix A and o × p matrix B and returns a mo × np matrix
with copies of B tiled inside A. Visually, we have:
⎛ A1,1 B1,1 ... A1,1 B1,p ... ... A1,n B1,1 ... A1,n B1,p ⎞
⎜ ⋮ ⋱ ⋮ ... ... ⋮ ⋱ ⋮ ⎟
⎜ ⎟
⎜ A1,1 Bo,1 ... A1,1 Bo,p ... ... A1,n B1,1 ... A1,n Bo,p ⎟
⎜ ⎟
⎜ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⎟
⎜ ⎟
⎜ ⎟
⎜ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⎟
⎜ ⎟
⎜ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⎟
⎜ ⎟
⎜A B Am,n B1,p ⎟
⎜ m,1 1,1 ... Am,1 B1,p ... ... Am,n B1,1 ... ⎟
⎜ ⎟
⎜ ⋮ ⋱ ⋮ ... ... ⋮ ⋱ ⋮ ⎟
⎝Am,1 Bo,1 ... Am,1 Bo,p ... ... Am,n B1,1 ... Am,n Bo,p ⎠
Note that in the vector case, multiplying an m length vector by an n length vector
returns a vector of length mn. However, the general case of the Kronecker product
will prove useful, as we will see shortly.
Exercise 4. Write (α ∣0⟩+β ∣1⟩)⊗(γ ∣0⟩+δ ∣1⟩) as a vector, first by taking the Kronecker
product directly and then by simplifying the expression and transforming it into vector
notation. Confirm that both results are equal.
A valid quantum operation should preserve this property and the size of the vector.
We call such operations unitary.
Unitary transformations correspond precisely to unitary matrices, square matrices
U satisfying the following:
U U † = I = U †U
Here I is the identity matrix, and the adjoint of U , U † , is a generalization of the
transpose that takes the complex conjugate Aij of all the elements. That is, it flips
the sign of the imaginary components of all the elements. For an example, let’s take
14
the transpose of Wolfgang Pauli’s Y matrix:
†
0 −i 0 i 0 −i
Y =(
†
) =( )=( )=Y
i 0 −i 0 i 0
0 −i 0 −i 0 + (−i)i 0+0 1 0
( )( )=( )=( )
i 0 i 0 0+0 i(−i) + 0 0 1
1 1 1 0 1 1 0
H=√ ( ), X = ( ), Z = ( )
2 1 −1 1 0 0 −1
The controlled version of any n-qubit gate U is represented by the block matrix
I2n 0
( )
0 U
The CNOT is simply the controlled X gate, and the controlled CNOT is called the
Toffoli (TOF or CCNOT ) gate.
Exercise 5. Note that H, X, Z, and CNOT are all their own adjoints. Verify that
these matrices are unitary.
Exercise 6. Show that H, X, Z, and CNOT have the behavior described in the
previous section. That is, show that when applied to basis vectors ( 10 ) and ( 01 ) they
produce the claimed output.
What does it mean mathematically to apply an operation to a single qubit in a
multi-qubit system? Suppose we want to apply an H to the second qubit of a three
15
qubit system. We pad H on either side with 2 × 2 identity matrices and then apply
I2 ⊗ H ⊗ I2 to the quantum state. An arithmetic identity called the Kronecker mixed
product says that (A ⊗ B)(C ⊗ D) = AC ⊗ BD (provided the dimensions line up), so
if the target system is separable into ∣ψ⟩1 ∣ϕ⟩ ∣ψ⟩2 , we get
as we would hope.
In general, a quantum computer can be expected to implement some number
of unitary operations as primitive gates, though the precise set of primitives will
differ based on architecture. It is important, however, that the implemented set be
universal for quantum computation – that is, it can be used to efficiently approximate
any unitary transformation. Here, the following two theorems are relevant:
The Solovay-Kitaev1 theorem (Dawson and Nielsen, 2005; Nielsen and Chuang,
2010), which was generalized to multiple qubit matrices, tells us that universal gate
sets can generally be interchanged with little loss of efficiency, provided that they
consist of gates on small numbers of qubits. Hence, the specific choice of gate set is
likely to depend on a given quantum computer’s hardware. Shi (2003) gives a number
of strong candidates for universal sets to use in practice; Aharonov (2003) discusses
the variety of gate sets known to be universal.
Many functions do not correspond to valid unitary transformation and therefore
cannot be applied to quantum states. One important such function is the subject of
the no-cloning theorem:
Theorem 4 (No Cloning). There is no unitary transformation that copies the state
of an arbitrary qubit (that is, takes ∣ϕ⟩ ∣0⟩ to ∣ϕ⟩ ∣ϕ⟩).
This theorem is due to Dieks (1982) and Wooters and Zurek (1982); a succinct
proof is given on page 523 of Nielsen and Chuang (2010). The no-cloning theorem
will motivate our use of linear types (which prevent us from copying terms) in the
Qwire quantum circuit language (Chapter 4).
1
This result was announced by both Solovay and Kitaev, but there is no corresponding publica-
tion; see Dawson.
16
2.5 Mixed States as Density Matrices
At this point, we want to expand our notion of quantum states. So far, a quantum
state has simply been a 2n -length complex vector, whose norm is equal to one. From
here on we will call this a pure state. Note, however, that one of our operations—
measurement—takes a pure state to a distribution over pure states. Since we would
like to talk about these distributions directly, we will refer to them as mixed states.
Consider what happens if we apply a Hadamard H to the basis state ∣0⟩ and then
measure it. We will obtain a distribution over ∣0⟩ and ∣1⟩, with 12 probability assigned
to each outcome. We can (naively) write this as
1 1
{ ( , ∣0⟩), ( , ∣1⟩) }
2 2
where the real numbers on the left represent probabilities and the quantum states on
the right represent measurement outcomes.
What if, without looking at the outcome of the measurement, we then apply
another Hadamard to the state? We should obtain
1 1
{ ( , H ∣0⟩), ( , H ∣1⟩) }
2 2
which expands out to
1 1 1 1 1 1
{ ( , √ ∣0⟩ + √ ∣1⟩), ( , √ ∣0⟩ − √ ∣1⟩ }.
2 2 2 2 2 2
An interesting theorem of quantum mechanics says that the two distributions
mentioned above are physically indistinguishable. For instance, if we measured either
of the distributions above and examined the outcome, we would obtain ∣0⟩ with prob-
ability 12 and ∣1⟩ with probability 12 . If we applied a Hadamard to either state, we
would simply toggle between the two indistinguishable states, since HH ∣0⟩ = ∣0⟩ and
likewise for ∣1⟩. Ideally, any language for talking about these states would identify
them, but here the language of probability distributions over quantum states fails us.
Instead, we present an alternative way of representing quantum states that iden-
tifies these distributions with each other. A density matrix is a square matrix of
dimensions 2n × 2n that we can use to represent both pure and mixed quantum states.
We can convert a pure state ∣ϕ⟩ in vector form to its density matrix representation by
multiplying it by its adjoint, commonly written ⟨ϕ∣. So, for instance, the basis states
∣0⟩ and ∣1⟩ become
1 1 0
∣0⟩ ⟨0∣ = ( ) (1 0) = ( )
0 0 0
and
0 0 0
∣1⟩ ⟨1∣ = ( ) (0 1) = ( ).
1 0 1
17
Conveniently, we can check if a density matrix corresponds to a pure state by
squaring it. For any pure state ρ in density matrix form, ρ2 = ρ, and this is true only
of pure states.
Exercise 7. Prove the first half of the above statement.
What if we want to apply a unitary matrix U to some quantum state ρ in its
density matrix form? Let us first consider the case in which ρ = ∣ϕ⟩ ⟨ϕ∣ (that is, ρ is a
pure state). Applying U to ∣ϕ⟩ ⟨ϕ∣ should give us (U ∣ϕ⟩)(U ∣ϕ⟩)† . We can distribute the
†
adjoint over multiplication, obtaining (U ∣ϕ⟩)(∣ϕ⟩ U † ), which we write as U ∣ϕ⟩ ⟨ϕ∣ U † .
This gives us the formula for applying a unitary to a density matrix: We multiply
the matrix by U on its left and U † on its right. Since density matrices and unitary
operators are always square, if the dimensions are correct on the left, they will match
up on the right.
What about measurement? This representation has the advantage of treating mea-
surement as a deterministic operation on density matrices, rather than a probabilistic
operation on vectors. Measuring a single qubit can be represented as follows:
You can think of this operation as adding together the two outcomes of measure-
ment. The left hand side represents the event of measuring ∣0⟩ and the right-hand
side, measuring ∣1⟩.
Let us return to the example that started this section. We start with the 0 qubit,
represented in density matrix form as
1 0
( ).
0 0
1 1 1 1 0 1 1 1 1 1 1
√ ( )( ) (√ ( )) = ( ).
2 1 −1 0 0 2 1 −1 2 1 1
1 0 1 1 1 1 0 0 0 1 1 1 0 0
( )( ( )) ( )+( )( ( )) ( )
0 0 2 1 1 0 0 0 1 2 1 1 1 0
1 1 0 1 0 0
= ( )+ ( )
2 0 0 2 0 1
1 1 0
= ( )
2 0 1
As we see from the second line, there is a one-half probability of measuring ∣0⟩ and
one-half-probability of measuring ∣1⟩. This helps us interpret the result. Each element
18
along the diagonal represents the probability of obtaining the corresponding basis
state upon measurement (when we look at the result). Note that this was also true
before we measured the state: Measurement simply removed the elements that weren’t
along the main diagonal, which indicated that the qubit was in a superposition, rather
than a simple distribution.
As we noted earlier, applying another Hadamard to this state doesn’t change it:
1 1 1 1 1 0 1 1 1
√ ( )( ( )) ( √ ( ))
2 1 −1 2 0 1 2 1 −1
1 1 1 1 1
= ( )( )
4 1 −1 1 −1
1 2 0
= ( )
4 0 2
1 1 0
= ( )
2 0 1
Exercise 8. Show that for a pure state in density matrix form, the ith element along
the diagonal is the probability of measuring ∣i⟩.
We can do the same thing for ∣1⟩. In density matrix form, we write (⟨0∣⊗I)ρ(∣0⟩⊗I)
or (⟨1∣⊗I)ρ(∣1⟩⊗I). Density matrices also allow us to deal with the more general case,
where we may not know whether the qubit to be discarded is ∣0⟩ or ∣1⟩. We then write
the discard operation as (∣0⟩ ⊗ I)ρ(⟨0∣ ⊗ I) + (∣1⟩ ⊗ I)ρ(⟨1∣ ⊗ I). Note that if the qubit
to be discarded is ∣0⟩, the right hand side will contain a ⟨1∣ ∣0⟩ = 0, and everything to
the right of the + will be the zero matrix. The same is true for ∣1⟩ and the left hand
side. This form of discard is convenient, in that it also applies to a superposition—in
this case, the qubit is implicitly being measured and then discarded. This accounts
for the similarity to meas above: Measurement can be thought of as measuring and
19
discarding a qubit, then adding a new qubit in the measured state.
This should be sufficient to understand the semantics of quantum programs, which
we will introduce in the upcoming sections.
20
Chapter 3
Classical Quantum
Computer Computer
measurement results
This model describes low-level languages like QASM (Balensiefer et al., 2005),
21
OpenQASM (Cross et al., 2017), and Quil (Smith et al., 2016) fairly precisely: Each
has distinct registers used for quantum computation, which the controlling machine
may measure and use in its computation. These “quantum assembly” languages are
used in practice to run quantum computations on IBM’s 20-qubit quantum computer
(the IBM Quantum Experience) and Rigetti Computing’s online Quantum Processing
Units.
Knill’s pseudocode guidelines suggest that quantum registers might also be used
as the guard in an IF-THEN-ELSE block, without detailing how to ensure such oper-
ations are quantum mechanically valid. In “Towards a Quantum Programming Lan-
guage,” Selinger (2004a) proposes a narrower model for quantum computing known
as quantum data, classical control. This widely adopted model states that the control
flow of a quantum program should always be classical: Though we take advantage
of the superposition of data, such as qubits, we should not attempt to run superpo-
sitions of programs. Instead, a quantum program should use classical conditionals,
loops, and recursion. Most of the languages discussed below follow this framework,
with the exception of QML (Altenkirch and Grattage, 2005). We will discuss the
alternative approach, known as quantum control, in Section 3.9.
So far, we’ve portrayed the interaction between classical and quantum processors
as unidirectional: The classical processor sends operations to the quantum computer,
which returns measurement results. However, this doesn’t tell the whole story. Occa-
sionally, a quantum computation will itself depend upon some complicated classical
computation, which we wouldn’t want to run on a dedicated quantum processor. This
classical computation, in turn, might depend on some measurement results. To deal
with this, Green et al. (2013a) introduce the notion of dynamic lifting. This operation
is initialized by the quantum processor, which sends data to the classical processor
and asks it to compute the remainder of the quantum operation (in Quipper’s case,
a circuit) for the QRAM to execute.
classical queries
Classical Quantum
Computer Computer
circuit continuations
Many of the languages we will look at implement some form of dynamic lifting.
22
follow. His QCL, an imperative-style language, included support for advanced features
like management of scratch qubits (or ancillae) and automatic circuit reversal.
QCL adheres pretty closely to Knill’s (1996) guidelines for quantum programming
languages. It assumes that execution of a quantum program is primarily guided by a
classical computer, which has an attached QRAM device for quantum operations.
In QCL, quantum operations are applied to sets of quantum registers. There are
various restricted forms of registers that allow for constant-valued qubits or registers
used exclusively for scratch space. These quscratch registers are garbage-collected
by a procedure that returns them to the ∣0⟩ state using Bennett’s (1973) technique.
We discuss this technique in detail in Chapter 8.
QCL also allows for a sort of quantum conditional. We can annotate any function
with the keyword cond to control all of its operations by a control qubit provided as an
argument. This necessarily restricts the function being controlled—it must correspond
to a unitary transformation on all its qubits; moreover, it cannot reference the control
qubit itself. This is accomplished via strict scoping rules. This construction is then
extended to allow for a limited quantum if statement and a bounded quantum while
loop.
Even more so than Knill (1996), QCL established a baseline for what quantum
programming languages should be able to do as well as a yardstick against which
other languages could compare themselves (see, for instance, Rüdiger (2006); Green
et al. (2013a)).
23
new qbit q:=0
q ∗= H
measure q
0 1
output q output q
the number of bits and qubits, respectively, by treating bits as simply qubits that
are always in one of the basis states. This representation is rejected in the paper in
favor of economy of representation, since large sparse matrices take up a lot of space,
but it is more conceptually parsimonious (easy to explain and reason about) and was
adopted as the semantics for QPL by Kakutani (2009).
QPL syntax prohibits cloning qubits: While QCL and other languages fail at
runtime if the user attempts to use the same qubit as both arguments to a CNOT
gate, QPL doesn’t allow aliasing and can therefore check that the arguments are
distinct at compile time.
While representing circuits as flowcharts didn’t catch on among quantum pro-
gramming languages, QPL conveyed some important ideas that gained wide currency.
Instead of including a quantum analogue of the IF statement, QPL treats measure-
ment itself as a branching construct, as can be easily seen in Figure 3.1. QPL was
also adopted as a target for verification efforts: Kakutani’s (2009) quantum Hoare
logic QHL reasons about QPL programs, and QPL programs are given a weakest
pre-expectation semantics by D’Hondt and Panangaden (2006). D’Hondt and Panan-
gaden’s WP semantics is dual to the given semantics for QPL and was used in a
subsequent line of work on quantum logics (Ying, 2011; Ying et al., 2017; Li and
Ying, 2018).
Muerer’s cQPL (2005) extends QPL with the ability to communicate with a clas-
sical computer, in line with the QRAM model, and a compiler to C code via QCL.
Nagarajan et al. (2007) provide a compiler to an instruction set for a Sequential
Quantum Random Access Memory (SQRAM) machine, based on Knill’s QRAM. Un-
fortunately, neither contribution was sufficient to make QPL into a general purpose
quantum programming language. Instead, QPL made a lasting contribution to the
24
areas of denotational semantics for quantum programs and compile time restrictions
on cloning qubits. This work would form the basis for the quantum lambda calculi.
1. reversibility of computation,
25
alice bob
∣ϕ⟩ H meas
0 H meas
0 X Z ∣ϕ⟩
Figure 3.2: The teleportation function, composed of the entangled functions “alice”
and “bob”
Selinger and Valiron’s (2006; 2008; 2009) Quantum Lambda Calculus is primarily
concerned with quantum functions and linear type systems for typing these functions.
To get a sense for quantum functions, let’s take another look at the teleport circuit
(Figure 3.2). Normally we would think of the alice circuit as a function from two
qubits to two bits, and we would think of bob as a function from a qubit and two
bits to a qubit. But this isn’t quite accurate: Quantum teleportation only works when
Alice and Bob share a pair of entangled qubits, or Bell pair, produced by the sub-
circuit at the bottom left. These should be treated as a shared resource, not a separate
pair of inputs. The alice function then takes a single qubit and returns a pair of
bits, while bob takes a pair of bits and returns a qubit. We can then say that for any
qubit q, bob (alice q) = q. Since these two functions share entangled qubits, we
call them entangled.
Another unique feature of these two quantum functions is that they’re limited
in their use. The alice circuit can clearly only be used once, since it measures (and
thereby destroys) its half of the Bell Pair. By contrast, bob never measures its half, but
it outputs that qubit and, hence, can no longer use it. This inspires the development
of a type system to guarantee that quantum data, including quantum functions, is
never duplicated.
To be precise, Selinger and Valiron’s lambda calculus incorporates an affine type
system that ensures that quantum data is used at most once. This prohibits the
programmer from copying data, whether in the form of qubits or quantum functions.
The type system also provides a ! (bang) operator to indicate types that may be
used multiple times, along with a subtyping system that allow terms of type !A to be
used wherever an A is called for. The quantum lambda calculus has an operational
semantics and a categorical semantics, which are valuable but not of direct relevance
to this thesis, and proofs of type soundness (progress and preservation).
These lambda calculi, and their type systems in particular, had significant impact
on subsequent programming languages, especially Quipper and our language, Qwire.
Before we talk about Quipper and Qwire, though, we should address another lan-
26
guage that strongly influenced both.
2. it gives QIO access to the full power of Haskell, including its typeclasses and
libraries; and
This last point was clearly illustrated by Green’s thesis (2010), which embed-
ded the Quantum IO Monad inside Agda. Agda (Bove et al., 2009), like Coq, is a
dependently-typed programming language that can also be used as a proof assistant.
The Agda implementation of QIO uses dependent types to prevent some instances of
qubit copying; for instance, applying a CNOT to the wires x and y requires a proof
that x and y are distinct. However, Green embedded QIO in Agda mainly with an
eye towards formal verification.
QIO includes a USem structure for representing the semantics of unitary opera-
tors. This is easily defined upon the classical fragment of unitary gates—gates like
X, CNOT , and CCNOT that can be expressed as functions on bits. For an arbitrary
unitary gate U , it defines the semantics of U in terms of its effect on each of the basis
states. Unfortunately, due to Agda’s lack of automation or a real or complex number
library (the author wrote a small axiomatic library of his own), it proved difficult to
prove that unitaries are, in fact, unitary, or to prove any properties of quantum cir-
cuits. Nevertheless, QIO presaged our own efforts in this area and influenced Quipper,
from which we took substantial inspiration.
27
required to implement quantum algorithms on a realistic quantum computer.” Javadi-
Abhari et al.’s Scaffold (2012; 2015), a powerful imperative quantum programming
language, was also developed as part of the QCS initiative. Quipper, like QML and
QIO, is embedded within Haskell, but its primary focus is on scalable quantum com-
puting. Towards that end, Quipper has a number of advanced features, including the
ability to compile classical programs to quantum circuits, optimize circuits, and sim-
ulate quantum computation within Haskell. Quipper was initially used to implement
seven complex quantum algorithms and study their resource requirements (Green
et al., 2013a; Smith et al., April 2014). Siddiqui et al. (2014) also used Quipper to
program a number of popular quantum algorithms, including Grover’s and Shor’s.
More than most languages, Quipper is transparent about its weaknesses. Quipper
describes circuit families, broad classes of circuits that can be instantiated with a
variety of different inputs. Unfortunately, this means that we only know the shape of
these circuits (their inputs and outputs) at runtime. Quipper lacks both linear types
and dependent types, the first of which can guarantee that qubits are not cloned,
while the second can describe precise circuit families by giving their dependently
typed signatures at compile time. On account of being embedded inside Haskell,
Quipper lacks a denotational semantics, which makes it difficult to reason about
Quipper programs. Quipper also makes heavy use of assertive terminations, where the
programmer asserts that a qubit is in a specific state, but has no way of guaranteeing
that these assertions are true. These assertions are used throughout the Quipper
development, particularly in its compiler from classical to quantum programs.
These flaws directly influenced the development of our language, Qwire. In fact,
the Quipper papers can be read as a series of challenges to quantum programming
language designers to which this thesis is a response. Chapter 4 takes up the challenge
of including both linear and dependent types in a quantum programming language and
giving that language a formal semantics. Chapter 5 addresses the issue of embedding
a Quipper-like language inside a proof assistant, and Chapters 6 and 7 explore the
payoff of doing so. Chapter 8 tackles the question of guaranteeing ancillae are used
correctly and writing a verified compiler from classical programs to quantum circuits.
Having posed these challenges, the designers of Quipper also sought to answer
them, in the context of a series of self-contained (non-embedded) languages called
Proto-Quippers1 . The original Proto-Quipper (Ross, 2015) came equipped with a lin-
ear type system, inspired by Selinger and Valiron’s quantum lambda calculus (Selinger
and Valiron, 2009). This type system treats all types as linear by default and uses
the bang operator (!) to denote a persistent type. A subtyping relation allows us to
use persistent variables in place of linear variables, though never the reverse. Proto-
Quipper also allows us to package (or box) functions on qubits into circuits that are
treated as data, and then to unbox these circuits later. As we will see, Qwire uses
1
We feel that these languages should be called Meta-Quippers, for “that which comes after Quip-
per.” The Proto-Quipper authors seemingly intended that these language should eventually evolve
into an idealized Quipper, with all the functionality of Quipper and all the underlying challenges
addressed.
28
boxing and unboxing in a similar fashion.
Another version of Proto-Quipper, called Proto-Quipper M (Rios and Selinger,
2017), endows Proto-Quipper with a categorical semantics. Lindenhovius et al. (2018)
extend Proto-Quipper M with general recursion and give it an abstract categorical
model. This model takes inspiration from Rennela and Staton’s (2017) categorical
model for EWire, itself an extension of Qwire, completing the loop.
29
which will be checked by the simulator and ignored by a real quantum computer,
since checking these assertions requires inspecting the quantum state without mea-
suring it. This capability augments Q#’s facility for managing ancillae, including
borrowing arbitrary qubits to return them to their initial state, but still doesn’t guar-
antee that ancillae are used correctly, as ReVerC does in the classical setting. As a
highly expressive standalone language with support for polymorphism and a variety
of quantum-specific abstractions, Q# stands on the frontier of quantum programming
languages, albeit in a way that is largely orthogonal to Proto-Quipper and Qwire.
30
view on the prospects for quantum control, see Badescu and Panangaden (2015).
This view, and the argument that quantum control is in the general case impossible,
has failed to dissuade certain researchers in the field. Ying et al. (2012, 2014) pro-
poses notions of quantum alternation and quantum recursion. QML (Altenkirch and
Grattage, 2005) includes a basic form of quantum branching subject to strong con-
straints; indeed, notions of quantum branching go back to the original QRAM paper
(Knill, 1996). More recently, Sabry et al. (2018) proposed a language with quantum
loops and recursion, but without measurement, in which all programs are guaranteed
to terminate and shown to correspond to valid quantum computations.
A few other approaches don’t use quantum circuits at all. A one-way quantum
computer (Raussendorf and Briegel, 2001, 2002) can do general-purpose quantum
computation using only an initial fully-entangled state and single qubit measure-
ments. The measurement calculus (Danos et al., 2007, 2009) can be viewed as a
programming language for this kind of one-way quantum computer. Inspired by the
category theory of quantum computation, categorical quantum mechanics (Abramsky
and Coecke, 2004; Coecke and Kissinger, 2017) models a quantum process as an undi-
rected graph, leading to languages like the ZX-Calculus (Coecke and Duncan, 2008;
Backens, 2014) and ZW-Calculus (Hadzihasanovic, 2015, 2017). One crucial contri-
bution of these languages is their equational theories and extensive rewriting systems,
which are used to optimize ZX-diagrams in the Quantomatic tool (Kissinger, 2011;
Fagan and Duncan, 2018). Further afield lies D-Wave’s approach to quantum com-
puting, which is based on adiabatic quantum computing (Albash and Lidar, 2018)
and is targeted at specific problems like simulated annealing (an approach to finding
maxima for functions) (Johnson et al., 2011). The D-Wave machines are programmed
using quantum machine instructions in a variety of programming languages (D-Wave
Systems, Inc, 2013).
Unfortunately, most surveys of quantum programming languages are at least seven
years old, a lifetime in this field. For more information on early quantum programming
languages, we refer the reader to surveys by Selinger (2004b), Gay (2006), Rüdiger
(2006), and Miszczak (2011). For more up-to-date information, the discussion section
of Svore et al. (2018) may prove enlightening.
31
3.10.1 Quantum Logics
A variety of approaches have been taken towards verifying quantum programs, the
most common being program logics. These include quantum versions of guarded com-
mand language (Sanders and Zuliani, 2000), dynamic logics (Brunet and Jorrand,
2004; Baltag and Smets, 2006, 2011), and Hoare logics (Chadha et al., 2006; Kaku-
tani, 2009; Ying, 2011; Ying et al., 2017). Two of these logics are of particular interest
to us.
Ying’s (2011) quantum Hoare logic reasons about quantum weakest preconditions.
A quantum weakest precondition (D’Hondt and Panangaden, 2006) adapts the no-
tion of a weakest precondition to a quantum setting in much the same way that
Kozen’s (1985) weakest pre-expectations generalize preconditions to a probabilistic
setting. In both settings, the claims are arithmetic: The judgment {P } c {Q} says
that for any initial state σ, P (σ) ≤ Q(JcKσ) (plus a probability of non-termination,
in the partial case) for some suitable order ≤. In the probabilistic case, this is just
the standard order on real numbers, and P and Q are measurable functions. In the
quantum case, P and Q come from a class of matrices called observables, and ≤ is the
Löwner partial order on matrix traces. Ying (2011) embeds this in a logic, later ex-
tended with proof techniques to guarantee program termination (Ying et al., 2017).
This logic was embedded within the Isabelle/HOL proof assistant (Nipkow et al.,
2002), allowing for mechanized proofs about quantum programs (Liu et al., 2016).
Another interesting logic was also mechanized using Isabelle/HOL. Unruh’s (2018)
Quantum Relational Hoare Logic (QRHL) is based upon Barthe et al.’s (2012) Prob-
abilistic Relational Hoare Logic, used in the EasyCrypt cryptographic tool. QRHL
makes assertions about the relationships of two quantum programs to one another,
with the goal of proving indistinguishability. These assertions allow us to prove the
security of quantum security protocols and show that classical protocols are secure
in the quantum setting. QRHL forms the core of an EasyCrypt-like tool for proving
quantum security, available at https://github.com/dominique-unruh/qrhl-tool.
32
ing discretizes qubit states, allowing us to take simple sums. Amy uses these path
sums to give a semantics to quantum circuits and proposes an algorithm for sim-
plifying these sums, allowing us to check equivalence. This approach is shown to be
complete for Clifford-group circuits, in that simplification will always terminate and
produce a unique normal form. In the general case, this procedure is not guaranteed
to terminate, but in practice, it has proven the correctness of a number of important
programs, including the quantum Fourier transform. It has some drawbacks, though,
in that these proofs are only for circuits of fixed size, and the technique is only used
to verify simple circuits rather than complex quantum programs. Interestingly, this
verification is all done in Haskell, which means that it doesn’t produce proof terms
that can be used in larger proof developments.
This concludes our introduction to quantum programming and verification. In
subsequent chapters, we will describe our attempt to apply formal verification in the
context of a full-fledged quantum programming language, Qwire.
33
Chapter 4
Qwire in Theory
4.1 Introduction
The standard architecture for quantum computers follows the quantum circuit model,
which presents quantum computations as sequences of gates over qubits. As with
classical circuits, quantum circuits exist at a very low level of abstraction, and yet
in spite of this, researchers and industry professionals write complex quantum al-
gorithms in state-of-the-art quantum circuit languages like Quipper (Green et al.,
2013a), Scaffold (Javadi-Abhari et al., 2012) and Liquid (Wecker and Svore, 2014).
Why is the quantum circuit model so successful? It’s partly because circuits, un-
like quantum computation more broadly, are simple and easy to understand. Research
into operations that directly interface with quantum data, like qubit-controlled con-
ditionals and recursion, is still in its infancy (Ying, 2014; Badescu and Panangaden,
2015), so programmers cannot be sure that their algorithms using such abstractions
are quantum-mechanically valid.
Although circuits manipulate quantum data, they themselves are classical data—
a circuit is just a sequence of instructions describing how to apply gates to wires. In
practice, this means that circuits can be used to build up layers of abstractions, hiding
low-level details. The QRAM model of quantum computing (Knill, 1996) formalizes
this intuition by describing how a quantum computer could work in tandem with a
classical computer. In the QRAM model, the classical computer handles the majority
of ordinary tasks, while the quantum computer performs specialized quantum oper-
ations. To communicate, the classical computer sends instructions to the quantum
machine in the form of quantum circuits. Over the course of execution, the quantum
computer sends measurement results back to the classical computer as needed.
34
circuits
Classical Quantum
Computer Computer
measurement results
Embedded languages like Quipper, Liquid, the Q language (Bettelli et al., 2003),
and the quantum IO monad (Altenkirch and Green, 2010) can be thought of as
instantiations of this model. They execute by running host language programs on the
classical computer, making specialized calls to the quantum machine. The classical
host languages allow programmers to easily build up high-level abstractions out of
low-level quantum operations.
However, such abstractions are only worthwhile if the circuits they produce are
safe—if they do not cause errors when executed on a quantum computer. Unfor-
tunately, proving that an embedded language produces well-formed circuits is hard
because it means reasoning about the entirety of the classical host language. This is
frustrating when we care most about the correctness of quantum programs, which we
expect to be more expensive and error-prone than the embedded language’s classical
programs.
One way of ensuring the safety of circuits is via a strong type system. Type safety
for a quantum programming language means that well-formed circuits will not get
stuck or “go wrong” when executed on a quantum machine. A subtlety is that this
definition implies that the quantum program is implementable in the first place on a
quantum computer—that the high-level operational view of the language is compat-
ible with quantum physics. One way of ensuring that the language is implementable
is to give a denotational semantics for programs in terms of quantum mechanics.
Several quantum programming languages have been proposed with an emphasis
on type safety, including Selinger’s QPL language (Selinger, 2004a), the quantum
lambda calculus (Selinger and Valiron, 2009), QML (Altenkirch and Grattage, 2005),
and Proto-Quipper (Ross, 2015). However, these are toy languages, not designed for
real-world, scalable quantum programming.
In this chapter we address the tension between expressive embedded languages
and denotationally sound type-safe languages.
35
The quantum lambda-calculus (Selinger and Valiron, 2009) popularized the use of
linear types for quantum systems. The “no-cloning” theorem of quantum mechanics
states that quantum data cannot be cloned; in a programming environment, linear
types ensure that quantum programs do not try to violate this property. However, the
programming model should also allow for non-linear programming of ordinary classical
data. The quantum lambda calculus addresses this via subtyping, but for Qwire we
take an alternative approach inspired by the symmetry between the QRAM model
and Benton’s Linear/Non-Linear (LNL) logic (1995), as depicted in the following
diagram:
lower
Non-Linear
Linear Types
Types
lift
In Qwire, quantum circuits execute on the quantum computer and are given linear
types, while host language programs execute on the classical computer and are given
ordinary non-linear types.
Structuring the system in this way has several advantages. First, the interface to
circuits is minimal, which means that they can easily be reasoned about. Second, the
host language is extensible, since changes to the host language don’t induce changes
to the circuit language, and vice versa. Third, the relationship between the circuit
language and host language can be axiomatized: every circuit can be promoted to the
host language via a box operator and later unboxed for reuse in other circuits. This
allows circuits to be treated as classical data structures in the host language, while
prohibiting quantum data, such as qubits, from escaping the linear type system.
The axiomatic approach means that the circuit language is relatively independent
from the host language. In particular, the host language can be instantiated with
a wide range of programming languages depending on the intended use: high-level
functional programming languages for developing and reasoning about algorithms;
theorem provers for verification of quantum circuits; and perhaps even hardware de-
scription languages for deployment with real quantum computers. In Chapter 5 and
subsequent chapters, we will focus on one specific host: The Coq proof assistant (Coq
Development Team, 2018) and its programming language, Gallina.
36
classical host language that allows for modularity and communication via the
QRAM model.
Note that we
sometimes write (gate g w) as shorthand for the
(w' <- gate g w; output w') that appears in the example.
1
We will use Coq-style syntax for consistency with the rest of the thesis, though Qwire could
be embedded in any number of host languages, depending on the features desired.
37
The reason wires must be treated linearly is that applying a gate changes the
nature of the wire w. It is meaningless to apply two gates to the same wire, because
wires (and in particular qubits) cannot be duplicated. The following code, for example,
is absurd:
absurd :=
box w ⇒
x ← gate meas w;
w' ← gate H w;
output (x,w')
38
Definition bell00 : Definition bob :
Box One (Qubit⊗Qubit) := Box (Bit⊗Bit⊗Qubit) Qubit :=
box () ⇒ box (x,y,b) ⇒
a ← gate init0 (); (y,b) ← gate (bit-ctrl X) (y,b);
b ← gate init0 (); (x,b) ← gate (bit-ctrl Z) (x,b);
a ← gate H a; () ← gate discard y;
(a,b) ← gate CNOT (a,b) () ← gate discard x;
output (a,b) output b
alice bob
∣ϕ⟩ H meas
bell00
0 H meas
0 X Z ∣ϕ⟩
39
Quantum Teleportation. The quantum teleportation algorithm of Chapter 2
highlights the relationship between boxed and unboxed circuits. Figure 4.1 shows
the quantum teleportation circuit broken up into four parts. Alice is trying to send
the input qubit q to Bob. The circuit bell00 initializes two qubits in the zero state
(written init0 ), places qubit a in a superposition of ∣0⟩ and ∣1⟩ via the Hadamard (H)
gate, and entangles it with qubit b by applying a controlled-not (CNOT) gate. Qubit a
is then given to Alice, and qubit b to Bob. Alice entangles a and q and measures
them, outputting a pair of bits x and y. Bob then uses these bits to control an X
and Z gate applied to his own qubit b, thereby placing b in the state of the original
qubit q.
40
flip : Bool =
run (q ← gate init0 ();
q ← gate H q; ∣0⟩ H meas
b ← gate meas q;
output b)
Note that the Coq implementation of Qwire does not include a run operation,
since Coq programs are not intended to be executed. Moreover, Coq is a pure lan-
guage, and hence cannot handle input and output or probabilistic operations. How-
ever, given that Qwire is host-language agnostic – and even Qwire programs written
in Coq should eventually be executed, either on a QRAM device or through extrac-
tion to OCaml or Haskell (see Section 11.2) – we will discuss run and its semantics
in this chapter.
u† ∈ U(W, W )
ctrl u ∈ U(Qubit ⊗ W, Qubit ⊗ W )
bit-ctrl u ∈ U(Bit ⊗ W, Bit ⊗ W )
41
A typing judgment Γ;Ω ⊢ C ∶ W specifies when a circuit is well-formed. In this
judgment,
• C is a circuit;
• Ω = w1 ∶W1 , . . . , wn ∶Wn is a context of input wire names with their wire types;
Ω
W
C
Wires in Qwire are linear, which means that they cannot be duplicated or dis-
carded (though some gates may duplicate or discard classical bits) and when we write
Ω,Ω′ we assume that Ω and Ω′ contain only disjoint wire names. Both Ω and Γ are
unordered contexts.
The output of a circuit is built up as a pattern of its input wires:
Ω⇒p∶W Ω
W
⋅; Ω ⊢ output p ∶ W
Ω1 ⇒ p1 ∶ W1 Ω2 ⇒ p2 ∶ W2
() ∶ One w∶W ⇒w∶W Ω1 , Ω2 ⇒ (p1 , p2 ) ∶ W1 ⊗ W2
42
4.3.2 Host Language
In the QRAM model, a classical computer works together with a quantum com-
puter. The classical computer communicates with the quantum computer by sending
it instructions—that is, circuits in Qwire. Terms in the host language, meanwhile,
describe computations on the classical computer. We refer to the host language as
host and describe some of its properties.
We assume that host is statically typed, and we write its types using the meta-
variable A. We further assume that the language has unit, boolean and product types,
to correspond with Qwire’s One, Bit and tensor wire types. We add to host a type
representing Qwire circuits between two wire types, which we write Box W1 W2 . Of
course, host will often contain many other types, including functions and inductive
data types, but the interface with Qwire does not depend on the particular structure
of host. For this reason we say that host is arbitrary.
Overall, we can summarize the types of host as follows:
Boxing and Unboxing. The Box type bridges Qwire circuits and host terms.
The type Box W1 W2 is a wrapper around Qwire circuits of the form Γ;Ω ⊢ C ∶ W2 ,
where the wires in Ω come from a pattern destructing the input type W1 .
Ω ⇒ p ∶ W1 Γ; Ω ⊢ C ∶ W2 Ω W
C
Γ ⊢ box (p ∶ W1 ) ⇒ C ∶ Box W1 W2
A boxed term of type Box W1 W2 can be turned back into a Qwire circuit by
describing how to match up the available input wires to the input type of the boxed
representation.
Γ ⊢ t ∶ Box W1 W2 Ω ⇒ p ∶ W1 Ω W2
Γ; Ω ⊢ unbox t p ∶ W t
2
Lifting. In the QRAM model described above, the quantum computer also com-
municates with the classical computer by sending it the results of measurement. For
example, given a circuit with no input wires and a bit output, running that circuit
should result in a host language boolean value. (Note that this is probabilistic oper-
ation and hence impure. In a pure language we would require a probability monad M
and run C would have type M B.)
Γ; ⋅ ⊢ C ∶ Bit
Γ ⊢ run C ∶ Bool
43
We can generalize this operation so that running a circuit that outputs a qubit im-
plicitly measures that qubit and returns the corresponding boolean. In fact, this
relationship generalizes to any wire type, which can be lifted to a classical type as
follows:
∣Bit∣ = Bool ∣One∣ = Unit
∣Qubit∣ = Bool ∣W1 ⊗ W2 ∣ = ∣W1 ∣ × ∣W2 ∣
The run operator now has the following form:
Γ; ⋅ ⊢ C ∶ W
Γ ⊢ run C ∶ ∣W ∣
Run is a static lifting operator, meaning that there is no residual state left on the
quantum computer after run C has completed. In contrast, dynamic lifting describes
the case when, over the course of a quantum computation, a subset of the wires
are measured and communicated to the classical computer. In this case, the classical
computer uses those results to compute the remainder of the quantum circuit, and
eventually sends the results to the quantum computer. Dynamic lifting is expensive
because while the classical computer is computing the rest of the circuit, the exist-
ing state on the quantum computer must continuously undergo error correction to
prevent degradation. However, dynamic lifting is a fundamental form of communica-
tion between the two machines, needed to implement algorithms like quantum error
correction.
We write the dynamic lifting operator x ⇐ lift p; C to mean that the wires in p are
measured, lifted to the classical computer as the host variable x , and used to compute
the circuit C.
Ω⇒p∶W Γ, x ∶ ∣W ∣; Ω′ ⊢ C ∶ W ′
Γ; Ω, Ω′ ⊢ x ⇐ lift p; C ∶ W ′
The dynamic and static lifting operations are not mutually derivable, as they rep-
resent two fundamentally different ways to communicate the results of measurement
between the two systems.
The typing rules are summarized in Figure 4.2. Note that we often write box p ⇒ C
instead of box (p ∶ W ) ⇒ C when the type of the input pattern is clear. Note that
typing contexts are unique for both patterns and circuits:
44
Ω⇒p∶W
TypeCircOutput
Γ; Ω ⊢ output p ∶ W
Ω1 ⇒ p1 ∶ W1 Ω2 ⇒ p2 ∶ W2
g ∈ G(W1 , W2 ) Γ; Ω2 , Ω ⊢ C ∶ W
TypeCircGate
Γ; Ω1 , Ω ⊢ p2 ← gate g p1 ; C ∶ W
Γ; Ω1 ⊢ C ∶ W Γ; Ω0 , Ω2 ⊢ C ′ ∶ W ′
TypeCircLet
Γ; Ω1 , Ω2 ⊢ p ← C; C ′ ∶ W ′
Ω⇒p∶W Γ, x ∶ ∣W ∣; Ω′ ⊢ C ∶ W ′
TypeCircLift
Γ; Ω, Ω′ ⊢ x ⇐ lift p; C ∶ W ′
Γ ⊢ t ∶ Box W1 W2 Ω ⇒ p ∶ W1
TypeCircUnbox
Γ; Ω ⊢ unbox t p ∶ W2
Γ; ⋅ ⊢ C ∶ W
TypeRun
Γ ⊢ run C ∶ ∣W ∣
Ω ⇒ p ∶ W1 Γ; Ω ⊢ C ∶ W2
TypeBox
Γ ⊢ box (p ∶ W1 ) ⇒ C ∶ Box W1 W2
45
Lemma 1. If Ω1 ⇒ p ∶ W and Ω2 ⇒ p ∶ W then Ω1 = Ω2 . If Γ; Ω1 ⊢ C ∶ W and
Γ; Ω2 ⊢ C ∶W then Ω1 = Ω2 .
Notice that the lifting operator x ⇐ lift p; C does not assume that its continuation
C is also normal. This is because C has a free host-level variable x that cannot in
general be normalized. For example, consider the circuit x ⇐ lift w ; unbox ( init x ) ():
the continuation unbox ( init x ) () cannot be normalized to init0 or init1 since x is
not assigned a value until circuit execution time.
In the rest of this section, we define a small-step operational semantics that reduces
concrete circuits typed by ⋅;Q ⊢ C ∶ W to normal circuits. The operational rules rely
on a fairly complex substitution relation, which we briefly address.
Substitution. A substitution {p′ /p} describes a finite map from wire names to
patterns. It is well defined only when p generalizes p′ (written p′ ≼ p) in the following
sense:
p′1 ≼ p1 p′2 ≼ p2
p′ ≼ w () ≼ () (p′1 , p′2 ) ≼ (p1 , p1 )
We say p′ ≺ p when p′ ≼ p and ¬(p ≼ p′), and we say p is concrete for W when, for all
Ω ⇒ p′ ∶W , ¬(p′ ≺ p).
46
The substitution map is defined as follows:
{()/()} = ∅
{p′ /w } = w ↦ p′
{(p′1 ,p′2 )/(p1 ,p2 )} = {p′1 /p1 }, {p′2 /p2 }
(){p′ /p} = ()
⎧
⎪
′ ⎪p0 if w ↦ p0 ∈ {p′ /p}
w {p /p} = ⎨
⎪
⎪
⎩w otherwise
(p1 ,p2 ){p′ /p} = (p1 {p′ /p},p2 {p′ /p})
⋅ {p′ /p} = ⋅
⎧
⎪
′ ′ ⎪Ω′ {p′ /p},Ω0 if w ↦ p0 ∈ {p′ /p}and Ω0 ⇒ p0 ∶W
(Ω ,w ∶W ) {p /p} = ⎨ ′ ′
⎪
⎩Ω {p /p},w ∶W
⎪ otherwise
2. Ω {p′ /p} = Ω′ .
47
Lemma 4. Suppose {p′ /p} is consistent with Ω.
Ω1 ⇒ p1 ∶ W1 Ω2 ⇒ p2 ∶ W2 g ∈ G(W1 , W2 ) ⋅; Ω2 , Ω ⊢ C ∶ W
⋅; Ω1 , Ω ⊢ p2 ← gate g p1 ; C ∶ W
By part 1, we have Ω1 {p′ /p} ⇒ p1 {p′ /p} ∶ W1 , and by the inductive hypothesis we
know Γ;(Ω2 ,Ω) {p′ /p} ⊢ C {p′ /p}∶W . By α-equivalence, we can assume that the wires
in Ω2 are disjoint from those in p′ and p (and therefore from the substitution {p′ /p}),
and so by Lemma 3, (Ω2 ,Ω) {p′ /p} = Ω2 ,(Ω {p′ /p}). Thus
1. Ð→H is the operational semantics derived from the host language alone, and
It is reasonable to assume that the host language relation Ð→H treats the type Box W1
W2 as an abstract data type, meaning that all terms of the form box p ⇒ C are treated
as opaque values by the Ð→H relation. The relation Ð→b reduces such a boxed circuit
to one of the form box p′ ⇒ N where p′ is concrete for the type W1 . Let v h consists
of values of host extended with boxed circuits as opaque values, and v c consists of
host’s values along with normalized boxed circuits:
v h ∶∶= . . . ∣ box p ⇒ C
v c ∶∶= . . . ∣ box p ⇒ N
48
(Box)
p is concrete for W C Ô⇒ C ′
StepTermBoxStructural
box (p ∶W ) ⇒ C Ð→b box (p ∶W ) ⇒ C ′
p ′ ≺ p p ′ is concrete for W
StepTermBoxEta
box (p ∶W ) ⇒ C Ð→b box (p ′ ∶W ) ⇒ C {p ′ /p}
(Unbox)
t Ð→ t ′
StepCircUnboxStructural
unbox t p Ô⇒ unbox t ′ p
StepCircUnbox
unbox (box (p ∶W ) ⇒ N ) p ′ Ô⇒ N {p ′ /p}
(Gate)
g ∈ G(W1 , W2 ) p2 is concrete for W2 C Ô⇒ C ′
StepCircGateStructural
p2 ← gate g p1 ; C Ô⇒ p2 ← gate g p1 ; C ′
(Composition)
C1 Ô⇒ C1′
StepCircLetStructural
p ← C1 ; C2 Ô⇒ p ← C1′ ; C2
StepCircLetOutput
p ← output p ′ ; C Ô⇒ C {p ′ /p}
StepCircLetGate
p ← (p2 ← gate g p1 ; N ); C Ô⇒ p2 ← gate g p1 ; p ← N ; C
StepCircLetMeas
p ′ ← (x ⇐ lift p; C ′ ); C Ô⇒ x ⇐ lift p; p ′ ← C ′ ; C
49
The relations Ô⇒ on circuits and Ð→b on boxed circuits are given in Figure 4.3.
The structural rules reduce circuits underneath binders. For composition and un-
boxing, these structural rules are straightforward, in that they don’t have any pre-
conditions restricting when they apply. For boxes and gates, on the other hand, the
continuations C of the circuit have some additional inputs that are not concrete even
if the entire circuit is. For example, in the circuit w ← gate CNOT (w1 ,w2 ); C, the
continuation C has a compound wire w even though the entire circuit has only con-
crete wires w1 and w2 . To address this issue, the η-expansion rules for gates and boxes
show that any such binding is equivalent to one with concrete inputs throughout.
Lemma 5. If p is concrete for W then there is a unique Q such that Q ⇒ p ∶ W .
Furthermore, for every wire type W there exists p (not necessarily unique) such that
p is concrete for W .
Since an unbox operator is not a normal circuit, we eliminate it via a β rule once
its argument t reaches a value of the form box p ⇒ N . Similarly, the composition
operator reduces its first argument to a normal form before taking a step. When the
argument is an output output p′ , the composition p ← output p′ ; C uses substitution
to take a β-reduction step. On the other hand, when the argument consists of a gate
or lifting step, the semantics commutes that command to the front of the circuit; we
call these operators commuting conversions.
50
1. If ⋅ ⊢ t∶A, there exists some value v c such that t Ð→∗ v c .
2. If ⋅;Q ⊢ C ∶W , there exists some normal circuit N such that C Ô⇒∗ N .
Proof. By induction on the number of constructors in the term and circuit (Ap-
pendix B.1).
0 H
⎛ /2
1 0 0 1/2
⎞
⎜0 0 0 0⎟
⎜ ⎟
⎜0 0 0 0⎟
⎝1/2 0 0 1/2⎠
where the 1/2 in the top left represents the probability of measuring two zeros, while
the 1/2 in the bottom right represents the probability of measuring two ones. If we
measured this system, we would obtain the (mixed state) matrix
⎛ /2
1 0 0 0⎞
⎜0 0 0 0⎟
⎜ ⎟
⎜0 0 0 0⎟
⎝0 0 0 1/2⎠
51
g ∈ G(W1 ,W2 ) as a superoperator from JW1 K to JW2 K. Although the set of gates is a
parameter of the system, the denotation of a unitary gate U applied to a matrix ρ
should always be U ρU † . The interpretation of other likely gates is as follows:
Γ; Ω′ ⊢ C ∶ W π ∶ Ω ≡ Ω′
Γ; Ω′ ⊢ C ∶ W
π1 ∶ Ω1 ≡ Ω2 π 2 ∶ Ω2 ≡ Ω3
′ ′
ϵ∶Ω≡Ω swap Ω1 Ω2 ∶ Ω, Ω1 , Ω2 , Ω ≡ Ω, Ω2 , Ω1 , Ω π2 ○ π1 ∶ Ω1 ≡ Ω3
Note that permutations are reflected in the typing judgments of circuits but not in
the syntax. We extend the substitution relation to permutations in a natural way,
writing π {p′ /p}.
ϵ {p′ /p} = ϵ
(π2 ○ π1 ) {p′ /p} = π2 {p′ /p} ○ π1 {p′ /p}
(swap Ω1 Ω2 ) {p′ /p} = swap (Ω1 {p′ /p}) (Ω2 {p′ /p})
Although the context of wires can be permuted inside a circuit, it will not be
permuted inside a pattern. Therefore, a pattern Ω ⇒ p ∶ W is just a reassociation of
the input wires; all permutations must be done outside the pattern. This means that
whenever Ω ⇒ p∶W , it must be the case that JΩK = JW K.
A permutation π ∶ Ω ≡ Ω′ will be interpreted as a linear isomorphism from JΩK to
4
We elided these details in Section 4.3 as they complicate the operational semantics.
52
Ω⇒p∶W
J⋅; Ω ⊢ output p ∶ W K = I∗
⋅; Ω ⊢ output p ∶ W
⋅; Ω ⊢ C ∶ W π ∶ Ω ≡ Ω′
JΩ ⊢ C ∶ W K = JΩ′ ⊢ C ∶ W K ○ [π]∗
⋅; Ω ⊢ C ∶ W
⋅ ⊢ t ∶ Circ(W1 , W2 ) Ω ⇒ p ∶ W1
JΩ ⊢ unbox t p ∶ W ′ K = Jt ∶ Circ(W, W ′ )K
⋅; Ω ⊢ unbox t p ∶ W2
g ∈ G(W1 , W2 ) Ω1 ⇒ p 1 ∶ W 1
Ω2 ⇒ p2 ∶ W2 ⋅; Ω2 , Ω ⊢ C ∶ W JΩ1 ,Ω ⊢ p2 ← gate g p1 ; C ∶ W K
⋅; Ω1 , Ω ⊢ p2 ← gate g p1 ; C ∶ W =JΩ2 ,Ω ⊢ C ∶ W K ○ (JgK ⊗ I∗ )
⋅; Ω1 ⊢ C ∶ W ⋅; Ω0 , Ω2 ⊢ C ′ ∶ W ′ JΩ1 , Ω2 ⊢ p ← C; C ′ ∶ W ′ K
⋅; Ω1 , Ω2 ⊢ p ← C; C ′ ∶ W ′ =JΩ0 , Ω2 ⊢ C ′ ∶ W ′ K ○ (JΩ1 ⊢ C ∶ W K ⊗ I∗ )
Lemma 6. If π ∶ Ω ≡ Ω′ and {p′ /p} is consistent with Ω, then Jπ{p′ /p}K = JπK.
Proof. Straightforward by induction on the permutation.
For ⋅;Ω ⊢ C ∶ W , we write JΩ ⊢ C ∶ W K for its interpretation as a superoperator
between JΩK and JW K. Furthermore, for ⋅ ⊢ t∶Box W1 W2 , we write JtK for JΩ ⊢ C ∶ W2 K
where t Ð→∗H box p ⇒ C in the host language and Ω ⇒ p ∶ W1 . This operation is
functional exactly when the host language semantics is strongly normalizing.
The interpretation of circuits is defined in Figure 4.4.
Lemma 7. If ⋅; Ω ⊢ C ∶ W and {p′ /p0 } is consistent with Ω, then
Proof. By induction on the typing judgment. The proof is almost completely straight-
forward because the interpretation of circuits does not depend on the content of
53
patterns.
Theorem 8 (Soundness). If ⋅;Q ⊢ C ∶W and C Ô⇒ C ′ , then
JQ ⊢ C ∶ W K = JQ ⊢ C ′ ∶ W K.
⌈∗⌉ = I1
⌈false⌉ = ∣0⟩ ⟨0∣
⌈true⌉ = ∣1⟩ ⟨1∣
⌈(v1 , v2 )⌉ = ⌈v1 ⌉ ⊗ ⌈v2 ⌉
Now, if ⋅; ⋅ ⊢ C ∶ W , then
J⋅ ⊢ C ∶ W KI1
is a density matrix in JW K. We can write this density matrix as
⎛ α11 ⋯ α1n ⎞
⎜ ⋮ ⋱ ⋮ ⎟
⎝αn1 ⋯ αnn ⎠
Recall that the elements αii along the diagonal correspond to basis states, and there-
fore to terms vi in the host language (via lowering). Hence, for each i, we say that the
probability of C being vi is αi i , written prob(C =vi ) = αi i . The operational semantics
rule for run C can be summarized with respect to this relation: run C steps to vi with
probability αi i .
prob(C = vi ) = αii
run C Ð→αii vi
54
izes Qwire. EWire is shown to be an enriched category in which the morphisms of
one category become objects in another. In context, we can view a circuit as a func-
tion (morphism) from wires types to wire types, but we also treat circuits as terms
(objects) in the host language. As a result, we can impose a layered categorical struc-
ture on Qwire: Circuits correspond to an an enriched symmetric monoidal category
and the host language corresponds to Cartesian closed category with the run monad
connecting the two.
This categorical framework allows the authors to consider adding features to
Qwire, such as recursion, which is modeled using directed complete partial orders
(DCPOs). This builds on previous work by Rennela (2014) that uses W ∗ -algebras
to model quantum computation. Further work by Lindenhovius et al. (2018) builds
upon this semantics in the contexts of the Proto-Quipper language (Ross, 2015; Rios
and Selinger, 2017).
where tensor (⊗) is a type-level function that duplicates the argument wire type
(Qubit) some number of times (defined below).
Combining linear and dependent types is still an area of active research (Krish-
naswami et al., 2015; McBride, 2016), but thanks to the separation between the circuit
and host languages, we can get away with a limited form of dependent types due to
Krishnaswami et al. (2015). Under this strategy, types can depend on terms, but
only terms of classical (non-linear) type. These include dependencies on wire types
themselves.
To be precise, let W be the kind of wire types, and consider an indexed hierarchy
of host language types Ai . We define the following well-formedness judgment: first,
W has type Ai for any index i , and Ai has type Ai+1 :
Γ ⊢ W ∶ Ai Γ ⊢ Ai ∶ Ai+1
55
Π types have the usual introduction and elimination rules:
Γ, x ∶ A1 ⊢ t ∶ A2 Γ ⊢ t ∶ Π(x ∶ A1 ).A2 Γ ⊢ t′ ∶ A1
Γ ⊢ λx.t ∶ Π(x ∶ A1 ).A2 Γ ⊢ t t′ ∶ A2 {t′ /x}
A more thorough analysis of this type structure is needed, but it is beyond the
scope of this chapter.
56
w ← unbox qft n' w;
unbox rotations (S n') n' (q,w)
end
where hadamard = box w => gate H w.
4.8 Summary
Qwire is a minimal and highly modular core circuit language. It is minimal in
that Qwire has only five distinct commands, two of which are eliminated in the
normalization procedure. It is modular in that Qwire isn’t attached to any spe-
cific programming language. We expect that the Qwire interface will be useful in
dependently-typed host languages like Coq for verification and formal analysis of cir-
cuits, in higher-order functional languages like Haskell, OCaml or F#, or potentially
even in imperative languages like Python, Java, or C.
Qwire uses linear types to enforce no-cloning, but it does not allow them to spill
over into the host language. This is crucial because linear types are the most natural
way to enforce no-cloning, but they are difficult to integrate into existing languages.
Qwire gets the best of both worlds by ensuring that circuits are linearly typed while
allowing an arbitrarily powerful type system in the classical host language.
As a circuit description language, Qwire is a low-level piece in the development
of sophisticated quantum programming languages. Ultimately however, all quantum
computation will boil down to circuit generation, necessitating the use of a circuit
language like Qwire. Having Qwire as a safe, small circuit language is an excellent
building block on which to rest the complex world of quantum computation.
In the following chapters, we will focus on a particular implementation of Qwire
inside the Coq proof assistant and what we gain from this embedding, in terms of
dependently typed structures and a formally verified metatheory.
57
Chapter 5
Qwire in Practice
This chapter discusses the implementation of Qwire inside the Coq proof assis-
tant (Coq Development Team, 2018). Coq consists of both a programming language,
called Gallina, and an interactive system for proving properties of Gallina programs.
Gallina features dependent types, which may depend on both terms and other types
from the language. For instance, we can define the type Sized_List 7 B, for lists of
length 7 that contain boolean values. Gallina is also restrictive in that all Gallina
programs must terminate, and hence only restricted forms of recursion are permitted.
While the Coq proof language may appear to be separate from Gallina, it actually
constructs dependently typed Gallina terms, which correspond to proofs of desired
properties. Coq also includes an untyped programming language, called Ltac, which
is used to construct Coq proofs. We assume some familiarity with Coq in this disser-
tation, and refer the interested reader to the online textbook / Coq library “Software
Foundations” (Pierce et al., 2018) or our Coq tutorial with Arthur Azevedo de Amorim
(Rand and de Amorim, 2016).
Implementing Qwire forced us to confront issues like variable representation,
compilation of circuits to functions on density matrices, and implementing matrices
and complex numbers in Coq. This chapter draws on Rand et al. (2017) along with a
CoqPL workshop presentation on phantom types for quantum programs (Rand et al.,
2018b).
58
Wires in a circuit can be collected into patterns corresponding to a given wire
type, written Pat W. A pattern is just a nested tuple of wires of base types, meaning
that all the variables in a pattern have type Bit or Qubit.
Inductive Pat : WType → Set :=
| unit : Pat One
| qubit : Var → Pat Qubit
| bit : Var → Pat Bit
| pair : ∀ {W1 W2 }, Pat W1 → Pat W2 → Pat (W1 ⊗ W2 ).
The type Var is identical to N. We use the notation () to refer to the unit pattern and
(p1,p2) to refer to pair p1 p2. Note that the wire types corresponding to unit, qubit
and bit are fixed; the type of a pair can therefore be inferred from the patterns it
contains.
Gates are indexed by a pair of wire types—a gate of type Gate W1 W2 takes an
input wire of type W1 and outputs a wire of type W2 . In our setting, gates will include
a universal set of unitary gates, as well as initialization, measurement, and control.
Inductive Unitary : WType → Set :=
| H : Unitary Qubit (* Hadamard *)
| X : Unitary Qubit (* Pauli X *)
| Y : Unitary Qubit (* Pauli Y *)
| Z : Unitary Qubit (* Pauli Z *)
| control : ∀ {W} (U : Unitary W), Unitary (Qubit ⊗ W).
59
Gate W1 W2 → Pat W1 → (Pat W2 → Circuit W) → Circuit W
| lift : Pat Bit → (B → Circuit W) → Circuit W.
An output circuit output p is just a pattern whose wire type uniquely determines
the wire type of the circuit. A gate application, which we write using the notation
gate p2 ← g @p1; c, is made up of a gate g : Gate W1 W2 , an input pattern p1 : Pat W1 ,
and a continuation c : Pat W2 → Circuit W. The intended meaning is that p1 is the
input to the gate g, and its output is bound to p2 in the continuation.
The lift operation, which we write as lift x ← p; C, takes as input a bit wire
p : Pat Bit and a function fun x ⇒ C that takes a bool and returns a circuit. The
intended semantics is that the QRAM will transmit the value of p as a Coq boolean
to the classical computer, which will then compute the remainder of the circuit. We
use notations to define lifting on qubits (which is equal to a measurement followed
by lift) and patterns of bits and qubits (see Section 5.6).
A boxed circuit is simply a function from an input pattern to a circuit:
Inductive Box w1 w2 : Set :=
| box : (Pat w1 → Circuit w2) → Box w1 w2.
The corresponding unbox function takes a boxed circuit and a input pattern and
returns a Circuit:
Definition unbox {w1 w2} (b : Box w1 w2) (p : Pat w1) : Circuit w2 :=
match b with box c ⇒ c p end.
Our higher-order abstract syntax also allows us to easily define composition, where
Coq performs variables substitution for us:
Fixpoint compose {w1 w2} (c : Circuit w1) (f : Pat w1 → Circuit w2) :
Circuit w2 :=
match c with
| output p ⇒ f p
| gate g p c' ⇒ gate g p (fun p' ⇒ compose (c' p') f)
| lift p c' ⇒ lift p (fun bs ⇒ compose (c' bs) f)
end.
60
and circuits. Our prior approach had the advantage of making it impossible to con-
struct ill-typed circuits, but also made Qwire circuits quite bulky and difficult to
compute with. We can regain the safety features of that version of Qwire by only
exposing typed circuits – sigma types consisting of circuits with their typing proofs –
to the user.
Typing Contexts A typing context Γ of type Ctx is a partial map from variables
(represented concretely as natural numbers) to wire types. We implement contexts
as lists of option WTypes. In this representation, the variable i is mapped to W if the
ith element in the list is Some W, and is undefined if the list has no ith element or that
element is None.
The disjoint merge (⋓) operation ensures that the same wire cannot occur twice
in one circuit. Mathematically, it is defined on two typing contexts as follows:
[] ⋓ Γ2 = Γ2
Γ1 ⋓ [] = Γ1
None :: Γ1 ⋓ None :: Γ2 = None :: (Γ1 ⋓ Γ2 )
Some W :: Γ1 ⋓ None :: Γ2 = Some W :: (Γ1 ⋓ Γ2 )
None :: Γ1 ⋓ Some W :: Γ2 = Some W :: (Γ1 ⋓ Γ2 )
Since disjoint merge is a partial function, we represent it in Coq as a function on
possibly invalid contexts, OCtx = Invalid | Valid Ctx. For convenience, most opera-
tions on contexts are lifted to work with OCtx values, and so the type signature of
merge is OCtx → OCtx → OCtx. For convenience, we use the notation Γ == Γ1 ● Γ2 for
Γ = Γ1 ⋓ Γ2 ∧ is_valid Γ, where is_valid asserts validity.
Definition is_valid (Γ : OCtx) : P := ∃ (Γ' : Ctx), Γ = Valid Γ'.
For proofs about contexts, we also provide an inductive relation merge_ind and prove
that merge_ind Γ1 Γ2 Γ if and only if Γ == Γ1 ● Γ2 . This inductive relation makes it
easier to reason about merged typing contexts, though (unlike ⋓) we can no longer
compute with it or use it for rewriting.
61
Ω⇒p∶W
TypeCircOutput
Γ; Ω ⊢ output p ∶ W
Ω1 ⇒ p1 ∶ W1 Ω2 ⇒ p2 ∶ W2
g ∈ G(W1 , W2 ) Γ; Ω2 , Ω ⊢ C ∶ W
TypeCircGate
Γ; Ω1 , Ω ⊢ p2 ← gate g p1 ; C ∶ W
Ω⇒p∶W Γ, x ∶ ∣W ∣; Ω′ ⊢ C ∶ W ′
TypeCircLift
Γ; Ω, Ω′ ⊢ x ⇐ lift p; C ∶ W ′
Γ; Ω1 ⊢ C ∶ W Γ; Ω0 , Ω2 ⊢ C ′ ∶ W ′
TypeCircLet
Γ; Ω1 , Ω2 ⊢ p ← C; C ′ ∶ W ′
Γ ⊢ t ∶ Box W1 W2 Ω ⇒ p ∶ W1
TypeCircUnbox
Γ; Ω ⊢ unbox t p ∶ W2
Ω ⇒ p ∶ W1 Γ; Ω ⊢ C ∶ W2
TypeBox
Γ ⊢ box (p ∶ W1 ) ⇒ C ∶ Box W1 W2
Figure 5.1: The typing rules for Qwire from Chapter 4. We’ve rearranged the rules
to match this presentation.
Typing Qwire Circuits Once our circuits use continuations (in gate g p1 (fun p2
⇒ c)), we have to include a form of continuation in the typing judgment as well. In
the following definition, we use the notation Γ ⊢ c :Circ for Types_Circuit Γ c.
Inductive Types_Circuit : OCtx → ∀ {w}, Circuit w → Set :=
| types_output : ∀ {Γ w} {p : Pat w}, Γ ⊢ p :Pat → Γ ⊢ output p :Circ
| types_gate : ∀ {Γ Γ1 Γ1 ' w1 w2 w} {f : Pat w2 → Circuit w}
{p1 : Pat w1} {g : Gate w1 w2},
Γ1 ⊢ p1 :Pat →
(∀ Γ2 Γ2 ' (p2 : Pat w2) {pf2 : Γ2 ' == Γ2 ● Γ},
Γ2 ⊢ p2 :Pat → Γ2 ' ⊢ f p2 :Circ) →
∀ {pf1 : Γ1 ' == Γ1 ● Γ},
Γ1 ' ⊢ gate g p1 f :Circ
| types_lift : ∀ {Γ1 Γ2 Γ w } {p : Pat Bit} {f : B → Circuit w},
Γ1 ⊢ p :Pat →
(∀ b, Γ2 ⊢ f b :Circ) →
∀ {pf : Γ == Γ1 ⋓ Γ2 },
Γ ⊢ lift p f :Circ
Compare this to the original presentation of the typing rules (reproduced in Fig-
62
ure 5.1). The rule for output is straightforward: If Γ types a pattern p, it types output
p. For gate application, we again implement the rule from Figure 5.1, except now we
have to quantify over typing contexts Γ2 that type the continuation. We name the
disjoint unions Γ ⋓ Γ1 and Γ ⋓ Γ2 as Γ1 ' and Γ2 ', respectively. For lift, we limit our-
selves to the Bit case, meaning that Γ2 merely has to type the continuation whether
we measured ∣1⟩ (true) or ∣0⟩ (false).
Note that by our construction, the typing rules for unbox and let are derived
rules, as these operations are themselves derived. We say that a boxed circuit is well
typed if the underlying circuit is well typed:
Definition Typed_Box {W1 W2 : WType} (b : Box W1 W2 ) : Set :=
∀ Γ (p : Pat W1 ), Γ ⊢ p :Pat → Γ ⊢ unbox b p :Circ.
The proof of TypeCircUnbox is then immediate. We can likewise show that the
composition of two circuits typed by disjoint contexts is itself well-typed, though the
proof in this case is slightly more involved:
Lemma compose_typing : ∀ Γ Γ' Γ'' W W'
(c : Circuit W) (f : Pat W → Circuit W'),
Γ ⊢ c :Circ →
(∀ Γ2 Γ2 ' (p2 : Pat w2) {pf2 : Γ2 ' == Γ2 ● Γ'},
Γ2 ⊢ p2 :Pat → Γ2 ' ⊢ f p2 :Circ) →
Γ'' == Γ ● Γ' →
Γ'' ⊢ compose c f :Circ.
This corresponds to TypeCircLet in Figure 5.1.
63
but compiling to flat, concrete circuits poses a much harder challenge than simply
compiling to concrete circuits1 .
To address this challenge, we define de Bruijn circuits, inspired by de Bruijn
indices, where wire initialization automatically binds a wire to the first available
numerical index, and discarding shifts the remaining indices downwards2 .
We will introduce de Bruijn (or DB) circuits, and how to construct them, by
example. Here is our bob circuit (from our teleportation example in Section 2.2), both
in higher-order abstract syntax and compiled to a (prettified) boxed DeBruijn_Circuit
:
Definition bob := Definition db_bob :=
box (x,y,q) ⇒ db_box (Bit ⊗ Bit ⊗ Qubit) ⇒
gate (y,q) ← bit_ctrl X @ (y,q); db_gate (bit_ctrl X) (1, 2);
gate (x,q) ← bit_ctrl Z @ (x,q); db_gate (bit_ctrl Z) (0, 2);
gate () ← discard @ x; db_gate discard 0;
gate () ← discard @ y; db_gate discard 0;
output q. db_output 0.
In the bob circuit, we begin by binding two bits and a qubit to x, y and q,
respectively. We then apply a controlled X from y to q and then a controlled Z from
x to q. We then discard x and y (binding the outputs to the empty pattern ()) and
output the qubit q.
In the de Bruijn circuit, we begin by allocating two bits and a qubit, implicitly to
0, 1 and 2. We then apply a controlled X from wire 1 to 2 and a controlled Z from 0
to 2. We then discard bit 0. This operation shifts all the subsequent indices, so that
the remaining bit is now referred to as 0 and the qubit as 1. Discarding the other bit
repeats this shifting operation, leaving our qubit as 0. We then output the qubit.
We see that discard effectively closes the scope of a given binder. What opens a
binding scope? Clearly, the db_box operator at the start of the circuit binds variables,
but what if I wish to initialize a qubit in my circuit? In the example above, inserting
a db_gate init0 after the box would create a new qubit bound to 3. If instead we
placed the init0 between the two discards, it would bind that qubit to 2, since 2 was
freed up by the previous discard. The initialization gates init0 , init1 , new0 and new1
are the only gates that bind new variables; discard is the only one that terminates
them. (Additional gates for discarding wires will be introduced in Chapter 8.) The
remaining gates can be though of as merely functions on existing variables, though
meas changes the type of its input variable from a qubit to a bit.
We can now describe the compilation procedure. The first step in compiling HOAS
circuits to DB circuits is to concretize the variables, so that we can pattern-match
on the circuit’s own patterns. The get_fresh function takes in a wire type W and a
1
In the latter case, we would simply maintain a natural number n corresponding to the smallest
wire number used so far and allocate fresh patterns with indices greater than n.
2
These could reasonably be called “reverse de Bruijn circuits”, since the indices increase with
successive initializations, but the analogy to de Bruijn indices is loose in either case.
64
context Γ, and returns a fresh pattern p and context Γ' such that Γ' types p at W:
Fixpoint get_fresh w (Γ : Ctx) : Pat w * Ctx:=
match w with
| One ⇒ (unit, [])
| Bit ⇒ (bit (length Γ), singleton (length Γ) w)
| Qubit ⇒ (qubit (length Γ), singleton (length Γ) w)
| w1 ⊗ w2 ⇒ let (p1, Γ1 ) := get_fresh w1 Γ in
match Γ ⋓ Γ1 with
| Invalid ⇒ (dummy_pat _, dummy_ctx)
| Valid Γ' ⇒ let (p2, Γ2 ) := get_fresh w2 Γ' in
match Γ1 ⋓ Γ2 with
| Invalid ⇒ (dummy_pat _, dummy_ctx)
| Valid Γ'' ⇒ ((pair p1 p2), Γ'')
end
end
end.
Note that the input and output contexts of get_fresh will never overlap so the Invalid
branches will never be entered. (We prove this in get_fresh_merge_valid.) In fact,
the first ∣Γ∣ elements of the output Γ' will always be None. This allows us to define
add_fresh, which also returns a pattern and a context, except here the context is the
Γ ⋓ Γ'. This context plays the role of a state in constructing the circuit.
The following hoas_to_db_box function simply provides a fresh pattern and state
for compiling the inner HOAS circuit to a DB circuit:
Definition hoas_to_db_box {w1 w2} (B : Box w1 w2) : DeBruijn_Box w1 w2 :=
match B with
| box f ⇒ let (p,Γ) := add_fresh w1 [] in
db_box w1 (hoas_to_db Γ (f p))
end.
We can now give the full code for hoas_to_db, which essentially threads this state
through its computation (but contains several functions that we will need to explain):
Fixpoint hoas_to_db {w} Γ (c : Circuit w) : DeBruijn_Circuit w :=
match c with
| output p ⇒ db_output (subst_pat Γ p)
| gate g p f ⇒ let p0 := subst_pat Γ p in
let (p',Γ') := process_gate g p Γ in
db_gate g p0 (hoas_to_db Γ' (f p'))
| lift p f ⇒ let p0 := subst_pat Γ p in
let Γ' := remove_pat p Γ in
db_lift p0 (fun b ⇒ hoas_to_db Γ' (f b))
end.
Let us begin with the simplest function, process_gate, which handles the con-
cretization part of the compilation procedure.
65
Definition process_gate {w1 w2} (g : Gate w1 w2)
: Pat w1 → Ctx → Pat w2 * Ctx :=
match g with
| U _ | BNOT ⇒ fun p st ⇒ (p,st)
| init0 | init1 ⇒ fun _ st ⇒ add_fresh Qubit st
| new0 | new1 ⇒ fun p st ⇒ add_fresh Bit st
| meas ⇒ fun p st ⇒ match p with
| qubit v ⇒ (bit v, change_type v Bit st)
end
| discard ⇒ fun p st ⇒ (unit, remove_pat p st)
end.
This function takes in a gate, a concrete input pattern, and a state, then returns a new
concrete pattern and an updated state. For unitary gates, which have the same input
and output wire types, it simply returns the provided pattern and state. In effect, this
says “you can continue using this pattern in the continuation”. Similarly, process_gate
meas simply changes the given pattern from qubit v to bit v and updates the state
to reflect that change. Initialization produces a fresh bit or qubit and adds it to the
end of the state, and discard returns the pattern () and removes a bit from the state.
To be precise, it updates Some Bit to None in the state — this will be important for
what follows.
If we left out the subst_pats in the code above, it would convert bob to the
following circuit3 :
Definition bob :=
box (bit 0, bit 1, qubit 2) ⇒
gate (bit_ctrl X) @ (1,2);
gate (bit_ctrl Z) @ (0,2);
gate discard @ 0;
gate discard @ 1;
output 2.
This circuit is concrete but it is not yet flat: By the end of the circuit, there is a
wire 2 but no 0 or 1. In order to flatten this circuit we need substitution contexts to
map variables to their flat equivalents. Fortunately, our Ctxs, which served admirably
in the role of state, also make good substitution contexts. To see why, note that there
are two ways of giving the size of a Ctx that differ by whether we count Nones, as
illustrated by the following example:
length [None; Some Bit; None; None; Some Qubit] = 5
size [None; Some Bit; None; None; Some Qubit] = 2
We can similarly define an index function that ignores Nones. In the above example
index 1 Γ = 0 and position 4 Γ = 1. If index is given an argument that corresponds
3
Note that we don’t have a type for this intermediate representation, which is simply meant to
be illustrative.
66
to a None or lies outside the bounds of the list, it returns 0. To perform substitution,
we simply map index throughout a pattern:
Fixpoint σ (Γ : Ctx) {w} (p : Pat w) : Pat w :=
match p with
| unit ⇒ unit
| qubit x ⇒ qubit (index x Γ)
| bit x ⇒ bit (index x Γ)
| pair p1 p2 ⇒ pair (σ Γ p1) (σ Γ p2)
end.
To see how this looks in practice, we return to our bob circuit, annotating each
line with the value of σ Γ 2 after each operation:
Definition bob :=
box (bit 0, bit 1, qubit 2) ⇒
gate (bit_ctrl X) @ (1,2); σ [Some Bit; Some Bit; Some Qubit] 2 = 2
gate (bit_ctrl Z) @ (0,2); σ [Some Bit; Some Bit; Some Qubit] 2 = 2
gate discard @ 0; σ [None ; Some Bit; Some Qubit] 2 = 1
gate discard @ 1; σ [None ; None ; Some Qubit] 2 = 0
output 2.
Performing all of the substitutions as we go yields the de Bruijn circuit db_bob
with which we began this section.
67
those of the Mathematical Components (Mahboubi et al., 2016) and C-CORN (Cruz-
Filipe et al., 2004) libraries. On the other hand, a major advantage of extending Coq’s
reals is that it gives us access to Coq’s automation techniques, including field, which
converts field expressions into a normal form to check equality, and fourier which
applies the Fourier-Motzkin algorithm (Fourier, 1826; Motzkin, 1936) to decide real
(in)equalities. The Coq standard library also provides the powerful lra (linear real
arithmetic) tactic which subsumes field and fourier. We define our own tactics that
extend this automation to complex numbers, which we discuss in Chapter 9.
Our additions to Coquelicot are relatively modest. We show that for any complex
number c, c ∗ c̄ is a real number, which is important for multiplying a matrix by its
adjoint, along with a few related lemmas about the complex conjugate. We also prove
a number of lemmas about taking square roots, which are important for reasoning
about states with Hadamard matrices applied.
Since certain quantum algorithms apply phase shift gates, which correspond to
the matrix
1 0
( )
0 eiθ
for some real number θ, we define eiθ using Euler’s formula:
Definition Cexp (θ : R) : C := cos θ + i * sin θ
We also use this to prove the special case of Euler’s identity, which we write as
Cexp PI = −1. Note that we cannot define the general case of complex exponentiation
as a function, since xy can have multiple solutions for x, y ∈ C.
Our modified version of Coquelicot’s complex number library is available in the
Qwire Github repository (https://github.com/inQWIRE/QWIRE) as Complex.v.
This file also removes all of Coquelicot’s dependencies, including the SSReflect and
Mathematical Components libraries.
68
Definition WF_Matrix {m n} (M : Matrix m n) : P :=
∀ i j, i ≥ m ∨ j ≥ n → M i j = 0.
The library is designed to facilitate reasoning about and computing with matri-
ces. Treating matrices as functions allows us to easily express otherwise complicated
matrix operations. Consider the definitions of Kronecker product (⊗) and adjoint († ),
where x∗ is the complex conjugate of x:
Definition kron {m n o p} (A : Matrix m n) (B : Matrix o p) :
Matrix (m*n) (o*p) :=
fun x y ⇒ A (x / o) (y / p) * B (x mod o) (y mod p).
Infix "⊗" := kron (at level 40, left associativity).
69
Mixed_State ρ1 →
Mixed_State ρ2 →
Mixed_State (p .* ρ1 .+ (1-p) .* ρ2 ).
Note that every mixed state is also well formed, since scaling and addition preserve
well-formedness.
A superoperator is a function on square matrices that takes mixed states to mixed
states.
Definition Superoperator m n := Matrix m m → Matrix n n.
Definition WF_Superoperator m n (f : Superoperator m n) :=
∀ (ρ : Matrix m m), Mixed_State ρ → Mixed_State (f ρ).
Any m × n matrix A can be lifted to a superoperator from n to m by multiplying an
input matrix by A and its adjoint:
Definition super {m n} (A : Matrix m n) : Superoperator n m :=
fun ρ ⇒ A × ρ × A† .
Of course, not every matrix so lifted will produce a well-formed superoperator that
preserves mixed states. We will address which matrices have this property, along with
broader questions about well-formed quantum structures, in Chapter 6.
70
Unitaries Every gate of type Unitary W corresponds to a unitary matrix of dimen-
sion 2JW K × 2JW K . The following gates are built-in to Qwire, but additional gates may
be added:
0 1 0 −i 1 0 1 1 1 1 0
JXK = ( ) , JY K = ( ) , JZK = ( ) , JHK = √ ( ) , JRϕ K = ( )
1 0 i 0 0 −1 2 1 −1 0 eiϕ
I 0
( ).
0 JU K
We can prove that every denoted unitary satisfies the is_unitary predicate defined
in the previous section:
Lemma unitary_gate_unitary : ∀ {W} (u : Unitary W), is_unitary JuK.
Gates We can now look at denoting gates in general. We will begin in a simplified
setting, where the gate is being applied to a system of the corresponding size in the
correct order (for instance, CNOT being applied to qubits 0 and 1 of a two qubit
system). In the unitary case, we simply apply U and its adjoint to the state, written
mathematically by
JU uKρ = JuKρJuK†
or in Coq as
JU uK ρ = super U ρ
We can give the denotation of the remaining gates in Coq, following the denotation
given in Section 4.5:
Definition denote_gate {W1 W2 } (g : Gate W1 W2 ) :
Superoperator 2^JW1 K 2^JW2 K :=
match g with
| U u ⇒ super JuK
| init0 | new0 ⇒ super ∣0⟩
| init1 | new1 ⇒ super ∣1⟩
| meas ⇒ Splus (super ∣0⟩⟨0∣) (super ∣1⟩⟨1∣|)
| discard ⇒ Splus (super ⟨0∣) (super ⟨1∣)
end.
where Splus sums over superoperators.
Gates in Context It takes some work to lift this denotation function to the con-
text of denoting gates in a circuit, where we may have additional unused wires or
non-adjacent wires input to one gate. We will begin by giving the denotation for sin-
gle qubit unitaries, which we pad with identity matrices before applying them to a
71
quantum state. For instance, if we want to apply a unitary U to qubit 3 in a 5-qubit
system ρ, this amounts to the operation
where I is the identity matrix with the same dimensions as U . This expression can
easily be padded with the identity in the middle, as in
or reversed, as in
U ⊗ ∣1⟩ ⟨1∣ + I ⊗ ∣0⟩ ⟨0∣
when the target is above the control.
This gives us a blueprint for applying unitary gates which may have multiple
control qubits to arbitrary systems. First we need to know where we will be placing the
controls and where we will be placing the single-qubit gate. We put this information
into a zipper structure (see Figure 5.2), containing the controls above the unitary,
those after it, and the 2 × 2 unitary matrix. For instance, suppose we wished to apply
ctrl (ctrl (ctrl Z)) to the control wires 0, 2, 7, and the target wire 4 in an eight-qubit
system: We would construct the zipper ([true; false; true; false], JZK, [false; false
; true]).
5
This observation is due to Kesha Hietala, who proposed the algorithm that follows as an efficient
alternative to the liberal use of swap gates (our prior approach).
72
t
f
t
f
Z Z
f
f
t
Figure 5.2: A ctrl (ctrl (ctrl Z)) gate applied to 0, 2, 7 and 4, and it’s corre-
sponding zipper.
We would then feed this zipper into the following (symmetric) functions:
Fixpoint ctrl_list_to_unitary_l (l r : list B) (u : Square 2) :
(Square (2^(length l + length r + 1))) :=
match l with
| false :: l' ⇒ 'I_ 2 ⊗ ctrl_list_to_unitary l' r u
| true :: l' ⇒ ∣1⟩⟨1∣ ⊗ ctrl_list_to_unitary l' r u .+ ∣0⟩⟨0∣ ⊗ 'I_ _
| [] ⇒ ctrl_list_to_unitary_r (rev r) u
end.
∣1⟩⟨1∣ ⊗ (I2 ⊗ (∣1⟩⟨1∣ ⊗ (I2 ⊗ (Z ⊗ I2 ⊗ I2 ⊗ ∣1⟩⟨1∣ + I8 ⊗ ∣0⟩⟨0∣)) + ∣0⟩⟨0∣ ⊗ I32 )) + ∣0⟩⟨0∣ ⊗ I128
73
Circuits We are now in a position to define the general denotation of the De Bruijn
circuits from Section 5.3:
Fixpoint denote_db_circuit {w} padding input (c : DeBruijn_Circuit w) :
Superoperator (2^(padding+input)) (2^(padding+JwK)) :=
match c with
| db_output p ⇒ super (pad (padding+input) JpK)
| db_gate w1 w2 g p c' ⇒
let input' := (input + Jw2K - Jw1K) in
compose_super (denote_db_circuit padding input' c')
(apply_gate g (pat_to_list p))
| db_lift p c' ⇒
let k := get_var p in
Splus
(compose_super
(denote_db_circuit padding (input-1) (c' false))
(super ('I_(2^k) ⊗ ⟨0∣ ⊗ 'I_(2^(input-k-1)))))
(compose_super
(denote_db_circuit padding (input-1) (c' true))
(super ('I_(2^k) ⊗ ⟨1∣ ⊗ 'I_(2^(input-k-1)))))
end.
Here input is the number of input qubits and padding allows us to pad the denotation
with identities, which is useful in a number of lemmas.
The denotation of output p is simply the denotation of p: a reordering of the qubits
via SWAP gates. Applying a gate consists of composing the apply_gate operation above
with the denotation of the rest of the circuit. Finally, lift applies the discard operations
super ('I_(2^k) ⊗ ⟨0∣ ⊗ 'I_(2^(input−k−1)))) and super ('I_(2^k) ⊗ ⟨1∣ ⊗ 'I_(2^(input
−k−1)))), takes the denotation of the rest of the circuit, and sums the results.
This gives us a superoperator on density matrices and allows us to verify properties
of our circuits.
74
Imperative Syntax To get a sense for the imperative Qwire syntax, we will
present an implementation of Deutsch’s algorithm6 . Note that throughout this thesis
we elide the underscores that serve to differentiate our notations from our constructors
and Coq’s built-in functions.
Definition deutsch Uf :
Box One Bit :=
box () ⇒
gate x ← init0 @ ();
gate x ← H @ x;
gate y ← init1 @ (); 0 H H meas
gate y ← H @ y; Uf
let (x,y) ← unbox Uf (x,,y); 1 H meas
gate y ← meas @ y;
gate () ← discard @ y;
gate x ← H @ x;
gate x ← meas @ x;
output x.
Note that Deutsch’s algorithm consists mostly of applying basic gates to single
qubit wires, along with one unboxing of the input circuit Uf . In the simplest case, our
gate notation simply hides some higher order abstract syntax:
Notation "'gate' p2 ← g @ p ; c2" := (gate g p (fun p2 ⇒ c2))
We also have special cases of the gate notation, firstly for gates with the unit
output,
Notation "'gate' () ← g @ p ; c2" := (gate g p (fun _ ⇒ c2))
and secondly for gates with multiple outputs
Notation "'gate' ( p1 , p2 ) ← g @ p ; c2" :=
(gate g p (fun x ⇒ let (p1,p2) := wproj x in c2))
The wproj function here matches on a pattern of type Pat (W1 ⊗ W2 ) and returns
its two constituent sub-patterns as p1 and p2. Coq’s limited capacity for recursive
notations doesn’t allow us to extend this notation to have arbitrary patterns on the
left (since (p1,p2) cannot be made independent of the rest of the notation), instead
we provide additional notations for patterns of three and four sub-patterns.
Similarly to gate, we write box p ⇒ C for box (fun p ⇒ C) and let p ← c1 ; c2 for
compose c1 (fun p ⇒ c2). These notations also have variants for () and pairs, imple-
mented in the same manner as gate. The perceptive reader will notice that when
we unbox Uf we provide the pattern (p1,,p2). This notation is defined using Coq’s
recursive notations7 as
6
We will leave the explanation of this algorithm for Section 7.1.3, in which we verify its correctness.
For this chapter, the reader only needs to know the circuit we are implementing.
7
The Coq reference manual calls these recursive patterns (Coq Development Team, 2018). We
try to avoid using “patterns” to refer to anything but wire patterns, hence “recursive notations”.
75
Notation "( x ,, y ,, .. ,, z )" := (pair .. (pair x y) .. z)
and can be nested. We use the (admittedly ugly) double comma notation in order to
save the single comma notation for Qwire’s functional syntax.
We also define a lift_wire function that checks if a wire is a Bit or Qubit and
either directly calls lift on it or else measures and then lifts it. This is built into our
notation for lift, along with variants that allow the lift notation to be applied on
patterns of wires (implicitly measuring and lifting them one at a time).
Functional Syntax We can now introduce our “functional” syntax for quantum
circuit, again via the example of Deutsch’s algorithm:
Definition deutsch (Uf : Square_Box (Qubit ⊗ Qubit)) : Box One Bit :=
box () ⇒
let x ← H $ init0 $ ();
let y ← H $ init1 $ ();
let (x,y) ← Uf $ (x,y);
let () ← discard $ meas $ y;
meas $ _H $ x.
The reader will notice a few changes:
2. Using a boxed circuit Uf looks no different than applying a basic gate like H or
meas.
These work through two simple coercions: We use output to coerce patterns to
circuits and boxed_gate to coerce gates to boxed circuits. We then define $ as a
notation for the following function:
Definition apply_box {w1 w2} (b : Box w1 w2) (c : Circuit w1) :
Circuit w2 := let x ← c; unbox b x.
When we write init0 $ (), then, we are really calling apply_box with the arguments
boxed_gate init0 and output (). This function returns a circuit producing a qubit,
which can then be provided as the second argument to apply_box (boxed_gate H),
producing a superimposed qubit.
How then do we interpret Uf $ (x,y)? It is natural to assume that this is sim-
ply notation for apply_box Uf (output (pair x y)). However, things are slightly more
complicated than that. We would like to be able to write let (x,y) ← (H,H) $ (x,y) or
even let (x,y) ← (H $ x, y). This requires (_,_) to take a pair of circuits with outputs
W1 and W2 and return a Circuit W1 ⊗ W2 . This notation calls the function pair_circ
76
0 H H meas
0 H H meas
0 H H meas
0 H H meas
0 H
Uf H meas
0 H H meas
0 H H meas
1 H meas
H
which does exactly that. This notation is also defined as a recursive notation, allowing
us to write (H,X,Z,q) and to nest circuit pairs inside other circuit pairs.
All of the functions we use here are fairly lightweight. Still, it is impossible to write
a circuit in normal form using these notations (and we would like our normal forms
to be readable when stepping through proofs). Hence, we maintain the imperative
syntax for representing circuits, and the second presentation of deutsch efficiently
reduces to the first.
Qwire in Action Just to give the reader a better sense for the flavor of Qwire,
we will conclude with two more interesting programs.
The first is the Deutsch-Josza algorithm (Deutsch and Jozsa, 1992), a generaliza-
tion of Deutsch’s algorithm to an arbitrary number of qubits. Our implementation
uses the notations g #n for inParMany g n (that is, apply n copies of g in parallel) and
(()) for a pattern containing only units:
Definition Deutsch_Jozsa (n : N)
(Uf : Box ((n ⊗ Qubit) ⊗ Qubit) ((n ⊗ Qubit) ⊗ Qubit)) :
Box One (n ⊗ Bit) :=
box () ⇒
let qs ← H #n $ init0 #n $ (());
let q ← H $ init1 $ ();
let (qs,q) ← Uf $ (qs,q);
let () ← discard $ meas $ q;
meas #n $ _H #n $ qs.
We also provide a coin tossing program that uses dynamic lifting (Figure 5.4).
First, we will define a simple coin toss.
Definition coin_flip : Box One Bit :=
77
coin_flip
0 H meas
coin_flips_lift n
n 0
coin_flip x
coin_flips_lift (n-1)
Figure 5.4: A basic coin flip circuit and a multiple-coin flipping circuit using dynamic
lifting. The braces denote branching on a classical term (nats or bools).
78
Chapter 6
Verifying Qwire
Before we begin verifying quantum circuits in Qwire, it’s important to verify Qwire
itself. What do we mean by “verifying Qwire ”? Qwire has notions like unitaries,
density matrices, mixed states, superoperators, and even matrices themselves that
aren’t enforced at the type level. One can write the following matrix definition in
Coq:
Definition bad_matrix : Matrix 4 4 := fun x y ⇒ 6.
This clearly doesn’t correspond to a valid 4 × 4 matrix: It has infinitely many non-
zero elements. Similarly, Density n is just a notation for an n × n matrix, and a
Superoperator, which should be a mapping between proper density matrices, is simply
a function from some Density m to Density n. Instead, the properties we care about are
enforced by extrinsic predicates like WF_Matrix, WF_Unitary, Pure_State, Mixed_State,
and WF_Superoperator that guarantee that our terms have the desired properties. In
the following section, we will discuss each of these properties and how we show that
our matrices possess them and our functions preserve them.
We are also concerned with broader questions about the correctness of Qwire.
One such question is whether circuit composition corresponds to function composi-
tion, as it should. We will deal with these questions in the following section.
79
Beyond proving that the matrices we frequently use, such as unitary operators
and qubit matrices, are well-formed, we want to show that the various operations we
perform on matrices preserve well-formedness. Our matrix library proves this property
about all of our functions from matrices to matrices, including +, ∗, ×, ⊗, ⊺ , and † .
It is interesting to note which theorems about matrices require well-formedness
and which do not. This tells us whether these are theorems about functions that just
happen to apply to matrices as a special case, or whether they are specific to matrices.
Naturally, the left and right additive identities on matrices apply to all functions: If
we lift + to operate on functions, then ∀f, (λx.0)+f = f . By similar reasoning, matrix
addition is commutative and distributive even for ill-formed matrices. The transpose
and adjoint operators can be thought of as simply swapping their arguments (and
negating the complex component in one case) and thus are trivially involutive.
Operations like the trace, matrix multiplication, and Kronecker product are more
difficult to analyze, given that they use the matrix’s dimensions in their definitions.
Still, it is interesting to note that, of the core properties of matrix arithmetic, only
three required well-formedness in their proofs:
Lemma Mmult_1_l: ∀ m n (A : Matrix m n), WF_Matrix m n A → 'I_m × A = A.
Lemma Mmult_1_r: ∀ m n (A : Matrix m n), WF_Matrix m n A → A × 'I_n = A.
Lemma Kron_1_l : ∀ m n (A : Matrix m n), WF_Matrix m n A → 'I_1 ⊗ A = A.
Kron_1_r, by contrast, simply states that ∀ m n (A : Matrix m n), A ⊗ 'I_1 = A. This is
because the dimensions of the right-side matrix appear in the definition of the Kro-
necker product, so (A ⊗ 'I_1) x y becomes A (x/1) (y/1) ∗ 'I_1 (x mod 1) (y mod 1). Since
x mod 1 is always 0 and 'I_1 0 0 = 1, this easily simplifies to A x y.
Obviously, well-formedness is important for all of our unitary operators and den-
sity matrices. Therefore, our predicates WF_Unitary U and Mixed_State ρ themselves
assert that U and ρ are well-formed matrices.
6.1.2 Unitarity
For every gate introduced in Chapter 5, we have a corresponding unitary matrix. Our
WF_Unitary predicate is quite simple:
Definition WF_Unitary {n: N} (U : Matrix n n): P :=
WF_Matrix n n U ∧ U † × U = Id n.
We can easily prove that every concrete unitary operator satisfies this predicate
and that the control and adjoint operations preserve it. For most of our operators,
with the exception of the phase shift by arbitrary real numbers, we can further prove
that they are their own adjoints and, hence, inverses.
We can take things a step further. Not only do we want to know that our basic
unitary matrices are in fact unitary, but we also want to know that when we apply a
unitary gate to a large quantum state, this transformation is unitary. In the case of
applying a single-qubit unitary U , this amounts to verifying that Im ⊗ U ⊗ In is a uni-
tary matrix for any m and n. In the case of controlled unitaries, this involves proving
80
that the rather involved procedure in Section 5.5 produces unitary matrices. We have
verified this procedure, which will allow us to show that our circuits correspond to
valid superoperators in the next section.
2. It is positive semidefinite.
3. trace(ρ) = 1.
4. ρ2 = ρ.
81
witness. However, it has proven far more usable in practice than any of the definitions
given above.
A mixed state is generally defined as a sum ∑i pi ρi , where each ρi is a pure state,
every pi is in [0, 1], and ∑i pi = 1. We express this using the following inductive
predicate:
Inductive Mixed_State {n} : (Matrix n n) → P :=
| Pure_S : ∀ ρ, Pure_State ρ → Mixed_State ρ
| Mix_S : ∀ (p : R) ρ1 ρ2 , 0 < p < 1 → Mixed_State ρ1 → Mixed_State ρ2 →
Mixed_State (p * ρ1 + (1-p) * ρ2 ).
Note that this definition makes mixed states into a superset of pure states, as did
our use of square brackets in the equation above. This is a fairly common practice
and useful for our purposes: We will often care that a matrix corresponds to a valid
quantum state, but we will almost never care that it is impure. If we wished to express
that a state was mixed in the strict sense, we could simply write Mixed_State ρ ∧ ¬
Pure_State ρ.
We separately prove important properties of mixed states: for instance, that they
all correspond to well-formed matrices and have traces that are equal to one. Most
importantly, we show that they are preserved by unitary transformations and other
operations. This brings us to the notion of a superoperator.
82
This lemma deals only with the application of gates to the correct number of
qubits, outside of the context of a larger circuit. However, it contains most of the
reasoning about the different kinds of gates relevant to our main theorem of this
section. In particular, it uses our WF_Superoperator_unitary lemma and proves sim-
ilar results about measurement, initialization, and discard: Each operation preserves
mixed states. However, it is limited by its assumption that gates are being applied
to quantum states of exactly the same arity: for instance, measurement to a single
qubit or CNOT to two qubits. Hence, we prove the following theorem, which cannot
use denote_gate_correct directly but generalizes its result to larger quantum states.
Theorem 9. Every well-typed static circuit corresponds to a valid superoperator.
83
is a valid superoperator if and only if
†
∑ Am Am = I.
m
We have axiomatized this theorem in the Coq development due to the difficulty of
connecting our definition of mixed states to the mathematical description given in the
previous subsection, and thereby to the definitions used in proving the operator sum
decomposition theorem. In principle, we could use this theorem to define mixed states
but we feel that this definition would be less intuitive. Note that we can immediately
derive that applying unitaries preserves mixed states from this axiom, however we
prefer to prove that (and the initialization case) directly, without recourse to an
axiom. We summarize the axioms used in the Qwire development in Chapter 10.
84
If we assume the denote_compose lemma, we get a number of desirable corollaries,
including a characterization of our circuit sequencing function:
Lemma inSeq_correct : ∀ W1 W2 W2 (c' : Box W2 W2 ) (c : Box W1 W2 ),
Typed_Box c → Typed_Box c' →
denote_box (inSeq c c') =
compose_super (denote_box g) (denote_box f).
Mathematically, for boxed circuits c and c′ , Jc; ; c′ K = Jc′ K ○ JcK. A similar (sketched
but unproven) lemma for parallel composition says that Jc1 ∥ c2 K(ρ1 ⊗ ρ2 ) = (Jc1 Kρ1 ) ⊗
(Jc2 Kρ2 ), provided that the dimensions line up:
Fact inPar_correct : ∀ W1 W1 ' W2 W2 ' (f : Box W1 W1 ') (g : Box W2 W2 ') (safe
: B)
(ρ1 : Square ⟦(2^W1 ⟧)) (ρ2 : Square ⟦(2^W2 ⟧)),
Typed_Box f → Typed_Box g →
WF_Matrix ⟦(2^W1 ⟧) ⟦(2^W1 ⟧) ρ1 →
WF_Matrix ⟦(2^W2 ⟧) ⟦(2^W2 ⟧) ρ2 →
denote_box safe (inPar f g) (ρ1 ⊗ ρ2 ) =
(denote_box safe f ρ1 ⊗ denote_box true g ρ2 ).
Note that this statement is narrower than we would like it to be, in that it re-
quires the input matrix to the product of two non-entangled states. Really, we would
like to write something of the form Jc1 ∥ c2 K = Jc1 K ⊗ Jc2 K, for a tensor product that
corresponds to the tensor product on unitary matrices. However, our representation
of superoperators as simple functions from matrices to matrices limits us from intro-
ducing such an operator. This suggests implementing alternative representations of
of superoperators, such as the Choi or Stinespring representations (Watrous, 2018,
Section 2.2), that have additional structure that we could exploit. These could also
aid us in proving the operator-sum decomposition theorem of the previous section.
85
directly through our de Bruijn circuits. We would also like to convert OpenQASM
and QUIL programs to Qwire programs, allowing us to typecheck and verify circuits
generated by a variety of quantum programming languages. Translating these pro-
grams to de Bruijin circuits would substantially simplify this process. However, this
requires us to have a procedure for typechecking de Bruijin circuits and proofs that
well-typed de Bruijin circuits correspond to valid superoperators. We leave this for
future work.
86
Chapter 7
We can now move on to the other goal of our thesis: formal verification of quantum
programs. This verification can take a number of forms, from low-level checks that a
given circuit produces the right output matrix to high level specifications of program
properties, generally as functions from matrices to matrices. In this section, we will
begin with the simplest forms of verification and move on to more complicated forms.
where the one-half in the top left corresponds to the probability of measuring ∣0⟩.
The proof of this property is quite simple, consisting of simply unfolding defini-
tions and computing, using our matrix_denote, Msimpl and solve_matrix tactics from
Chapter 9.
87
7.1.2 Teleport
On occasion we can write similar proofs about open circuits: for instance, the teleport
example from Chapter 2.
Here is the code for teleport
Definition teleport :=
box q ⇒
let (a,b) ← bell00 $ () ;
let (x,y) ← alice $ (q,a) ;
bob $ (x,y,b).
and the lemma we desire to prove about it:
Lemma teleport_eq : teleport ≡ id_circ.
This says that the denotation of teleport is identical to the denotation of our identity
circuit.
We could also write this out more explicitly as
Lemma teleport_eq': ∀ (ρ : Density 2),
WF_Matrix ρ → JteleportK ρ = ρ.
That is, for any input matrix ρ corresponding to a one-qubit quantum state, teleport-
ing ρ returns ρ.
Given that teleport takes an input qubit, it might seem difficult to use the tech-
nique above. In the one-qubit case, at least, this happens not to be true. We can
rewrite our input matrix as simply
ρ ρ
( 0,0 0,1 )
ρ1,0 ρ1,1
88
bell00 bob b1 b2 alice
0 H X Z H meas
b1
0 meas
b2
89
7.1.3 Deutsch’s Algorithm
Next, we verify an implementation of a classic algorithm from the the quantum com-
puting literature, Deutsch’s algorithm (Deutsch, 1985; Cleve et al., 1998). Deutsch’s
Problem presents the programmer with a function f ∶ {0, 1} → {0, 1} and asks her to
determine whether the function is constant or not. In the classical case, this obviously
requires that we query the function on both 0 and 1. Deutsch’s algorithm, as modified
by Cleve et al., solves this on a quantum computer by using a single query. First,
however, we must guarantee that f corresponds to a unitary transformation. We use
a standard trick to transform f into a Uf , which is guaranteed to be unitary:
Uf (x ⊗ y) = x ⊗ (y ⊕ f (x))
That is, Uf maintains the state of the input qubit and puts the result of f (x) onto
the second qubit in the form of y ⊕ f (x).
We can now recall Deutsch’s algorithm:
Definition deutsch Uf :
Box One Bit :=
box () ⇒
let x ← H $ init0 $ (); 0 H H meas
Uf
let y ← H $ init1 $ (); meas
1 H
let (x,y) ← Uf $ (x,y);
let () ← discard $ meas $ y;
meas $ H $ x.
Here are the two statements we would like to prove about Deutsch’s algorithm:
Lemma deutsch_constant : ∀ f, constant f →
⟦deutsch (fun_to_box f)⟧ I1 = ∣0⟩⟨0∣.
90
coin_flip
0 H meas
coin_flips_lift n
n 0
coin_flip x
coin_flips_lift (n-1)
91
else new0 $ ()
end.
This circuit flips a coin up to n times, stopping and returning tails (∣0⟩) if it ever
lands tails. If all n tosses come up heads, it returns heads.
We would like to prove that that this circuit simulates a biased coin that returns
heads with probability 21n . This is trivially encoded in the biased_coin matrix
1 − bias 0
( )
0 bias
0 0 1 − 210 0
( )=( 1)
0 1 0 20
1 − 211+n 0
p∗( 1 ).
0 21+n
92
We can then apply this lemma to the special case where p = 1, giving us our
desired result.
show that the denotation of Jadj UK is JUK† , and then use the fact (proved in Chapter 6)
that the denotation of every unitary gate is a unitary matrix to replace JUK† × JUK with
the identity matrix.
Hence, proving a simple fact about unitary gates requires careful management of
the goal and the application of lemmas from across the Qwire development.
We have yet to use this technique to prove properties of complex circuits, but we
suspect that the correctness proof for the quantum fourier transform (or QFT) will
be similarly algebraic. Here is the statement of that theorem for the basis qubits,
written out mathematically:
1 2 −1 2πixy
n
93
7.4 Equational Rewriting
One of the more powerful techniques for reasoning about circuit behavior and opti-
mizing those circuits is equational reasoning. Using a set of basic circuit identities,
we could rewrite Qwire circuits, shrinking them and making them easier to run on
a real-world quantum computer. One common identity (a unitary followed by its ad-
joint is equal to the identity) is given in Section 7.3.1. Here, we present some other
useful transformations, drawn from Staton’s (2015) equational theory for quantum
computation.
Rather than negate a qubit and then measure it, we can always measure the qubit
and then negate it. We can represent this as the equivalence of the following circuits:
meas meas
Definition X_meas := Definition meas_NOT :=
box q ⇒ meas $ X $ q. box q ⇒ BNOT $ meas $ q.
BNOT here is simply the classical (bit-valued) NOT gate.
We can prove this by crunching matrices, but it also proves to be straightforward
algebraically: The denotation of X is equal to the denotation of BNOT and commutes
with measurement. Many of the equalities in this section will be similarly easy to
prove via computation or matrix rewriting.
The equality of the following two circuits is obvious in the classical setting but less
intuitive in the presence of entanglement, where measurement may disturb multiple
qubits:
U meas meas
Definition U_meas_discard U := Definition meas_discard :=
box q ⇒ discard $ meas $ U $ q. box q ⇒ discard $ meas $ q.
This says that applying a unitary to a qubit and then measuring and discarding it
is the same as simply measuring and then discarding the qubit. We prove the equality
of these circuits computationally.
A number of additional equalities drawn from Staton’s theory are available in the
file Equations.v in the Coq development.
Our rewriting system should also account for dynamic lifting and optimize around
it when called for. The following dynamically lifted circuit with is equal to the identity
circuit on one Bit:
94
Definition lift_new : Box Bit Bit :=
box b ⇒
lift x ← b;
new x $ ().
Here, new x is new1 when x is true and, otherwise, new0 .
While we have a small library for rewriting circuits, an optimizing compiler is still
a work-in-progress. Substantial work has gone into rewriting libraries for quantum
circuits, most notably using the ZX-calculus (Coecke and Duncan, 2008; Backens,
2014) and the related Quantomatic tool (Kissinger, 2011). This tool faces two chal-
lenges, in that ZX graphs are more expressive than quantum circuits, and its rewrite
rules are not directed, making it hard to write a terminating procedure for shrink-
ing circuits. A recent paper by Fagan and Duncan (2018) makes some headway on
these issues, but we have yet to address the second in the Qwire setting. Fortu-
nately, Qwire circuits correspond precisely to valid quantum circuits, so we don’t
have to convert between representations; however, graphs may well be more amenable
to rewriting than sequences of gate applications. This form of rewriting would be a
significant step forward for automated circuit optimization and motivates the need
for compositionality lemmas of the style proposed in Section 6.2).
95
Chapter 8
Reversibility
a a a a
b b b b
z z ⊕ (a ∧ b) z z ⊕ (a ∨ b)
Figure 8.1: Quantum oracles implementing the boolean ∧ and ∨. The ⊕ gates represent
negation, and ● represents control.
96
a a
b b
0 a∨b
c a
d b
0 c∨d
z z ⊕ ((a ∨ b) ∧ (c ∨ d))
a a
b b
0 0
c a
d b
0 0
z z ⊕ ((a ∨ b) ∧ (c ∨ d))
entangled with.)
How can we verify that such an assertion is actually true? We cannot dynamically
check the assertion, since we can only access the value of a qubit by measuring it,
thereby collapsing the qubit in question to a 0 or 1 state. However, we can statically
reason that the qubit must be in the state ∣0⟩ by analyzing the circuit semantics.
The claim that a qubit is in the 0 state is a semantic assertion about the behavior
of the circuit. Unfortunately, this makes it hard to verify—computing the semantics
of a quantum program is computationally intractable in the general case. Circuit
programming languages often allow users to make such assertions but not to verify
that they are true. For example, Quipper (Green et al., 2013a) allows programmers
to make assertions about the state of ancillae, but these assertions are never checked.
Likewise, in Q# (Svore et al., 2018) the assertion will be checked by a simulator but
cannot be checked when a program is run on a quantum computer. Hence, when the
qubit is reused, a common use for ancillae which Q# emphasizes, it may be in the
wrong state. The QCL quantum circuit language (Ömer, 2005) provides a built-in
method for creating reversible circuits from classical functions, but the programmer
must trust this method to safely manage ancillae. In a step in the right direction, the
ReV erC compiler (Amy et al., 2017) for the (non-quantum) reversible computing
97
language Revs (Parent et al., 2017) provides a similar approach to compilation and
verifies that it correctly uncomputes its ancilla. However, other assertions in Revs
that a wire is correctly in the 0 state are ignored if they cannot be automatically
verified.
In this chapter, we develop verification techniques for safely working with ancillae.
Our approach allows the programmer to discard qubits that are in the state ∣0⟩ or
∣1⟩, provided that she first formally proves that the qubits are in the specified state.
Inspired by the ReV erC compiler (Amy et al., 2017), we also provide syntactic
conditions that the programmer may satisfy to guarantee that her assertions are true.
However, our quantum circuits do not need to match this syntactic specification: a
programmer may instead manually prove that her circuit safely discards qubits using
the denotational semantics of the language. This gives the programmer the flexibility
to use ancillae where the proofs of such assertions are non-trivial.
This chapter makes the follow core contributions:
• We give semantic conditions for the closely related properties of (a) when a
circuit is reversible and (b) when a circuit contains only valid assertions about
its ancillae.
• We show how this compilation can be used perform quantum arithmetic via a
quantum adder.
We should note that the results of this chapter have not yet been fully verified
in Coq. In particular, our section on syntactic guarantees for circuits (Section 8.3)
describes a number of lemmas that have mostly been sketched out in Coq or proved
based on admitted lemmas. Our section on oracles also admits the denotation of
two functions that apply CNOT and Toffoli gates to wires based on their positions
within the circuit (as in “wire number 7”) instead of referencing named patterns.
More broadly, this chapter assumes the correctness of two important lemmas from
Section 6.2: compose_correct and inPar_correct, which say that the denotation of
circuits arranged in sequence and in parallel correspond to functional composition
and the tensor product, respectively. The lemmas assumed in this chapter (excluding
the lemmas of Section 8.3) are summarized in Table 8.1.
98
Assumption Description
denote_compose The composition of circuits is equal to the compo-
sition of their denotations (Section 6.2)
inPar_correct Gives the denotation of circuits composed in parallel
valid_ancillae_box_equal Our two notations of assertion validity are equiva-
lent
valid_ancillae_unbox Relates the validity of assertions on boxed and un-
boxed circuits
[gate]_at_spec Describes the denotation of the [gate]_at [indices]
circuit, which applies a gate to the given indices
ancilla_free_[gate]_at [gate]_at has no ancillae
ancilla_free_seq The composition of two ancilla free circuits has no
ancillae
strip_one_l_out_eq Converting a Box W (One ⊗ W') to a Box W W' preserves
its denotation
strip_one_r_out_eq The same for Box W (W' ⊗ One)
valid_ancillae_box'_equiv Denotationally equivalent circuits must have the
same validity
valid_inSeq The composition of two valid circuits is valid
HOAS_Equiv_inSeq' If c1 ≡ c′1 and c2 ≡ c′2 then c1 ; ; c2 ≡ c′1 ; ; c′2
Table 8.1: Assumptions underlying the reversible computing development. The first
two are in Composition.v, the next two are in Ancilla.v, two instances of [gate]
_at_spec are in Oracles.v and the remaining assumptions are in Symmetric.v.
99
denote_safe U ρ = JU KρJU K†
denote_safe init0 ρ = ∣0⟩ ρ ⟨0∣
denote_safe init1 ρ = ∣1⟩ ρ ⟨1∣
denote_safe meas ρ = ∣0⟩ ⟨0∣ ρ ∣0⟩ ⟨0∣ + ∣1⟩ ⟨1∣ ρ ∣1⟩ ⟨1∣
denote_safe {discard, assert0 , assert1 } ρ = ⟨0∣ ρ ∣0⟩ + ⟨1∣ ρ ∣1⟩
Under the safe semantics, the assertions assert0 and assert1 are treated as a
measurement followed by a discard. This is semantically the same as the denotation
of discard, except that discard is guaranteed by the type system to only throw away
a classically valued bit. This operation on qubits is safe even if the qubit is in a
superposition of ∣0⟩ and ∣1⟩, due to the implicit measurement.
The unsafe semantics is the same as the safe semantics, except for assert0 and
assert1 :
It should be immediately clear why this is unsafe: if ρ isn’t in the zero state (in
the first case), then an assertion produces a density matrix with a trace less than 1.
Operationally, this corresponds to the instruction “throw away this qubit in the zero
state,” which is quantum-mechanically impossible in the general case. However, this
semantics corresponds to the intended meaning of assertx when we know the assertion
is true. It also ensures that the composition of initx with assertx is equivalent to
the identity, which allows us to optimize away qubit initialization and discarding.
We can now define what it means for the ancilla assertions in a circuit to be valid.
Definition valid_ancillae W (c : Circuit W) : P :=
(denote c = denote_unsafe c).
An equivalent definition states that the unsafe semantics preserves the trace of its
input, which is always 1, and therefore maps it to a total probability distribution.
Definition valid_ancillae' W (c : Circuit W) : P :=
∀ ρ, Mixed_State ρ → trace (denote_unsafe c ρ) = 1.
The second definition follows from the first because the safe semantics is trace pre-
serving. The first follows from the second since denote_unsafe c ρ corresponds to a
sub-distribution of denote_safe c ρ. If its trace is one then they must represent the
same distribution.
These two definitions precisely characterize what it means for circuits to have
always correct assertions. For brevity, we call such circuits valid. In the next section,
we define syntactic conditions that are sufficient but not necessary for validity. Pro-
grammers will often write syntactically valid circuits like those produced by compile
100
function in Section 8.4), but when needed the semantic definition of validity is still
available.
An important property related to the validity of a circuit is its reversibility. We say
that c and c' are equivalent, written c ≡ c', if both their safe and unsafe denotations are
equal. (If c and c' are valid, this is equivalent to denote c = denote c', but otherwise
it is a stronger claim.) Reversibility says that a circuit has a left and right inverse:
Definition reversible {W1 W2 } (c : Box W1 W2 ) : P :=
(∃ c', c' ;; c ≡ id_circ) ∧ (∃ c', c ;; c' ≡ id_circ)
In Section 8.4, the compiler produces circuits that are their own inverses:
Definition self_inverse {W} (c : Box W W) : P := c ;; c ≡ id_circ.
We can now show that in any reversible circuit all the ancilla assertions hold.
Proof. Let c' be c’s inverse. By the second definition of validity, it suffices to show
that the trace of denote_unsafe c ρ is equal to 1 for every initial mixed state ρ. We
know that the trace of
denote_unsafe id_circ ρ is 1; hence,
1 = trace (denote_unsafe (c;;c') ρ)
= trace (denote_unsafe c' (denote_unsafe c ρ))
Because the unsafe semantics is trace-non-increasing, it must be the case that the
trace of denote_unsafe c ρ is 1 as well.
101
all source qubits. In addition, it guarantees that assertions are only made on source
qubits with a corresponding initialization.
A classical gate acts on the qubit i if it affects the value of that qubit in an m-qubit
system: X acts on its only argument, CNOT acts on its second argument (the target),
and Toffoli acts on its third argument.
The property of source symmetry on circuits is defined inductively as follows:
• The identity circuit is source symmetric.
• If g is a classical gate that acts on a qubit in the target and c is source symmetric,
then both g ;; c and c ;; g are source symmetric.
The key property of a source symmetric circuit is that it does not affect the value
of its source qubits. We say that a circuit c is a no-op at qubit i if, when initialized
with a boolean b, the qubit is still equal to b after executing the circuit. We could
define this as JcK(ρ1 ⊗ ∣b⟩ ⟨b∣ ⊗ ρ2 ) = ρ′1 ⊗ ∣b⟩ ⟨b∣ ⊗ ρ′2 for some ρ1 , ρ2 , ρ′1 , ρ′2 , but this
would require ρ1 and ρ2 (and ρ′1 and ρ2 ’) to be separable, which is an unnecessary
restriction. Instead, we use the valid_ancillae predicate and say if we initialize an
ancilla in state x at i, apply b, and then assert that i = x, our assertion will be valid:
Definition noop_on (m k : N) (c : Box (Qubits (1 + m)) (Qubits (1+m)) : P
:=
∀ b, valid_ancillae (init_at b i ;; c ;; assert_at b i).
We similarly define a predicate, noop_on_source n, that says that a given circuit is a
no-op on each of its first n inputs.
These inductive definitions allow us to state a number of closely related lemmas
about symmetric circuits:
Lemma 9. If the classical gate g acts on the qubit k and i ≠ k, then g is a no-op on
i.
Lemma 10. Let c be a circuit such that c ;; assert_at b i is a valid assertion.
Then c ;; assert_at b i ;; init_at b i ≡ c.
c b b c
Lemma 11. If c and c' are both no-ops on qubit i, then c ;; c' is also a no-op on
qubit i.
102
Conjecture 1. If c is source symmetric, then it is a no-op on its source.
These lemmas have been admitted, rather than proven, in the Coq development
(Symmetric.v). Conjecture 1 is labeled as a conjecture rather than a lemma, since we
do not yet have a paper proof of the statement. It may be the case that we need to
strengthen our definition of no-op for this conjecture to hold.
Since all ancillae in a source symmetric circuit occur on sources, we can prove
from the statements above that source symmetric circuits are valid.
Theorem 10. If c is source symmetric, then all its assertions are valid.
Source symmetric circuits also satisfy a more general property: they are reversible.
The inverse of a source symmetric circuit is defined by induction on source sym-
metry:
Clearly, the inverse of any source symmetric circuit is also source symmetric, and the
inverse is involutive, meaning (c−1 )−1 = c.
Proof. By induction on the proof of source symmetry. The only interesting case is the
case for ancilla, showing
init_at b i ;; c−1 ;; assert_at b i ;; init_at b i ;; c ;; assert_at b i ≡
id_circ.
From Theorem 10 we know that the circuit init_at b i ;; c−1 ;; assert_at b i is valid.
Then, by Lemma 10, we know that init_at b i ;; c−1 ;; assert_at b i;; init_at b i
is equivalent to init_at b i ;; c−1 . Thus the goal reduces to init_at b i ;; c−1 ;; c ;;
assert_at b i. This is equivalent to the identity by the induction hypothesis plus the
fact that init_at b i ;; assert_at b i is the identity.
We can now say that any circuit followed by its inverse is valid. But this theorem
is easily extensible. For instance, we can add the following to our inductive definition
of symmetric, and the theorem will still hold:
103
This extension allows us to use existing (semantic) equivalences to satisfy our (syn-
tactic) source symmetry predicate, which in turn proves the semantic property of
validity. For example, because teleportation is semantically equivalent to the identity
circuit, we know trivially that it is valid, even though it is not source symmetric. The
Coq development provides many useful compiler optimizations in the file Equations.v
that can now be used in establishing source symmetry.
104
0 0
compile 0 0 compile
compile compile
b1 Γ b1 Γ
b2 Γ b2 Γ
105
apply a Toffoli gate from b1 and b2, now occupying the 1 and 2 positions in our list,
to the target qubit at 0. We then reapply the symmetric functions compile b2 Γ and
compile b1 Γ to their respective wires, returning the ancillae to their original states
and discarding them. We are left with the target wire z holding the boolean value
bz ⊕ (b1 ∧ b2 ) and |Γ| wires retaining their initial values.
Finally, we have the XOR case. Here we borrow a trick from ReVerC (Amy et al.,
2017) and allocate only a single ancilla instead of the two we used in the AND case.
Instead of calculating (b1 ⊕ b2 ) ⊕ t, where t is the target, we calculate the equivalent
b2 ⊕ (b1 ⊕ t), taking advantage of the associativity and commutativity of ⊕. Hence,
as soon as we’ve computed b1 , we can apply a CNOT from b1 to the target and
immediately uncompute b1 . This frees up our ancilla, which we then use as a target
for compile b2.
Note that our entire compile circuit is source symmetric, and therefore our asser-
tions are guaranteed to hold by Theorem 10.
We can now go about proving the correctness of this compilation.
Theorem compile_correct : ∀ (b : bexp) (Γ : Ctx) (f : Var → B) (z : B),
vars b ⊆ domain Γ →
Jcompile b ΓK (bool_to_matrix t ⊗ basis_state Γ f) =
bool_to_matrix (z ⊕ JbKf ) ⊗ basis_state Γ f.
The function basis_state takes the wires referenced by Γ and the assignments of
f and produces the corresponding basis state. This forms the input to the compiled
boolean expression along with the target, a classical qubit in the ∣0⟩ or ∣1⟩ state. The
statement of compile’s correctness says that when we apply Jcompile b ΓK to this basis
state with an additional target qubit, we obtain the same matrix with the result of
the boolean expression on the target. The proof follows by induction on the boolean
expression.
106
Definition adder_sum : Box (4 ⊗ Qubit) (4 ⊗ Qubit) :=
compile ((c_in ∧ (x ⊕ y)) ⊕ (x ∧ y)) (list_of_Qubits 4).
Definition adder_carry : Box (5 ⊗ Qubit) (5 ⊗ Qubit) :=
compile (x ⊕ y ⊕ c_in) (list_of_Qubits 5).
Definition adder_1 : Box (5 ⊗ Qubit) (5 ⊗ Qubit) :=
adder_carry ;; (id_circ ∥ adder_sum).
Here, adder_sum computes the sum of its three input bits and adder_carry computes
the carry, ignoring the result of adder_sum. Semantically, the adder should produce the
appropriate boolean values; the operation bools_to_matrix converts a list of booleans
to a density matrix.
Lemma adder_1_spec : ∀ (cin x y sum cout : B),
Jadder_1K (bools_to_matrix [cout; sum; y; x; cin])
= (bools_to_matrix [ cout ⊕ (c_in ∧ (x ⊕ y) ⊕ (x ∧ y));
; sum ⊕ (x ⊕ y ⊕ c_in)
; y; x; cin]).
Next, we extend the 1-qubit adder to n qubits. The n-qubit adder contains two
parts—adder_left and adder_right—defined recursively using padded adder_1 and
adder_carry circuits. The left part computes the sum and carry sequentially from the
least significant bit, initializing an ancilla for the carry in each step. When it reaches
the most significant bit, it computes the most significant bit of the sum and carry-
out using the 1-qubit adder. The right part of the adder uncomputes the carries and
discards the ancillae. The definitions of the circuits are shown below and illustrated
in Figure 8.5.
Fixpoint adder_left (n : N) : Box ((1+3*n) ⊗ Qubit) ((1+4*n) ⊗ Qubit) :=
match n with
| S n' ⇒ (id_circ ∥ (id_circ ∥ (id_circ ∥ (adder_left n')))) ;;
(init_at false (4*n) 0) ;;
(adder_1_pad (4*n'))
end.
Fixpoint adder_right (n : N) : Box ((1+4*n) ⊗ Qubit) ((1+3*n) ⊗ Qubit) :=
match n with
| O ⇒ id_circ
| S n' ⇒ (adder_carry_pad (4*n')) ;;
(assert_at false (4*n) 0) ;;
(id_circ ∥ (id_circ ∥ (id_circ ∥ (adder_right n'))))
end.
Fixpoint adder_circ (n : N) : Box ((2+3*n) ⊗ Qubit) ((2+3*n) ⊗ Qubit) :=
match n with
| O ⇒ id_circ
| S n' ⇒ (id_circ ∥ (id_circ ∥ (id_circ ∥ (id_circ ∥ (adder_left n')))));;
(adder_1_pad (4*n')) ;;
(id_circ ∥ (id_circ ∥ (id_circ ∥ (id_circ ∥ (adder_right n')))))
end.
107
cin cin
x1∶n′ x1∶n′
y1∶n′ adder_left n′ adder_right n′ y1∶n′
sum 1∶n′ sum ′ 1∶n′
xn xn
yn adder_1 yn
sum n sum ′ n
cout c′out
Figure 8.5: A quantum circuit for the n-adder where n′ = n−1 . The n′ ancillae created
in adder_left are all terminated inside adder_right.
108
adder in our boolean expression language and then compile that to a circuit. In order
to accomplish this, we would need to add the following features to our bexp language:
We could also make our bexps dependently typed, which would allow us to associate
bexps with the number of wires entering and exiting the corresponding circuit. We
could even include types for n-bit numbers that correspond to product types. And
naturally, there is much more that we could do with the bexp language, including
adding lambdas, branching, recursion, and other common programming language id-
ioms.
We would also like to optimize our current compiler. Our compile function borrows
a trick from ReVerC (Amy et al., 2017), in that it doesn’t use additional ancilla to
compile exclusive-ors. However, there is a lot of optimization that could potentially
be done, and, given the limitations of today’s quantum computers, it is all worth
doing.
Finally, a recent innovation in the area of quantum computing concerns so-called
dirty ancillae. We call an ancilla “dirty” if it may be initialized in an arbitrary state,
not only ∣0⟩. Häner et al. (2016) show that these can take the place of our “clean”
ancillae in many quantum circuits, and Q# (Svore et al., 2018) allows us to assert that
a qubit has been returned to its initial state, whatever that state may be. Extending
the work in this paper to verify that dirty ancillae are returned to their initial states
would require substantial additional machinery, however we believe that the payoff
in terms of programming and verification justifies the added effort.
109
Chapter 9
Automation
The entire Qwire language makes heavy use of Coq automation tools, particularly
its LTac tactic language and its hint databases. In this chapter, we will look at some
of the more interesting automation in Qwire, with a particular focus on typechecking
and verification.
110
Γ0,Γ3,Γ4 ⊢ (p0,p3,p4)
Γ1,Γ2 ⊢ (p1,p2) Γ0,Γ3,Γ4 ⊢ output (p0,p3,p4)
Γ1,Γ2,Γ0 ⊢ gate (p3,p4) ← CNOT (p1,p2); output (p0,p3,p4)
Figure 9.1: The typing derivation for a simple Qwire program that applies a CNOT
to the last two qubits in a 3-qubit system. We haven’t expanded out the proofs for
typing patterns since they’re trivial.
111
second context that would type the rest of the circuit. We also had to call a tactic,
solve_merge, to discharge an obligation of the form Γ1 ⋓ Γ2 == Γ1 ● Γ2 . In this case,
the solution was easy: split gives us the goals Γ1 ⋓ Γ2 = Γ1 ⋓ Γ2 , which is trivial,
and is_valid (Γ1 ⋓ Γ2 ), which follows from our hypothesis V : is_valid (Γ0 ⋓ Γ1 ⋓
Γ2 ). But this won’t always be so easy, as we will see later.
We now have two goals, corresponding to the second row in Figure 4.2. In that
derivation, the solution to the first ((Γ1 ⋓ Γ2 ) ⊢ (p1,,p2)) was simple enough that we
didn’t bother writing it; in Coq, it requires another explicit application and call to
solve_merge:
apply types_pair with (Γ1 := Γ1 ) (Γ2 := Γ2 ); try solve_merge.
The cases that follow from that actually are trivial for Coq to solve: They consist of
applying our hypotheses TP1 and TP2.
Let’s now take a look at our remaining goal, corresponding to the continuation:
∀ (Γ Γ' : OCtx) (p : Pat (Qubit ⊗ Qubit)),
Γ' == Γ ● Γ0 → Γ ⊢ p :Pat →
Γ' ⊢ (let (p3,p4) ← p; (output (p0,, p3,, p4))) :Circ
Once again, destructing the typing judgment gives us more useful patterns and
contexts:
Γ' ⊢ output (p0,, p3,, p4) :Circ
with Γ' = Γ3 ⋓ Γ4 ⋓ Γ0 and proofs that each Γi types pi in the context.
We can now apply types_output and solve for the remaining patterns. The full
proof is given in Figure 9.2.
Unfortunately, this proof isn’t quite automatic. At several points, we stopped and
manually specified contexts based on our knowledge of how the final proof should look.
On the other hand, this process should be automatic because the typing derivation
is syntax directed. As we see in Figure 9.1., we can fill in this derivation by blindly
applying the appropriate rules from bottom to top, leaving the typing contexts out.
The only challenge, then, is in finding the correct contexts. We can obtain these from
the leaves of the typing derivation, then percolate the typing contexts downwards.
In order to mechanize this strategy, we use Coq’s evars, or existential variables.
An evar acts like a placeholder whose value we can fill in later.2 Using evars, we can
leave some context unspecified until we determine their values at the leaves of the
typing derivation.
We can now present a “more automatic” version of our typing derivation in Fig-
ure 9.3.
Let’s walk through this proof. The first change from the previous proof is that our
call to intros doesn’t specify any names for our variables, instead letting Coq name
2
Naturally, this is subject to restrictions. An evar can only be unified with a value that was
in scope at the time it was created. Otherwise, we could use them to prove false statements, like
∃ x, ∀ y, x = y, by replacing x with an evar, introducing y, and then unifying x with y.
112
Lemma cnot12_WT_manual : Typed_Box cnot12.
Proof.
unfold Typed_Box, cnot12.
intros Γ p TP. simpl.
dependent destruction TP.
dependent destruction TP1.
(* Give contexts and patterns the correct names *)
rename Γ0 into Γ, Γ1 into Γ0 . rename Γ into Γ1 .
rename p3 into p1.
rename TP1_1 into TP0, TP1_2 into TP1.
(* Apply gate typing rule *)
apply @types_gate with (Γ := Γ0 ) (Γ1 := Γ1 ⋓ Γ2 ); try solve_merge.
- (* types (p1,p2) *)
apply types_pair with (Γ1 := Γ1 ) (Γ2 := Γ2 ); try solve_merge.
+ apply TP1. (* types p1 *)
+ apply TP2. (* types p2 *)
- (* types `output (p0, p3, p4)` *)
intros Γ Γ' p M TP.
dependent destruction TP.
apply (@types_output _ _ _ _ eq_refl).
(* types (p0, p3, p4) *)
apply types_pair with (Γ1 := Γ0 ⋓ Γ3 ) (Γ2 := Γ4 ); try solve_merge.
+ (* types (p0, p3) *)
apply types_pair with (Γ1 := Γ0 ) (Γ2 := Γ3 ); try solve_merge.
* apply TP0. (* types p0 *)
* apply TP3. (* types p3 *)
+ apply TP4. (* types p4 *)
Qed.
113
Lemma cnot12_WT_evars : Typed_Box cnot12.
Proof.
unfold Typed_Box, cnot12.
intros; simpl.
invert_patterns.
eapply types_gate.
Focus 1.
eapply @types_pair. (* types (p1, p2) *)
4: eauto. (* types p2 *)
3: eauto. (* types p1 *)
2: monoid. (* unifies ?Γ = Γ1 ⋓ Γ2 *)
1: validate. (* solves is_valid (Γ1 ⋓ Γ2 ) *)
Focus 2. (* 3 *)
split. (* _ == _ ● _ *)
2: monoid. (* unifies Γ0 ⋓ Γ1 ⋓ Γ2 = Γ1 ⋓ Γ2 ⋓ ?Γ *)
1: validate. (* solves `is_valid (Γ0 ⋓ Γ1 ⋓ Γ2 )` *)
Focus 1. (* 2 *)
intros; simpl.
invert_patterns.
eapply @types_output.
Focus 1.
monoid.
Focus 1. (* 2 *)
destruct_merges; subst.
eapply @types_pair.
Focus 4.
eauto. (* types p4 *)
Focus 3.
eapply @types_pair. (* types (p0,p3) *)
4: eauto. (* types p3 *)
3: eauto. (* types p0 *)
2: monoid. (* unifies ?Γ = Γ0 ⋓ Γ3 *)
1: validate. (* solves `is_valid (Γ1 ⋓ Γ2 )` *)
Focus 2.
monoid. (* unifies Γ3 ⋓ Γ4 ⋓ Γ0 = Γ0 ⋓ Γ3 ⋓ Γ4 *)
Focus 1.
validate. (* solves `is_valid (Γ1 ⋓ Γ2 )` *)
Qed.
114
them itself. This is because we don’t want to refer to any specific terms or hypotheses
in our proof, since it should be fully automatable. The next line calls invert_patterns.
This corresponds to the dependent destructions in our manual proof, breaking down
complex patterns into bits, qubits, and units, and simultaneously breaking down the
contexts that type them. We can now apply our first typing rule.
Where previously we called apply types_gate and specified values for Γ1 and Γ2 ,
here we simply call eapply types_gate. This applies the same rule, but instead of
using our specified values for Γ1 and Γ2 , it leaves them as evars to be filled in later.
We are left with the following three goals to prove (we have replaced Coq’s generated
names with our own, for readability):
subgoal 1 (ID 1463) is:
?Γ1 ⊢ (p1,,p2) :Pat
115
Γ' ⊢ (let p3 p4 ← p; (output (p0,, p3,, p4))) :Circ
We do this in exactly the same way that we typechecked the broader circuit. The
only addition is a call to destruct_merges, which replaces any Γ == Γ1 ● Γ2 in the
hypotheses with Γ = Γ1 ⋓ Γ2 and is_valid Γ, followed by subst, which replaces all
instances of Γ with Γ1 ⋓ Γ2 .
We can now present the core of our typecheck tactic:
2. intros hypotheses
3. invert_patterns
4. destruct_merges
Note that step (a) must precede (b), which in turn must precede (c) and (d). We
need to typecheck patterns to infer the values of any evars and then use monoid to
instantiate whatever evars remain. We can now present our final proof that cnot12
is well-typed:
Lemma cnot23_WT : Typed_Box cnot12.
Proof.
type_check.
Qed.
Our type_check tactic has some additional functionality not captured by the al-
gorithm above. Since our circuits are highly modular and often included in larger
circuits, we generally want to reuse proofs of typing judgments wherever possible. In
particular, if we compose two circuits together, we should not compute the result in
order to type them; rather, we should use our compose_typing lemma (corresponding
to TypeCircGate in Figure 4.2) and then typecheck the component circuits sepa-
rately. Moreover, if these circuits already have typing proofs, we should apply those
directly. In order to facilitate this practice, we maintain a Coq Hints database, called
typed_db. Whenever a new circuit is typechecked, we can add its proof to typed_db.
Our typechecking tactics always calls out to typed_db before attempting to typecheck
a circuit, speeding up the typechecking process. The typing proofs for higher-order
116
functions on circuits, like inPar and inSeq (which compose circuit in parallel and in
sequence), are also added to the database.
We next discuss monoid and validate, which lie at the heart of our typechecking
procedure.
9.1.1 Monoid
Partial Commutative Monoids The structure that underlies the monoid tactic
is called a partial commutative monoid, or PCM for short. Partiality refers to the
fact that some operations may lead to an invalid result, called . To be precise, our
structure is
{A, ⊺, , ○}
for some set A, obeying the following properties:
a○⊺=a
a○=
(a ○ b) ○ c = a ○ (b ○ c)
a○b=b○a
A PCM Solver Our monoid tactic is based upon the tactic of the same name in
Adam Chlipala’s “Certified Programming with Dependent Types” (Chlipala, 2013)
for solving monoidal equalities using reflection. A similar approach is taken by Coq’s
built-in tactics ring and field for solving ring and field equalities. First, an Ltac
reifies an expression as a list of base variables, ignoring identity elements ⊺, flattening
out the associativity of ○, and collapsing the expression to if occurs anywhere in
the expression:
3
https://github.com/inQWIRE/LinearTypingContexts
117
Ltac reify a :=
match a with
| ⊺ ⇒ constr:(Some [])
| ⇒ constr:(None)
| ?a1 ○ ?a2 ⇒ let e1 := reify a1 in
let e2 := reify a2 in
match e1, e2 with
| Some ls1, Some ls2 ⇒ constr:(Some (ls1 ++ ls2))
| _, _ ⇒ constr:(None)
end
| _ ⇒ constr:(Some [a])
end.
A goal a1 = a2 can then be exchanged with one of the form from_list ls1 =
from_list ls2, where lsi is the result of calling reify on ai. We can then check if
ls1 and ls2 are permutations of one another and, if so, apply a lemma to solve the
goal.
Our extensions to monoid add commutativity (by looking for permutations rather
than simple equality) and also allow us to unify expressions that contain a single evar.
We limit this to one evar, since multiple evars admit multiple solutions, just like an
additive equation of the form a + x = b + y admits infinite possible values for x and y.
(If x and y were on the same side of the equals sign and constrained to be natural
numbers, there would be a finite number of solutions, and the same is true for our
OCtxs. Unfortunately for our purposes, most finite numbers are not 1.)
Conveniently, our typechecking algorithm above always instantiates all but one
evar before calling monoid.
9.1.2 Validate
Our validate tactic solve goals of the form is_valid Γ, where Γ may be the merger
of many contexts, thereby showing that Γ is not Invalid and can type a circuit. The
validate tactic makes use of a simple observation: Γ1 ⋓ Γ2 ⋓ Γ3 is valid if and only if
Γ1 ⋓ Γ2 , Γ2 ⋓ Γ3 , and Γ1 ⋓ Γ3 are valid. Hence, checking validity amounts to checking
pairwise disjointness.
The validate tactics first rewrites in the premises to find the largest expressions
such that Γ1 ⋓ ... ⋓ Γn is valid. For instance, if it finds a hypothesis H : Γ = Γ1 ⋓ Γ2 ,
and Γ appears in some larger merge expression, it will replace all instances of Γ with Γ1
⋓ Γ2 and clear H. It then breaks down our large merge expressions into pairwise claims
of validity. Once Coq’s hypothesis context is saturated with expressions of validity,
we similarly replace the goal with pairwise claims of validity. If we can unify these
goals with our existing hypotheses, we’ve proven validity. If not, it’s impossible to
show validity since no more information about our abstract contexts can be gathered.
This concludes our discussion of Qwire’s linear typechecker.
118
9.2 Arithmetic
As noted in Section 5.4, we use the Coquelicot (Boldo et al., 2015) extension of the
Coq reals to complex numbers to populate our matrices. This is mainly to make use
of Coq’s built-in tactics for solving real number equalities, particularly the linear real
arithmetic tactic lra. We define an equivalent function for complex numbers called
clra4 that breaks a complex equality c = c' into its real components, fst c = fst c'
and snd c = snd c', and then solves each using lra:
Ltac clra := eapply c_proj_eq; simpl; lra.
Here c_proj_eq says that if the first and second projections are equal, so are the pairs
that make up the complex numbers.
Note that clra, like lra, is what the Mathematical Components library (Mahboubi
et al., 2016) calls a terminating tactic: It either solves the goal or fails without making
progress. We will also need tactics that simplify the goal state without solving it. The
most straightforward of these is Csimpl, which rewrites using the basic additive and
multiplicative identities for 0 and 1 and replaces c∗ (our notation for the complex
conjugate) with c when the imaginary part is 0. This lightweight technique proves
particularly valuable for dealing with the products of sparse matrices, since their
elements contain many sub-expressions of the form A x y ∗ 0 and 0∗ ∗ B x y.
Coq has little automation support for √ two kinds of formulae that appear frequently
in our development: equations involving 2 and equations involving natural number
powers of 2. The first appear whenever we apply the Hadamard matrix, which, you
may recall, has the form
1 1 1
√ ( ).
2 1 −1
√
Our group_radicals tactic groups together all of the 2 terms in our formula and
simplifies what it can. This often results in a substantially more manageable goal
state.
The other expression, 2n for natural numbers 2 and n, is even more common in
our development. To understand why, recall that an n-qubit system corresponds to
a density matrix with dimensions 2n × 2n . When we take the Kronecker product of
an m × n and o × p matrix, we get an mo × np matrix as the result. Hence, in the
case of m- and n-qubit systems, we should obtain a matrix of height 2m ∗ 2n or 2m+n .
Since multiplying A and B requires that the second dimension of A should match
the first dimension of B, we need to reduce these dimensions to a normal form. Our
unify_pows_two does exactly this through a series of rewriting rules.
Both clra and Csimpl are simple, unextensible tactics, so we also provide the
user with C_db, a hints database of complex number equalities. C_db is a rewriting
database, meaning that it is used to simplify the goal rather than to solve it. The
4
Technically, this should be lca for “linear complex arithmetic,” but clra makes the connection
to lra clear, as will our mlra tactic for matrices
119
idiom
autorewrite with C_db; clra is pretty common in the Qwire development.
Pure and Mixed States For quantum computation, it is often important to know
that we are working with pure or mixed states (discussed in Section 6.1.3). We provide
tactics show_pure and show_mixed to establish that a matrix possesses the desired
property, with show_mixed including show_pure as a subroutine (since all pure states
are mixed states). These mostly exploit existing lemmas about applying operations
to pure states, though they often need to first show that dimensions line up. This can
be accomplished using the dim_solve and unify_dim_solve tactics.
Lightweight Equalities For simple matrix equalities, we provide the tactic mlra,
for matrix linear real arithmetic. The tactic begins by unfolding matrix definitions
using the unfolding database M_db. It then applies functional_extensionality twice
120
and destructs the results using destruct_m_eq, allowing it to compare matrices at the
element level. Hence, the goal
a a b b
( 0,0 01 ) = ( 0,0 01 )
a1,0 a11 b1,0 b11
becomes
a a b b
∀x, ∀y, ( 0,0 01 ) (x, y) = ( 0,0 01 ) (x, y)
a1,0 a11 b1,0 b11
which becomes the four goals
along with a small number of “0 = 0” goals (due to the construction of our matrices),
which are immediately discharged by reflexivity. Our mlra tactic then solves the
four goals using our favorite tool for complex number equalities, clra.
Msimpl is the matrix counterpart to Csimpl. Unlike Csimpl, Msimpl has extensi-
bility built in via the M_db rewriting database. (Coq allows us to use the same name
for unfolding and rewriting databases.) Msimpl contains some additional code for
rewriting expressions involving the Kronecker product or controlled matrices, since
autorewrite can often struggle to unify these terms due to difficulty matching on the
matrix dimensions. Otherwise, however, it behavess much like our other simplification
tactics, in that it only uses simple equalities to rewrite a goal into a more manageable
state.
A×B×C
121
time of m ∗ o ∗ n. The resulting matrix has dimensions m × o, so multiplying it by
C takes an additional m ∗ p ∗ o steps, for a total of mon + mpo = mo(n + p). By
contrast, if we started with the right-most matrices, it would take np(m + o) time.
Imagining that m = o = 32 and n = p = 8, the first approach takes 214 steps, and the
second takes 212 . And these effects compound as we multiply more matrices. Hence,
we take an approach where, if m or o is the smallest of the four numbers, we associate
left; otherwise, we associate right. (We could compute mo(n + p) vs. np(m + o) in
the tactic language, but this turns out to be a good and cheap proxy.) The tactic
assoc_least reassociates at all levels of a complex matrix expression, though we will
begin computing with the innermost matrices.
Once we’ve identified the matrices A and B that we want to multiply first, how
do we multiply them together while ignoring the rest of the equation? We found that
the easiest approach is simply to construct an appropriately-sized matrix E full of
evars and then to replace A × B with E. This allows us to focus on the separate goal
of computing E and to simplify A × B as much as possible before unifying it with E.
This work is all done by the reduce_aux tactic:
Ltac reduce_aux M :=
match M with
| ?A .+ ?B ⇒ compound A; reduce_aux A
| ?A .+ ?B ⇒ compound B; reduce_aux B
| ?A × ?B ⇒ compound A; reduce_aux A
| ?A × ?B ⇒ compound B; reduce_aux B
| @Mmult ?m ?n ?o ?A ?B ⇒ let E := evar_matrix m o in
replace M with E;
[| crunch_matrix ]
| @Mplus ?m ?n ?A ?B ⇒ let E := evar_matrix m n in
replace M with E;
[| crunch_matrix ]
end.
The compound A tactic simply checks that A consists of the sum or matrix product
of two matrices, in which case reduce_aux is recursively called on A. Otherwise, if
reduce_aux is called on two irreducible matrices, it constructs a matrix full of evars
using evar_matrix. Note that in this case, the match clause expands ?A × ?B to @Mmult
?m ?n ?o ?A ?B. This gives us the dimensions of the matrices and, therefore, of the
desired evar matrix. Finally, we call another tactic to unify ?A × ?B with E.
The crunch_matrix tactic handles unification. It works much like mlra, except that
when called as a subroutine of reduce_matrices and solve_matrix, it’s guaranteed to
work because we can unify any expression with an evar. Hence, it mostly has to make
decisions regarding the degree of simplification required before unification. In practice,
we only use simpl and Csimpl on the elements of the matrix, as heavy rewriting would
dramatically slow down the tactic. The goal is solved by try reflexivity: The try is
there so that crunch_matrix makes progress even if one side doesn’t consist of evars.
This basically describes the full process of reduce_matrices. It looks for matrices
122
in the goal and calls assoc_least and reduce_matrix_aux on them. It keeps calling
reduce_matrix_aux until no more matrices can be combined. Note that throughout
this process, the relevant operations are matrix multiplication and addition. The
Kronecker product and transpose are both easy enough to compute using our repre-
sentation that (A ⊗ B)† is treated like an irreducible matrix in this process.
The solve_matrix tactic is essentially reduce_matrices with an extra step. Once
it has reduced both sides of a matrix equality to atomic matrices, it makes a final call
to solve_matrix. This tactic will rarely discharge the m ∗ n goals produced, as it only
does basic simplifications and try reflexivity. Our solve_matrix will then attempt
to unify the complex number equalities by rewriting with C_db and calling try clra.
If clra fails to discharge all of the goals, they will be left for the user to complete (or,
frequently, to revise their theorem).
123
Tactic Effect
General Use Tactics
bdestruct t Destructs a boolean relation on natural numbers t and
inserts the corresponding propositional relation into the
context (from Appel (2018))
bdestructΩ t Calls bdestruct t then tries to solve the goal with omega
simpl_rewrite H Simplifies H and uses it to rewrite in the goal
simpl_rewrite' H Like simpl_rewrite H but for rewriting right-to-left
unify_pows_two Simplifies natural number expressions involving powers
of two
Real and Complex Number Arithmetic
clra Linear real arithmetic (lra) extended to complex num-
bers
nonzero Solves goals of the form c ≠ 0 (for complex c)
group_radicals Simplifies real and complex expressions involving
square roots of two
Rsimpl Simplifies real expressions
Csimpl Simplifies complex expressions
Rsolve Terminating tactic calling Rsimpl and group_radicals
Csolve Terminating tactic calling Rsolvea
Matrix Tactics
prep_matrix_equality Applies functional_extensionality twice to show ma-
trix equality
show_wf Manually shows that a matrix is well-formed
show_pure Shows that a matrix corresponds to a pure state
show_mixed Shows that a matrix corresponds to a pure state
dim_solve Shows that the dimensions of two matrices are equal
unify_dim_solve Solves equations of the form A ⊗ B = A ⊗ B where the
implicit dimensions are different
Msimpl Uses matrix equalities to simplify matrix expressions
destruct_m_eq Repeatedly destructs natural numbers in match state-
ments
mlra Uses destruct_m_eq to replace a matrix equality with
m ∗ n complex number equalities; attempts to solve
these using clra
124
Tactic Effect
evar_matrix m n Creates an m × n matrix of evars
assoc_least Reassociates matrices so that the smallest dimensions
are multiplied first
crunch_matrix Attempts to unify all the elements in two matrices
reduce_matrix Does a single reduction of A × B or A + B, where A and
B are irreducible matrices in the goal
reduce_matrices Reduces all of the matrices in the goal
solve_matrix Solves matrix equalities using assoc_least,
reduce_matrices and crunch_matrix
Typechecking
invert_patterns Reduces all patterns in the hypotheses to bit v, qubit v
or unit
monoid Solves monoidal equalities with at most one evar
validate Shows that a context is valid
solve_merge Solves goals of the form Γ == Γ1 ⋅ Γ2 using monoid and
validate
simple_typing Typechecks a circuit using only existing lemmas
type_check_once A single iteration of the typechecking tactic
type_check Typechecks all of the goals until they are solved
Circuit Denotation
matrix_denote Turns a circuit without into its vector denotation via
unfolding and simplification
vector_denote Turns a unitary circuit without measurement into its
vector denotation
case_safe Replaces the denotation of an ancilla-free circuit with
its “safe” denotation
case_unsafe Replaces the denotation of an ancilla-free circuit with
its “safe” denotation
rewrite_inPar Rewrites using the admitted fact inPar_correct
compose_denotations Rewrites using the admitted fact denote_compose
Database Description
R_db Real number rewriting
125
C_db Complex number rewriting
C_db_light Lightweight complex rewriting
Cdist_db Normalizing complex expressions
M_db Matrix rewriting
proof_db Circuit denotation rewriting
monad_db Monad unfolding
M_db Matrix unfolding
den_db Circuit denotation unfolding
vector_den_db Circuit denotation unfolding (vector representation)
wf_db Matrix well-formedness proofs
typed_db Typing proofs
126
Chapter 10
The concept of literate programming (Knuth, 1984; Ramsey, 1994) has gained wide
currency among the formal verification community. A literate program consists of a
program and its exposition interleaved in a single file, allowing for clearer code and
readable documentation. The popular “Software Foundations” series (Pierce et al.,
2018; Appel, 2018) and “Certified Programming with Dependent Types” (Chlipala,
2013) are both literate programs written in Coq, typeset using Coq’s literate pro-
gramming utility, Coqdoc. One could easily argue that this dissertation ought to be
a literate program: It describes a tool, Qwire, that is written entirely inside the Coq
proof assistant. Another argument would suggest that this is not a dissertation: It is
a pointer to a dissertation hosted on Github. Constrained as we are by formatting
requirements, we have provided a text that conveys the ideas of Qwire. However,
this is not enough.
In this chapter, we focus on the details of Qwire. We describe the development
itself in terms of its structure, the files that make up the structure, and the definitions
and lemmas that give it substance. We also discuss the assumptions that underlie the
Qwire development.
• 25 Coq files,
• 557 definitions,
127
File LOC Definitions Fixpoints Inductives Ltacs
Prelim.v 397 3 8 0 7
Monad.v 409 28 4 0 4
Monoid.v 641 1 8 1 21
Complex.v 677 16 1 0 7
Matrix.v 1484 25 5 0 23
Quantum.v 1261 41 5 1 1
Contexts.v 1639 14 14 12 10
HOASCircuits.v 113 3 1 3 0
TypeChecking.v 415 3 2 0 6
DBCircuits.v 503 14 11 3 0
Denotation.v 4380 35 13 4 3
HOASLib.v 302 20 6 0 0
SemanticLib.v 110 0 0 0 0
HOASExamples.v 510 37 7 0 0
Composition.v 200 0 0 0 0
Ancilla.v 416 4 0 3 2
Symmetric.v 1536 25 3 2 1
Oracles.v 1376 1 18 2 14
Deutsch.v 232 2 0 0 3
Equations.v 458 20 0 0 0
HOASProofs.v 772 19 1 0 2
Arithmetic.v 1677 27 13 0 1
QASM.v 499 17 10 10 0
QASMPrinter.v 142 10 9 0 0
QASMExamples.v 93 12 0 0 1
Totals 20242 377 139 41 106
Table 10.1: A brief summary of the Qwire Coq development.
128
In definitions, we include code beginning with Definition, Fixpoint, or Inductive.
By theorems and lemmas, we only mean Coq propositions that begin with Theorem
or Lemma and end with Qed or Defined. We will delve into detail about our theorems
and lemmas, as well as other kinds of statements, in the next section. We provide a
fuller account of the Qwire development in Table 10.1 and Table 10.2.
We can break down the twenty-four Coq files as follows1 :
• Preliminaries
129
• Compositionality (Section 6.2)
We have annotated the divisions with the chapters that focus on them, where ap-
propriate, though this characterization is fairly broad. Typechecking.v, for instance,
is covered in substantial detail in Chapter 9, as is Monoid.v. We have also excluded
some experimental files, including Dong-Ho Lee’s files for generating well-typed cir-
cuits, Generator.v and DBGenerator.v (see Section 11.2). We have included Lee’s
compiler to QASM, though it is not our own work, which will also appear in Sec-
tion 11.2.
130
File Lemmas Theorems Facts Propositions Examples
Prelim.v 32 0 0 0 0
Monad.v 3 0 0 1 0
Monoid.v 18 0 0 0 10
Complex.v 84 0 0 0 0
Matrix.v 91 5 0 1 1
Quantum.v 84 0 0 2 2
Contexts.v 72 0 0 0 0
HOASCircuits.v 2 0 0 0 0
TypeChecking.v 4 0 0 0 1
DBCircuits.v 17 0 0 1 0
Denotation.v 113 2 2 19 0
HOASLib.v 22 0 0 0 0
SemanticLib.v 14 0 0 0 0
HOASExamples.v 38 0 0 4 1
Composition.v 1 1 2 0 0
Ancilla.v 8 0 2 2 0
Symmetric.v 45 3 18 1 0
Oracles.v 35 1 2 3 1
Deutsch.v 5 0 0 0 1
Equations.v 26 0 0 3 0
HOASProofs.v 22 0 0 8 2
Arithmetic.v 38 0 0 1 32
QASM.v 0 0 0 0 1
QASMPrinter.v 0 0 0 0 0
QASMExamples.v 0 0 0 0 2
Totals 774 12 26 46 54
Table 10.2: A summary of the different kinds of statements in the Qwire development.
131
of a square matrix is also its left inverse and kron_assoc says that the Kronecker
product is associative. Proving these lemmas requires a substantial amount of linear
algebra that we haven’t yet formalized. Similarly, we have axiomatized the operator
sum decomposition theorem,
Axiom operator_sum_decomposition : ∀ {m n} (l : list (Matrix m n)),
outer_sum l = 'I_n ↔ WF_Superoperator (operator_sum l).
whose proof requires more concepts from linear algebra than we were able to provide.
See Section 6.1.4 for details.
Beyond these, we have a number statements beginning with Fact, to emphasize
that these were admitted. All of these are used exclusively in the files on reversibil-
ity, plus Deutsch.v which depends on compositionality axioms and isn’t discussed in
this dissertation. We refer the reader to Table 8.1 for an synopsis of the admitted
statements.
Finally, we include a number of conjectures, which begin with Proposition2 , and
correspond to aborted claims that we would like to prove in the future.
We give a summary of the claims in Qwire in Table 10.2. A complete list of
theorems, lemmas, and facts in the Qwire development is provided in Appendix C.
2
Conjecture is unfortunately used by Coq as a synonym for Axiom.
132
Chapter 11
The arguably grandiose title of this dissertation is “Formally Verified Quantum Pro-
gramming”. Despite substantial recent interest, this area of research is in its infancy.
In Chapter 1, we made an bold claim: Quantum programming demands formal verifi-
cation, and therefore quantum programming languages must have well-defined seman-
tics and support for verification. This thesis, along with the broader Qwire project
and the work that inspired it, only begins to tackle this issue. In this chapter, we will
discuss the issues Qwire still needs to address in order to serve both as a real-world
quantum programming language and a robust, user-friendly verification tool.
This chapter will also seek to address a more interesting question, and hopefully
one that excites the reader. What else can Qwire do? To be precise, what challenges
does quantum computing face, in both the short term and the long term, and how
can Qwire help address those challenges? In this thesis, we have depicted quantum
computing as an exciting new technology that lies somewhere along the horizon.
But as John Preskill pointed out in a recent survey (Preskill, 2018), we should be
looking at multiple horizons, the first of which (Noisy Intermediate-Scale Quantum
Computing, or NISQ) is years, not decades, away. We will try to address how Qwire
and formal verification can help us run the quantum programs of tomorrow, not just
those of the far future.
133
quelicot’s C is simply a pair of Coq Rs. Coq’s real numbers, in turn, are axiomatized:
0, 1, +, −, ∗, ∖ and < are simply declared as Coq parameters; they have no computa-
tional content. Likewise, the associativity, commutativity, and distributivity of + and
∗ are declared as axioms, as are the remaining field laws.
From a computational standpoint, this is awful. It is never possible to reduce real
number expressions using call-by-value or call-by-name reduction rules, because no
definitions exist to reduce. In Coq’s defense, this limitation is inherent to the real
numbers: e + π cannot normalize to anything but e + π. The exact nature of our proofs
prohibit using floating point numbers instead of reals, though once we account for
error terms (see the next section), we may be able to loosen this restriction.
How can we improve Qwire’s real number library to allow for computation?
Potentially, we could restrict ourselves to the algebraic numbers. Right now, only one
of our unitary gates, the Rθ = ( 10 e0iθ ) gate, allows us to multiply our states by non-
algebraic
√ numbers, and we typically instantiate θ with π/n for an integer n, yielding
n
−1. We could then compute by grouping like terms. It’s not clear how difficult this
would be to implement, and we are not aware of a library that does this.
The other bottleneck is our matrix library. which is quite slow. In fact, we have
trouble accounting for quite how slow it is, struggling to multiply even 16 × 16 di-
mensional matrices. In our QPL paper, we suggested adopting the Mathematical
Components library’s matrices (Mahboubi et al., 2016) for proofs, while reflecting
into the Coq Effective Algebra library (Cano et al., 2016) for efficient computation.
This ultimately raised several obstacles.
The Mathematical Components library, written in the SSReflect proof language
and used in the formally verified proofs of the Four Color Theorem (Gonthier, 2008)
and Feit-Thompson Theorem (Gonthier et al., 2013), uses dependently typed ma-
trices. On the face of it, this is an excellent use-case for dependent types. Matrix
multiplication is only defined on two matrices of dimensions m × n and n × o, respec-
tively, and dependent types can enforce this property. Unfortunately, the Kronecker
product, which is integral to quantum computation, multiplies the dimensions of its
argument matrices. As soon as we start dealing with matrices of dimensions 2m and
2n , where neither m nor n is concrete, convincing the Coq typechecker that we are
indeed multiplying compatible matrices becomes exceedingly difficult. This motivated
our decision to use phantom types (Leijen and Meijer, 1999), lightweight types meant
to guide development that are not enforced by the typechecker, in our matrices. We
discussed this design choice in detail at the Fourth International Workshop on Coq
for Programming Languages (Rand et al., 2018b).
CoqEAL has a number of advantages in terms of efficiently computing with large
matrices, including an implementation of Strassen’s Algorithm (Strassen, 1969) for
efficient multiplication, but a number of drawbacks as well. For one, it is not designed
for proofs, but rather, for computation. That means we would have to convert some
other matrix representation to CoqEAL matrices and only use them in the final
stages of certain proofs involving concrete matrices. The current version of CoqEAL
134
also does not work with the Coq real numbers library and, hence, will not work with
our complex numbers. These challenges could probably be overcome, but doing so
would have limited payoff in the absence of the mathematical components library
and computational complex numbers.
135
Depth Gates Clean Qubits Total Qubits
Shor (1994) Θ(nM (n)) Θ(nM (n)) Θ(n) Θ(n)
Beckman et al. (1996) Θ(n3 ) Θ(n3 ) 5n + 1 5n + 1
Vedral et al. (1996) Θ(n3 ) Θ(n3 ) 4n + 3 4n + 3
Beauregard (2002) Θ(n3 lg 1ε ) Θ(n3 lg nε lg 1ε ) 2n + 3 2n + 3
Takahashi et al. (2006) Θ(n3 lg 1ε ) Θ(n3 lg nε lg 1ε ) 2n + 2 2n + 2
Zalka (2006) Θ(n3 lg 1ε ) Θ(n3 lg nε lg 1ε ) 1.5n + O(1) 1.5n + O(1)
Häner et al. (2016) Θ(n3 ) Θ(n3 lg n) 2n + 2 2n + 2
Gidney (2017) Θ(n3 ) Θ(n3 lg n) n+2 2n + 1
Table 11.1: Space-efficient constructions of Shor’s algorithm over time. M (n) is the
classical time-complexity of multiplication and ε is the maximum error when synthe-
sizing the circuit out of a fixed set of universal gates. Reproduced with permission
from Gidney (2017).
136
like to optimize these circuits subject to constraints. These constraints may take a
variety of forms, from limiting the available gate set to restricting the interactivity
of qubits. For instance, Kutin (2006) provides a version of Shor’s algorithm for a
computer on which only adjacent qubits may interact with one another. This will re-
quire us to develop a means of specifying constraints in Qwire and to prove that our
optimizations not only preserve a circuit semantics, but also satisfy these constraints.
Once we have optimized our circuits, we would like to extend Dong-Ho Lee’s
compiler to convert them to OpenQASM (Cross et al., 2017) or QUIL (Smith et al.,
2016). The translation should also be bidirectional: We should be able to convert
OpenQASM or QUIL programs to Qwire to typecheck, optimize, and verify them.
This would greatly increase the practical utility of Qwire in the short term.
137
exciting. In principle, Qwire should be able to verify a broad range of quantum
programs, from Shor (1994) and Grover’s (1996) algorithms to quantum random
walks (Aharonov et al., 2001; Childs et al., 2003) and quantum simulation of physical
systems (Georgescu et al., 2014).
One of the most interesting problems for Qwire is to verify quantum crypto-
graphic protocols. Unruh’s Quantum Relational Hoare Logic (2018) seeks to form
the foundation for a tool to verify quantum cryptographic protocols, modeled on the
EasyCrypt tool (Barthe et al., 2011, 2012) for non-quantum cryptography. While
such deductive systems are useful, they themselves often rest on weak foundations.
We could attempt to prove the security of a cryptographic protocol by programming it
in Qwire and proving it directly or, alternatively, by developing a logic and proving
it sound with respect to Qwire’s semantics. This would provide a strong foundation
for reasoning about quantum cryptographic systems.
In a field as young as quantum computing, we cannot predict what researchers
will want to verify next year, let alone once we have scalable quantum computers to
experiment with and program. But we do know that there is a great deal to verify. And
we are confident that Qwire and tools like it will play an increasingly important role
as this field develops and gives us new protocols to verify and challenges to overcome.
138
Appendix A
Solutions to Exercises
Solution. Let us first consider H applied to the basis states. We have already shown
that H(H ∣0⟩) = ∣0⟩. The proof that H(H ∣1⟩) = ∣1⟩ follows similarly:
1 1
H(H ∣1⟩) = H ( √ ∣0⟩ − √ ∣1⟩)
2 2
1 1
= √ H ∣0⟩ − √ H ∣1⟩
2 2
1 1 1 1 1 1
= √ ( √ ∣0⟩ + √ ∣1⟩) − √ ( √ ∣0⟩ − √ ∣1⟩)
2 2 2 2 2 2
1 1 1 1
= ∣0⟩ + ∣1⟩ − ∣0⟩ + ∣1⟩
2 2 2 2
1 1
= ∣1⟩ + ∣1⟩
2 2
= ∣1⟩
since unitaries distribute over superposition, H(H ∣0⟩) = ∣0⟩, and H(H ∣1⟩) = ∣1⟩. ∎
What if we want to measure one qubit in a multiple qubit system? Let ∑i αi ∣i⟩
represent the part of the state in which the qubit to be measured is ∣0⟩ and ∑j βj ∣j⟩
represent the part in which the qubit is ∣1⟩. Then the probability of measuring ∣0⟩ is
2
∑i ∣αi ∣ , returning the state
1
√ ∑ αi ∣i⟩
2 i
∣α
∑i i ∣
139
and similarly for ∣1⟩. The scaling factor on the left renormalizes the quantum state so
that the squares of the amplitudes still add up to 1.
Exercise 2. Now try measuring the second qubit in both of these cases. Verify that
the distribution of results is the same as if we had measured the whole system at
once.
Solution. Let us begin by simplifying the expression for the case where we measured
a ∣0⟩: √
3 1 2+i 1 2+i
( ∣00⟩ + ∣01⟩) = √ ∣00⟩ + √ ∣01⟩
2 3 3 6 6
2
The probability of measuring ∣00⟩ here is ∣ √16 ∣ = 1
6 and the probability of measuring
2
∣01⟩ is ∣ 2√+6i ∣ = 4+61 = 56 . We can scale these by the 32 probability of having measured
the first qubit as ∣0⟩ to get total probabilities of 19 and 95 , respectively.
In the case where we measured the first qubit as ∣1⟩, we are guaranteed to measure
∣11⟩ and so the total probability of measuring ∣11⟩ is 13 .
Now, if we had initially measured the entire state we would have gotten
⎧
⎪ ∣00⟩
2
with probability ∣ 13 ∣ = 1
⎪
⎪
⎪ 9
1 2+i 1 ⎪ 2
meas ( ∣00⟩ + ∣01⟩ + √ ∣11⟩) = ⎨∣01⟩ with probability ∣ 23+i ∣ = 5
3 3 3 ⎪
⎪
⎪ 2
9
⎪
⎪
⎩∣11⟩ with probability ∣ √13 ∣ = 1
3
as expected.
∎
Exercise 3. Verify that after measuring a qubit, the norm of the quantum state is
still one.
Exercise 4. Write (α ∣0⟩+β ∣1⟩)⊗(γ ∣0⟩+δ ∣1⟩) as a vector, first by taking the Kronecker
product directly and then by simplifying the expression and transforming it into vector
notation. Confirm that both results are equal.
α γ
Solution. We can write the two components as the vectors ( ) and ( ). Taking the
β δ
140
Kronecker product we get
⎛ γ ⎞ ⎛αγ ⎞
⎜α ( δ )⎟ ⎜ αδ ⎟
⎜ ⎟
⎜ γ ⎟=⎜ ⎟.
⎜ ⎟ ⎜βγ ⎟
β( )
⎝ δ ⎠ ⎝ βδ ⎠
Alternatively, we can simplify the expression first using left and right distributiv-
ity:
⎛αγ ⎞
⎜ αδ ⎟
⎜ ⎟
⎜βγ ⎟
⎝ βδ ⎠
Exercise 5. Note that H, X, Z and CNOT are all their own adjoints. Verify that
these matrices are unitary.
Solution.
2
1 1 1+1 1 + −1 2 0
H∶ ( √12 ( )) = 12 ( ) = 21 ( ) = I2
1 −1 1 + −1 1 + − − 1 0 2
2
0 1 0+1 0+0
X∶ ( ) =( ) = I2
1 0 0+0 1+0
2
1 0 1+0 0+0
Z∶ ( ) =( ) = I2
0 −1 0+0 0+−−1
141
I2 0
CNOT = ( ):
0 X
2
⎛1 0 0 0⎞ ⎛1 + 0 + 0 + 0 0+0+0+0 0+0+0+0 0 + 0 + 0 + 0⎞
⎜0 1 0 0⎟ ⎜0 + 0 + 0 + 0 0+1+0+0 0+0+0+0 0 + 0 + 0 + 0⎟
⎜ ⎟ =⎜ ⎟=I
⎜0 0 0 1⎟ ⎜0 + 0 + 0 + 0 0+0+0+0 0+0+0+1 0 + 0 + 0 + 0⎟ 4
⎝0 0 1 0⎠ ⎝0 + 0 + 0 + 0 0+0+0+0 0+0+0+0 0 + 0 + 1 + 0⎠
∎
Exercise 6. Show that H, X, Z, and CNOT have the behavior described in the
previous section. That is, show that when applied to basis vectors ( 10 ) and ( 01 ) they
produce the claimed output.
Solution.
1 1 1 1 1 1 0 1
H∶ √1 ( )( ) = √1 ( ) √1 ( )( ) = √1 ( )
2 1 −1 0 2 1 2 1 −1 1 2 −1
0 1 1 0 0 1 0 1
X∶ ( )( ) = ( ) ( )( ) = ( )
1 0 0 1 1 0 1 0
1 0 1 1 1 0 0 0
Z∶ ( )( ) = ( ) ( )( ) = ( )
0 −1 0 0 0 −1 1 −1
CNOT :
142
Exercise 8. Show that for a pure state in density matrix form, the ith element along
the diagonal is the probability of measuring ∣i⟩.
Solution. As we noted, a pure state in density matrix form can be written out as
∣ϕ⟩ ⟨ϕ∣. If ∣ϕ⟩ consists of the elements α0 , α1 , . . . , αn , then this produces the following
matrix:
⎛ α0 α0 α0 α1 . . . α0 αn ⎞
⎜ α1 α0 α1 α1 . . . α1 αn ⎟
⎜ ⎟
⎜ ⋮ ⋮ ⋱ ⋮ ⎟
⎝αn α0 αn α1 . . . αn αn ⎠
Thus, the k th element along the diagonal will be αk αk . It remains to show that every
2
αk αk = ∣α∣ (the probability of measuring ∣k⟩).
Let us expand αk out as a + bi.
. Similarly
2
√ 2
∣a + bi∣ = a2 + b 2 = a2 + b 2
.
∎
143
Appendix B
2. If ⋅; Q ⊢ C ∶ W and C Ô⇒ C ′ , then ⋅; Q ⊢ C ′ ∶ W .
Proof.
1. If t steps via Ð→H then the result is immediate by the assumption that Ð→H
satisfies preservation. Otherwise, suppose t Ð→b t′ . It must be the case that A =
Box W1 W2 and t = box p ⇒ C where Ω ⇒ p ∶ W1 and ⋅; Ω ⊢ C ∶ W2 . If t steps via the
structural rule with C Ô⇒ C ′ , then t′ = box p ⇒ C ′ , and by the inductive hypothesis,
⋅; Ω ⊢ C ′ ∶ W2 and so ⋅ ⊢ box p ⇒ C ′ ∶Box W1 W2 .
If t steps instead by an η rule, then t′ = box p′ ⇒ C {p′ /p} where p′ is concrete
for W1 . By Lemma 5 there is some Q such that Q ⇒ p′ ∶ W1 , so by the substitution
lemma (Lemma 4), we have ⋅; Q ⊢ C {p′ /p} ∶ W2 , and thus ⋅ ⊢ t′ ∶Circ(W1 , W2 ).
2. By induction on C Ô⇒ C ′ .
144
(b) Suppose C is p2 ← gate g p1 ; C0 , where Q = Q1 , Q0 and
⋅; Q1 ⊢ C1 ∶ W ′ Ω ⇒ p∶W ′ ⋅; Ω, Q2 ⊢ C2 ∶ W
If C steps via a structural rule, the result is immediate. If it steps via a β-rule,
then C1 = output p′ , and by inversion, Q1 ⇒ p′ ∶ W . By Lemma 4, we have
⋅; Q1 , Q2 ⊢ C ′ {p′ /p} ∶ W ′ .
If C1 = p2 ← gate g p1 ; C0 such that
p ← C1 ; C2 Ô⇒ p2 ← gate g p1 ; p ← C0 ; C2
⋅; Q′1 , Q0 , Q2 ⊢ p2 ← gate g p1 ; p ← C0 ; C2 ∶ W.
p ← C1 ; C2 Ô⇒ x ⇐ lift p′ ; p ← C0 ; C2
Theorem 6 (Progress). Suppose Ð→H satisfies progress with respect to the values v h .
Proof.
145
1. By the progress hypothesis for Ð→H , either t = v h for some v h or there exists
some t′ such that t Ð→H t′ (in which case t Ð→ t′ as well). In first case however, t is
either a value in the original host language (v), or t = box p ⇒ C, where
Ω ⇒ p∶W1 ⋅; Ω ⊢ C ∶W2
⋅ ⊢ box p ⇒ C ∶Box W1 W2
If p is not concrete for W1 , then box p ⇒ C can step via the η rule. If p is concrete, then
by the inductive hypothesis, C is either normal already (in which case so is box p ⇒ C),
or there is some C ′ such that C Ô⇒ C ′ . In that case, box p ⇒ C Ð→b box p ⇒ C ′ .
⋅ ⊢ t ∶ Box W1 W2 Ω ⇒ p ∶ W1
⋅; Ω ⊢ unbox t p ∶ W2
Ω1 ⇒ p1 ∶ W1 Ω2 ⇒ p2 ∶ W2 g ∈ G(W1 , W2 ) ⋅; Ω2 , Ω ⊢ C ∶ W
⋅; Ω1 , Ω ⊢ p2 ← gate g p1 ; C ∶ W
⋅; Ω1 ⊢ C ∶ W ⋅; Ω0 , Ω2 ⊢ C ′ ∶ W ′
⋅; Ω1 , Ω2 ⊢ p ← C; C ′ ∶ W ′
By the inductive hypothesis, either C can take a step, in which case so can
p ← C; C ′ , or C is normal. The latter cases are straightforward:
146
Theorem 7 (Normalization). Suppose that Ð→H is strongly normalizing with respect
to v h .
1. By the normalization property for Ð→H , there is some value v c such that t Ð→∗H
v c . This value v c is either a regular host language value v, in which case we are done,
or it is some uninterpreted boxed circuit box (p∶W ) ⇒ C. If p is concrete with respect
to W , then by the inductive hypothesis, there is some N such that C Ô⇒∗ N , and
so box p ⇒ C Ð→∗ box p ⇒ N .
If p is not concrete, then by an η-expansion, there is some p′ that is concrete for
W and box p ⇒ C Ð→b box p′ ⇒ C {p′ /p}. By induction we know that C {p′ /p}
normalizes (since the number of constructors in C {p′ /p} is the same as the number
in C), and thus so does box p ⇒ C.
Ω1 ⇒ p1 ∶ W1 Ω2 ⇒ p2 ∶ W2 g ∈ G(W1 , W2 ) ⋅; Ω2 , Ω ⊢ C ∶ W
⋅; Ω1 , Ω ⊢ p2 ← gate g p1 ; C ∶ W
⋅; Ω1 ⊢ C ∶ W ⋅; Ω0 , Ω2 ⊢ C ′ ∶ W ′
⋅; Ω1 , Ω2 ⊢ p ← C; C ′ ∶ W ′
147
Finally, if N = x ⇐ lift p′ ; C0 , then
p ← C; C ′ Ô⇒ x ⇐ lift p′ ; p ← C0 ; C ′ ,
JQ ⊢ C ∶ W K = JQ ⊢ C ′ ∶ W K.
JQ ⊢ C ∶ W K = JQ′ ⊢ C ∶ W K ○ [π]∗
= JQ′ ⊢ C ′ ∶ W K ○ [π]∗ = JQ ⊢ C ′ ∶ W K
If
⋅ ⊢ t ∶Box W1 W2 Q ⇒ p ∶W1
TypClosedConcreteUnbox
⋅; Q ⊢ unbox t p ∶ W2
and the circuit steps by a structural rule with t Ð→ t′ , then, assuming host is strongly
normalizing we have some box p′ ⇒ N such that t, t′ Ð→∗ box p′ ⇒ N . Then
Suppose
Ω1 ⇒ p1 ∶ W1 Ω2 ⇒ p2 ∶ W2 g ∈ G(W1 , W2 ) ⋅; Ω2 , Ω ⊢ C ∶ W
⋅; Ω1 , Ω ⊢ p2 ← gate g p1 ; C ∶ W
If the circuit steps via a structural rule, the result is immediate. If it steps via an η rule
to p′2 ← gate g p1 ; C {p′2 /p2 }, then the result follows from the fact that JC {p′2 /p2 }K =
JCK (Lemma 7).
148
Next, consider
⋅; Q1 ⊢ C1 ∶ W Ω0 ⇒ p∶W ⋅; Ω0 , Q2 ⊢ C2 ∶ W ′
⋅; Q1 , Q2 ⊢ p ← C1 ; C2 ∶ W ′
If the circuit steps via a structural rule, the result follows immediately. Otherwise,
we know C1 is normal, and the circuit stepped via a β or commuting conversion rule.
We proceed by a further case analysis on the typing judgment of C1 .
For a permutation rule π ∶ Q1 ≡ Q′1 , by induction we know that
JQ′1 , Q2 ⊢ p ← C1 ; C2 ∶ W ′ K = JQ′1 , Q2 ⊢ C ′ ∶ W ′ K
But then
JQ1 , Q2 ⊢ p ← C1 ; C2 ∶ W ′ K
= JΩ0 , Q2 ⊢ C2 ∶ W ′ K ○ (JQ1 ⊢ C1 ∶ W K ⊗ I∗ )
= JΩ0 , Q2 ⊢ C2 ∶ W ′ K ○ ((JQ′1 ⊢ C1 ∶ W K ○ [π]∗ ) ⊗ I∗ )
= JΩ0 , Q2 ⊢ C2 ∶ W ′ K ○ (JQ′1 ⊢ C1 ∶ W K ⊗ I∗ ) ○ ([π] ⊗ I)∗
= JQ′1 , Q2 ⊢ p ← C1 ; C2 ∶ W ′ K ○ ([π] ⊗ I)∗
= JQ1 , Q2 ⊢ p ← C1 ; C2 ∶ W ′ K
p ← C1 ; C2 Ô⇒ C2 {p′ /p},
we know
JQ1 , Q2 ⊢ p ← output p′ ; C2 ∶ W ′ K
= JΩ0 , Q2 ⊢ C2 ∶ W ′ K ○ (JQ1 ⊢ output p′ ∶ W K ⊗ I∗ )
= JΩ0 , Q2 ⊢ C2 ∶ W ′ K ○ (I∗ ⊗ I∗ )
= JΩ0 , Q2 ⊢ C2 ∶ W ′ K = JQ1 , Q2 ⊢ C2 {p′ /p} ∶ W ′ K
by Lemma 7.
If C1 is
p ← C1 ; C2 Ô⇒ p2 ← gate g p1 ; p ← C0 ; C2
149
then
Finally, if C1 is
Q0 ⇒ p0 ∶W0 x ∶∣W0 ∣; Q′ ⊢ C0 ∶W
⋅; Q0 , Q′ ⊢ x ⇐ lift p0 ; C0 ∶ W
and steps via a commuting conversion
p ← C1 ; C2 Ô⇒ x ⇐ lift p0 ; p ← C0 ; C2
then
JQ0 , Q′ , Q2 ⊢ p ← (x ⇐ lift p0 ; C0 ); C2 ∶ W ′ K
= JΩ0 , Q2 ⊢ C2 ∶ W ′ K ○ (JQ0 , Q′ ⊢ x ⇐ lift p0 ; C0 ∶ W K ⊗ I∗ )
⎛⎛ ′ † ∗⎞ ∗⎞
= JC2 K ○ ∑ JQ ⊢ C0 {v/x } ∶ W K ○ ([v ∶∣W0 ∣] ⊗ I) ⊗ I
⎝⎝⊢v∶∣W0 ∣ ⎠ ⎠
= JC2 K ○ ∑ ((JQ′ ⊢ C0 {v/x } ∶ W K ○ ([v ∶∣W0 ∣]† ⊗ I)∗ ) ⊗ I∗ )
⊢v∶∣W0 ∣
150
Appendix C
Qwire Documentation
C.1 Prelim.v
Lemma xorb_nb_b : ∀ b, ¬ b ⊕ b = true.
Lemma andb_xorb_dist : ∀ b b1 b2, b && (b1 ⊕ b2) = (b && b1) ⊕ (b && b2).
151
Lemma firstn_repeat_le : ∀ A (a : A) m n, (m ≤ n) →
firstn m (repeat a n) = repeat a m.
Lemma firstn_repeat_ge : ∀ A (a : A) m n, (m ≥ n) →
firstn m (repeat a n) = repeat a n.
Lemma firstn_repeat : ∀ A (a : A) m n,
firstn m (repeat a n) = repeat a (min m n).
Lemma skipn_repeat : ∀ A (a : A) m n,
skipn m (repeat a n) = repeat a (n-m).
Lemma disjoint_symm : ∀ ls1 ls2, disjoint ls1 ls2 = disjoint ls2 ls1.
Lemma subset_app : ∀ ls1 ls2 ls, (ls1 ++ ls2) ⊆ ls → ls1 ⊆ ls ∧ ls2 ⊆ ls.
Lemma inb_fmap_S : ∀ ls x,
inb (S x) (fmap S ls) = inb x ls.
152
Lemma double_pow : ∀ (n : N), (2^n + 2^n = 2^(n+1)).
C.2 Monad.v
Lemma fmap_compose' {f} (F : Functor f) `{Functor_Correct f} :
∀ {A B C} (g : A → B) (h : B → C) (a : f A),
fmap h (fmap g a) = fmap (h ○ g) a.
C.3 Monoid.v
Lemma M_unit_l : ∀ a, ⊺ ○ a = a.
Lemma M_comm_assoc : ∀ a b c, a ○ b ○ c = b ○ a ○ c.
Lemma M_absorb_l : ∀ a, ○ a = .
153
Lemma index_wrt_cons : ∀ idx a values,
index_wrt (a :: values) (fmap S idx) = index_wrt values idx.
C.4 Matrix.v
Lemma mat_equiv_refl : ∀ m n (A : Matrix m n), mat_equiv A A.
154
WF_Matrix m n B →
mat_equiv A B →
A = B.
Lemma Csum_plus : ∀ f g n,
Csum (fun x ⇒ f x + g x) n = Csum f n + Csum g n.
∗
Lemma Csum_conj_distr : ∀ f n, (Csum f n) = Csum (fun x ⇒ (f x)∗ ) n.
Lemma Csum_extend_l : ∀ n f,
f O + Csum (fun x ⇒ f (S x)) n = Csum f (S n).
Lemma Csum_unique : ∀ k (f : N → C) n,
(∃ x, (x < n) ∧ f x = k ∧ (∀ x', x ≠ x' → f x' = 0)) →
Csum f n = k.
155
Lemma Csum_product : ∀ m n f g, n ≠ O →
Csum f m * Csum g n =
Csum (fun x ⇒ f (x / n) * g (x mod n)) (m * n).
156
Lemma WF0_Zero_r :∀ (n : N) (A : Matrix n 0),
WF_Matrix _ _ A →
A = Zero n 0.
157
Lemma Mmult_inf_r : ∀(m n : N) (A : Matrix m n),
WF_Matrix m n A → A × ∞I = A.
158
Lemma kron_plus_distr_r : ∀ (m n o p : N) (A B : Matrix m n)
(C : Matrix o p), (A .+ B) ⊗ C = A ⊗ C .+ B ⊗ C.
Lemma kron_mixed_product : ∀ (m n o p q r : N)
(A : Matrix m n) (B : Matrix p q ) (C : Matrix n o) (D : Matrix q r),
(A ⊗ B) × (C ⊗ D) = (A × C) ⊗ (B × D).
159
Lemma kron_transpose : ∀ (m n o p : N) (A : Matrix m n) (B : Matrix o p),
(A ⊗ B)⊺ = A⊺ ⊗ B⊺.
Lemma divmod_eq : ∀ x y n z,
fst (Nat.divmod x y n z) = (n + fst (Nat.divmod x y 0 z)).
Lemma divmod_S : ∀ x y n z,
fst (Nat.divmod x y (S n) z) = (S n + fst (Nat.divmod x y 0 z)).
C.5 Quantum.v
Lemma bool_to_matrix_eq : ∀ b, bool_to_matrix b = bool_to_matrix' b.
Lemma bool_to_ket_matrix_eq : ∀ b,
outer_product (bool_to_ket b) = bool_to_matrix b.
160
Lemma cnot_eq : cnot = control σx.
Lemma WF_bools_to_matrix : ∀ l,
WF_Matrix (2^(length l)) (2^(length l)) (bools_to_matrix l).
161
Lemma WF_cnot : WF_Matrix 4 4 cnot.
162
Lemma cnot_sa : cnot† = cnot.
163
Lemma mixed_state_diag_real : ∀ {n} (ρ : Density n) i , Mixed_State ρ →
snd (ρ i i) = 0.
Lemma super_I : ∀ n ρ,
WF_Matrix n n ρ →
super ('I_n) ρ = ρ.
Lemma compose_super_correct : ∀ {m n p}
(g : Superoperator n p) (f : Superoperator m n),
WF_Superoperator g →
WF_Superoperator f →
WF_Superoperator (compose_super g f).
Lemma compose_super_assoc : ∀ {m n p q}
(f : Superoperator m n) (g : Superoperator n p) (h : Superoperator p q),
compose_super (compose_super f g) h = compose_super f (compose_super g h).
164
Lemma WF_Superoperator_compose : ∀ m n p (s : Superoperator n p)
(s' : Superoperator m n), WF_Superoperator s → WF_Superoperator s' →
WF_Superoperator (compose_super s s').
Lemma swap_0_2 :
swap_two 3 0 2 = ('I_2 ⊗ swap) × (swap ⊗ 'I_2) × ('I_2 ⊗ swap).
C.6 Contexts.v
Lemma size_ntensor : ∀ n W, size_wtype (n ⊗ W) = (n * size_wtype W).
Lemma singleton_singleton : ∀ x W,
SingletonCtx x W (singleton x W).
Lemma singleton_equiv : ∀ x W Γ,
SingletonCtx x W Γ → Γ = singleton x W.
165
Lemma merge_merge' : ∀ (Γ1 Γ2 : Ctx), Γ1 ⋓ Γ2 = (merge' Γ1 Γ2 ).
Lemma merge_cancel_l : ∀ Γ Γ1 Γ2 , Γ1 = Γ2 → Γ ⋓ Γ1 = Γ ⋓ Γ2 .
Lemma merge_cancel_r : ∀ Γ Γ1 Γ2 , Γ1 = Γ2 → Γ1 ⋓ Γ = Γ2 ⋓ Γ.
Lemma merge_nil_l : ∀ Γ, ∅ ⋓ Γ = Γ.
Lemma merge_nil_r : ∀ Γ, Γ ⋓ ∅ = Γ.
Lemma merge_comm : ∀ Γ1 Γ2 , Γ1 ⋓ Γ2 = Γ2 ⋓ Γ1 .
Lemma cons_distr_merge : ∀ Γ1 Γ2 ,
cons_o None (Γ1 ⋓ Γ2 ) = cons_o None Γ1 ⋓ cons_o None Γ2 .
166
Lemma merge_offset : ∀ (n : N) (Γ1 Γ2 Γ : Ctx),
Valid Γ = Γ1 ⋓ Γ2 →
Valid (repeat None n ++ Γ1 ) ⋓ Valid (repeat None n ++ Γ2 ) =
Valid (repeat None n ++ Γ).
Lemma valid_join : ∀ Γ1 Γ2 Γ3 ,
is_valid (Γ1 ⋓ Γ2 ) →
is_valid (Γ1 ⋓ Γ3 ) → is_valid (Γ2 ⋓ Γ3 ) → is_valid (Γ1 ⋓ Γ2 ⋓ Γ3 ).
Lemma merge_o_ind_fun : ∀ o1 o2 o,
merge_o o1 o2 o → merge_wire o1 o2 = Valid [o].
Lemma merge_ind_fun : ∀ Γ1 Γ2 Γ,
merge_ind Γ1 Γ2 Γ →
Γ == Γ1 ● Γ2 .
Lemma merge_o_fun_ind : ∀ o1 o2 o,
merge_wire o1 o2 = Valid [o] →
merge_o o1 o2 o.
Lemma merge_fun_ind : ∀ Γ1 Γ2 Γ,
Γ == Γ1 ● Γ2 →
merge_ind Γ1 Γ2 Γ.
167
Lemma merge_intersection : ∀ Γ1 Γ2 Γ3 Γ4 ,
is_valid (Γ1 ⋓ Γ2 ) → (Γ1 ⋓ Γ2 ) = (Γ3 ⋓ Γ4 ) →
{ Γ13 : OCtx & { Γ14 : OCtx & { Γ23 : OCtx & { Γ24 : OCtx &
Γ1 == Γ13 ● Γ14 ∧ Γ2 == Γ23 ● Γ24 ∧ Γ3 == Γ13 ● Γ23 ∧ Γ4 == Γ14 ● Γ24
} } } }.
Lemma disjoint_valid : ∀ Γ1 Γ2 ,
Disjoint Γ1 Γ2 → is_valid Γ1 → is_valid Γ2 →
is_valid (Γ1 ⋓ Γ2 ).
Lemma disjoint_merge : ∀ Γ Γ1 Γ2 ,
Disjoint Γ Γ1 → Disjoint Γ Γ2 → Disjoint Γ (Γ1 ⋓ Γ2 ).
Lemma disjoint_split : ∀ Γ1 Γ2 Γ,
is_valid Γ1 → is_valid Γ2 →
Disjoint Γ1 Γ2 → Disjoint (Γ1 ⋓ Γ2 ) Γ →
Disjoint Γ1 Γ ∧ Disjoint Γ2 Γ.
Lemma index_trim : ∀ Γ i,
index (trim Γ) i = index Γ i.
168
Lemma trim_non_empty : ∀ Γ, ¬ empty_ctx Γ → trim Γ ≠ [].
Lemma trim_merge : ∀ Γ Γ1 Γ2 , Γ == Γ1 ● Γ2 →
otrim Γ == otrim Γ1 ● otrim Γ2 .
169
C.7 HOASCircuits.v
Lemma compose_typing : ∀ Γ1 Γ1 ' Γ W W' (c : Circuit W)
(f : Pat W → Circuit W'),
Γ1 ⊢ c :Circ →
Γ ⊢ f :Fun →
∀ {pf : Γ1 ' == Γ1 ● Γ},
Γ1 ' ⊢ compose c f :Circ.
C.8 DBCircuits.v
Lemma get_fresh_split : ∀ w Γ,
get_fresh w Γ = (get_fresh_pat w Γ, get_fresh_state w Γ).
Lemma get_fresh_typed : ∀ w Γ0 p Γ,
(p, Γ) = get_fresh w Γ0 → Γ ⊢ p:Pat.
Lemma add_fresh_split : ∀ w Γ,
add_fresh w Γ = (add_fresh_pat w Γ, add_fresh_state w Γ).
170
Lemma SingletonCtx_dom : ∀ x w Γ,
SingletonCtx x w Γ →
ctx_dom Γ = [x].
Lemma SingletonCtx_flatten : ∀ x w Γ,
SingletonCtx x w Γ →
flatten_ctx Γ = [Some w].
Lemma remove_flatten : ∀ Γ,
remove_indices Γ (get_nones Γ) = flatten_ctx Γ.
C.9 Denotation.v
Lemma WF_Matrix_U : ∀ {W} (U : Unitary W),
WF_Matrix (2^JWK) (2^JWK) (JUK).
171
Lemma denote_gate_correct : ∀ {W1 } {W2 } (g : Gate W1 W2 ),
WF_Superoperator (denote_gate true g).
Lemma WF_swap_to_0_aux : ∀ n i,
(i + 1 < n) →
WF_Matrix (2^n) (2^n) (swap_to_0_aux n i).
Lemma WF_swap_list_aux : ∀ m n l,
(∀ i j, In (i,j) l → (i < n) ∧ (j < n)) →
(m ≤ n) →
WF_Matrix (2^n) (2^n) (swap_list_aux m n l).
172
Lemma swap_list_aux_unitary : ∀ m n l,
(∀ i j, In (i,j) l → (i < n) ∧ (j < n)) →
(m ≤ n) →
WF_Unitary (swap_list_aux m n l).
Lemma ctrls_to_list_empty : ∀ W lb u,
@ctrls_to_list W lb [] u = (O, [], Zero 2 2).
173
Lemma denote_ctrls_unitary : ∀ W n (g : Unitary W) l,
(forallb (fun x ⇒ x <? n) l = true) →
(length l = JWK) →
WF_Unitary (denote_ctrls n g l).
Lemma ctrl_list_to_unitary_transpose : ∀ l r u,
ctrl_list_to_unitary l r (u† ) = (ctrl_list_to_unitary l r u)† .
174
Lemma init1 _superoperator : ∀ (n i j : N) (ρ : Square (2 ^ n)),
(i * j = 2^n) →
Mixed_State ρ →
Mixed_State (('I_i ⊗ ∣1⟩ ⊗ 'I_j) × ρ × ('I_i ⊗ ⟨1∣ ⊗ 'I_j)).
Lemma map_same_id : ∀ a l,
map (fun z : N * N ⇒ if a =? snd z then (fst z, a) else z) (combine l l)
= combine l l.
Lemma swap_list_aux_id : ∀ m n l,
swap_list_aux m n (combine l l) = Id (2 ^ n).
175
Lemma apply_U_spec_1 : ∀ n i j (A1 : Square (2^i)) (A2 : Square (2^j))
(U : Square (2^1)) (ρ : Square (2^1)), (i + j + 1 = n) →
@apply_U 1 n U [i] (A1 ⊗ ρ ⊗ A2) = A1 ⊗ (super U ρ) ⊗ A2.
Lemma apply_U_spec_2 : ∀ n i j k
(A1 : Square (2^i)) (A2 : Square (2^j)) (A3 : Square (2^k))
(U : Square (2^2)) (ρ1 ρ2 ρ1 ' ρ2 ': Square (2^1)), (i + j + k + 2 = n) →
(super U (ρ1 ⊗ ρ2 )) = ρ1 ' ⊗ ρ2 ' →
@apply_U 2 n U [i; (i+j+1)] (A1 ⊗ ρ1 ⊗ A2 ⊗ ρ2 ⊗ A3) =
A1 ⊗ ρ1 ' ⊗ A2 ⊗ ρ2 ' ⊗ A3.
Lemma denote_pat_fresh_id : ∀ w,
denote_pat (add_fresh_pat w []) = Id (2^JwK).
Lemma maps_to_app : ∀ Γ w,
maps_to (length Γ) (Γ ++ [Some w]) = Some (size_ctx Γ).
Lemma add_fresh_state_no_gaps : ∀ W Γ,
no_gaps Γ → no_gaps (add_fresh_state W Γ).
Lemma add_fresh_pat_bounded : ∀ W Γ,
no_gaps Γ →
Bounded_Pat (length Γ + size_wtype W) (add_fresh_pat W Γ).
176
Lemma subst_var_no_gaps : ∀ Γ w,
no_gaps Γ →
subst_var (Γ ++ [Some w]) (length Γ) = length Γ.
Lemma maps_to_no_gaps : ∀ v Γ,
(v < length Γ) →
no_gaps Γ →
maps_to v Γ = Some v.
Lemma subst_var_no_gaps : ∀ Γ v,
(v < length Γ) →
no_gaps Γ →
subst_var Γ v = v.
Lemma subst_pat_fresh : ∀ w Γ,
no_gaps Γ →
subst_pat (add_fresh_state w Γ) (add_fresh_pat w Γ)
= add_fresh_pat w Γ.
Lemma subst_pat_fresh_empty : ∀ w,
subst_pat (add_fresh_state w []) (add_fresh_pat w [])
= add_fresh_pat w [].
177
Lemma singleton_update : ∀ Γ W W' v,
SingletonCtx v W Γ →
SingletonCtx v W' (update_at Γ v (Some W')).
Lemma remove_at_singleton : ∀ x w Γ,
SingletonCtx x w Γ →
empty_ctx (remove_at x Γ).
Lemma update_none_singleton : ∀ x w Γ,
SingletonCtx x w Γ →
empty_ctx (update_at Γ x None).
Lemma index_merge_l : ∀ Γ Γ1 Γ2 n w,
Γ == Γ1 ● Γ2 →
index Γ1 n = Some w →
index Γ n = Some w.
Lemma index_merge_r : ∀ Γ Γ1 Γ2 n w,
Γ == Γ1 ● Γ2 →
index Γ2 n = Some w →
index Γ n = Some w.
178
Lemma denote_gate_circuit : ∀ {w1 w2 w'} (safe:B) (g : Gate w1 w2)
(p1 : Pat w1) (f : Pat w2 → Circuit w') (Γ0 Γ Γ1 Γ2 : Ctx),
Γ == Γ1 ● Γ2 → Γ1 ⊢ p1 :Pat →
denote_circuit safe (gate g p1 f) Γ0 Γ =
compose_super
(denote_circuit safe (f (process_gate_pat g p1 Γ)) Γ0
(process_gate_state g p1 Γ))
(apply_gate safe g (pat_to_list (subst_pat Γ p1))).
Lemma lookup_maybe_S : ∀ x l,
lookup_maybe (S x) (map S l) = lookup_maybe x l.
179
Lemma remove_bit_merge : ∀ (Γ Γ' : Ctx) W (p : Pat W) v,
Γ ⊢ p:Pat →
Γ' == singleton v Bit ● Γ →
remove_pat (bit v) Γ' = Γ.
180
Lemma HOAS_Equiv_refl : ∀ w1 w2 (c : Box w1 w2), c ≡ c.
Lemma inSeq_assoc : ∀ {w1 w2 w3 w4} (c1 : Box w1 w2) (c2 : Box w2 w3)
(c3 : Box w3 w4), c3 ⋅ (c2 ⋅ c1) = (c3 ⋅ c2) ⋅ c1.
C.10 HOASLib.v
Lemma boxed_gate_WT {W1 W2 } (g : Gate W1 W2 ) : Typed_Box (boxed_gate g).
Lemma inPar_WT : ∀ W1 W1 ' W2 W2 ' (c1 : Box W1 W2 ) (c2 : Box W1 ' W2 '),
Typed_Box c1 → Typed_Box c2 →
Typed_Box (inPar c1 c2).
181
Lemma inParMany_WT : ∀ n W W' (c : Box W W'), Typed_Box c →
Typed_Box (inParMany n c).
C.11 SemanticLib.v
Lemma id_circ_spec : ∀ W ρ safe,
WF_Matrix (2^JWK) (2^JWK) ρ →
denote_box safe (@id_circ W) ρ = ρ.
Lemma init0 _spec : ∀ safe, denote_box safe init0 (Id (2^0)) = ∣0⟩⟨0∣.
Lemma init1 _spec : ∀ safe, denote_box safe init1 (Id (2^0)) = ∣1⟩⟨1∣.
182
Lemma CNOT_spec : ∀ (b1 b2 safe : B),
denote_box safe CNOT (bool_to_matrix b1 ⊗ bool_to_matrix b2) =
bool_to_matrix b1 ⊗ bool_to_matrix (b1 ⊕ b2).
C.12 HOASExamples.v
Lemma new_discard_WT : Typed_Box new_discard.
183
Lemma Deutsch_Jozsa_WT' : ∀ n Uf , Typed_Box Uf →
Typed_Box (Deutsch_Jozsa n Uf ).
184
Lemma n_coins_WT' : ∀ n, Typed_Box (n_coins' n).
C.13 HOASProofs.v
Lemma init_ket1 : Jinit trueK I1 = (∣1⟩⟨1∣ : Density 2).
Lemma flips_lift_correct_gen : ∀ n a,
Jcoin_flips_lift nK (a .* I1) = a .* biased_coin (1/(2^n)).
185
Lemma flips_lift_correct : ∀ n,
Jcoin_flips_lift nK I1 = biased_coin (1/(2^n)).
C.14 Equations.v
Lemma X_meas_WT : Typed_Box X_meas.
186
Lemma NOT_meas_comm : X_meas ≡ meas_NOT.
187
Lemma super_super : ∀ m n o (U : Matrix o n) (V : Matrix n m)
(ρ : Square m),
super U (super V ρ) = super (U × V) ρ.
C.15 Composition.v
Fact denote_compose : ∀ safe w (c : Circuit w) (Γ : Ctx),
Γ ⊢ c :Circ →
∀ w' (f : Pat w → Circuit w') (Γ0 Γ1 Γ1 ' Γ0 1 : Ctx),
Γ1 ⊢ f :Fun →
Γ1 ' == Γ1 ● Γ →
Γ0 1 == Γ0 ● Γ1 →
denote_circuit safe (compose c f) Γ0 Γ1 ' =
compose_super
(denote_circuit safe (f (add_fresh_pat w Γ1 )) Γ0 (add_fresh_state w Γ1 ))
(denote_circuit safe c Γ0 1 Γ).
Lemma HOAS_Equiv_inSeq : ∀ w1 w2 w3
(c1 c1' : Box w1 w2) (c2 c2' : Box w2 w3),
Typed_Box c1 → Typed_Box c1' → Typed_Box c2 → Typed_Box c2' →
c1 ≡ c1' → c2 ≡ c2' → (c2 ⋅ c1) ≡ (c2' ⋅ c1').
188
C.16 Ancilla.v
Fact valid_ancillae_box_equal : ∀ W1 W2 (c : Box W1 W2 ),
valid_ancillae_box c ↔ valid_ancillae_box' c.
C.17 Symmetric.v
Lemma unitary_at1_WT : ∀ n (U : Unitary Qubit) i (pf : i < n),
Typed_Box (unitary_at1 n U i pf).
189
Lemma X_at_WT : ∀ n i pf, Typed_Box (X_at n i pf).
Lemma lt_leS_le : ∀ i j k,
i < j → j ≤ S k → i ≤ k.
Lemma strong_induction' :
∀ P : N → Type,
(∀ n : N, (∀ k : N, (k < n → P k)) → P n) →
∀ n i, i ≤ n → P i.
Theorem strong_induction:
∀ P : N → Type,
(∀ n : N, (∀ k : N, (k < n → P k)) → P n) →
∀ n : N, P n.
Lemma CNOT_at_i0_SS : ∀ n j
(pfj : 0 < S (S j)) (pfj' : 0 < S j)
(pfn : S (S j) < S (S n)) (pfn' : S j < S n),
CNOT_at_i0 (S (S n)) (S (S j)) pfj pfn =
box_ q ⇒ let_ (q0,(q1,qs)) ← q;
let_ (q0,qs) ← CNOT_at_i0 (S n) (S j) pfj' pfn' $ (q0,qs);
(q0,(q1,qs)).
Lemma CNOT_at_j0_SS : ∀ n i
(pfi : 0 < S (S i)) (pfi' : 0 < S i)
(pfn : S (S i) < S (S n)) (pfn' : S i < S n),
CNOT_at_j0 (S (S n)) (S (S i)) pfi pfn =
box_ q ⇒ let_ (q0,(q1,qs)) ← q;
let_ (q0,qs) ← CNOT_at_j0 (S n) (S i) pfi' pfn' $ (q0,qs);
(q0,(q1,qs)).
190
Lemma CNOT_at'_WT : ∀ (n i j : N)
(pf_i : i < n) (pf_j : j < n) (pf_i_j : i ≠ j),
Typed_Box (CNOT_at' n i j pf_i pf_j pf_i_j).
191
Lemma TOF_at_k0_WT : ∀ n i j pf_ij pf_ik pf_jk pf_in pf_jn,
Typed_Box (TOF_at_k0 n i j pf_ij pf_ik pf_jk pf_in pf_jn).
192
Lemma symmetric_reverse_symmetric : ∀ n t c
(pf_sym : source_symmetric n t c),
source_symmetric n t (symmetric_reverse n t c pf_sym).
Fact gate_acts_on_noop_at : ∀ m g k i,
@gate_acts_on (S m) k g →
i ≠ k → i < S m →
noop_on m i g.
193
Fact valid_ancillae_box'_equiv : ∀ W1 W2 (b1 b2 : Box W1 W2 ),
b1 ≡ b2 → valid_ancillae_box' b1 ↔ valid_ancillae_box' b2.
Fact symmetric_gate_noop_source : ∀ n t k g c,
gate_acts_on k g →
noop_source n t c →
noop_source n t (g ⋅ c ⋅ g).
Fact init_at_noop : ∀ b m i j,
valid_ancillae_box'
(assert_at b (S m) i ⋅ init_at b (S m) j ⋅ init_at b m i).
Fact symmetric_ancilla_noop_source : ∀ n t k c b,
k < S n →
noop_source (S n) t c →
noop_source n t (assert_at b (n+t) k ⋅ c ⋅ init_at b (n+t) k).
Lemma source_symmetric_noop : ∀ n t c,
source_symmetric n t c → noop_source n t c.
Fact ancilla_free_Toffoli_at : ∀ n a b c,
ancilla_free_box (Toffoli_at n a b c).
Fact ancilla_free_seq : ∀ W W' W'' (c1 : Box W W') (c2 : Box W' W''),
ancilla_free_box c1 → ancilla_free_box c2 → ancilla_free_box (c1 ;; c2).
194
Theorem source_symmetric_valid : ∀ (n t : N)
(c : Square_Box ((n + t) ⊗ Qubit)),
source_symmetric n t c →
valid_ancillae_box c.
Fact HOAS_Equiv_inSeq' :
∀ (w1 w2 w3 : WType) (b1 b1' : Box w1 w2) (b2 b2' : Box w2 w3),
b1 ≡ b1' → b2 ≡ b2' → b1;; b2 ≡ b1';; b2'.
C.18 Oracles.v
Lemma classical_merge_nil_l : ∀ Γ, [] ∪ Γ = Γ.
Lemma classical_merge_nil_r : ∀ Γ, Γ ∪ [] = Γ.
Lemma subset_classical_merge : ∀ Γ Γ1 Γ2 ,
Γ1 ∪ Γ2 ⊂ Γ → (Γ1 ⊂ Γ) * (Γ2 ⊂ Γ).
Lemma position_of_lt : ∀ v Γ W,
nth v Γ None = Some W → (position_of v Γ < JΓK).
Lemma singleton_nth_classical : ∀ Γ v,
singleton v Qubit ⊂ Γ → ∃ W, nth v Γ None = Some W.
195
Lemma ctx_dom_repeat : ∀ n, ctx_dom (repeat (Some Qubit) n) = seq 0 n.
Lemma pat_max_fresh : ∀ m n,
(pat_max (add_fresh_pat (n ⊗ Qubit) (repeat (Some Qubit) m)) < S (m+n)).
Lemma singleton_repeat : ∀ n W,
singleton n W = repeat None n ++ repeat (Some W) 1.
Lemma ctx_dom_none_repeat : ∀ m n,
ctx_dom (repeat None m ++ repeat (Some Qubit) n) = seq m n.
Lemma qubit_at_reflect : ∀ v Γ,
qubit_at v Γ = true ↔ nth v Γ None = Some Qubit.
Lemma WF_ctx_to_matrix : ∀ Γ f,
WF_Matrix (2^JΓK) (2^JΓK) (ctx_to_matrix Γ f).
Lemma WF_ctx_to_mat_list : ∀ Γ f,
WF_Matrix (2^JΓK) (2^JΓK) (big_kron (ctx_to_mat_list Γ f)).
196
Lemma big_kron_append : ∀ m n (l1 l2 : list (Matrix m n))
(A B : Matrix m n),
(∀ j, WF_Matrix m n (nth j l1 A)) →
(∀ j, WF_Matrix m n (nth j l2 B)) →
⊗ (l1 ++ l2) = (⊗ l1) ⊗ (⊗ l2).
197
Bibliography
Dorit Aharonov. A simple proof that toffoli and hadamard are quantum universal.
arXiv preprint quant-ph/0301040, 2003.
Dorit Aharonov and Michael Ben-Or. Fault-tolerant quantum computation with con-
stant error. In Proceedings of the twenty-ninth annual ACM symposium on Theory
of computing, pages 176–188. ACM, 1997.
Dorit Aharonov, Andris Ambainis, Julia Kempe, and Umesh Vazirani. Quantum
walks on graphs. In Proceedings of the thirty-third annual ACM symposium on
Theory of computing, pages 50–59. ACM, 2001.
198
Matthew Amy. Towards large-scale functional verification of universal quantum cir-
cuits. In Proceedings of the 15th International Conference on Quantum Physics
and Logic, QPL 2018, June 2018.
Sanjeev Arora and Boaz Barak. Computational complexity: a modern approach. Cam-
bridge University Press, 2009.
Miriam Backens. The zx-calculus is complete for stabilizer quantum mechanics. New
Journal of Physics, 16(9):093021, 2014.
Alexandru Baltag and Sonja Smets. LQP: the dynamic logic of quantum information.
Mathematical structures in computer science, 16(03):491–525, 2006.
Alexandru Baltag and Sonja Smets. Quantum logic as a dynamic logic. Synthese,
179(2):285–306, 2011.
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin.
Computer-aided security proofs for the working cryptographer. In Advances in
Cryptology–CRYPTO 2011, pages 71–90. Springer, 2011.
Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. Probabilistic rela-
tional Hoare logics for computer-aided security proofs. In Mathematics of Program
Construction, pages 1–6. Springer, 2012.
Stephane Beauregard. Circuit for shor’s algorithm using 2n+ 3 qubits. arXiv preprint
quant-ph/0205095, 2002.
199
David Beckman, Amalavoyal N Chari, Srikrishna Devabhaktuni, and John Preskill.
Efficient networks for quantum factoring. Physical Review A, 54(2):1034, 1996.
P.N. Benton. A mixed linear and non-linear logic: Proofs, terms and models. In
Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic, volume 933
of Lecture Notes in Computer Science, pages 121–135. Springer Berlin Heidelberg,
1995. doi:10.1007/BFb0022251.
Ethan Bernstein and Umesh Vazirani. Quantum complexity theory. SIAM Journal
on Computing, 26(5):1411–1473, 1997.
Stefano Bettelli, Tommaso Calarco, and Luciano Serafini. Toward an architecture for
quantum programming. The European Physical Journal D, 25(2):181–200, 2003.
Alex Bocharov, Martin Roetteler, and Krysta M Svore. Efficient synthesis of proba-
bilistic quantum circuits with fallback. Physical Review A, 91(5):052317, 2015a.
Alex Bocharov, Martin Roetteler, and Krysta M Svore. Efficient synthesis of univer-
sal repeat-until-success quantum circuits. Physical review letters, 114(8):080502,
2015b.
Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of agda–a functional lan-
guage with dependent types. In International Conference on Theorem Proving in
Higher Order Logics, pages 73–78. Springer, 2009.
200
Olivier Brunet and Philippe Jorrand. Dynamic quantum logic for quantum programs.
International Journal of Quantum Information, 2(01):45–54, 2004.
Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, and Vincent Siles.
CoqEAL - the coq effective algebra library. https://github.com/CoqEAL/CoqEAL,
2016.
Rohit Chadha, Paulo Mateus, and Amílcar Sernadas. Reasoning about imperative
quantum programs. Electronic Notes in Theoretical Computer Science, 158:19–39,
2006.
Andrew M Childs, Richard Cleve, Enrico Deotto, Edward Farhi, Sam Gutmann, and
Daniel A Spielman. Exponential algorithmic speedup by a quantum walk. In
Proceedings of the thirty-fifth annual ACM symposium on Theory of computing,
pages 59–68. ACM, 2003.
Richard Cleve, Artur Ekert, Chiara Macchiavello, and Michele Mosca. Quantum al-
gorithms revisited. In Proceedings of the Royal Society of London A: Mathematical,
Physical and Engineering Sciences, volume 454, pages 339–354. The Royal Society,
1998.
Bob Coecke and Aleks Kissinger. Picturing quantum processes. Cambridge University
Press, 2017.
Coq Development Team. The Coq proof assistant reference manual, version 8.8, 2018.
Electronic resource, available from https://coq.inria.fr/refman/.
Andrew W Cross, Lev S Bishop, John A Smolin, and Jay M Gambetta. Open quantum
assembly language. arXiv preprint arXiv:1707.03429, 2017.
Luís Cruz-Filipe, Herman Geuvers, and Freek Wiedijk. C-corn, the constructive coq
repository at nijmegen. In International Conference on Mathematical Knowledge
Management, pages 88–103. Springer, 2004.
201
D-Wave Systems, Inc. Programming with D-Wave: Map coloring problem, 2013.
Vincent Danos, Elham Kashefi, and Prakash Panangaden. The measurement calculus.
Journal of the ACM (JACM), 54(2):8, 2007.
Vincent Danos, Elham Kashefi, Prakash Panangaden, and Simon Perdrix. Extended
measurement calculus. Semantic techniques in quantum computation, pages 235–
310, 2009.
Joëlle Despeyroux, Amy Felty, and André Hirschowitz. Higher-order abstract syntax
in coq. In International Conference on Typed Lambda Calculi and Applications,
pages 124–138. Springer, 1995.
David Deutsch. Quantum theory, the church-turing principle and the universal quan-
tum computer. In Proceedings of the Royal Society of London A: Mathematical,
Physical and Engineering Sciences, volume 400, pages 97–117. The Royal Society,
1985.
David Deutsch and Richard Jozsa. Rapid solution of problems by quantum compu-
tation. In Proceedings of the Royal Society of London A: Mathematical, Physical
and Engineering Sciences, volume 439, pages 553–558. The Royal Society, 1992.
Andrew Fagan and Ross Duncan. Optimising Clifford circuits with Quantomatic. In
Proceedings of the 15th International Conference on Quantum Physics and Logic,
QPL 2018, Halifax, Nova Scotia, 3-7 June 2018, 2018.
202
Richard P Feynman and Albert R Hibbs. Quantum mechanics and path integrals.
International series in pure and applied physics. McGraw Hill, 1965.
Jean Baptiste Joseph Fourier. Solution d’une question particuliere du calcul des
inégalités. Nouveau Bulletin des Sciences par la Société philomatique de Paris, 99:
100, 1826.
Iulia M. Georgescu, Sahel Ashhab, and Franco Nori. Quantum simulation. Reviews
of Modern Physics, 86(1):153, 2014.
Craig Gidney. Factoring with n+ 2 clean qubits and n-1 dirty qubits. arXiv preprint
arXiv:1706.07884, 2017.
Georges Gonthier. Formal proof–the four-color theorem. Notices of the AMS, 55(11):
1382–1393, 2008.
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen,
François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould
Biha, et al. A machine-checked proof of the odd order theorem. In International
Conference on Interactive Theorem Proving, pages 163–179. Springer, 2013.
Daniel Gottesman. Stabilizer codes and quantum error correction. arXiv preprint
quant-ph/9705052, 1997.
Alexander Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît
Valiron. Quipper: A scalable quantum programming language. In Proceedings
of the 34th ACM SIGPLAN Conference on Programming Language Design and
Implementation, PLDI 2013, pages 333–342, 2013a.
Alexander Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît
Valiron. An introduction to quantum programming in Quipper. In Proceedings
of the 5th International Conference on Reversible Computation, volume 7948 of
Lecture Notes in Computer Science, pages 110–124, 2013b. ISBN 978-3-642-38985-
6.
203
Lov K. Grover. A fast quantum mechanical algorithm for database search. In Pro-
ceedings of the Twenty-eighth Annual ACM Symposium on Theory of Computing,
STOC ’96, pages 212–219, New York, NY, USA, 1996. ACM. ISBN 0-89791-785-5.
doi:10.1145/237814.237866. URL http://doi.acm.org/10.1145/237814.237866.
Brian C Hall. Quantum theory for mathematicians, volume 267. Springer, 2013.
Thomas Häner, Martin Roetteler, and Krysta M Svore. Factoring using 2n+ 2 qubits
with toffoli based modular multiplication. arXiv preprint arXiv:1611.07995, 2016.
Jeff Heckey, Shruti Patil, Ali Javadi-Abhari, Adam Holmes, Daniel Kudrow, Ken-
neth R Brown, Diana Franklin, Frederic T Chong, and Margaret Martonosi. Com-
piler management of communication and parallelism for quantum computation.
ACM SIGARCH Computer Architecture News, 43(1):445–456, 2015.
IARPA. IARPA quantum computer science program, April 2010. URL https:
//www.fbo.gov/notices/637e87ac1274d030ce2ab69339ccf93c. Broad Agency
Announcement IARPA-BAA-10-02.
Ali Javadi-Abhari, Arvin Faruque, Mohammad J Dousti, Lukas Svec, Oana Catu, Am-
lan Chakrabati, Chen-Fu Chiang, Seth Vanderwilt, John Black, and Fred Chong.
Scaffold: Quantum programming language. Technical report, PRINCETON UNIV
NJ DEPT OF COMPUTER SCIENCE, 2012.
Ali Javadi-Abhari, Shruti Patil, Daniel Kudrow, Jeff Heckey, Alexey Lvov, Frederic T
Chong, and Margaret Martonosi. Scaffcc: Scalable compilation and analysis of
quantum programs. Parallel Computing, 45:2–17, 2015.
204
Nathan Killoran, Josh Izaac, Nicolás Quesada, Ville Bergholm, Matthew Amy, and
Christian Weedbrook. Strawberry fields: A software platform for photonic quantum
computing. arXiv preprint arXiv:1804.03159, 2018.
Aleks Kissinger. Pictures of Processes: Automated Graph Rewriting for Monoidal
Categories and Applications to Quantum Computing. PhD thesis, University of
Oxford, 2011.
A Yu Kitaev. Quantum error correction with imperfect gates. In Quantum Commu-
nication, Computing, and Measurement, pages 181–188. Springer, 1997.
Alexei Yu Kitaev, Alexander Shen, and Mikhail N Vyalyi. Classical and quantum
computation. Number 47. American Mathematical Soc., 2002.
Vadym Kliuchnikov, Dmitri Maslov, and Michele Mosca. Practical approximation
of single-qubit unitaries by single-qubit quantum clifford and t circuits. IEEE
Transactions on Computers, 65(1):161–172, 2016.
Emmanuel H. Knill. Conventions for quantum pseudocode. Technical Report LAUR-
96-2724, Los Alamos National Laboratory, 1996.
Donald Ervin Knuth. Literate programming. The Computer Journal, 27(2):97–111,
1984.
Dexter Kozen. A probabilistic pdl. Journal of Computer and System Sciences, 30(2):
162–178, 1985.
Neelakantan R. Krishnaswami, Pierre Pradic, and Nick Benton. Integrating
linear and dependent types. SIGPLAN Notices, 50(1):17–30, January 2015.
doi:10.1145/2775051.2676969.
Samuel A Kutin. Shor’s algorithm on a nearest-neighbor machine. arXiv preprint
quant-ph/0609001, 2006.
Leonidas Lampropoulos. Random Testing for Language Design. PhD thesis, Univer-
sity of Pennsylvania, 2018.
Leonidas Lampropoulos and Benjamin C. Pierce. QuickCHick: Property-Based Test-
ing In Coq. Software Foundations series, volume 4. Electronic textbook, August
2018. Version 1.0. https://softwarefoundations.cis.upenn.edu/qc-current/
index.html.
Daan Leijen and Erik Meijer. Domain specific embedded compilers. SIGPLAN Not.,
35(1):109–122, December 1999. doi:10.1145/331963.331977.
Yangjia Li and Mingsheng Ying. Algorithmic analysis of termination problems for
quantum programs. Proceedings of the ACM on Programming Languages, 2(POPL):
35, 2018.
205
Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev. Enriching a
linear/non-linear lambda calculus: A programming language for string diagrams.
In Proceedings of the 33rd Annual IEEE Symposium on Logic in Computer Science,
LICS 2018, 2018.
Tao Liu, Yangjia Li, Shuling Wang, Mingsheng Ying, and Naijun Zhan. A the-
orem prover for quantum hoare logic and its applications. arXiv preprint
arXiv:1601.03835, 2016.
Assia Mahboubi, Enrico Tassi, Yves Bertot, and Georges Gonthier. Mathemat-
ical Components. 2016. Electronic resource, available from https://math-
comp.github.io/mcb/book.pdf.
Mohamed Yousri Mahmoud and Amy P Felty. Formal meta-level analysis framework
for quantum programming languages. Electronic Notes in Theoretical Computer
Science, 338:185–201, 2018.
Theodore Samuel Motzkin. Beiträge zur Theorie der linearen Ungleichungen. PhD
thesis, University of Basel, 1936.
Yunseong Nam, Neil J Ross, Yuan Su, Andrew M Childs, and Dmitri Maslov. Au-
tomated optimization of large quantum circuits with continuous parameters. npj
Quantum Information, 4(1):23, 2018.
Michael A Nielsen and Isaac L Chuang. Quantum computation and quantum infor-
mation. Cambridge university press, 2010.
206
Bernhard Ömer. Quantum programming in QCL. Master’s thesis, Institute of Infor-
mation Systems, Technical University of Vienna, 2000.
Luca Paolini and Margherita Zorzi. qPCF: A language for quantum circuit com-
putations. In International Conference on Theory and Applications of Models of
Computation, pages 455–469. Springer, 2017.
Luca Paolini, Luca Roversi, and Margherita Zorzi. Quantum programming made
easy. arXiv preprint arXiv:1711.00774, 2017.
Jennifer Paykin and Steve Zdancewic. The linearity monad. In Proceedings of the
10th ACM SIGPLAN International Symposium on Haskell, pages 117–132. ACM,
2017.
Jennifer Paykin, Robert Rand, and Steve Zdancewic. QWIRE: A core language for
quantum circuits. In Proceedings of the 44th ACM SIGPLAN Symposium on Prin-
ciples of Programming Languages, POPL 2017, pages 846–858, New York, NY,
USA, 2017. ACM. doi:10.1145/3009837.3009894.
207
John Preskill. Fault-tolerant quantum computation. In Introduction to quantum
computation and information, pages 213–269. World Scientific, 1998.
John Preskill. Quantum computing in the nisq era and beyond. arXiv preprint
arXiv:1801.00862, 2018.
Robert Rand and Arthur Azevedo de Amorim. Programs and proofs in the coq
proof assistant. Tutorial at Principles of Programming Languages, 2016. URL
http://www.cis.upenn.edu/~rrand/popl_2016/.
Robert Rand, Jennifer Paykin, and Steve Zdancewic. QWIRE practice: Formal ver-
ification of quantum circuits in Coq. In Proceedings 14th International Confer-
ence on Quantum Physics and Logic, QPL 2017, Nijmegen, The Netherlands,
3-7 July 2017., pages 119–132, 2017. doi:10.4204/EPTCS.266.8. URL https:
//doi.org/10.4204/EPTCS.266.8.
Robert Rand, Jennifer Paykin, Dong-Ho Lee, and Steve Zdancewic. ReQWIRE: Rea-
soning about reversible quantum circuits. In Proceedings of the 15th International
Conference on Quantum Physics and Logic, QPL 2018, Halifax, Nova Scotia, 3-7
June 2018, 2018a.
Robert Rand, Jennifer Paykin, and Steve Zdancewic. Phantom types for quantum
programs. The Fourth International Workshop on Coq for Programming Lan-
guages, January 2018b.
Robert Raussendorf and Hans J Briegel. Computational model for the one-way quan-
tum computer: Concepts and summary. arXiv preprint quant-ph/0207183, 2002.
Ran Raz and Avishay Tal. Oracle separation of BQP and PH. Electronic Col-
loquium on Computational Complexity (ECCC), 25:107, 2018. URL https:
//eccc.weizmann.ac.il/report/2018/107.
Mathys Rennela and Sam Staton. Classical control and quantum circuits in enriched
category theory. In Proceedings of the 33rd Conference on the Mathematical Foun-
dations of Programming Semantics, MFPS 2017, 2017.
208
Rigetti Computing. Pyquil documentation. URL http://pyquil.readthedocs.io/
en/latest/.
Francisco Rios and Peter Selinger. A categorical model for a quantum circuit descrip-
tion language. In Proceedings of the 14th International Conference on Quantum
Physics and Logic, QPL 2017, 2017.
Neil J. Ross. Algebraic and Logical Methods in Quantum Computation. PhD thesis,
Dalhousie University, 2015.
Amr Sabry, Benoît Valiron, and Juliana Kaizer Vizzotto. From symmetric pattern-
matching to quantum control. In International Conference on Foundations of
Software Science and Computation Structures, pages 348–364. Springer, 2018.
Mehdi Saeedi and Igor L Markov. Synthesis and optimization of reversible circuits—a
survey. ACM Computing Surveys (CSUR), 45(2):21, 2013.
Jeff W. Sanders and Paolo Zuliani. Quantum programming. In Proceedings of the 5th
International Conference on Mathematics of Program Construction, volume 1837
of Lecture Notes in Computer Science, pages 80–99, 2000.
Peter Selinger and Benoît Valiron. A lambda calculus for quantum computation with
classical control. Mathematical Structures in Computer Science, 16(03):527–552,
2006.
Peter Selinger and Benoît Valiron. A linear-non-linear model for a computational call-
by-value lambda calculus. In Proceedings of the Eleventh International Conference
on Foundations of Software Science and Computation Structures, FOSSACS 2008,
Springer Lecture Notes in Computer Science 4962, pages 81–96, Budapest, Hungary,
April 2008.
Peter Selinger and Benoît Valiron. Quantum lambda calculus. In Simon Gay and Ian
Mackie, editors, Semantic Techniques in Quantum Computation, pages 135–172.
Cambridge University Press, 2009.
209
Yaoyun Shi. Both toffoli and controlled-not need little help to do universal quantum
computing. Quantum Information & Computation, 3(1):84–92, 2003.
Peter W. Shor. Algorithms for quantum computation: Discrete logarithms and fac-
toring. In Foundations of Computer Science, 1994 Proceedings., 35th Annual Sym-
posium on, pages 124–134. IEEE, 1994.
Safat Siddiqui, Mohammed Jahirul Islam, and Omar Shehab. Five quantum algo-
rithms using Quipper. arXiv preprint arXiv:1406.4481, 2014.
Jonathan M. Smith, Julien Neil Ross, Peter Selinger, and Benoît Valiron. Quip-
per: Concrete resource estimation in quantum algorithms. In Proceedings of the
Twelfth Workshop on Quantitative Aspects of Programming Languages and Systems
(QAPL), April 2014. URL http://arxiv.org/abs/1412.0625.
Robert S Smith, Michael J Curtis, and William J Zeng. A practical quantum instruc-
tion set architecture. arXiv preprint arXiv:1608.03355, 2016.
Damian S. Steiger, Thomas Häner, and Matthias Troyer. Projectq: an open source
software framework for quantum computing. Quantum, 2:49, 2018.
Krysta Svore, Alan Geller, Matthias Troyer, John Azariah, Christopher Granade,
Bettina Heim, Vadym Kliuchnikov, Mariia Mykhailova, Andres Paz, and Martin
Roetteler. Q#: Enabling scalable quantum computing and development with a
high-level dsl. In Proceedings of the Real World Domain Specific Languages Work-
shop 2018, page 7. ACM, 2018.
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bharga-
van, and Jean Yang. Secure distributed programming with value-dependent types.
In ACM SIGPLAN Notices, volume 46, pages 266–278. ACM, 2011.
210
Yasuhiro Takahashi and Noboru Kunihiro. A quantum circuit for shor’s factoring
algorithm using 2n+ 2 qubits. Quantum Information & Computation, 6(2):184–
192, 2006.
André van Tonder. A lambda calculus for quantum computation. SIAM Journal of
Computation, 33(5):1109–1135, 2004.
André van Tonder and Miquel Dorca. Quantum computation, categorical semantics
and linear logic. arXiv preprint quant-ph/0312174, 2003.
Vlatko Vedral, Adriano Barenco, and Artur Ekert. Quantum networks for elementary
arithmetic operations. Physical Review A, 54(1):147, 1996.
Juliana Kaizer Vizzotto, André Rauber Du Bois, and Amr Sabry. The arrow calculus
as a quantum programming language. In Hiroakira Ono, Makoto Kanazawa, and
Ruy de Queiroz, editors, Proccedings of Logic, Language, Information and Compu-
tation: 16th International Workshop, WoLLIC 2009, pages 379–393. Springer Berlin
Heidelberg, June 2009a. doi:10.1007/978-3-642-02261-6_30.
Juliana Kaizer Vizzotto, Giovani Rubert Librelotto, and Amr Sabry. Reasoning about
general quantum programs over mixed states. In Marcel Vinícius Medeiros Oliveira
and Jim Woodcock, editors, Formal Methods: Foundations and Applications: 12th
Brazilian Symposium on Formal Methods, SBMF 2009 Gramado, Brazil, August
19-21, 2009 Revised Selected Papers, pages 321–335, Berlin, Heidelberg, 2009b.
Springer Berlin Heidelberg. doi:10.1007/978-3-642-10452-7_22.
Juliana Kaizer Vizzotto, Bruno Crestani Calegaro, and Eduardo Kessler Piveta. A
double effect λ-calculus for quantum computation. In André Rauber Du Bois and
Phil Trinder, editors, Programming Languages, volume 8129 of Lecture Notes in
Computer Science, pages 61–74, Berlin, Heidelberg, 2013. Springer Berlin Heidel-
berg. doi:10.1007/978-3-642-40922-6_5.
John Watrous. Succinct quantum proofs for properties of finite groups. In Foundations
of Computer Science, 2000. Proceedings. 41st Annual Symposium on, pages 537–
546. IEEE, 2000.
211
Dave Wecker and Krysta M Svore. LIQUiD: A software design architecture and
domain-specific language for quantum computing. arXiv:1402.4467 [quant-ph],
2014.
Mingsheng Ying, Nengkun Yu, and Yuan Feng. Defining Quantum Control Flow.
ArXiv e-prints, September 2012.
Mingsheng Ying, Nengkun Yu, and Yuan Feng. Alternation in quantum programming:
From superposition of data to superposition of programs. CoRR, abs/1402.5172,
2014. URL http://arxiv.org/abs/1402.5172.
Mingsheng Ying, Shenggang Ying, and Xiaodi Wu. Invariants of quantum programs:
characterisations and generation. In Proceedings of the 44th ACM SIGPLAN Sym-
posium on Principles of Programming Languages, pages 818–832. ACM, 2017.
Christof Zalka. Shor’s algorithm with fewer (pure) qubits. arXiv preprint quant-
ph/0601097, 2006.
212