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


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