License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2023.36
URN: urn:nbn:de:0030-drops-174974
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/17497/
Go to the corresponding LIPIcs Volume Portal

Vilmart, Renaud

Completeness of Sum-Over-Paths for Toffoli-Hadamard and the Dyadic Fragments of Quantum Computation

pdf-format:
LIPIcs-CSL-2023-36.pdf (0.8 MB)

Abstract

The "Sum-Over-Paths" formalism is a way to symbolically manipulate linear maps that describe quantum systems, and is a tool that is used in formal verification of such systems.
We give here a new set of rewrite rules for the formalism, and show that it is complete for "Toffoli-Hadamard", the simplest approximately universal fragment of quantum mechanics. We show that the rewriting is terminating, but not confluent (which is expected from the universality of the fragment). We do so using the connection between Sum-over-Paths and graphical language ZH-Calculus, and also show how the axiomatisation translates into the latter.
Finally, we show how to enrich the rewrite system to reach completeness for the dyadic fragments of quantum computation - obtained by adding phase gates with dyadic multiples of π to the Toffoli-Hadamard gate-set - used in particular in the Quantum Fourier Transform.

BibTeX - Entry

@InProceedings{vilmart:LIPIcs.CSL.2023.36,
  author =	{Vilmart, Renaud},
  title =	{{Completeness of Sum-Over-Paths for Toffoli-Hadamard and the Dyadic Fragments of Quantum Computation}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{36:1--36:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/17497},
  URN =		{urn:nbn:de:0030-drops-174974},
  doi =		{10.4230/LIPIcs.CSL.2023.36},
  annote =	{Keywords: Quantum Computation, Verification, Sum-Over-Paths, Rewrite Strategy, Toffoli-Hadamard, Completeness}
}

Keywords: Quantum Computation, Verification, Sum-Over-Paths, Rewrite Strategy, Toffoli-Hadamard, Completeness
Collection: 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)
Issue Date: 2023
Date of publication: 01.02.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI