Graphical Reasoning in Compact Closed Categories for Quantum Computation Export

@article{citeulike:4009848, abstract = {Compact closed categories provide a foundational formalism for a variety of important domains, including quantum computation. These categories have a natural visualisation as a form of graphs. We present a formalism for equational reasoning about such graphs and develop this into a generic proof system with a fixed logical kernel for equational reasoning about compact closed categories. Automating this reasoning process is motivated by the slow and error prone nature of manual graph manipulation. A salient feature of our 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.}, archivePrefix = {arXiv}, author = {Dixon, Lucas and Duncan, Ross}, citeulike-article-id = {4009848}, citeulike-linkout-0 = {http://arxiv.org/abs/0902.0514}, citeulike-linkout-1 = {http://arxiv.org/pdf/0902.0514}, eprint = {0902.0514}, keywords = {category-theory, computation, graphs, logic, printed, quantum-computation}, month = {Feb}, posted-at = {2009-02-05 01:03:30}, priority = {3}, title = {Graphical Reasoning in Compact Closed Categories for Quantum Computation}, url = {http://arxiv.org/abs/0902.0514}, year = {2009} }

TY - JOUR ID - citeulike:4009848 L3 - citeulike-article-id:4009848 N2 - Compact closed categories provide a foundational formalism for a variety of important domains, including quantum computation. These categories have a natural visualisation as a form of graphs. We present a formalism for equational reasoning about such graphs and develop this into a generic proof system with a fixed logical kernel for equational reasoning about compact closed categories. Automating this reasoning process is motivated by the slow and error prone nature of manual graph manipulation. A salient feature of our 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. TI - Graphical Reasoning in Compact Closed Categories for Quantum Computation KW - category-theory KW - computation KW - graphs KW - logic KW - printed KW - quantum-computation AU - Dixon, Lucas AU - Duncan, Ross PY - 2009/Feb/03/ UR - http://arxiv.org/abs/0902.0514 ER -