Edinburgh Research Explorer

Graphical reasoning in compact closed categories for quantum computation

Research output: Contribution to journalArticle

Original languageEnglish
Pages (from-to)23-42
Number of pages20
JournalAnnals of Mathematics and Artificial Intelligence
Volume56
Issue number1
DOIs
StatePublished - 2009

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 reasoning about compact closed categories. 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.

ID: 6361577