Solid applications of category theory in TCS?

I've been learning a few bits of category theory. It certainly is a different way of looking at things. (Very rough summary for those who haven't seen it: category theory gives ways of expressing all kinds of mathematical behavior solely in terms of functional relationships between objects. For example, things like the Cartesian product of two sets are defined completely in terms of how other functions behave with it, not in terms of what elements are members of the set.)

I have some vague understanding that category theory is useful on the programming languages/logic (the "Theory B") side, and am wondering how much algorithms and complexity ("Theory A") could benefit. It might help me get off the ground though, if I know some solid applications of category theory in Theory B. (I am already implicitly assuming there are no applications in Theory A found so far, but if you have some of those, that's even better for me!)

By "solid application", I mean:

(1) The application depends so strongly on category theory that it's very difficult to achieve without using the machinery.

(2) The application invokes at least one non-trivial theorem of category theory (e.g. Yoneda's lemma).

It could well be that (1) implies (2), but I want to make sure these are "real" applications.

While I do have some "Theory B" background, it's been a while, so any de-jargonizing would be much appreciated.

(Depending on what kind of answers I get, I might turn this question into community wiki later. But I really want good applications with good explanations, so it seems a shame not to reward the answerer(s) with something.)

I can think of one instance where category theory was directly "applied" to solve an open problem in programming languages: Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Phil Scott, "Normalization by evaluation for typed lambda calculus with coproducts". From their abstract: "We solve the decision problem for simply typed lambda calculus with strong binary sums, equivalently the word problem for free cartesian closed categories with binary coproducts. Our method is based on the semantical technique known as 'normalization by evaluation' and involves inverting the interpretation of the syntax into a suitable sheaf model and from this extracting appropriate unique normal forms."

In general, though, I think that category theory is not usually applied to prove deep theorems in programming languages (of which there aren't so many), but instead offers a conceptual framework that is often useful (for example in the above, the idea of (pre)sheaf semantics).

An important historical example is Eugenio Moggi's suggestion that the notion of monad (which is basic and ubiquitous in category theory) could be used as part of a semantic explanation of side effects in programming languages (e.g., state, nondeterminism). This also inspired some reflection on the syntax of programming languages, for example leading directly to the "Monad typeclass" in Haskell (used to encapsulate effects).

More recently (the past decade), this explanation of effects in terms of monads has been revisited from the point of view of the old connection (established by category theorists, in the 60s) between monads and algebraic theories: see Martin Hyland and John Power's, "The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads". The idea is that the monadic view of effects is compatible with the (in some ways more appealing) algebraic view of effects, wherein effects (e.g., store) can be explained in terms of operations (e.g., "lookup" and "update") and associated equations (e.g., idempotency of update). There is a recent paper building on this connection by Paul-André Melliès, "Segal condition meets computational effects", which also relies heavily on ideas coming from "higher category theory" (for example the notion of "Yoneda structure" as a way of organizing presheaf semantics).

Another, related class of examples comes from linear logic. Soon after its introduction by Jean-Yves Girard in the 80s (with an aim of a better understanding of constructive logic), solid connections to category theory were established. For some explanation of this connection, see John Baez and Mike Stay's, "Physics, Topology, Logic and Computation: A Rosetta Stone".

Finally, this answer would be incomplete without reference to sigfpe's illuminating blog "A Neighborhood of infinity". In particular you could check out "A Partial Ordering of some Category Theory applied to Haskell".

• Hi Noam, I think that after that excellent answer, your rep is high enough to add links ! – Suresh Venkat Sep 4 '10 at 14:54
• I faced the same problem as a newbie. I just waited to get my answer voted up, then I put in the links. You could do the same... – Andrej Bauer Sep 4 '10 at 16:58
• Thanks! Sorry about the hyperlink restriction... wish there was some way to tell the system "yo, I'm Noam Zeilberger, I'm legit" – Ryan Williams Sep 4 '10 at 17:16
• added the links! Yeah it's a totally reasonable policy, just gets in the way sometimes. – Noam Zeilberger Sep 5 '10 at 10:14

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.

I am already implicitly assuming there are no applications in Theory A found so far, but if you have some of those, that's even better for me!

• My understanding is that Joyal's theory of species is used relatively widely in enumerative combinatorics, as a generalization of generating functions which additionally tell you how to permute things in addition to how many there are.

• Pippenger has applied Stone duality to relate regular languages and varieties of semigroups. Jeandel has introduced topological automata apply these ideas to give unified accounts (and proofs!) for quantum, probabilistic, and ordinary automata.

• Roland Backhouse has given abstract characterizations of greedy algorithms by means of Galois connections with the tropical semiring.

In a much more speculative vein, Noam mentioned sheaf models. These abstractly characterize the syntactic technique of logical relations, which is probably one of the most powerful techniques in semantics. We mostly use them to prove inexpressibility and consistency results, but it should be interesting for complexity theorists since it is a nice example of a practical non-natural (in the sense of Razborov/Rudich) proof technique. (However, logical relations are usually very carefully designed to guarantee that they relativize -- as language designers, we want to be able to assure programmers that function calls are black boxes!)

EDIT: I'll continue speculating, at Ryan's request. As I understand it, a natural proof is roughly one along the lines of trying to define an inductive invariant of the structure of a circuit, subject to various sensible conditions. Similar ideas are (unsurprisingly) pretty common in programming languages as well, when you try to define invariant maintained inductively by a lambda-calculus term (for instance, to prove type safety). 1

However, this technique often breaks down at higher (ie, function) types. For example, the simply-typed lambda calculus is total -- every program written in it terminates. However, straightforward attempts to prove this tend to founder on the problem of first-class functions: it's not enough to prove that every term of type $A \to B$ terminates. Since we can additionally apply arguments to functions, we not only need to ensure that every term of type $A \to B$ halts, we also need to ensure that this property holds "hereditarily" -- we also need to know that given any term of type $A$, the application will also halt.

This is what logical relations do. Instead of defining a single inductive invariant, we define a whole family of predicates by recursion over the structure of (typically) the type. Then, we prove that every definable term lies in the appropriate predicate, which lets us establish what we sought. So for termination, we would say that good values of base type are the values of base type, and the good values of type $A \to B$ are the values of this type which, given a good value of $A$, evaluates to a good value of $B$. Note that there is no single inductive invariant -- we define a whole family of invariants by recursion over the structure of the input, and use other means to show that all terms lie within these invariants. Proof-theoretically, this is a vastly stronger technique, and is why it lets you prove consistency results.

The connection to sheaves arises from the fact that we often need to reason about open terms (ie, terms with free variables), and so need to distinguish between getting stuck due to errors and getting stuck due to needing to reduce a variable. Sheaves arise from considering the reductions of the lambda calculus as defining the morphisms of a category whose terms are the objects (ie, the partial order induced by reduction), and then considering the functors from this category into sets (ie, predicates). Jean Gallier wrote some nice papers about this in the early 2000s, but I doubt they are readable unless you have already assimilated a fair amount of lambda calculus.

• Could you give a reference to the Backhouse paper? He has several that mention "Galois connection" in the title, but a quick search didn't obviously reveal which one is about greedy algorithms (and I don't think I'm familiar enough with the area to wade through the details and figure out easily which one is "really" about greedy algorithms). Thanks! – Joshua Grochow Sep 4 '10 at 18:41
• Along with Joshua's question, I'm also interested in how sheaf models and logical relations relate to natural proofs. – Ryan Williams Sep 4 '10 at 19:22
• Re: Stone duality, for more exciting recent work see Mai Gehrke's "Stone duality and the recognisable languages over an algebra" (math.ru.nl/~mgehrke/Ge09.pdf) and Gehrke, Grigorieff and Pin's "A topological approach to recognition" (math.ru.nl/~mgehrke/GGP10.pdf) – Noam Zeilberger Sep 5 '10 at 10:44
• Re: Gallier, you mean the late '90s (as in sciencedirect.com/science/article/pii/0304397594002800 ?) – Blaisorblade Mar 8 '15 at 0:40

There are many examples, the first one that comes to mind is Alex Simpson's use of category theory to prove properties of programming languages, see e.g. "Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory", Annals of Pure and Applied Logic, 130:207-275, 2004. Even though the title mentions set theory the technique is category-theoretic. See Alex's home page for more examples.

• Thanks for the refs, but please note that I did not ask: "what results were obtained by using category theory that could not be obtained otherwise?" – Ryan Williams Sep 4 '10 at 17:21
• True, you didn't. I edited my answer. – Andrej Bauer Sep 4 '10 at 20:15

I think you are asking two questions about applicability, type A and type B separately.

As you note, there are many substantive applications of category theory to type B topics: semantics of programming languages (monads, cartesian closed categories), logic and provability (topoi, varieties of linear logic).

However, there seems to be little substantive applications to theory A (algorithms or complexity).

There are some uses in elementary objects, such as describing categories of automata or combinatorial objects (graphs, sequences, permutations, etc). But these don't seem to account for a deeper understanding of language theory or algorithms.

Speculatively, it could be a mismatch between the current strategies of category theory and theory A subjects:

• The central strategy of category theory is dealing with equality (when things are the same and when they are different and how they map to each other).

• For complexity theory, the primary strategy is reductions and setting bounds (one would think a reduction is like an arrow, but I don't think anything beyond this superficial similarity has been studied).

• For algorithms, there is no overarching strategy to it other than ad hoc clever combinatorial thinking. For certain domains, I'd expect there could be fruitful exploration (algorithms for algebras?) but I haven't seen it yet.

• it turns out that reductions are related to categorical reconstructions of Goedel's Dialectica interpretation and the semantics of linear logic. See Andreas Blass's "Questions and Answers -- A Category Arising in Linear Logic, Complexity Theory, and Set Theory". math.lsa.umich.edu/~ablass/qa.pdf – Neel Krishnaswami Jul 23 '12 at 5:56

"TCS-A" applications that come to my mind are Joyal's combinatorial species (generalisations of power series to functors so as to describe combinatorial objects like trees, sets, multisets, etc) and the formalisation of cryptographic "game-hopping" using relational, probabilistic Hoare logic (Easycrypt, Certicrypt, Andreas Lochbihler's work). While categories do not directly appear in the latter they were instrumental in the development of the underlying logics (e.g. monads).

PS: Since my name was mentioned in the first answer: the use of fibrations of groupoids to show nonderivability of a certain axiom in Martin-Löf's type theory by Thomas Streicher and myself can also be considered a "solid" use of category theory (albeit in logic or "TCS-B").

The more recent book Seven Sketches in Compositionality lists several applications of category theory in computer science and engineering. Notable the chapter on databases where the authors describe querying, combining, migrating, and evolving databases based on a categorical model. The authors took this further and developed the Categorical Query Language (CQL) and an integrated development environment (IDE) based on their categorical model of databases.