Skip to main content Accessibility help

We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.

Close cookie message
×
Hostname: page-component-745bb68f8f-g4j75 Total loading time: 0 Render date: 2025-02-06T18:52:47.270Z Has data issue: false hasContentIssue false

8 - Predicate Transformer Semantics of Quantum Programs

Published online by Cambridge University Press:  05 July 2014

By
Mingsheng Ying ,
Runyao Duan ,
Yuan Feng  and
Zhengfeng Ji
Edited by
Simon Gay  and
Ian Mackie
Mingsheng Ying
Affiliation:
University of Technology Sydney
Runyao Duan
Affiliation:
University of Technology Sydney
Yuan Feng
Affiliation:
University of Technology Sydney
Zhengfeng Ji
Affiliation:
Perinmeter Institute for Theoretical Physics
Simon Gay
Affiliation:
University of Glasgow
Ian Mackie
Affiliation:
Imperial College London
Get access

Summary

Abstract

This chapter presents a systematic exposition of predicate transformer semantics for quantum programs. It is divided into two parts: The first part reviews the state transformer (forward) semantics of quantum programs according to Selinger's suggestion of representing quantum programs by superoperators and elucidates D'Hondt-Panangaden's theory of quantum weakest preconditions in detail. In the second part, we develop a quite complete predicate transformer semantics of quantum programs based on Birkhoff-von Neumann quantum logic by considering only quantum predicates expressed by projection operators. In particular, the universal conjunctivity and termination law of quantum programs are proved, and Hoare's induction rule is established in the quantum setting.

8.1 Introduction

In the mid-1990s Shor and Grover discovered, respectively, the famous quantum factoring and searching algorithms. Their discoveries indicated that in principle quantum computers offer a way to accomplish certain computational tasks much more efficiently than classical computers, and thus stimulated an intensive investigation in quantum computation. Since then a substantial effort has been made to develop the theory of quantum computation, to find new quantum algorithms, and to exploit the physical techniques needed in building functional quantum computers, including in particular fault tolerance techniques.

Currently, quantum algorithms are expressed mainly at the very low level of quantum circuits. In the history of classical computation, however, it was realized long time ago that programming languages provide a technique that allows us to think about a problem that we intend to solve in a high-level, conceptual way, rather than the details of implementation.

