Foundations of Quantum Programming.

Format:

Book

Author/Creator:

Ying, Mingsheng.

Language:

English

Subjects (All):

Quantum computers.

Programming languages (Electronic computers).

Physical Description:

1 online resource (474 pages)

Edition:

2nd ed.

Place of Publication:

San Diego : Elsevier Science & Technology, 2024.

Summary:

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, computer-aided drug design, generative chemistry, and any scientific or enterprise application that requires computation speed or reach beyond the limits of current conventional computer systems. Foundations of Quantum Programming, Second Edition discusses how programming methodologies and technologies developed for current computers can be extended for quantum computers, along with new programming methodologies and technologies that can effectively exploit the unique power of quantum computing. The Second Edition includes two new chapters describing programming models and methodologies for parallel and distributed quantum computers. The author has also included two new chapters to introduce Quantum Machine Learning and its programming models - parameterized and differential quantum programming. In addition, the First Edition's preliminaries chapter has been split into three chapters, with two sections for quantum Turing machines and random access stored program machines added to give the reader a more complete picture of quantum computational models. Finally, several other new techniques are introduced in the Second Edition, including invariants of quantum programs and their generation algorithms, and abstract interpretation of quantum programs.

Contents:

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.

Notes:

Description based on publisher supplied metadata and other sources.

ISBN:

9780443159435

OCLC:

1432733931