Algorithms arising from category theory

Algorithms arising from category theory

[Mike Stay]

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

Re: Algorithms arising from category theory

[Altenkirch Thorsten]

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

Re: Algorithms arising from category theory

[Jeremy Gibbons]

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

Re: Algorithms arising from category theory

[Jocelyn Ireson-Paine]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: MULTIPART/MIXED; BOUNDARY="1566387330-329797118-1350414111=:21164", Size: 5312 bytes --]

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/Rydeheard%20D.E.,%20Burstall%20R.M.%20Computational%20category%20theory%20(c.%201990)(263s).pdf 
, "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%253AACATUO%253E/www1.elsevier.com%252Fgej-ng%252F31%252F29%252F23%252F120%252F52%252F26%252F66.5.004.pdf 
, "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.pdf, 
"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/ ]

Re: Algorithms arising from category theory

[Robert Harper]

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

Re: Algorithms arising from category theory

[Robin Houston]

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

Re: Algorithms arising from category theory

[Martin Escardo]

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

Re: Algorithms arising from category theory

[Mike Stay]

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

Re: Algorithms arising from category theory

[Barbara Koenig]

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

Re: Algorithms arising from category theory

[Zinovy Diskin]

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