Foundations of Quantum Programming
Quantum computers promise dramatic advantages in processing speed over currently available computer systems. Quantum computing offers great promise in a wide variety of computing and scientific research, including Quantum cryptography, machine learning, computational biology, renewable energy, compu...
| Autor principal: | |
|---|---|
| Formato: | Libro electrónico |
| Idioma: | Inglés |
| Publicado: |
San Diego :
Elsevier Science & Technology
2024.
|
| Edición: | 2nd ed |
| Materias: | |
| Ver en Biblioteca Universitat Ramon Llull: | https://discovery.url.edu/permalink/34CSUC_URL/1im36ta/alma991009816677206719 |
Tabla de Contenidos:
- 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.
