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 gr...
| Main Authors: | , |
|---|---|
| Format: | Conference item |
| Published: |
Springer
2008
|
| _version_ | 1797091889083580416 |
|---|---|
| author | Dixon, L Duncan, R |
| author_facet | Dixon, L Duncan, R |
| author_sort | Dixon, L |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T03:38:48Z |
| format | Conference item |
| id | oxford-uuid:bd30c667-2951-4d30-8610-7179b78b7061 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T03:38:48Z |
| publishDate | 2008 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:bd30c667-2951-4d30-8610-7179b78b70612022-03-27T05:29:52ZExtending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum ComputationConference itemhttp://purl.org/coar/resource_type/c_5794uuid:bd30c667-2951-4d30-8610-7179b78b7061Department of Computer ScienceSpringer2008Dixon, LDuncan, RGraph-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. |
| spellingShingle | Dixon, L Duncan, R Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation |
| title | Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation |
| title_full | Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation |
| title_fullStr | Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation |
| title_full_unstemmed | Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation |
| title_short | Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation |
| title_sort | extending graphical representations for compact closed categories with applications to symbolic quantum computation |
| work_keys_str_mv | AT dixonl extendinggraphicalrepresentationsforcompactclosedcategorieswithapplicationstosymbolicquantumcomputation AT duncanr extendinggraphicalrepresentationsforcompactclosedcategorieswithapplicationstosymbolicquantumcomputation |