Open Graphs and Computational Reasoning

TL;DR

This paper introduces a graph-based algebraic reasoning framework for modeling and simulating various computational systems, including electronic circuits and quantum information, through compositional graph rewriting rules.

Contribution

It presents a novel algebraic approach for reasoning about computational objects using graphs with rich compositional principles and rewriting rules.

Findings

Graphs can encode diverse computational models like circuits and quantum systems.

Rewriting rules enable simulation of computational dynamics.

The framework supports formal reasoning and derivation of new rules.

Abstract

We present a form of algebraic reasoning for computational objects which are expressed as graphs. Edges describe the flow of data between primitive operations which are represented by vertices. These graphs have an interface made of half-edges (edges which are drawn with an unconnected end) and enjoy rich compositional principles by connecting graphs along these half-edges. In particular, this allows equations and rewrite rules to be specified between graphs. Particular computational models can then be encoded as an axiomatic set of such rules. Further rules can be derived graphically and rewriting can be used to simulate the dynamics of a computational system, e.g. evaluating a program on an input. Examples of models which can be formalised in this way include traditional electronic circuits as well as recent categorical accounts of quantum information.