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.
LanguageEnglish
Pages23-43
Number of pages20
JournalAnnals of Mathematics and Artificial Intelligence
Volume56
Issue number1
DOIs
Publication statusPublished - May 2009

Fingerprint

Quantum computers
Quantum Computation
Reasoning
Closed
Graph in graph theory
Visualization
Proof System
Symbolic Computation
Notation
Manipulation
kernel
Graphics

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

@article{2cfa85aa10d5458f9257cf5803271465,
title = "Graphical reasoning in compact closed categories for quantum computation",
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.",
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",
author = "Lucas Dixon and Ross Duncan",
year = "2009",
month = "5",
doi = "10.1007/s10472-009-9141-x",
language = "English",
volume = "56",
pages = "23--43",
journal = "Annals of Mathematics and Artificial Intelligence",
issn = "1012-2443",
number = "1",

}

Graphical reasoning in compact closed categories for quantum computation. / Dixon, Lucas; Duncan, Ross.

In: Annals of Mathematics and Artificial Intelligence, Vol. 56, No. 1, 05.2009, p. 23-43.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Graphical reasoning in compact closed categories for quantum computation

AU - Dixon, Lucas

AU - Duncan, Ross

PY - 2009/5

Y1 - 2009/5

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.

AB - 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.

KW - graphical reasoning

KW - compact

KW - closed categories

KW - quantum computation

KW - 05C20

KW - 81P68

KW - graph rewriting

KW - quantum computing

KW - categorical logic

KW - interactive theorem proving

KW - graphical calculi

KW - ellipses notation

KW - 03G30

KW - 18C10

KW - 03G12

U2 - 10.1007/s10472-009-9141-x

DO - 10.1007/s10472-009-9141-x

M3 - Article

VL - 56

SP - 23

EP - 43

JO - Annals of Mathematics and Artificial Intelligence

T2 - Annals of Mathematics and Artificial Intelligence

JF - Annals of Mathematics and Artificial Intelligence

SN - 1012-2443

IS - 1

ER -