{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:36:02Z","timestamp":1773192962135,"version":"3.50.1"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61502467"],"award-info":[{"award-number":["61502467"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DP160101652"],"award-info":[{"award-number":["DP160101652"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>We introduce the notion of linear ranking super-martingale (LRSM) for quantum programs (with nondeterministic choices, namely angelic and demonic choices). Several termination theorems are established showing that the existence of the LRSMs of a quantum program implies its termination. Thus, the termination problems of quantum programs is reduced to realisability and synthesis of LRSMs. We further show that the realisability and synthesis problem of LRSMs for quantum programs can be reduced to an SDP (Semi-Definite Programming) problem, which can be settled with the existing SDP solvers. The techniques developed in this paper are used to analyse the termination of several example quantum programs, including quantum random walks and quantum Bernoulli factory for random number generation. This work is essentially a generalisation of constraint-based approach to the corresponding problems for probabilistic programs developed in the recent literature by adding two novel ideas: (1) employing the fundamental Gleason's theorem in quantum mechanics to guide the choices of templates; and (2) a generalised Farkas' lemma in terms of observables (Hermitian operators) in quantum physics.<\/jats:p>","DOI":"10.1145\/3158123","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Algorithmic analysis of termination problems for quantum programs"],"prefix":"10.1145","volume":"2","author":[{"given":"Yangjia","family":"Li","sequence":"first","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mingsheng","family":"Ying","sequence":"additional","affiliation":[{"name":"University of Technology Sydney, Australia \/ Institute of Software at Chinese Academy of Sciences, China \/ Tsinghua University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/380752.380758"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.1"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005299"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.90.032311"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0219749904000067"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.003"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958114"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837639"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_6"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1038\/ncomms9203"},{"key":"e_1_2_2_14_1","first-page":"200","volume":"52","author":"Derksen H.","year":"2005","journal-title":"Quiver representations, Notices of the American Mathematical Society"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-015-8222-3"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.06.011"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2013.04.002"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177728976"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005378"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_51"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1512\/iumj.1957.6.56050"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462177"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.2953952"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.parco.2014.12.001"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10622-4_7"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005153"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/175007.175019"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-013-0185-3"},{"key":"e_1_2_2_33_1","unstructured":"T. Liu Y. J. Li S. L. Wang N. J. Zhan and M. S. Ying A theorem prover for quantum Hoare logic and its applications http:\/\/arxiv.org\/pdf\/1601.03835.pdf  T. Liu Y. J. Li S. L. Wang N. J. Zhan and M. S. Ying A theorem prover for quantum Hoare logic and its applications http:\/\/arxiv.org\/pdf\/1601.03835.pdf"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1098\/rspa.2000.0714"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_7"},{"key":"e_1_2_2_40_1","volume-title":"Proceedings of the 2003 ACM SIGPLAN workshop on Haskell, 39-49","author":"Sabry A"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722010_6"},{"key":"e_1_2_2_42_1","first-page":"1","volume":"2998","author":"Seinger P.","year":"2004","journal-title":"Springer LNCS"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_2_2_44_1","unstructured":"D. Wecker and K. M. Svore LIQUi | \u27e9: A software design architecture and domain-specific language for quantum computing http:\/\/research.microsoft.com\/pubs\/209634\/1402.4467.pdf.  D. Wecker and K. M. Svore LIQUi | \u27e9: A software design architecture and domain-specific language for quantum computing http:\/\/research.microsoft.com\/pubs\/209634\/1402.4467.pdf."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_2_2_46_1","volume-title":"Morgan-Kaufmann","author":"Ying M. S.","year":"2016"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-010-0117-4"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629680"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009840"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.03.016"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_24"},{"key":"e_1_2_2_52_1","unstructured":"S. G. Ying and M. S. Ying Reachability analysis of quantum Markov decision processes arXiv:1406.6146  S. G. Ying and M. S. Ying Reachability analysis of quantum Markov decision processes arXiv:1406.6146"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_7"},{"key":"e_1_2_2_54_1","first-page":"179","volume-title":"Proceedings of the 2nd International Workshop on Quantum Programming Languages (QPL)","author":"Zuliani P.","year":"2004"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158123","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158123","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158123"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":52,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158123"],"URL":"https:\/\/doi.org\/10.1145\/3158123","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}