Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation
Lucas Dixon and Ross Duncan abstract
Graph-based formalisms of quantum computation provide an abstract and symbolic way to represent and simulate computations. However, manual manipulation of such graphs is slow and error prone. We present a formalism, based on compact closed categories, that supports mechanised reasoning about such graphs. This gives a compositional account of graph rewriting that preserves the underlying categorical semantics. Using this representation, we describe a generic system with a fixed logical kernel that supports reasoning about models of compact closed category. A salient feature of the 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.
infobook title | Intelligent Computer Mathematics, 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings |
editor | Autexier, Serge and Campbell, John and Rubio, Julio and Sorge, Volker and Suzuki, Masakazu and Wiedijk, Freek |
keywords | rewriting; quantum computing; categorical logic; interactive theorem proving; graphical calculi |
pages | 77-92 |
publisher | Springer |
series | Lecture Notes in Computer Science |
volume | 5144 |
year | 2008 |
links
BibTeX
Download
DOI (10.1007/978-3-540-85110-3_8)
related pages
|
