Abstract
We define a dynamic logic for QASM (Quantum Assembly) programming language, a language that requires the handling of quantum and probabilistic information. We provide a syntax and a model to this logic, providing a probabilistic semantics to the classical part. We exercise it with the quantum coin toss program.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The probability of obtaining \(\varphi \) in a measurement is
where s is a state and 
is the internal product of the Hilbert space. In equation (1), \(|\alpha |^2\) and \(|\beta |^2\), are the probabilities of obtaining 
and 
, which is 0.5 in both cases: (\(\left( \frac{1}{\sqrt{2}} \right) ^2 = 0.5\)). - 2.
Tests correspond to the \(\sigma \)-algebra over the valuation set \(\mathcal {C}\). For valuations with a discrete domain, it corresponds to the powerset \(2^{\mathcal {C}}\). Tests form a Boolean algebra.
- 3.
A fuzzy predicate corresponds to a measurable function [Koz85] from the set of states to the probability interval [0, 1], in this case, \(\mathcal {C} \rightarrow [0,1]\). The fuzzy predicate is characteristic of a test.
where s is a state and 
is the internal product of the Hilbert space. In equation (
and 
, which is 0.5 in both cases: (References
Baltag, A., Bergfeld, J., Kishida, K., Sack, J., Smets, S., Zhong, S.: PLQP & company: decidable logics for quantum algorithms. Int. J. Theor. Phys. 53(10), 3628–3647 (2014)
Baltag, A., Smets, S.: The logic of quantum programs. In: Proceedings of the 2nd International Workshop on Quantum Programming Languages, pp. 39–56 (2004). https://www.mathstat.dal.ca/~selinger/qpl2004/proceedings.html
Cross, A.W., Bishop, L.S., Smolin, J.A., Gambetta, J.M.: Open quantum assembly language. arXiv preprint arXiv:1707.03429 (2017)
Deutsch, D.: Quantum theory, the Church-Turing principle and the universal quantum computer. Proc. Roy. Soc. Lond. A. Math. Phys. Sci. 400(1818), 97–117 (1985)
Deutsch, D.E.: Quantum computational networks. Proc. Roy. Soc. Lond. A. Math. Phys. Sci. 425(1868), 73–90 (1989)
Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: de Bakker, J., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 299–309. Springer, Heidelberg (1980). https://doi.org/10.1007/3-540-10003-2_79
IBM Q - quantum computing, June 2018. https://www.research.ibm.com/ibm-q/
Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328–350 (1981)
Kozen, D.: A probabilistic PDL. J. Comput. Syst. Sci. 30(2), 162–178 (1985)
Nielsen, M.A., Chuang, I.: Quantum computation and quantum information (2002)
Acknowledgements
The author wishes to thank LuÃs Barbosa and Leandro Gomes, for the useful discussions during the course of this work. The author was funded by an individual grant of reference SFRH/BD/116367/2016, conceded by the FCT - Fundação para a Ciência e Tecnologia under the POCH programme and MCTES national funds. This work was also supported by the KLEE project(POCI-01-0145-FEDER-030947-PTDC/CCI-COM/30947/2017), funded by ERDF by the Operational Programme for Competitiveness and Internationalisation, COMPETE2020 Programme and by National Funds through the Portuguese funding agency, FCT.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Tavares, C. (2020). A Dynamic Logic for QASM Programs. In: Soares Barbosa, L., Baltag, A. (eds) Dynamic Logic. New Trends and Applications. DALI 2019. Lecture Notes in Computer Science(), vol 12005. Springer, Cham. https://doi.org/10.1007/978-3-030-38808-9_13
Download citation
DOI: https://doi.org/10.1007/978-3-030-38808-9_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-38807-2
Online ISBN: 978-3-030-38808-9
eBook Packages: Computer ScienceComputer Science (R0)