[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] Introduction to Category Theory
From: |
Bill Page |
Subject: |
Re: [Axiom-developer] Introduction to Category Theory |
Date: |
Wed, 17 Aug 2011 18:23:46 -0400 |
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
>