{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T01:45:47Z","timestamp":1787017547438,"version":"build-2736575974"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000038","name":"NSERC","doi-asserted-by":"crossref","award":["RGPIN-2022- 03319"],"award-info":[{"award-number":["RGPIN-2022- 03319"]}],"id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>The phase folding optimization is a circuit optimization used in many quantum compilers as a fast and effective way of reducing the number of high-cost gates in a quantum circuit. However, existing formulations of the optimization rely on an exact, linear algebraic representation of the circuit, restricting the optimization to being performed on straightline quantum circuits or basic blocks in a larger quantum program.<\/jats:p>\n                  <jats:p>\n                    We show that the phase folding optimization can be re-cast as an\n                    <jats:italic toggle=\"yes\">affine relation analysis<\/jats:italic>\n                    , which allows the direct application of classical techniques for affine relations to extend phase folding to quantum\n                    <jats:italic toggle=\"yes\">programs<\/jats:italic>\n                    with arbitrarily complicated classical control flow including nested loops and procedure calls. Through the lens of relational analysis, we show that the optimization can be powered-up by substituting other classical relational domains, particularly ones for\n                    <jats:italic toggle=\"yes\">non-linear<\/jats:italic>\n                    relations which are useful in analyzing circuits involving classical arithmetic. To increase the precision of our analysis and infer non-linear relations from gate sets involving only linear operations \u2013 such as Clifford+\n                    <jats:sc>t<\/jats:sc>\n                    \u2013 we show that the\n                    <jats:italic toggle=\"yes\">sum-over-paths<\/jats:italic>\n                    technique can be used to extract precise symbolic transition relations for straightline circuits. Our experiments show that our methods are able to generate and use non-trivial loop invariants for quantum program optimization, as well as achieve some optimizations of common circuits which were previously attainable only by hand.\n                  <\/jats:p>","DOI":"10.1145\/3704873","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1072-1103","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Linear and Non-linear Relational Analyses for Quantum Program Optimization"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3514-420X","authenticated-orcid":false,"given":"Matthew","family":"Amy","sequence":"first","affiliation":[{"name":"Simon Fraser University, Burnaby, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-0253-9227","authenticated-orcid":false,"given":"Joseph","family":"Lunderville","sequence":"additional","affiliation":[{"name":"Simon Fraser University, Burnaby, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.287.1"},{"key":"e_1_3_2_3_2","unstructured":"Matthew Amy. 2019. Formal Methods in Quantum Circuit Design. Ph. D. Dissertation. University of Waterloo. http:\/\/hdl.handle.net\/10012\/14480"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/ab9359"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","unstructured":"Matthew Amy and Joseph Lunderville. 2024. Linear and Non-linear Relational Analyses for Quantum Program Optimization: Artifact. https:\/\/doi.org\/10.5281\/zenodo.13921830 10.5281\/zenodo.13921830","DOI":"10.5281\/zenodo.13921830"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2014.2341953"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.2019.2906374"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.52.3457"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539796300921"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.22331\/q-2023-11-20-1185"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2008.02.017"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/1088216.1088219"},{"key":"e_1_3_2_13_2","volume-title":"Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra","author":"Cox David A.","year":"2010","unstructured":"David A. Cox, John Little, and Donal O\u2019Shea. 2010. Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra (3rd ed.). Springer Publishing Company, Incorporated.","edition":"3"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3505636"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632867"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.26421\/QIC5.2-2"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TQC.2020.11"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.102.110502"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/2651361"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(99)00005-5"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.06.011"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2023.105077"},{"key":"e_1_3_2_23_2","volume-title":"Quantum mechanics and path integrals","author":"Feynman Richard P.","year":"1965","unstructured":"Richard P. Feynman and Albert R. Hibbs. 1965. Quantum mechanics and path integrals. McGraw-Hill."},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.86.032324"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21493-6_9"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1038\/46503"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428201"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/aad604"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434318"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3491247"},{"key":"e_1_3_2_31_2","unstructured":"Ali Javadi-Abhari Matthew Treinish Kevin Krsulich Christopher J. Wood Jake Lishman Julien Gacon Simon Martiel Paul D. Nation Lev S. Bishop Andrew W. Cross Blake R. Johnson and Jay M. Gambetta. 2024. Quantum computing with Qiskit. (2024). arXiv:2405.08810 [quant-ph]"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_3"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_26"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.318.14"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.102.022406"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.22331\/q-2019-03-05-128"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.93.022311"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_85"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964029"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1038\/s41534-018-0072-4"},{"key":"e_1_3_2_42_2","volume-title":"Quantum Computation and Quantum Information","author":"Nielsen Michael A.","year":"2000","unstructured":"Michael A. Nielsen and Isaac L. Chuang. 2000. Quantum Computation and Quantum Information. Cambridge University Press."},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_18"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/1005285.1005324"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611973075.37"},{"key":"e_1_3_2_47_2","unstructured":"Francisco J. R. Ruiz Tuomas Laakkonen Johannes Bausch Matej Balog Mohammadamin Barekatain Francisco J. H. Heras Alexander Novikov Nathan Fitzpatrick Bernardino Romera-Paredes John van de Wetering Alhussein Fawzi Konstantinos Meichanetzidis and Pushmeet Kohli. 2024. Quantum Circuit Optimization with AlphaTensor. (2024). arXiv:2402.14396"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964028"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1994.365700"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/ab8e92"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.26421\/QIC10.9-10-12"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/322261.322273"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/322261.322272"},{"key":"e_1_3_2_54_2","unstructured":"John van de Wetering. 2024. Private communication."},{"key":"e_1_3_2_55_2","doi-asserted-by":"crossref","unstructured":"Vivien Vandaele. 2024. Lower T-count with faster algorithms. (2024). arXiv:2407.08695","DOI":"10.22331\/q-2025-09-16-1860"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71995-1_27"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591254"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454061"},{"key":"e_1_3_2_60_2","unstructured":"Fang Zhang and Jianxin Chen. 2019. Optimizing T gates in Clifford+T circuit as \u03c0\/4 rotations around Paulis. (2019). arXiv:1903.12456"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704873","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704873","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:18:05Z","timestamp":1770200285000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704873"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":59,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704873"],"URL":"https:\/\/doi.org\/10.1145\/3704873","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}