logo

SCIENCE CHINA Information Sciences, Volume 62, Issue 12: 222501(2019) https://doi.org/10.1007/s11432-018-9847-0

Implementing termination analysis on quantum programming

More info
  • ReceivedJun 1, 2018
  • AcceptedMar 12, 2019
  • PublishedNov 11, 2019

Abstract

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.


Acknowledgment

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.


References

[1] Bourdoncle F. Abstract debugging of higher-order imperative languages. SIGPLAN Not, 1993, 28: 46-55 CrossRef Google Scholar

[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--426. Google Scholar

[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--393. Google Scholar

[4] Ying M S. Foundations of quantum programming. In: Proceedings of the 8th Asian Conference on Programming Languages and Systems, 2010. Google Scholar

[5] Ying M, Feng Y. Quantum loop programs. Acta Informatica, 2010, 47: 221-250 CrossRef Google Scholar

[6] Ying M, Yu N, Feng Y. Verification of quantum programs. Sci Comput Programming, 2013, 78: 1679-1700 CrossRef Google Scholar

[7] Li Y, Yu N, Ying M. Termination of nondeterministic quantum programs. Acta Informatica, 2014, 51: 1-24 CrossRef Google Scholar

[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--83. Google Scholar

[9] Li Y J, Ying M S. Algorithmic analysis of termination problems for quantum programs. In: Proceedings of ACM on Programming Languages, 2017. Google Scholar

[10] Horn A R, Johnson R C. Matrix Analysis. Cambridge: Cambridge University Press, 1990. Google Scholar

[11] Paulsen V. Completely Bounded Maps and Operator Algebras. Cambridge: Cambridge University Press, 2002. Google Scholar

[12] Beelen T, van Dooren P M. Computational aspects of the Jordan canonical form. In: Reliable Numerical Computation. Oxford: Clarendon Press, 1990. 57--72. Google Scholar

[13] Liu S S, Zhou L, Guan J, et al. $Q|SI~\rangle$: a quantum programming environment (in Chinese). Sci Sin Inform, 2017, 47: 1300--1315. Google Scholar

  • Figure 1

    The flowchart of Qloop.

  • Figure 2

    Algorithms 1and 2are programmed onto Matlab 2017b. The experiment is conducted on the PC with Core i7 and 16 GB memory. Qloops 3and 4are executed repeated 1000 times for one setting and statistics over the total running time. The figure clearly illustrates Algorithm 2without the Jordan decomposition process has a significant acceleration on analysing of the termination. For both termination and almost-surely scenario, Algorithm 2speeds up almost 300 times than Algorithm 1.

  •   

    Algorithm 1 The algorithm for checking termination with the Jordan decomposition

    Require:$G$;

    Output:State, Instead.

    Function State, Instead = CheckTermination($G$);

    ${\left|~\Phi\right\rangle}~\gets$ MaxEntangledState where $d({\left|~\Phi\right\rangle})=d(G)$;

    $[J,S]\gets~{\rm~Jordan}(G)$ s.t. $G=SJS^{-1}$, ${\left|~\phi\right\rangle}'~\gets~S^{-1}{\left|~\Phi\right\rangle}$;

    $[{\left|~u\right\rangle}~{\left|~v\right\rangle}~{\left|~w\right\rangle}]^{\rm~T}~\gets~{\left|~\phi\right\rangle}'$ where $d({\left|~u\right\rangle})=\text{number~of~eignvalues~with~value~}~0$,$d({\left|~w\right\rangle})=\text{number~of~eignvalues~with~module~}~1$,$d({\left|~v\right\rangle})=d({\left|~\phi\right\rangle}')-d({\left|~u\right\rangle})-d({\left|~w\right\rangle})$;

    if ${\left|~v\right\rangle}=0$ and ${\left|~w\right\rangle}=0$ then

    $k~\gets~{\rm~CalSteps}(G)$;

    State $\gets$ Finite termination;

    Instead $\gets~\sum_{n=0}^{k-1}N_0G^n$;ELSIF${\left|~w\right\rangle}=0$

    State $\gets$ Almost-surely termination;

    Instead $\gets~\sum_{n=0}^{\infty}N_0G^n=N_0(I-G)^{-1}$;

    else

    State $\gets$ Non-termination or unknown;

    Instead $\gets$ NULL;

    end if

  •   

    Algorithm 2 The algorithm for checking termination without the Jordan decomposition

    Require:$G$;

    Output:State, Instead.

    Function State, Instead = CheckTermination($G$);

    ${\left|~\Phi\right\rangle}~\gets$ MaxEntangledState;

    $[V,D]\gets$ eig($G^\dagger$);

    $D_1~\gets~D~\text{~where~their~eigenvalues~with~module~}~1~$;

    if $G^d~{\left|~\Phi\right\rangle}=0$ where $d$ is the dimension of $G$ then

    $k\gets$ CalSteps($G$);

    State $\gets$ Finite termination;

    Instead $\gets~\sum_{n=0}^{k-1}N_0G^n$;ELSIF${\left|~\Phi\right\rangle}~\perp~D_1$

    State $\gets$ Almost-surely termination;

    Instead $\gets~\sum_{n=0}^{\infty}N_0G^n=N_0(I-G)^{-1}$;

    else

    State $\gets$ Non-termination or unknown;

    Instead $\gets$ NULL;

    end if

  •   

    Algorithm 3 Qloop with Hadamard gate as a sub-program

    Require:$\rho=\rho_1={\left|~1\right\rangle}{\left\langle~1\right|}$, $M=\{|0\rangle\langle~0|,|1\rangle\langle~1|\}$, ${\rm~HGate}=\frac{1}{\sqrt{2}}\big[\tiny{\begin{matrix} 1~&1\\ 1~&-1 \end{matrix}}\big]$;

    Output:$\rho$.

    while $M(\rho)$ do

    HGate($\rho$);

    end while

    return $\rho$.

  •   

    Algorithm 4 Qloop with bit flip gate as a sub-program

    Require:$\rho=\rho_1={\left|~1\right\rangle}{\left\langle~1\right|}$, $M=\{|0\rangle\langle~0|,|1\rangle\langle~1|\}$, ${\rm~XGate}=\big[\tiny{\begin{matrix} 0&1\\ 1&0 \end{matrix}}\big]$;

    Output:$\rho$.

    while $M(\rho)$ do

    XGate($\rho$);

    end while

    return $\rho$.

Copyright 2020 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有

京ICP备18024590号-1