Graphical Reasoning in Compact Closed Categories for Quantum Computation

TL;DR

This paper develops a formal proof system for equational reasoning on graph-based representations of compact closed categories, with applications to quantum computation, enabling automated and symbolic reasoning.

Contribution

It introduces a generic, formal proof system for graph-based reasoning in compact closed categories, specifically tailored for quantum computation applications.

Findings

Automated reasoning on graph representations is feasible and reliable.

The system supports ellipses-style notation for derived results.

Application to quantum computation demonstrates practical utility.

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.