Re: Algorithms arising from category theory

[Altenkirch Thorsten <psztxa@exmail.nottingham.ac.uk>]

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