Dear Mike, thanks for posting the citation. I enjoyed reading the argument, which might help to convince others of the usefulness of categorical techniques, also when it comes to algorithmic problems. Coalgebraic techniques have often been used to obtain concrete algorithms, methods and proof principles for behavioural equivalences, with applications to system verification. For instance, we have recently proposed an abstract minimization (and determinization) algorithm that instantiates to well-known constructions for finite automata. Jirí Adámek, Filippo Bonchi, Mathias Hülsbusch, Barbara König, Stefan Milius, Alexandra Silva: A Coalgebraic Perspective on Minimization and Determinization. FoSSaCS 2012 In this context see also Sam Staton: Relating coalgebraic notions of bisimulation Logical Methods in Computer Science 7(1): (2011) and many other papers on coalgebra, for instance by Jan Rutten. Barbara Mike Stay <metaweta@gmail.com> writes:
I'd like to get more computer programmers interested in category theory. There's the obvious connection to type theory and categorical semantics, but programmers are usually far more interested in algorithms. Recently I found the excellent paper "Generalizing Compiler Optimizations from Proofs" by Tate, Stepp, and Lerner. They write,
"Some have asked us why we abstracted our proof generalization technique at all, and why we used category theory as our abstraction. However, we actually designed the abstract algorithm first, using category theory, and then used that to figure out how to solve our concrete problem. We got stuck with the concrete problem, overwhelmed by the details and the variables, and any solution we could think of seemed arbitrary. In order to reflect and simplify, we decided to phrase our question categorically. This lead to a diagram of sources and sinks, so we just used pushouts and pullbacks to glue things together. The biggest challenge was coming up with pushout completions, rather than using some existing standard concept. The categorical formulation was easy to specify and reason about. Afterwards, we instantiated the abstract processes, such as pushouts, with concrete algorithms, such as unification, in order to produce our final implementation with strong generality guarantees.
"We have actually found this process of abstracting to category theory whenever we get stuck to be quite fruitful. Not only does it end up solving our concrete problem, but we end up with a better understanding of our own problem as well as an abstract solution which can be easily adapted to other applications. Thus, our experience suggests that category theory may be useful in constructing actual algorithms, in addition to being useful as a framework for formalization. We would be interested to know of other similar experiences, either positive or negative."
Can any readers point me to other algorithms that were discovered by turning to category theory or to reports of problems solved by realizing they were instances of an abstraction of another solved problem?
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]