Algorithms arising from category theory
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? -- Mike Stay - metaweta@gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Hmm, an example may be the decision procedure for lambda calculus with coproducts using normalisation by evaluation. The known NBE algorithm for ordinary lambda calculus could be understood using presheaf semantics while you need sheaves to interpret coproducts. So sheaf theory certainly inspired this development but there were a number of technical issues which go beyond it. @InProceedings{alti:lics01, author = "Thorsten Altenkirch and Peter Dybjer and Martin Hofmann and Phil Scott", title = "Normalization by evaluation for typed lambda calculus with coproducts", pages = "303-310", booktitle = "16th Annual IEEE Symposium on Logic in Computer Science", year = "2001", www = "http://www.cs.nott.ac.uk/~txa/publ/lics01.pdf" } Cheers, Thorsten On 15/10/2012 17:42, "Mike Stay" <metaweta@gmail.com> wrote:
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? -- Mike Stay - metaweta@gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
a good chunk of generic programming can be seen as exploiting the functorial action of a type constructor. see chapter 14 of my "practical foundations for programming languages" for an exposition of this viewpoint. bob On Oct 16, 2012, at 4:46 AM, Altenkirch Thorsten wrote:
Hmm, an example may be the decision procedure for lambda calculus with coproducts using normalisation by evaluation. The known NBE algorithm for ordinary lambda calculus could be understood using presheaf semantics while you need sheaves to interpret coproducts. So sheaf theory certainly inspired this development but there were a number of technical issues which go beyond it.
@InProceedings{alti:lics01, author = "Thorsten Altenkirch and Peter Dybjer and Martin Hofmann and Phil Scott", title = "Normalization by evaluation for typed lambda calculus with coproducts", pages = "303-310", booktitle = "16th Annual IEEE Symposium on Logic in Computer Science", year = "2001", www = "http://www.cs.nott.ac.uk/~txa/publ/lics01.pdf" }
Cheers, Thorsten
On 15/10/2012 17:42, "Mike Stay" <metaweta@gmail.com> wrote:
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? -- Mike Stay - metaweta@gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On 15 Oct 2012, at 17:42, Mike Stay wrote:
Can any readers point me to other algorithms that were discovered by turning to category theory
My colleague Ralf Hinze and some others in my group just published a paper at WGP 2012 relating different sorting algorithms using bi-algebras: http://dx.doi.org/10.1145/2364394.2364405 (also available through their webpages). For example, naive insertion sort and naive bubblesort are "essentially" the same algorithm, with dual presentations. The same duality technique can be used to obtain some new sorting algorithms from existing ones; in particular, they come up with a "minglesort" as a dual to heapsort. (I'm not claiming that's a world-changing discovery, but it's elegant work.) Jeremy Jeremy.Gibbons@cs.ox.ac.uk Oxford University Department of Computer Science, Wolfson Building, Parks Road, Oxford OX1 3QD, UK. +44 1865 283521 http://www.cs.ox.ac.uk/people/jeremy.gibbons/ [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On Mon, 15 Oct 2012, Mike Stay wrote:
I'd like to get more computer programmers interested in category theory.
Yes!
There's the obvious connection to type theory and categorical semantics, but programmers are usually far more interested in algorithms. ... 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?
In http://kolxo3.tiera.ru/M_Mathematics/MA_Algebra/MAct_Category%20theory/Rydeh... , "Computational Category Theory", David Rydeheard and Rod Burstall derive an algorithm for unifying terms (in the sense used in logic programming), treating it as the construction of coequalisers. (Their original paper, "A Categorical Unification Algorithm", is on the Web, but I can only find copies that are locked up behind a Springer paywall.) There are more recent such algorithms, e.g. http://docis.info/docis/lib/goti/rclis/dbl/enitcs/(2002)66%253A5%253C%253AAC... , "A categorical approach to unification of generalised terms" by Eklund, Galán, Medina, Ojeda-Aciego and Valverde. My "Excelsior" spreadsheet-modularisation software, described in http://www.j-paine.org/calco2011/paper.html , "Module Expressions for Modularising Spreadsheets and Sharing Code between Them", was inspired by category theory, specifically by Joseph Goguen's sheaf semantics for interacting objects. Goguen has used colimits and 3/2-colimits to model conceptual blending and the interpretation of metaphors: http://cseweb.ucsd.edu/~goguen/pps/taspm.pdf , "Mathematical Models of Cognitive Space and Time". Michael Healy has used natural transformations and functors as a guide to combining neural networks: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.32.2635 , "Category Theory Applied to Neural Modeling and Graphical Representations". Michael Healy, Thomas Caudell, and Timothy Goldsmith have proposed that compound concepts could be represented as categorical diagrams, and that concepts could be compared by comparing these diagrams. They say that for some simple test examples, the results of these comparisons are fairly close to human performance, and that this is therefore worth considering as a mathematical model of human concept representation and comparison: http://repository.unm.edu/handle/1928/6724 , "A Model of Human Categorization and Similarity Based Upon Category Theory". Ronnie Brown and Tim Porter suggest that higher-dimensional algebra and colimits might be useful for sensoty integration, though they don't develop any algorithms: http://arxiv.org/PS_cache/math/pdf/0306/0306223v1.pdf , "Category Theory and Higher Dimensional Algebra: potential descriptive tools in neuroscience". Manfred Liebmann has used multicategories and operads as a guide to designing parallel numerical algorithms: http://paralleltoolbox.sourceforge.net/categorytheory.pdf , "Category Theory and the Design of Parallel Numerical Algorithms". There has been a lot of work on merging ontologies by using categorical constructions, usually pushout and colimit. See e.g. Pascal Hitzler, Markus Krötzsch, Marc Ehrig, York Sure in http://knoesis.cs.wright.edu/faculty/pascal/resources/publications/cando05.p..., "What Is Ontology Merging? - A Category-Theoretical Perspective Using Pushouts" and Google "combining ontologies categorically". I once suggested that, via algebraic-specification languages such as CafeOBJ, category theory could be used to guide the construction and modularisation of large Web sites: http://www.j-paine.org/alg_web_spec.html , "Algebraic Web specification". There's quite a lot of other stuff out there. I hope these examples fit the spirit of Mike's question. Quite often, it seems that the authors use category theory as a guide, searching it for constructions that they might instantiate as data structures. They then devise algorithms to build these structures. Usually, they do so informally, rather than by formally deriving the algorithm from a categorical definition. Very often, the categorical construction they use is a pushout or colimit. That's the impression I have, anyway. So what they're doing is along the lines suggested by Goguen in his "A Categorical Manifesto", http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.362 . By the way, in http://www.j-paine.org/dobbs/why_be_interested_in_categories.html , "What Might Category Theory do for Artificial Intelligence and Cognitive Science?", I suggest that these two fields are ripe for the plundering of apparently unrelated concepts that category theory might be able to unify.
Mike Stay - metaweta@gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com
Jocelyn Ireson-Paine http://www.j-paine.org/index.html Jocelyn's Cartoons http://www.j-paine.org/blog/jocelyns_cartoons/ [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On 15 October 2012 17:42, Mike Stay <metaweta@gmail.com> wrote:
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?
Hi Mike, I can offer a small example of both these phenomena, as recounted here: http://bosker.wordpress.com/2012/05/10/on-editing-text/ (This algorithm hasn’t actually been implemented yet, as far as I know, though it would not be hard.) All the best, Robin [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On 15/10/12 17:42, Mike Stay wrote:
I'd like to get more computer programmers interested in category theory.
Playing sequential games (such as chess) in an optimal way can be explained/derived categorically in a natural way: M.H. Escardo and Paulo Oliva. Selection functions, bar recursion, and backward induction. In Mathematical Structures in Computer Science, Volume 20, Issue 2, April 2010, Cambridge U.P. http://www.cs.bham.ac.uk/~mhe/papers/selection-escardo-oliva.pdf There is a tutorial with these and related ideas for mathematically minded functional programmers: M.H. Escardo and Paulo Oliva. What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common. In MSFP 2010 (ACM SIGPLAN Mathematically Structured Functional Programming, ACM Press). http://www.cs.bham.ac.uk/~mhe/papers/msfp2010/ The gist of the idea is this. Consider a cartesian closed category. For a functional programmer, this may be his programming language, where the objects are the types and the morphisms are the programs (probably keeping his fingers crossed and hiding his hands behind his back). Choose an object R of game "outcomes" (e.g. the reals if they are in your category, or 1+1+1 if your game is of the kind lose-draw-win). Define a strong monad J X = ((X->R)->X) where we write the exponential of R to the power X as (X->R). (Figure out the missing data.) An "element" of J X tells you how to (optimally) play a game that has just one move, where a move is an "element" of X. But now suppose you have a two-move game, with the first move in X and the second in Y. How do you (optimally) play this game? Simple: from the strength you get two maps J X x J Y -> J(X x Y). The monad is not commutative: you want the "left-to-right" map J X x J Y -> J(X x Y) for a sequential game (but the situation is symmetric, of course). What this map tells you is this: if you know how to play optimally the two one-move games on X and Y, then you know how to play optimally the sequential game on X x Y. If you have n moves, iterate this n times. If you have an unbounded number of moves, read the above papers. This is the rough idea. The second publication has computer programs coming from this idea, and some games completely worked out and implemented using this. There are applications to logic too, and to program extraction from classical proofs: Notice that J X -> X amounts to Peirce's Law. M.H. Escardo and Paulo Oliva. The Peirce translation. In APAL. http://www.cs.bham.ac.uk/~mhe/papers/peirce-revised.pdf Martin [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Thanks, everyone for your responses! They've been very helpful. On Mon, Oct 15, 2012 at 9:42 AM, Mike Stay <metaweta@gmail.com> wrote:
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? -- Mike Stay - metaweta@gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
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/ ]
There is an aspect of the story, which deserves a special mention. 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. ...
This seems to be a typical story of software design. Category theory provides a toolbox of design patterns, which can be useful before and irrespectively to an actual formalization. Tom Maibaum and I even wrote a paper trying to stress this aspect of CT: Category Theory and Model-Driven Engineering: From Formal Semantics to Design Patterns and Beyond http://rvg.web.cse.unsw.edu.au/eptcs/paper.cgi?ACCAT2012.1 Intuition of a healthy structure provided by CT is based on formal foundations, but its value goes beyond formal semantics. Cheers, Zinovy [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (9)
-
Altenkirch Thorsten -
Barbara Koenig -
Jeremy Gibbons -
Jocelyn Ireson-Paine -
Martin Escardo -
Mike Stay -
Robert Harper -
Robin Houston -
Zinovy Diskin