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/ ]