Graphical reasoning in compact closed categories for quantum computation

Dixon, Lucas and Duncan, Ross (2009) Graphical reasoning in compact closed categories for quantum computation. Annals of Mathematics and Artificial Intelligence, 56 (1). pp. 23-43. ISSN 1012-2443 (https://doi.org/10.1007/s10472-009-9141-x)

Full text not available in this repository.Request a copy

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.

ORCID iDs

Dixon, Lucas and Duncan, Ross ORCID logoORCID: https://orcid.org/0000-0001-6758-1573;
CORE (COnnecting REpositories)