Type
Chapter
Information
Semantic Techniques in Quantum Computation , pp. 311 - 360
Publisher: Cambridge University Press
Print publication year: 2009

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Birkhoff, G., and von Neumann, J. (1936) The logic of quantum mechanics. Annals of Mathematics 37:823–843.CrossRefGoogle Scholar
Bruns, G., and Harding, J. (2000) Algebraic aspects of orthomodular lattices. In Coecke, B., Moore, D., and Wilce, A., editors, Current Research in Operational Quantum Logic: Algebras, Categories, Languages, pages 37–65. Kluwer.Google Scholar
Butler, M. J., and Hartel, P. H. (1999) Reasoning about grover's quantum search algorithms using probabilistic wp. ACM Transactions on Programming Languages and Systems 21:417–130.CrossRefGoogle Scholar
D'Hondt, E., and Panangaden, P. (2006) Quantum weakest preconditions. Mathematical Structures in Computer Science 16:429–451.CrossRefGoogle Scholar
Diestel, J., and Uhl, J. J. Jr. (1977) Vector Measures. American Mathematical Society.CrossRefGoogle Scholar
Dijkstra, E. W. (1976) A Discipline of Programming. Prentice-Hall.Google Scholar
Dijkstra, E. W., and Scholten, C. S. (1990) Predicate Calculus and Program Semantics. SpringerVerlag.CrossRefGoogle Scholar
Dvurečenskij, A. (1993) Gleason's Theorem and Its Applications. Kluwer.CrossRefGoogle Scholar
Feng, Y., Duan, R. Y., Ji, Z. F., and Ying, M. S. (2007) Proof rules for correctness of quantum programs. Theoretical Computer Science 386:151–166.CrossRefGoogle Scholar
Gay, S. J. (2006) Quantum programming languages: survey and bibliography. Mathematical Structures in Computer Science 16:581–600.CrossRefGoogle Scholar
Gudder, S. (1996) Lattice properties of quantum effects. Journal of Mathematical Physics 37:2637-2642.CrossRefGoogle Scholar
Hesselink, W. H. (1992) Programs, Recursion and Unbounded Choice: Predicate-Transformation Semantics and Transformation Rules. Cambridge University Press.CrossRefGoogle Scholar
Hoare, C. A. R. (1971) Procedures and parameters: an axiomatic approach. In Engeler, E., editor, Symposium on Semantics of Algorithmic Languages, pages 102–116. Lecture Notes in Mathematics 188, Springer-Verlag.Google Scholar
Kadison, R. (1951) Order properties of bounded self-adjoint operators. Proceedings of American Mathical Society 34:505–510.Google Scholar
Kalmbach, G. (1983) Orthomodular Lattices. Academic Press.Google Scholar
Knill, E. (1996) Conventions for quantum pseudocode. Technical Report LAUR-96-2724, Los Alamos National Laboratory.CrossRefGoogle Scholar
Kozen, D. (1981) Semantics of probabilistic programs. Journal of Computer and System Sciences 22:328-350.CrossRefGoogle Scholar
Kraus, K. (1983) States, Effects and Operations: Fundamental Notions of Quantum Theory. Springer-Verlag.CrossRefGoogle Scholar
Lloyd, J. W. (1987) Foundations of Logic Programming. Springer-Verlag.CrossRefGoogle Scholar
Morgan, C. C., McIver, A. K., and Seidel, K. (1996) Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems 18:325–353.CrossRefGoogle Scholar
Nielsen, M. A., and Chuang, I. L. (2000) Quantum Computation and Quantum Information. Cambridge University Press.Google Scholar
Ömer, B. (2003) Structured Quantum Programming. Ph.D. thesis, Technicla Unviersity of Vienna.Google Scholar
Prugovečki, E. (1981) Quantum Mechanics in Hilbert Space. Academic Press.Google Scholar
Putnam, C. R. (1967) Commutation Properties of Hilbert Space Operators and Related Topics. Springer-Verlag.CrossRefGoogle Scholar
Sanders, J. W., and Zuliani, P. (2000) Quantum programming. In Proceedings of Mathematics of Program Construction 2000, pages 80–99. LNCS 1837.Google Scholar
Scott, D. S. (1970) Outline of a mathematical theory of computation. In Proceedings of 4th Annual Princeton Conference on Information Sciences and Systems, pages 169–176.Google Scholar
Selinger, P. (2004) Towards a quantum programming language. Mathematical Structures in Computer Science 14:527–586.CrossRefGoogle Scholar
Takeuti, G. (1981) Quantum set theory. In Beltrametti, E., and Fraassen, B. C. v., editors, Current Issues in Quantum Logics, pages 303–322. Plenum.Google Scholar
Varadarajan, V S. (1985) Geometry of Quantum Theory. Springer-Verlag.Google Scholar
Ying, M. S. (2000) Automata theory based on quantum logic (i), (ii). International Journal of Theoretical Physics 39:985-995; 2545-2557.Google Scholar
Ying, M. S. (2005) A theory of computation based on quantum logic (i). Theoretical Computer Science 344:134–207.CrossRefGoogle Scholar
Ying, M. S. (2007) Quantum logic and automata theory. In Engesser, K., Gabbay, D., and Lehmann, D., editors, Handbook of Quantum Logic and Quantum Structures, pages 619–754. Elsevier.Google Scholar
Ying, M. S., Chen, J. X., Feng, Y., and Duan, R. Y. (2007) Commputativity of quantum weakest preconditions. Information Processing Letters 104:152–158.CrossRefGoogle Scholar
Ying, M. S., and Feng, Y. (2006) Quantum loop programs. http://arxiv.org/abs/quant-ph/0605218.Google Scholar
Zuliani, P. (2004) Non-deterministic quantum programming. In Selinger, P., editor, Proceedings of the 2nd International Workshop on Quantum Programming Languages, pages 179–195. TUCS General Publication No 33, Turku Centre for Computer Science, Turku, Finland.Google Scholar

Save book to Kindle

To save this book to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.

Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.

Find out more about the Kindle Personal Document Service.

Available formats
×

Save book to Dropbox

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Dropbox.

Available formats
×

Save book to Google Drive

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Google Drive.

Available formats
×