Kooperativer Bibliotheksverbund

UID:

Umfang: 1 online resource (474 pages)

Ausgabe: 2nd ed.

ISBN: 9780443159435

Inhalt: 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.

Anmerkung: 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.

Weitere Ausg.: ISBN 9780443159428

Sprache: Englisch