Re: [Axiom-developer] Introduction to Category Theory

[Bill Page]

Martin,

If you are thinking about category theory and graphical calculus you
might be interesting in

http://sites.google.com/site/quantomatic/
http://dream.inf.ed.ac.uk/projects/quantomatic/
https://groups.google.com/forum/#!forum/quantomatic
http://sites.google.com/site/quantomatic/publications

A lot of this work is being done in the context of quantum computation
but the tools are much more general. The system uses the theorem
proving package Isabelle

http://www.cl.cam.ac.uk/research/hvg/Isabelle/

to reason about graphs and Poly/ML (a variant of standard ML that is
even more like SPAD) and Java for data structures and GUI.

This video

http://www.cs.ox.ac.uk/quantum/content/1005019/

is a pretty good introduction.

I became especially interested in this while implementing linear
operators as an extension of the Axiom CartesianTensor domain. See:

http://axiom-wiki.newsynthesis.org/LinearOperator

I think it would be great if there was a group of people who were
motivated to add something like this to Axiom.

Regards,
Bill Page.


On Wed, Aug 17, 2011 at 12:52 PM, Martin Baker <address@hidden> wrote:
> On Wednesday 17 Aug 2011 05:24:41 address@hidden wrote:
>> It seems that the Category Theory discussion has come around again on the
>> great wheel of life. These talks might be helpful for those who are lost.
>>
>> part 1: http://vimeo.com/17207564
>> part 2: http://www.youtube.com/watch?v=yilkBvVDB_w
>
> Tim,
>
> These are very good, I haven't come across them before.
>
> I especially like part 2 and the link between category theory string diagrams
> and combinators. Its interesting about adding iterators to combinators, it
> would be good to implement that.
>
> Also there was a throwaway line, something about removing the crossover
> cancellation rule from combinators gives braids. I thought before that it
> would be interesting to implement braid groups and I wonder if it could be
> done using combinators?
>
> Also string diagrams/combinators being so graphical reminds me once again how
> much I would like a 2-way graphical interface to Axiom.
>
> Martin
>
> _______________________________________________
> Axiom-developer mailing list
> address@hidden
> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>