Implementing termination analysis on quantum programming

  • Shusen LiuEmail author
  • Kan HeEmail author
  • Runyao Duan
Research Paper


Termination analysis is an essential part in programming. Especially quantum programming concerning measurement, entanglement and even superposition are the foundations of bizarre behaviours in quantum programs. In this paper, we analyse and extend the theoretical theorems on termination analysis proposed by Ying et al. into computational theorems and algorithms. The new algorithm without the Jordan decomposition process has a significant acceleration with polynomial complexity both on terminating and almost-surely terminating programs. Moreover, the least upper bound of termination programs steps is studied and utilized to output the substituted matrix representation of quantum programs. We also implement four groups of experiments to illustrate the advantages of the new algorithm in case of processing a simplified quantum walk example comparing with the original counterpart.


termination analysis quantum while-language quantum programming quantum experiment terminating steps 



This work was supported by National Natural Science Foundation of China (Grant Nos. 61672007, 11771011, 11647140). We were grateful to Ying DONG for his helpful dicussions.


  1. 1.
    Bourdoncle F. Abstract debugging of higher-order imperative languages. SIGPLAN Not, 1993, 28: 46–55CrossRefGoogle Scholar
  2. 2.
    Cook B, Podelski A, Rybalchenko A. Termination proofs for systems code. In: Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2006. 415–426Google Scholar
  3. 3.
    Brockschmidt M, Cook B, Ishtiaq S, et al. T2: temporal property verification. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2016. 387–393Google Scholar
  4. 4.
    Ying M S. Foundations of quantum programming. In: Proceedings of the 8th Asian Conference on Programming Languages and Systems, 2010Google Scholar
  5. 5.
    Ying M S, Feng Y. Quantum loop programs. Acta Inform, 2010, 47: 221–250MathSciNetCrossRefGoogle Scholar
  6. 6.
    Ying M S, Yu N K, Feng Y, et al. Verification of quantum programs. Sci Comput Program, 2013, 78: 1679–1700CrossRefGoogle Scholar
  7. 7.
    Li Y J, Yu N K, Ying M S. Termination of nondeterministic quantum programs. Acta Inform, 2014, 51: 1–24MathSciNetCrossRefGoogle Scholar
  8. 8.
    Yu N K, Ying M S. Reachability and termination analysis of concurrent quantum programs. In: Proceedings of International Conference on Concurrency Theory, 2012. 69–83Google Scholar
  9. 9.
    Li Y J, Ying M S. Algorithmic analysis of termination problems for quantum programs. In: Proceedings of ACM on Programming Languages, 2017Google Scholar
  10. 10.
    Horn A R, Johnson R C. Matrix Analysis. Cambridge: Cambridge University Press, 1990zbMATHGoogle Scholar
  11. 11.
    Paulsen V. Completely Bounded Maps and Operator Algebras. Cambridge: Cambridge University Press, 2002zbMATHGoogle Scholar
  12. 12.
    Beelen T, van Dooren P M. Computational aspects of the Jordan canonical form. In: Reliable Numerical Computation. Oxford: Clarendon Press, 1990. 57–72Google Scholar
  13. 13.
    Liu S S, Zhou L, Guan J, et al. Q|SI〉: a quantum programming environment (in Chinese). Sci Sin Inform, 2017, 47: 1300–1315CrossRefGoogle Scholar

Copyright information

© Science China Press and Springer-Verlag GmbH Germany, part of Springer Nature 2019

Authors and Affiliations

  1. 1.School of Data and Computer ScienceSun Yat-sen UniversityGuangzhouChina
  2. 2.Institute for Quantum ComputingBaidu, BeijingChina
  3. 3.Institute for Advanced StudyTsinghua UniversityBeijingChina
  4. 4.College of Mathematics & College of Information and Computer ScienceTaiyuan University of TechnologyTaiyuanChina

Personalised recommendations