Automating Equational Proofs in Dirac Notation
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866916487730561024 |
|---|---|
| author | Xu, Yingte Barthe, Gilles Zhou, Li |
| author_facet | Xu, Yingte Barthe, Gilles Zhou, Li |
| contents | Dirac notation is widely used in quantum physics and quantum programming languages to define, compute and reason about quantum states. This paper considers Dirac notation from the perspective of automated reasoning. We prove two main results: first, the first-order theory of Dirac notation is decidable, by a reduction to the theory of real closed fields and Tarski's theorem. Then, we prove that validity of equations can be decided efficiently, using term-rewriting techniques. We implement our equivalence checking algorithm in Mathematica, and showcase its efficiency across more than 100 examples from the literature. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_11617 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Automating Equational Proofs in Dirac Notation Xu, Yingte Barthe, Gilles Zhou, Li Programming Languages Dirac notation is widely used in quantum physics and quantum programming languages to define, compute and reason about quantum states. This paper considers Dirac notation from the perspective of automated reasoning. We prove two main results: first, the first-order theory of Dirac notation is decidable, by a reduction to the theory of real closed fields and Tarski's theorem. Then, we prove that validity of equations can be decided efficiently, using term-rewriting techniques. We implement our equivalence checking algorithm in Mathematica, and showcase its efficiency across more than 100 examples from the literature. |
| title | Automating Equational Proofs in Dirac Notation |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2411.11617 |