* Algorithms arising from category theory
@ 2012-10-15 16:42 Mike Stay
2012-10-16 8:46 ` Altenkirch Thorsten
` (7 more replies)
0 siblings, 8 replies; 10+ messages in thread
From: Mike Stay @ 2012-10-15 16:42 UTC (permalink / raw)
To: categories
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/ ]
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Algorithms arising from category theory
2012-10-15 16:42 Algorithms arising from category theory Mike Stay
@ 2012-10-16 8:46 ` Altenkirch Thorsten
2012-10-16 19:46 ` Robert Harper
2012-10-16 18:21 ` Jeremy Gibbons
` (6 subsequent siblings)
7 siblings, 1 reply; 10+ messages in thread
From: Altenkirch Thorsten @ 2012-10-16 8:46 UTC (permalink / raw)
To: Mike Stay, categories
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/ ]
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Algorithms arising from category theory
2012-10-15 16:42 Algorithms arising from category theory Mike Stay
2012-10-16 8:46 ` Altenkirch Thorsten
@ 2012-10-16 18:21 ` Jeremy Gibbons
2012-10-16 19:42 ` Jocelyn Ireson-Paine
` (5 subsequent siblings)
7 siblings, 0 replies; 10+ messages in thread
From: Jeremy Gibbons @ 2012-10-16 18:21 UTC (permalink / raw)
To: categories
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/ ]
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Algorithms arising from category theory
2012-10-15 16:42 Algorithms arising from category theory Mike Stay
2012-10-16 8:46 ` Altenkirch Thorsten
2012-10-16 18:21 ` Jeremy Gibbons
@ 2012-10-16 19:42 ` Jocelyn Ireson-Paine
2012-10-16 19:52 ` Robin Houston
` (4 subsequent siblings)
7 siblings, 0 replies; 10+ messages in thread
From: Jocelyn Ireson-Paine @ 2012-10-16 19:42 UTC (permalink / raw)
To: Mike Stay; +Cc: categories
[-- 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/ ]
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Algorithms arising from category theory
2012-10-16 8:46 ` Altenkirch Thorsten
@ 2012-10-16 19:46 ` Robert Harper
0 siblings, 0 replies; 10+ messages in thread
From: Robert Harper @ 2012-10-16 19:46 UTC (permalink / raw)
To: Altenkirch Thorsten; +Cc: Mike Stay, categories
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/ ]
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Algorithms arising from category theory
2012-10-15 16:42 Algorithms arising from category theory Mike Stay
` (2 preceding siblings ...)
2012-10-16 19:42 ` Jocelyn Ireson-Paine
@ 2012-10-16 19:52 ` Robin Houston
2012-10-16 23:25 ` Martin Escardo
` (3 subsequent siblings)
7 siblings, 0 replies; 10+ messages in thread
From: Robin Houston @ 2012-10-16 19:52 UTC (permalink / raw)
To: Mike Stay; +Cc: categories
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/ ]
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Algorithms arising from category theory
2012-10-15 16:42 Algorithms arising from category theory Mike Stay
` (3 preceding siblings ...)
2012-10-16 19:52 ` Robin Houston
@ 2012-10-16 23:25 ` Martin Escardo
2012-10-17 18:51 ` Mike Stay
` (2 subsequent siblings)
7 siblings, 0 replies; 10+ messages in thread
From: Martin Escardo @ 2012-10-16 23:25 UTC (permalink / raw)
To: categories; +Cc: Paulo Oliva
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/ ]
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Algorithms arising from category theory
2012-10-15 16:42 Algorithms arising from category theory Mike Stay
` (4 preceding siblings ...)
2012-10-16 23:25 ` Martin Escardo
@ 2012-10-17 18:51 ` Mike Stay
2012-10-18 5:48 ` Barbara Koenig
2012-10-18 13:52 ` Zinovy Diskin
7 siblings, 0 replies; 10+ messages in thread
From: Mike Stay @ 2012-10-17 18:51 UTC (permalink / raw)
To: categories
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/ ]
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Algorithms arising from category theory
2012-10-15 16:42 Algorithms arising from category theory Mike Stay
` (5 preceding siblings ...)
2012-10-17 18:51 ` Mike Stay
@ 2012-10-18 5:48 ` Barbara Koenig
2012-10-18 13:52 ` Zinovy Diskin
7 siblings, 0 replies; 10+ messages in thread
From: Barbara Koenig @ 2012-10-18 5:48 UTC (permalink / raw)
To: categories
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/ ]
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Algorithms arising from category theory
2012-10-15 16:42 Algorithms arising from category theory Mike Stay
` (6 preceding siblings ...)
2012-10-18 5:48 ` Barbara Koenig
@ 2012-10-18 13:52 ` Zinovy Diskin
7 siblings, 0 replies; 10+ messages in thread
From: Zinovy Diskin @ 2012-10-18 13:52 UTC (permalink / raw)
To: Mike Stay; +Cc: categories
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/ ]
^ permalink raw reply [flat|nested] 10+ messages in thread
end of thread, other threads:[~2012-10-18 13:52 UTC | newest]
Thread overview: 10+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2012-10-15 16:42 Algorithms arising from category theory Mike Stay
2012-10-16 8:46 ` Altenkirch Thorsten
2012-10-16 19:46 ` Robert Harper
2012-10-16 18:21 ` Jeremy Gibbons
2012-10-16 19:42 ` Jocelyn Ireson-Paine
2012-10-16 19:52 ` Robin Houston
2012-10-16 23:25 ` Martin Escardo
2012-10-17 18:51 ` Mike Stay
2012-10-18 5:48 ` Barbara Koenig
2012-10-18 13:52 ` Zinovy Diskin
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).