Geodesic
Natural quantum operational semantics with predicates
International Journal of Applied Mathematics and Computer Science, Tome 18 (2008) no. 3, pp. 341-359.

Voir la notice de l'article provenant de la source Library of Science

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.
Keywords: quantum computation, predicate notion for quantum programs, quantum labelled transition systems
Mots-clés : obliczenia kwantowe, predykat, program kwantowy, kwantowy system przejścia 
@article{IJAMCS_2008_18_3_a7,
     author = {Sawerwain, M. and Gierelak, R.},
     title = {Natural quantum operational semantics with predicates},
     journal = {International Journal of Applied Mathematics and Computer Science},
     pages = {341--359},
     publisher = {mathdoc},
     volume = {18},
     number = {3},
     year = {2008},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/IJAMCS_2008_18_3_a7/}
}
TY  - JOUR
AU  - Sawerwain, M.
AU  - Gierelak, R.
TI  - Natural quantum operational semantics with predicates
JO  - International Journal of Applied Mathematics and Computer Science
PY  - 2008
SP  - 341
EP  - 359
VL  - 18
IS  - 3
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/IJAMCS_2008_18_3_a7/
LA  - en
ID  - IJAMCS_2008_18_3_a7
ER  - 
%0 Journal Article
%A Sawerwain, M.
%A Gierelak, R.
%T Natural quantum operational semantics with predicates
%J International Journal of Applied Mathematics and Computer Science
%D 2008
%P 341-359
%V 18
%N 3
%I mathdoc
%U http://geodesic.mathdoc.fr/item/IJAMCS_2008_18_3_a7/
%G en
%F IJAMCS_2008_18_3_a7
Sawerwain, M.; Gierelak, R. Natural quantum operational semantics with predicates. International Journal of Applied Mathematics and Computer Science, Tome 18 (2008) no. 3, pp. 341-359. http://geodesic.mathdoc.fr/item/IJAMCS_2008_18_3_a7/

[1] Aceto L. (1994). GSOS and finite labelled transition systems, Theoretical Computer Science 131(1): 181-195.

[2] de Bakker J. W., de Roever W. P. (1972). A calculus for recursive programs schemes, in: M. Nivat (Ed.), Automata, Languages, and Programming, North-Holland, Amsterdam, pp. 167-196.

[3] de Bakker J. W., Meertens, L. G. L. T. (1975). On the completeness of the inductive assertion method, Journal of Computer and Systems Sciences 11(3): 323-357.

[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 Letters 70(13): 1895-1899.

[5] Birkhoff G. and von Neumann J. (1936). The logic of quantum mechanics, Annals of Mathematics 37(4): 823-843.

[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.

[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 Letters 80(6): 1121-1125.

[9] Bouwmeester D., Pan J.W., Mattle K., Eibl M., Weinfurter H. and Zeilinger A. (1997). Experimental quantum teleportation, Nature 390(6660): 575-579.

[10] Choi M.D. (1975). Completely positive linear maps on complex matrices, Linear Algebra and Its Applications 10(3): 285-290.

[11] Coecke B. and Martin K. (2002). A partial order on classical and quantum states, Technical report, PRG-RR-02-07, Oxford University.

[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.

[13] Dijkstra E. W. (1976). A Discipline of Programming, Prentice-Hall, Englewood Cliffs, NJ.

[14] D'Hondt E. and Panangaden P. (2006). Quantum weakest preconditions, Mathematical Structures in Computer Science 16(3): 429-451.

[15] Gielerak R. and Sawerwain M. (2007). Generalised quantum weakest preconditions, available at: arXiv:quant-ph/0710.5239v1.

[16] Gleason A. M. (1957). Measures on the closed subspaces of a Hilbert space, Journal of Mathematics and Mechanics 6(4): 885-893.

[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.

[18] Hirvensalo M. (2001). Quantum Computing, Springer-Verlag, Berlin.

[19] Hoare C. (1969). An axiomatic basis for computer programming, Communications of the ACM 12(10): 576-583.

[20] Jozsa R. (2005). An introduction to measurement based quantum computation, available at: arXiv:quant-ph/0508124.

[21] Kraus K. (1983). State, Effects, and Operations, Springer, Berlin.

[22] Kak S. (2003). Teleportation protocols requiring only one classical bit, available at: arXiv:quant-ph/0305085v4.

[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 Zeitschrift 38(1): 177--216.

[25] Mlnařík H. (2006): LanQ-Operational Semantics of Quantum Programming Language LanQ, Technical report FIMURS-2006-10, available at: http://www.muni.cz/research/publications/706560.

[26] Mauerer W. (2005). Semantics and simulation of communication in quantum programming, M.Sc. thesis, University Erlangen-Nuremberg Erlangen, Nürnberg, see: arXiv:quant-ph/0511145.

[27] Ömer B. (2005). Classical concepts in quantum programming, International Journal of Theoretical Physics, 44(7): 943-955, see: arXiv:quant-ph/0211100.

[28] Peres A. (1995). Quantum Theory: Concepts and Methods, Kluwer Academic Publishers, Dordrecht.

[29] Plotkin G.D. (2004). A structural approach to operational semantics, Journal of Logic and Algebraic Programming 60: 17-139.

[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: arXiv:quant-ph/0611133.

[31] Rüdiger R. (2007). Quantum programming languages: An introductory overview, The Computer Journal 50(2): 134-150.

[32] Raussendorf R., Briegel H.J. (2001). A one-way quantum computer, Physical Review Letters 86(22): 5188-5191, see: arXiv:quant-ph/0010033.

[33] Raussendorf R., Browne D.E., Briegel H.J. (2003). Measurement-based quantum computation with cluster states, Physical Review A, 68(2), 022312, see: arXiv:quant-ph/0301052.

[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. (Eds.), 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 Science 14(5): 527-586.

[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 Physics 56(2): 271-290, see: arXiv:math-ph/0505032.

[38] Shor P. (2004). Progress in quntum algorithms, Quantum Information Processing 3(1): 5-13.