{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T23:11:06Z","timestamp":1765667466940,"version":"3.40.3"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572661"},{"type":"electronic","value":"9783031572678"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper, we study quantitative properties of quantum programs. Properties of interest include (positive) almost-sure termination, expected runtime or expected cost, that is, for example, the expected number of applications of a given quantum gate, etc. After studying the completeness of these problems in the arithmetical hierarchy over the Clifford+T fragment of quantum mechanics, we express these problems using a variation of a quantum pre-expectation transformer, a weakest pre-condition based technique that allows to symbolically compute these quantitative properties. Under a smooth restriction\u2014a restriction to polynomials of bounded degree over a real closed field\u2014we show that the quantitative problem, which consists in finding an upper-bound to the pre-expectation, can be decided in time double-exponential in the size of a program, thus providing, despite its great complexity, one of the first decidable results on the analysis and verification of quantum programs. Finally, we sketch how the latter can be transformed into an efficient synthesis method.<\/jats:p>","DOI":"10.1007\/978-3-031-57267-8_2","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T16:02:01Z","timestamp":1712246521000},"page":"31-58","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["On the Hardness of Analyzing Quantum Programs Quantitatively"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6445-8833","authenticated-orcid":false,"given":"Martin","family":"Avanzini","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9240-6128","authenticated-orcid":false,"given":"Georg","family":"Moser","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0601-5425","authenticated-orcid":false,"given":"Romain","family":"P\u00e9choux","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1808-2409","authenticated-orcid":false,"given":"Simon","family":"Perdrix","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Aaronson, S., Gottesman, D.: Improved simulation of stabilizer circuits. Physical Review A 70(5), 052328 (2004)","DOI":"10.1103\/PhysRevA.70.052328"},{"key":"2_CR2","doi-asserted-by":"publisher","unstructured":"Altenkirch, T., Grattage, J.: A functional quantum programming language. In: 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings. pp. 249\u2013258. IEEE Computer Society (2005). https:\/\/doi.org\/10.1109\/LICS.2005.1","DOI":"10.1109\/LICS.2005.1"},{"key":"2_CR3","doi-asserted-by":"publisher","unstructured":"Arute, F., Arya, K., et al.: Quantum supremacy using a programmable superconducting processor. Nature 574, 505\u2013510 (2019). https:\/\/doi.org\/10.1038\/s41586-019-1666-5","DOI":"10.1038\/s41586-019-1666-5"},{"key":"2_CR4","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Barthe, G., Lago, U.D.: On continuation-passing transformations and expected cost analysis. Proc. of the ACM on Programming Languages 5(ICFP), 1\u201330 (2021). https:\/\/doi.org\/10.1145\/3473592","DOI":"10.1145\/3473592"},{"key":"2_CR5","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Lago, U.D., Yamada, A.: On probabilistic term rewriting. Science of Computer Programming 185 (2020). https:\/\/doi.org\/10.1016\/j.scico.2019.102338","DOI":"10.1016\/j.scico.2019.102338"},{"key":"2_CR6","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Moser, G., P\u00e9choux, R., Perdrix, S., Zamdzhiev, V.: Quantum expectation transformers for cost analysis. In: LICS \u201922: 37th Annual ACM\/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022. pp. 10:1\u201310:13 (2022). https:\/\/doi.org\/10.1145\/3531130.3533332","DOI":"10.1145\/3531130.3533332"},{"key":"2_CR7","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Moser, G., Schaper, M.: A modular cost analysis for probabilistic programs. Proc. of the ACM on Programming Languages 4(OOPSLA), 172:1\u2013172:30 (2020). https:\/\/doi.org\/10.1145\/3428240","DOI":"10.1145\/3428240"},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Moser, G., Schaper, M.: Automated expected value analysis of recursive programs. Proceedings of the ACM on Programming Languages 7(PLDI), 1050\u20131072 (2023). https:\/\/doi.org\/10.1145\/3591263","DOI":"10.1145\/3591263"},{"key":"2_CR9","doi-asserted-by":"publisher","unstructured":"Bournez, O., Garnier, F.: Proving Positive Almost-Sure Termination. In: Proc. of RTA 2005. LNCS, vol.\u00a03467, pp. 323\u2013337. Springer (2005). https:\/\/doi.org\/10.1142\/S0129054112400588","DOI":"10.1142\/S0129054112400588"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Bravyi, S., Kitaev, A.: Universal quantum computation with ideal clifford gates and noisy ancillas. Physical Review A 71(2), 022316 (2005). https:\/\/doi.org\/10.1103\/PhysRevA.71.022316","DOI":"10.1103\/PhysRevA.71.022316"},{"key":"2_CR11","doi-asserted-by":"publisher","unstructured":"Chen, Y.F., Chung, K.M., Leng\u00e1l, O., Lin, J.A., Tsai, W.L., Yen, D.D.: An automata-based framework for verification and bug hunting in quantum circuits. Proceedings of the ACM on Programming Languages 7(PLDI), 1218\u20131243 (2023). https:\/\/doi.org\/10.1145\/3591270","DOI":"10.1145\/3591270"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Cohn, P.M.: Further algebra and applications. Springer Science & Business Media (2002)","DOI":"10.1007\/978-1-4471-0039-3"},{"key":"2_CR13","unstructured":"Dijkstra, E.W.: A discipline of programming. Prentice-Hall Englewood Cliffs (1976)"},{"key":"2_CR14","doi-asserted-by":"publisher","unstructured":"Endrullis, J., Geuvers, H., Zantema, H.: Degrees of undecidability in term rewriting. In: Gr\u00e4del, E., Kahle, R. (eds.) Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7-11, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05771, pp. 255\u2013270. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-04027-6_20","DOI":"10.1007\/978-3-642-04027-6_20"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Fu, P., Kishida, K., Ross, N.J., Selinger, P.: Proto-quipper with dynamic lifting. POPL 7, 309\u2013334 (2023)","DOI":"10.1145\/3571204"},{"key":"2_CR16","doi-asserted-by":"publisher","unstructured":"Gosset, D., Kliuchnikov, V., Mosca, M., Russo, V.: An algorithm for the t-count. Quantum Information & Computation 14(15-16), 1261\u20131276 (2014). https:\/\/doi.org\/10.26421\/QIC14.15-16-1","DOI":"10.26421\/QIC14.15-16-1"},{"key":"2_CR17","doi-asserted-by":"publisher","unstructured":"Gretz, F., Katoen, J.P., McIver, A.: Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Performance Evaluation 73, 110\u2013132 (2014). https:\/\/doi.org\/10.1016\/j.peva.2013.11.004","DOI":"10.1016\/j.peva.2013.11.004"},{"key":"2_CR18","unstructured":"Halava, V., Harju, T., Hirvensalo, M., Karhum\u00e4ki, J.: Skolem\u2019s problem - on the border between decidability and undecidability. Tech. Rep.\u00a0683, Turku Center for Computer Science (2005)"},{"key":"2_CR19","doi-asserted-by":"publisher","unstructured":"Handelman, D.: Representing Polynomials by Positive Linear Functions on Compact Convex Polyhedra. PJM 132(1), 35\u201362 (1988). https:\/\/doi.org\/10.2140\/pjm.1988.132.35","DOI":"10.2140\/pjm.1988.132.35"},{"key":"2_CR20","doi-asserted-by":"publisher","unstructured":"Harrow, A.W., Hassidim, A., Lloyd, S.: Quantum algorithm for linear systems of equations. Physical Review Letters 103, 150502 (2009). https:\/\/doi.org\/10.1103\/PhysRevLett.103.150502","DOI":"10.1103\/PhysRevLett.103.150502"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Heintz, J., Roy, M.F., Solern\u00f3, P.: Sur la complexit\u00e9 du principe de tarski-seidenberg. Bulletin de la Soci\u00e9t\u00e9 math\u00e9matique de France 118(1), 101\u2013126 (1990)","DOI":"10.24033\/bsmf.2138"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Hillmich, S., Zulehner, A., Kueng, Richardand\u00a0Markov, I.L., Wille, R.: Approximating decision diagrams for quantum circuit simulation. ACM Trans. Quantum Comput. 3(4), 1\u201321 (2022)","DOI":"10.1145\/3530776"},{"key":"2_CR23","doi-asserted-by":"publisher","unstructured":"Jia, X., Kornell, A., Lindenhovius, B., Mislove, M.W., Zamdzhiev, V.: Semantics for variational quantum programming. Proc. ACM Program. Lang. 6(POPL), 1\u201331 (2022). https:\/\/doi.org\/10.1145\/3498687","DOI":"10.1145\/3498687"},{"key":"2_CR24","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L., Katoen, J.P.: On the hardness of almost-sure termination. In: MFCS 2015, Part I. pp. 307\u2013318. LNCS, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-48057-1_24","DOI":"10.1007\/978-3-662-48057-1_24"},{"key":"2_CR25","unstructured":"Kaminski, B.L.: Advanced weakest precondition calculi for probabilistic programs. Ph.D. thesis, RWTH Aachen University, Germany (2019), http:\/\/publications.rwth-aachen.de\/record\/755408"},{"key":"2_CR26","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L., Katoen, J.P.: A weakest pre-expectation semantics for mixed-sign expectations. In: LICS 2017. pp. 1\u201312. IEEE (2017). https:\/\/doi.org\/10.1109\/LICS.2017.8005153","DOI":"10.1109\/LICS.2017.8005153"},{"key":"2_CR27","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run-times of probabilistic programs. In: ESOP 2016. LNCS, vol.\u00a09632, pp. 364\u2013389. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_15","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Kozen, D.: A probabilistic PDL. Journal of Computer and System Sciences 30(2), 162\u2013178 (1985)","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"2_CR29","doi-asserted-by":"publisher","unstructured":"Leutgeb, L., Moser, G., Zuleger, F.: Automated Expected Amortised Cost Analysis of Probabilistic Data Structures. In: Proc. of 34th CAV. LNCS, vol. 13372, pp. 70\u201391 (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_4","DOI":"10.1007\/978-3-031-13188-2_4"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Liu, J., Zhou, L., Barthe, G., Ying, M.: Quantum weakest preconditions for reasoning about expected runtimes of quantum programs (2022)","DOI":"10.1145\/3531130.3533327"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Malherbe, O., D\u00edaz-Caro, A.: Quantum control in the unitary sphere: Lambda-s1 and its categorical model. Logical Methods in Computer Science 18(3) (2022)","DOI":"10.46298\/lmcs-18(3:32)2022"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.: Abstraction, refinement and proof for probabilistic systems. Springer Science & Business Media (2005)","DOI":"10.1145\/1059816.1059824"},{"key":"2_CR33","doi-asserted-by":"publisher","unstructured":"Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: resource analysis for probabilistic programs. ACM SIGPLAN Notices 53(4), 496\u2013512 (2018). https:\/\/doi.org\/10.1145\/3296979.3192394","DOI":"10.1145\/3296979.3192394"},{"key":"2_CR34","unstructured":"Odifreddi, P.: Classical recursion theory: The theory of functions and sets of natural numbers. Elsevier (1992)"},{"key":"2_CR35","unstructured":"Olmedo, F., D\u00edaz-Caro, A.: Runtime analysis of quantum programs: A formal approach. In: PLanQC 2020 (2020)"},{"key":"2_CR36","doi-asserted-by":"publisher","unstructured":"Perdrix, S.: Quantum entanglement analysis based on abstract interpretation. In: SAS. pp. 270\u2013282. LNCS (2008). https:\/\/doi.org\/10.1007\/978-3-540-69166-2_18","DOI":"10.1007\/978-3-540-69166-2_18"},{"key":"2_CR37","doi-asserted-by":"publisher","unstructured":"Schnabl, A., Simonsen, J.G.: The exact hardness of deciding derivational and runtime complexity. In: Proc. 20th CSL. LIPIcs, vol.\u00a012, pp. 481\u2013495 (2011). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2011.481","DOI":"10.4230\/LIPIcs.CSL.2011.481"},{"key":"2_CR38","unstructured":"Schrijver, A.: Theory of linear and integer programming. Wiley (1999)"},{"key":"2_CR39","doi-asserted-by":"publisher","unstructured":"Selinger, P.: Towards a quantum programming language. Mathematical Structures in Computer Science 14(4), 527\u2013586 (2004). https:\/\/doi.org\/10.1017\/S0960129504004256","DOI":"10.1017\/S0960129504004256"},{"key":"2_CR40","doi-asserted-by":"crossref","unstructured":"Sharir, M., Pnueli, A., Hart, S.: Verification of probabilistic programs. SIAM Journal on Computing 13(2), 292\u2013314 (1984)","DOI":"10.1137\/0213021"},{"key":"2_CR41","doi-asserted-by":"publisher","unstructured":"Shor, P.W.: Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer. SIAM Review 41(2), 303\u2013332 (1999). https:\/\/doi.org\/10.1137\/S0036144598347011","DOI":"10.1137\/S0036144598347011"},{"key":"2_CR42","unstructured":"Weihrauch, K.: Computable analysis: an introduction. Springer Science & Business Media (2012)"},{"key":"2_CR43","doi-asserted-by":"publisher","unstructured":"Wille, R., Van\u00a0Meter, R., Naveh, Y.: IBM\u2019s Qiskit Tool Chain: Working with and Developing for Real Quantum Computers. In: 2019 Design, Automation & Test in Europe Conference & Exhibition (DATE). pp. 1234\u20131240 (2019). https:\/\/doi.org\/10.23919\/DATE.2019.8715261","DOI":"10.23919\/DATE.2019.8715261"},{"key":"2_CR44","doi-asserted-by":"crossref","unstructured":"Winskel, G.: The formal semantics of programming languages - an introduction. Foundation of computing series, MIT Press (1993)","DOI":"10.7551\/mitpress\/3054.001.0001"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57267-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T16:02:49Z","timestamp":1712246569000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57267-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572661","9783031572678"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57267-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"72","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"25","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"35% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The proceedings also contain 4 artifact report that have not been part of the original submission","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}