×

Natural quantum operational semantics with predicates. (English) Zbl 1200.68118

Summary: A general definition of a quantum predicate and quantum labelled transition systems for finite quantum computation systems is presented. The notion of a quantum predicate as a positive operator-valued measure is developed. The main results of this paper are a theorem about the existence of generalised predicates for quantum programs defined as completely positive maps and a theorem about the existence of a GSOS format for quantum labelled transition systems. The first theorem is a slight generalisation of D’Hondt and Panagaden’s theorem about the quantum weakest precondition in terms of discrete support positive operator-valued measures.

MSC:

68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q55 Semantics in the theory of computing
81P68 Quantum computation

Software:

QPL; LanQ
PDFBibTeX XMLCite
Full Text: DOI EuDML

References:

[1] Aceto L. (1994). GSOS and finite labelled transition systems, Theoretical Computer Science131(1): 181-195. · Zbl 0822.68060 · doi:10.1016/0304-3975(94)90094-9
[2] de Bakker J. W., de Roever W. P. (1972). A calculus for recursive programs schemes, in: M. Nivat , Automata, Languages, and Programming, North-Holland, Amsterdam, pp. 167-196. · Zbl 0238.68006
[3] de Bakker J. W., Meertens L. G. L. T. (1975). On the completeness of the inductive assertion method, Journal of Computer and Systems Sciences11(3): 323-357. · Zbl 0353.68040 · doi:10.1016/S0022-0000(75)80056-0
[4] Bennett C. H., Brassard G., Crepeau C., Jozsa R., Peres A. and Wooters W. K. (1993). Teleporting an unknown state via dual classical and Einstein-Podolsky-Rosen channels, Physical Review Letters70(13): 1895-1899. · Zbl 1051.81505 · doi:10.1103/PhysRevLett.70.1895
[5] Birkhoff G. and von Neumann J. (1936). The logic of quantum mechanics, Annals of Mathematics37(4): 823-843. · Zbl 0015.14603 · doi:10.2307/1968621
[6] Bloom B. (1989): Ready Simulation, Bisimulation, and the Semantics of CCS-like Languages, Ph.D. thesis, Massachusetts Institute of Technology.
[7] Bloom B., Istrail S., Meyer A. R. (1989). Bisimulation can’t be traced: Preliminary report, Conference Record of the 15th Annual ACM Symposium on Principles of Programming Languages, San Diego, CA, USA, pp. 229-239. · Zbl 0886.68027 · doi:10.1145/200836.200876
[8] Boschi D., Branca S., de Martini F., Hardy L. and Popescu S. (1998). Experimental realization of teleporting an unknown pure quantum state via dual classical and Einstein-Podolsky-Rosen channels, Physical Review Letters80(6): 1121-1125. · Zbl 0947.81004 · doi:10.1103/PhysRevLett.80.1121
[9] Bouwmeester D., Pan J. W., Mattle K., Eibl M., Weinfurter H. and Zeilinger A. (1997). Experimental quantum teleportation, Nature390(6660): 575-579. · Zbl 1369.81006
[10] Choi M. D. (1975). Completely positive linear maps on complex matrices, Linear Algebra and Its Applications10(3): 285-290. · Zbl 0327.15018 · doi:10.1016/0024-3795(75)90075-0
[11] Coecke B. and Martin K. (2002). A partial order on classical and quantum states, Technical report, PRG-RR-02-07, Oxford University. · Zbl 1253.81008 · doi:10.1007/978-3-642-12821-9_10
[12] Deutsch D. and Jozsa R. (1992). Rapid solutions of problems by quantum computation, Proceedings of the Royal Society of London A, 439(1907): 553-558. · Zbl 0792.68058 · doi:10.1098/rspa.1992.0167
[13] Dijkstra E. W. (1976). A Discipline of Programming, Prentice-Hall, Englewood Cliffs, NJ. · Zbl 0368.68005
[14] D’Hondt E. and Panangaden P. (2006). Quantum weakest preconditions, Mathematical Structures in Computer Science16(3): 429-451. · Zbl 1122.68058 · doi:10.1017/S0960129506005251
[15] Gielerak R. and Sawerwain M. (2007). Generalised quantum weakest preconditions, available at: · Zbl 1197.81047 · doi:10.1007/s11128-009-0151-8
[16] Gleason A. M. (1957). Measures on the closed subspaces of a Hilbert space, Journal of Mathematics and Mechanics6(4): 885-893. · Zbl 0078.28803
[17] Grover L. K. (1996). A fast quantum-mechanical algorithm for database search, Proceedings of the 28th Annual ACM Symposium on the Theory of Computing, Philadelphia, PA, USA, ACM Press, New York, NY, pp. 212-219. · Zbl 0922.68044
[18] Hirvensalo M. (2001). Quantum Computing, Springer-Verlag, Berlin. · Zbl 0976.68063
[19] Hoare C. (1969). An axiomatic basis for computer programming, Communications of the ACM12(10): 576-583. · Zbl 0179.23105 · doi:10.1145/363235.363259
[20] Jozsa R. (2005). An introduction to measurement based quantum computation, available at:
[21] Kraus K. (1983). State, Effects, and Operations, Springer, Berlin.
[22] Kak S. (2003). Teleportation protocols requiring only one classical bit, available at:
[23] Lalire M., Jorrand P. (2004). A process algebraic approach to concurrent and distributed quantum computation: Operational semantics, Proceedings of the 2nd International Workshop on Quantum Programming Languages, Turku, Finland, pp. 109-126.
[24] Löwner K. (1934): Über monotone Matrixfunktionen, Mathematische Zeitschrift38(1): 177-216. · Zbl 0008.11301 · doi:10.1007/BF01170633
[25] Mlnařík H. (2006): LanQ-Operational Semantics of Quantum Programming Language LanQ, Technical report FIMURS-2006-10, available at:
[26] Mauerer W. (2005). Semantics and simulation of communication in quantum programming, M. Sc. thesis, University Erlangen-Nuremberg Erlangen, Nürnberg, see:
[27] Ömer B. (2005). Classical concepts in quantum programming, International Journal of Theoretical Physics, 44(7): 943-955, see: · Zbl 1119.81316 · doi:10.1007/s10773-005-7071-x
[28] Peres A. (1995). Quantum Theory: Concepts and Methods, Kluwer Academic Publishers, Dordrecht. · Zbl 0867.00010
[29] Plotkin G. D. (2004). A structural approach to operational semantics, Journal of Logic and Algebraic Programming60: 17-139. · Zbl 1082.68062 · doi:10.1016/j.jlap.2004.05.001
[30] Raynal P. (2006). Unambiguous state discrimination of two density matrices in quantum information theory, Ph.D. thesis, Institut für Optik, Information und Photonik, Max Planck Forschungsgruppe, see:
[31] Rüdiger R. (2007). Quantum programming languages: An introductory overview, The Computer Journal50(2): 134-150.
[32] Raussendorf R., Briegel H. J. (2001). A one-way quantum computer, Physical Review Letters86(22): 5188-5191, see: · doi:10.1103/PhysRevLett.86.5188
[33] Raussendorf R., Browne D. E., Briegel H. J. (2003). Measurement-based quantum computation with cluster states, Physical Review A, 68(2), 022312, see: · doi:10.1103/PhysRevA.68.022312
[34] Sawerwain M., Gielerak R. and Pilecki J. (2006). Operational semantics for quantum computation, in: Wȩgrzyn S., Znamirowski L., Czachórski T., Kozielski S. , New Technologies in Computer Networks, WKiŁ, Warsaw, Vol. 1, pp. 69-77, (in Polish).
[35] Selinger P.: (2004): Towards a quantum programming language, Mathematical Structures in Computer Science14(5): 527-586. · Zbl 1085.68014 · doi:10.1017/S0960129504004256
[36] Selinger P.: (2004). Towards a semantics for higher order quantum computation, Proceedings of the 2nd International Workshop on Quantum Programming Languages, Turku, Finland, pp. 127-143.
[37] Sewell G.: (2005). On the mathematical structure of quantum measurement theory, Reports on Mathematical Physics56(2): 271-290, see: · Zbl 1086.81016 · doi:10.1016/S0034-4877(05)80074-6
[38] Shor P. (2004). Progress in quntum algorithms, Quantum Information Processing3(1): 5-13. · Zbl 1075.68602 · doi:10.1007/s11128-004-3878-2
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.