Skip to main content

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.

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