Generalhttp://hdl.handle.net/10453/1532015-03-03T17:21:10Z2015-03-03T17:21:10ZPredicate Transformer Semantics of Quantum ProgramsYing, MDuan, RFeng, YJi, Zhttp://hdl.handle.net/10453/129652014-11-24T06:04:48Z2010-01-01T00:00:00ZPredicate Transformer Semantics of Quantum Programs
Ying, M; Duan, R; Feng, Y; Ji, Z
Gay, S; Mackie, I
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 coujunctivity and termination law of quantum programs are proved, and Hoareâs induction rule is established in the quantum setting.
2010-01-01T00:00:00Z