Graphical Reasoning in Compact Closed Categories for Quantum Computation
Lucas Dixon and Ross Duncan
Abstract
Compact closed categories provide a foundational formalism for a variety of important domains, including quantum computation. These categories have a natural visualisation as a form of graphs. We present a formalism for equational reasoning about such graphs and develop this into a generic proof system with a fixed logical kernel for equational reasoning about compact closed categories. Automating this reasoning process is motivated by the slow and error prone nature of manual graph manipulation. A salient feature of our system is that it provides a formal and declarative account of derived results that can include `ellipses'-style notation. We illustrate the framework by instantiating it for a graphical language of quantum computation and show how this can be used to perform symbolic computation.
Details
| Journal |
Annals of Mathematics and Artificial Intelligence |
| Keywords |
categorical quantum mechanics; compact closed categories; rewriting; graphical calculi |
| Note |
preprint available at http://arxiv.org/abs/0902.0514 |
| Year |
2009 |
Links
DOI (10.1007/s10472-009-9141-x)
Related pages
|
People |
|
|
Projects |
|
|
Activities |
|
|
Themes |