Front Cover
Foundations of Quantum Programming
Copyright
Contents
Biography
Prof. Mingsheng Ying (1964β)
Preface to the second edition
Preface to the first edition
Acknowledgements
1 Introduction
1.1 From classical programming to quantum programming β βEverything old is new again!β
1.1.1 Quantum programming languages and compilers
1.1.2 Semantics and type systems of quantum programs
1.1.3 Verification and analysis of quantum programs
1.2 Approaches to quantum programming
1.2.1 Classical parallel programming
1.2.2 Superposition-of-data versus superposition-of-programs
1.2.3 Classical and quantum parallelisms working together
1.3 Structure of the book
Reading the book
Teaching from the book
I Preliminaries
2 Quantum mechanics
2.1 Hilbert spaces
2.2 Linear operators
2.2.1 Unitary transformations
2.3 Quantum measurements
2.3.1 Observables and projective measurements
2.3.2 Noncommutativity and uncertainty principle
2.4 Tensor products of Hilbert spaces
2.4.1 Nocloning of quantum data
2.5 Density operators
2.6 Quantum operations
2.7 Bibliographic remarks and further readings
3 Models of quantum computation
3.1 Quantum circuits
3.1.1 Basic definitions
3.1.2 One-qubit gates
3.1.3 Controlled gates
3.1.4 Quantum multiplexor
3.1.5 Universality of gates
3.1.6 Measurements in circuits
3.2 Quantum Turing machines
3.3 Quantum random access stored-program machines
3.4 Bibliographic remarks and further readings
4 Quantum algorithms and communication protocols
4.1 Quantum parallelism and interference
4.2 Quantum algorithms based on Hadamard transforms
4.2.1 DeutschβJozsa algorithm
4.2.2 BernsteinβVazirani algorithm
4.2.3 Simon algorithm
4.3 Quantum Fourier transform
4.3.1 Phase estimation
4.4 Grover search algorithm
4.5 Quantum walks
4.5.1 Quantum-walk search algorithm
4.6 Basic quantum communication protocols
4.6.1 Quantum teleportation
4.6.2 Superdense coding
4.7 Bibliographic remarks and further readings
II Sequential quantum programs
5 Quantum while-programs
5.1 Syntax
5.2 Operational semantics
5.3 Denotational semantics
5.3.1 Basic properties
5.3.2 Quantum domains
5.3.3 Semantic functions of loops
5.3.4 Change and access of quantum variables
5.3.5 Termination and divergence
5.3.6 Semantic functions as quantum operations
5.4 Illustrative example: Grover search
5.5 Classical recursion in quantum programming
5.5.1 Syntax
5.5.2 Operational semantics
5.5.3 Denotational semantics
5.5.4 Fixed point characterisation
5.6 Adding classical variables
5.7 Bibliographic remarks and further readings
6 Quantum Hoare logic
6.1 Quantum predicates
6.1.1 Quantum weakest preconditions
6.1.2 Commutativity of quantum predicates
6.2 Correctness formulas of quantum programs
6.3 Weakest preconditions of quantum programs
6.4 Proof system for partial correctness
6.5 Proof system for total correctness
6.6 An illustrative example: verification of Grover search
6.7 Auxiliary inference rules
6.8 Bibliographic remarks and further readings
III Verification and analysis
7 Verification of quantum programs
7.1 Architecture of a quantum program verifier
7.1.1 Generating verification conditions
7.1.2 Proving verification conditions
7.1.3 Validity of the verifier
7.2 Localisation of correctness reasoning
7.3 Birkhoffβvon Neumann quantum logic
7.3.1 Orthomodular lattice of closed subspaces
7.3.2 Propositional quantum logic
7.3.3 First-order quantum logic
7.3.4 Effect algebra and unsharp quantum logic
7.4 Quantum logic with quantum variables
7.4.1 Syntax
7.4.2 Semantics
7.4.3 Proof system
7.5 Quantum logic as an assertion logic
7.5.1 Reformulating syntax and semantics of quantum programs
7.5.2 Quantum Hoare logic combined with quantum logic
7.5.3 Adaptation rules for quantum programs
7.6 An effect calculus as assertion logic
7.6.1 A calculus of quantum effects
7.6.2 Quantum Hoare logic combined with effect calculus
7.7 Discussion
7.8 Bibliographic remarks and further readings
8 Analysis of quantum programs
8.1 Control flows of quantum programs
8.1.1 Superoperator-valued transition systems
8.1.2 Quantum programs as transition systems
8.2 Invariants and their generation
8.2.1 Basic definitions
8.2.2 Partial correctness
8.2.3 Inductive assertion maps
8.2.4 Generation of inductive invariants
8.2.5 An illustrative example
8.3 Termination analysis β ranking functions
8.3.1 Termination problems
8.3.2 Ranking functions and termination theorems
8.3.3 Realisability and synthesis of ranking functions
8.4 Termination analysis β reachability
8.4.1 Termination of quantum while-loops
8.4.2 Quantum graph theory
8.4.3 Decomposition of the state Hilbert space
8.4.4 Reachability analysis of quantum Markov chains
8.5 Quantum abstract interpretation
8.5.1 Basics of abstract interpretation
8.5.2 Restriction and extension of projections
8.5.3 Abstraction of quantum states
8.5.4 Abstraction of quantum operations
8.6 Bibliographic remarks and further readings
IV Parallel and distributed quantum programs
9 Parallel quantum programs
9.1 Syntax of disjoint parallel quantum programs
9.2 Semantics of disjoint parallel quantum programs
9.2.1 Operational semantics
9.2.2 Denotational semantics
9.3 Proof system for disjoint parallel quantum programs
9.3.1 Sequentialisation rule
9.3.2 Tensor product of quantum predicates
9.3.3 Separable quantum predicates
9.3.4 Entangled quantum predicates
9.3.5 Auxiliary variables
9.3.6 Transferring separable predicates to entangled
9.3.7 Completeness of the auxiliary variables method
9.3.8 Completeness of the entanglement transformation method
9.4 Syntax of parallel quantum programs with shared variables
9.5 Semantics of parallel quantum programs with shared variables
9.6 Reasoning about parallel quantum programs with shared variables
9.6.1 A rule for component quantum programs
9.6.2 Proof outlines
9.6.3 Interference freedom
9.6.4 A rule for parallel composition of quantum programs with shared variables
9.7 Discussions
9.8 Bibliographic remarks and further readings
10 Distributed quantum programs
10.1 Quantum process algebra qCCS
10.1.1 Syntax
10.1.2 Operational semantics
10.1.3 Examples
10.1.4 Properties of transitions
10.2 Bisimulations between quantum processes
10.2.1 Basic definitions
10.2.2 Algebraic laws
10.2.3 Congruence
10.2.4 Recursion
10.2.5 Strong reduction-bisimilarity
10.2.6 Weak bisimulations
10.3 Approximate bisimulations between quantum processes
10.4 Adding classical variables
10.4.1 Syntax
10.4.2 Operational semantics
10.4.3 Examples
10.4.4 Bisimulations
10.5 Bibliographic remarks and further readings
V Quantum control flows
11 Quantum case statements
11.1 Case statements: from classical to quantum
11.2 QuGCL: a language with quantum case statements
11.3 Guarded compositions of quantum operations
11.3.1 Guarded composition of unitary operators
11.3.2 Operator-valued functions
11.3.3 Guarded composition of operator-valued functions
11.3.4 Guarded composition of quantum operations
11.4 Semantics of QuGCL programs
11.4.1 Classical states
11.4.2 Semi-classical semantics
11.4.3 Purely quantum semantics
11.4.4 Weakest precondition semantics
11.4.5 An example
11.5 Quantum choice
11.5.1 Choices: from classical to quantum via probabilistic
11.5.2 Quantum implementation of probabilistic choice
11.6 Algebraic laws
11.7 A new paradigm of quantum programming β superposition-of-programs
11.8 Illustrative examples
11.8.1 Quantum walks
11.8.2 Quantum phase estimation
11.8.3 Linear combination of unitary operators
11.9 Discussions
11.9.1 Coefficients in guarded compositions
11.9.2 Quantum case statements guarded by subspaces
11.10 Bibliographic remarks and further readings
12 Quantum recursion
12.1 Syntax of quantum recursive programs
12.2 Motivating examples: recursive quantum walks
12.2.1 Specification of recursive quantum walks
12.2.2 How to solve recursive quantum equations?
12.3 Second quantisation
12.3.1 Multiple-particle states
12.3.2 Fock spaces
12.3.3 Observables in Fock spaces
12.3.4 Evolution in Fock spaces
12.3.5 Creation and annihilation of particles
12.4 Solving recursive equations in the free Fock space
12.4.1 A domain of operators on the free Fock space
12.4.2 Semantic functionals of program schemes
12.4.3 Fixed point semantics
12.4.4 Syntactic approximation
12.5 Recovering symmetry and antisymmetry
12.5.1 Symmetrisation functional
12.5.2 Symmetrisation of semantics of quantum recursion
12.6 Principal system semantics of quantum recursion
12.7 Illustrative examples: revisit recursive quantum walks
12.8 Quantum while-loops (with quantum control)
12.9 Bibliographic remarks and further readings
VI Prospects
13 Prospects
13.1 Quantum machines and quantum programs
13.2 Implementation of quantum programming languages
13.3 Functional quantum programming
13.4 Categorical semantics of quantum programs
13.5 From concurrent quantum programs to quantum concurrency
13.6 Entanglement in quantum programming
13.7 Model-checking quantum systems
13.8 Programming techniques for quantum machine learning
13.9 Quantum programming applied to physics
A Omitted proofs in the main text
A.1 Omitted proofs in Chapter 5
A.2 Omitted proofs in Chapter 6
A.3 Omitted proofs in Chapter 7
A.3.1 Technical preparations
A.3.2 Proofs of the lemmas in Section 7.4.2
A.3.3 Substitutions and term-adjoint formulas
A.3.4 Proof of the soundness of logic QL (Theorem 7.5)
A.3.5 Proof of the soundness of adaptation rules (Theorem 7.8)
A.3.6 Proof of negation normal forms (Theorem 7.9)
A.4 Omitted proofs in Chapter 8
A.4.1 Proofs of the lemmas in Section 8.4
A.4.2 Proofs of the lemmas in Section 8.5
A.5 Omitted proofs in Chapter 9
A.5.1 Proof of the lemmas in Section 9.2
A.5.2 Proofs of facts in Section 9.3
A.5.3 Proof of Theorem 9.3
A.5.4 Proof of Theorem 9.6
A.5.5 Proof of Theorem 9.7
A.6 Omitted proofs in Chapter 10
A.6.1 Proofs of the lemmas in Section 10.1.4
A.6.2 Proofs of the results in Section 10.2.3
A.6.3 Proofs of the results in Section 10.2.4
A.6.4 Proof of Theorem 10.4.2.d
A.7 Omitted proofs in Chapter 11
A.7.1 Proof of Lemma 11.2
A.7.2 Proof of Proposition 11.1
A.7.3 Proof of Theorem 11.1
A.7.4 Proofs of the theorems in Section 11.6
References
Index
Back Cover