{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T13:04:25Z","timestamp":1760101465317,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The \"Sum-Over-Paths\" formalism is a way to symbolically manipulate linear\nmaps that describe quantum systems, and is a tool that is used in formal\nverification of such systems. We give here a new set of rewrite rules for the\nformalism, and show that it is complete for \"Toffoli-Hadamard\", the simplest\napproximately universal fragment of quantum mechanics. We show that the\nrewriting is terminating, but not confluent (which is expected from the\nuniversality of the fragment). We do so using the connection between\nSum-over-Paths and graphical language ZH-calculus, and also show how the\naxiomatisation translates into the latter. We provide generalisations of the\npresented rewrite rules, that can prove useful when trying to reduce terms in\npractice, and we show how to graphically make sense of these new rules. We show\nhow to enrich the rewrite system to reach completeness for the dyadic fragments\nof quantum computation, used in particular in the Quantum Fourier Transform,\nand obtained by adding phase gates with dyadic multiples of $\\pi$ to the\nToffoli-Hadamard gate-set. Finally, we show how to perform sums and\nconcatenation of arbitrary terms, something which is not native in a system\ndesigned for analysing gate-based quantum computation, but necessary when\nconsidering Hamiltonian-based quantum computation.<\/jats:p>","DOI":"10.46298\/lmcs-20(1:20)2024","type":"journal-article","created":{"date-parts":[[2024,3,8]],"date-time":"2024-03-08T10:40:09Z","timestamp":1709894409000},"source":"Crossref","is-referenced-by-count":1,"title":["Rewriting and Completeness of Sum-Over-Paths in Dyadic Fragments of Quantum Computing"],"prefix":"10.46298","volume":"Volume 20, Issue 1","author":[{"given":"Renaud","family":"Vilmart","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2024,3,7]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/13200\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/13200\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,8]],"date-time":"2024-03-08T10:40:09Z","timestamp":1709894409000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/11667"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,3,7]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-20(1:20)2024","relation":{"has-preprint":[{"id-type":"arxiv","id":"2307.14223v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2307.14223v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2307.14223","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2307.14223","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2024,3,7]]},"article-number":"11667"}}