[Axiom-math] Re: [Aldor-l] Hopf Algebra = Group + Monad

[David Casperson]

Hi Bill,

you may want to look at the work of the Charity group at the U of C.

Charity is a seriously category theoretical language that is explicitly 
aware of co-objects.  It is formally weaker than most programming 
languages in that any compiling program terminates.

It may be that a sub-language based on Charity like ideas is the correct 
language in which to formulate a calculus of types for a language with 
first class types like Aldor.

David
--
Dr. David Casperson, Assistant Professor     |  address@hidden
Department of Computer Science               |  (250)   960-6672 Fax 960-5544
College of Science and Management            |  3333 University Way
University of Northern British Columbia      |  Prince George, BC   V2N 4Z9
                                             |  CANADA

Bill Page, on 2008-08-07, you wrote:

> Date: Thu, 7 Aug 2008 11:45:28 -0400
> From: Bill Page <address@hidden>
> To: address@hidden, aldor-l <address@hidden>,
>     fricas-devel <address@hidden>,
>     open-axiom-devel <address@hidden>
> Subject: [Aldor-l] Hopf Algebra = Group + Monad
>
> Dear Axiom and Aldor users/developers;
>
> Here is an example of something that I would really like to work on in
> Axiom and/or Aldor:
>
> "Hopf Algebra = Group + Monad"
>
> http://sigfpe.blogspot.com/2008/08/hopf-algebra-group-monad.html
>
> by 'sigfpe' on the blog: "A Neighborhood of Infinity".
>
> This work is done using the programming language Haskell which
> although it does have a strong formal definition is not nearly as
> "categorical" as Axiom about the way it expressions mathematics. I
> hope that someday that people interested in this subject will be able
> to use Axiom and Aldor this way.
>
> In general I believe that computer algebra systems have not yet begun
> to catch up with recent developments in formal mathematics and in
> particular the ideas aboout co-algebra.
>
> The subject of co-algebra (and co-data) however has been a hot topic
> in programming language design and leads naturally semantics based on
> co-induction appropriate to "infinite" objects such as streams and
> generators. This leads back to the subject of exact real numbers and
> even p-adic numbers in computer algebra.
>
> For example it seems clear that support for concepts like "stream calculus"
>
> Elements of stream calculus (an extensive exercise in coinduction)
> by J. J.M.M. Rutten, 2001
>
> http://portal.acm.org/citation.cfm?id=869620
>
> could be easily added to the mathematical libraries implemented in
> strongly-typed computer algebra systems like Axiom and Aldor since
> they already support Stream and Generator data structures.
>
> The failure to treat co-algebraic properties on a par with algebraic
> properties is beginning to seem like a serious limitation for advanced
> applications of these systems especially since dual notions such as
> these arise naturally in the category theoretic treatment of almost
> any subject.
>
> Perhaps you know some other people working on this sort of thing? It
> would be very good to work together.
>
> Regards,
> Bill Page.
>
> _______________________________________________
> Aldor-l mailing list
> address@hidden
> http://aldor.org/mailman/listinfo/aldor-l_aldor.org