Il y a deux ans a été introduite la notion de “sum-over-paths” (SOP), avec des règles de
réécriture sur les termes, pour exprimer des évolutions quantiques, et potentiellement faire de
la vérification. Le formalisme a spécifiquement été introduit pour raisonner sur les circuits
quantiques, et une notion faible de complétude (qui permet de tester l'égalité de termes) a été
donnée pour le fragment “Clifford” de la mécanique quantique. Une barrière importante empêche
d'utiliser ce formalisme (avec son système de réécriture) pour attaquer le problème de simplification
de circuits : étant donné un morphisme de SOP, il n'existe pas de méthode pour extraire un circuit
qui représente ce morphisme. En fait, ces morphismes permettent même de représenter plus que
des unitaires (capturés par les circuits quantiques).
Nous montrons que SOP forme une catégorie dite “symétrique monoı̈dale †-compacte”. Cette
structure est notamment partagée par les langages graphiques comme le ZX-Calcul, le ZW-Calcul
et le ZH-Calcul. Nous montrons comment passer d'un morphisme de SOP à un diagramme
du ZH-Calculus équivalent, et vis-versa.
Une autre conséquence de la structure de la catégorie SOP est qu'il est possible d'y appliquer
la “construction discard”, ce qui permet d'enrichir le formalisme pour représenter la mesure.
Nous donnons un système de réécriture pour chacun des fragments Clifford des deux variantes
(avec et sans mesure). Nous montrons que ceux-ci sont complets, “terminants” et confluents dans
Clifford. Qui plus est, la réécriture termine en temps polynomial dans les deux cas.