Skip to main content
5 of 5
Commonmark migration

Quantum Computation

One very interesting area is the application of various monoidal categories to quantum computation. Some could argue that this is also physics, but the work is done by people in computer science departments. An early paper in this area is A categorical semantics of quantum protocols by Samson Abramsky and Bob Coecke; many recent papers by Abramsky and Coecke and others continue work in this direction.

In this body of work the quantum protocols are axiomatised as (certain kinds of) compact closed categories. Such categories have a beautiful graphical language in terms of string (and ribbon) diagrams. Equations in the category correspond to certain movements of the strings, such as straightening a tangled but not knotted string, which in turn correspond to something meaningful in quantum mechanics, such as a quantum teleportation.

The categorical approach offers a high level, logical view on what typically involves very low level calculations.

Theory of Systems

Coalgebra has been used as a general framework to model systems (streams, automata, transition systems, probabilistic systems). Its theory is rooted in category theory, being based on the notion of $F$-coalgebra, where $F$ is a functor that describes the structure of the transition system. Thus, the kind of system changes with the underlying functor, but much of the theory, such as the notion of bisimulation, is applicable for all functors. Category theory also enables the modular construction of modal logics for reasoning about systems described as coalgebras.

Graph Transformations

Graph transformations can be expressed quite nicely in the language of category theory. This has found application, for example, in model transformation (as in UML models) and other visual modelling formalisms. The approach takes place in the category of graphs and graph homomorphisms. Firstly, a pushout can be seen as a gluing construction: Given two graphs $G_1,G_2$. A graph $P$ and two morphisms $e_1:P\to G_1$ and $e_2:P\to G_2$ denote the parts the two graphs have in common. The pushout unifies these parts, adding in the remaining parts of $G_1$ and $G_2$, in effect, gluing $G_1$ and $G_2$ together along $P$.

A double pushout is used to describe a graph transformation. The rule is represented by a tuple $(L, K, R)$, where $L$ denotes the precondition of the rule, $R$ denotes the post condition of the rule, and $K$ denotes the part of the graph to apply the rule to. There are maps from $l:K\to L$ and $r:K\to R$, one of which will be used to match a part of the original graph, the other to create the resulting graph. $L\setminus K$ describes the part of the graph to be deleted. $R\setminus K$ describes the the part to be created. A map $d$ from $K$ into a context graph $D$ needs to be provided, and the pushout of $d$ and the map $l$ needs to equal the graph of interest $G$. The pushout of $d$ and $k$ then gives the result of performing the transformation.

Programming Languages (via MathOverflow)

There have been plenty of applications of category theory in the design of programming languages and programming language theory. Extensive answers can be found on MathOverflow. https://mathoverflow.net/questions/3721/programming-languages-based-on-category-theory) https://mathoverflow.net/questions/4235/relating-category-theory-to-programming-language-theory.

Bigraphs -- Process Calculi

Finally, there's Milner's bigraphs, a general framework for describing and reasoning about systems of interacting agents. It can be seen as a general framework for reasoning about process algebras and their structural and behavioural theories. The approach is also based on pushouts.

Dave Clarke
  • 16.7k
  • 3
  • 61
  • 106