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.
Details
| Book 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
DOI (10.1007/978-3-540-85110-3_8)
Related pages
|
People |
|
|
Projects |
|
|
Activities |
|
|
Themes |