×

Termination of nondeterministic quantum programs. (English) Zbl 1359.68092

Summary: We define a language-independent model of nondeterministic quantum programs in which a quantum program consists of a finite set of quantum processes. These processes are represented by quantum Markov chains over the common state space, which formalize the quantum mechanical behaviors of the machine. An execution of a nondeterministic quantum program is modeled by a sequence of actions of individual processes, and at each step of an execution a process is chosen nondeterministically to perform the next action. This execution model formalize the users’ behavior of calling the processes in the classical world. Applying the model to a quantum walk as an instance of physically realizable systems, we describe an execution step by step. A characterization of reachable space and a characterization of diverging states of a nondeterministic quantum program are presented. We establish a zero-one law for termination probability of the states in the reachable space. A combination of these results leads to a necessary and sufficient condition for termination of nondeterministic quantum programs. Based on this condition, an algorithm is found for checking termination of nondeterministic quantum programs within a fixed finite-dimensional state space.

MSC:

68Q12 Quantum algorithms and complexity in the theory of computing

Software:

QPL; qGCL; QML

References:

[1] Abramsky, S.: High-level methods for quantum computation and information. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 410-414 (2004) · Zbl 1214.68168
[2] Aharonov, D., Ambainis, A., Kempe, J., Vazirani, U.V.: Quantum walks on graphs. In: Proceedings on 33rd Annual ACM Symposium on Theory of Computing (STOC), pp. 50-59 (2001) · Zbl 1323.81020
[3] Altenkirch, T., Grattage, J.: A functional quantum programming language. In: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 249-258 (2005) · Zbl 1277.68078
[4] Baltag, A., Smets, S.: LQP: the dynamic logic of quantum information. Math. Struct. Comput. Sci. 16, 491-525 (2006) · Zbl 1103.03031 · doi:10.1017/S0960129506005299
[5] Betteli, S., Calarco, T., Serafini, L.: Toward an architecture for quantum programming. Eur. Phys. J. D25, 181-200 (2003)
[6] Brunet, O., Jorrand, P.: Dynamic quantum logic for quantum programs. Int. J. Quantum Inf. 2, 45-54 (2004) · Zbl 1069.81007 · doi:10.1142/S0219749904000067
[7] Chadha, R., Mateus, P., Sernadas, A.: Reasoning about imperative quantum programs. Electron. Notes Theor. Comput. Sci. 158, 19-39 (2006) · Zbl 1273.03104 · doi:10.1016/j.entcs.2006.04.003
[8] D’Hondt, E., Panangaden, P.: Quantum weakest preconditions. Math. Struct. Comput. Sci. 16, 429-451 (2006) · Zbl 1122.68058 · doi:10.1017/S0960129506005251
[9] Feng, Y., Duan, R.Y., Ji, Z.F., Ying, M.S.: Proof rules for the correctness of quantum programs. Theor. Comput. Sci. 386, 151-166 (2007) · Zbl 1137.68038
[10] Feng, Y., Duan, R.Y., Ying, M.S.: Bisimulation for quantum processes. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 523-534 (2011) · Zbl 1284.68425
[11] Gay, S.J.: Quantum programming languages: survey and bibliography. Math. Struct. Comput. Sci. 16, 581-600 (2006) · Zbl 1122.68021 · doi:10.1017/S0960129506005378
[12] Gay, S.J., Nagarajan, R.: Communicating quantum processes. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 145-157 (2005) · Zbl 1369.68207
[13] Hart, S., Sharir, M., Pnueli, A.: Termination of probabilistic concurrent programs. ACM Trans. Program. Lang. Syst. 5, 356-380 (1983) · Zbl 0511.68009 · doi:10.1145/2166.357214
[14] Jorrand, P., Lalire, M.: Toward a quantum process algebra. In: Proceedings of the First ACM Conference on Computing Frontiers, pp. 111-119 (2004)
[15] Mitchison, G., Josza, R.: Counterfactual computation. Proc. R. Soc. Lond. A 457, 1175-1193 (2001) · Zbl 1027.81514 · doi:10.1098/rspa.2000.0714
[16] Nagarajan, R., Papanikolaou, N., Williams, D.: Simulating and compiling code for the sequential quantum random access machine. Electron. Notes Theor. Comput. Sci. 170, 101-124 (2007) · Zbl 1277.68078 · doi:10.1016/j.entcs.2006.12.014
[17] Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information. Cambridge University Press, Cambridge (2000) · Zbl 1049.81015
[18] Ömer, B.: Structured Quantum Programming, Ph.D thesis, Technical University of Vienna (2003)
[19] Roman, S.: Advanced Linear Algebra. Springer, Berlin (2008) · Zbl 1132.15002
[20] Sanders, J.W., Zuliani, P.: Quantum programming. In: Proceedings, Mathematics of Program Construction, LNCS, pp. 80-99 (2000) · Zbl 0963.68037
[21] Selinger, P.: Towards a quantum programming language. Math. Struct. Comput. Sci. 14, 527-586 (2004) · Zbl 1085.68014 · doi:10.1017/S0960129504004256
[22] Selinger, P.: A brief survey of quantum programming languages. In: Proceedings of the 7th International Symposium Functional and Logic Programming (FLOPS), pp. 1-6 (2004) · Zbl 1122.68359
[23] Svore, K.M., Aho, A.V., Cross, A.W., Chuang, I., Markov, I.L.: A layered software architecture for quantum computing design tools. IEEE Comput. 39, 74-83 (2006) · Zbl 1069.81007
[24] Ying, M.S.: Floyd-Hoare logic for quantum programs. ACM Trans. Program. Langu. Syst. 33, 19 (2011)
[25] Ying, M.S., Duan, R.Y., Feng, Y., Ji, Z.F.: Predicate Transformer Semantics of Quantum Programs, Semantic Techniques in Quantum Computation. Cambridge University Press, Cambridge (2010) · Zbl 1196.68123
[26] Ying, M.S., Feng, Y.: Quantum loop programs. Acta Informatica 47, 221-250 (2010) · Zbl 1214.68168 · doi:10.1007/s00236-010-0117-4
[27] Ying, M.S., Feng, Y.: A flowchart language for quantum programming. IEEE Trans. Softw. Eng. 37, 466-485 (2011) · doi:10.1109/TSE.2010.94
[28] Zuliani, P.: Nondeterminstic quantum programming. In: Proceedings of the 2nd International Workshop on Quantum Programming Languages, pp. 179-195 (2004) · Zbl 1122.68058
[29] Zuliani, P.: Compiling quantum programs. Acta Informatica 41, 435-473 (2005) · Zbl 1079.68020 · doi:10.1007/s00236-005-0165-3
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.