Sciweavers

Share
AISC
2008
Springer

Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation

11 years 7 months ago
Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation
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. Key words: graph rewriting, quantum computing, categorical logic, interactive theorem proving, graphical calculi.
Lucas Dixon, Ross Duncan
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where AISC
Authors Lucas Dixon, Ross Duncan
Comments (0)
books