Graphical reasoning in compact closed categories for quantum computation

Lucas Dixon, Ross Duncan

Research output: Contribution to journalArticle

15 Citations (Scopus)

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.
Original languageEnglish
Pages (from-to)23-43
Number of pages20
JournalAnnals of Mathematics and Artificial Intelligence
Volume56
Issue number1
DOIs
Publication statusPublished - May 2009

    Fingerprint

Keywords

  • graphical reasoning
  • compact
  • closed categories
  • quantum computation
  • 05C20
  • 81P68
  • graph rewriting
  • quantum computing
  • categorical logic
  • interactive theorem proving
  • graphical calculi
  • ellipses notation
  • 03G30
  • 18C10
  • 03G12

Cite this