[Axiom-math] Hopf Algebra = Group + Monad

[Bill Page]

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.

[Bill Page]

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

Thanks! I haven't looked at the Charity project for a while:

http://pll.cpsc.ucalgary.ca/charity1/www/home.html

but "Latest News" and "Download ..." suggests that there has not been
much development since 2000. Is that accurate? Is there work
continuing on this elsewhere?

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.

In the context of co-algebra is seems a little strange to consider
only programs that terminate.

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.

That is a very interesting idea.

Regards,
Bill Page.

[David Casperson]

Date: Thu, 7 Aug 2008 12:25:06 -0400
Subject: Re: [Aldor-l] Hopf Algebra = Group + Monad

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

http://pll.cpsc.ucalgary.ca/charity1/www/home.html
but "Latest News" and "Download ..." suggests that there has not been
much development since 2000. Is that accurate? Is there work
continuing on this elsewhere?

I suspect that that is accurate. It still has ideas that I
haven't seen used elsewhere.

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.

In the context of co-algebra is seems a little strange to consider
only programs that terminate.

The Charity take on co-objects is stream like. The object itself
is infinite, but you can only elaborate a first, finite part.
For instance you can express the Ackerman function as a co-object
table, but the indices you elaborate to look up an element are
finite and terminating.

David

[Jacques Carette]

Post by Bill Page
In the context of co-algebra is seems a little strange to consider
only programs that terminate.

Indeed. But in the context of co-algebras being able to only write
programs which are productive does make a lot of sense. And in a lot of
recent research on process algebras and the like, productivity is a hot
topic. And, as we know, that is the natural dual to termination.

Jacques

[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 | ***@unbc.ca
Department of Computer Science | (250) 960-6672 Fax [phone]
College of Science and Management | 3333 University Way
University of Northern British Columbia | Prince George, BC V2N 4Z9
| CANADA

Date: Thu, 7 Aug 2008 11:45:28 -0400
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
"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
http://aldor.org/mailman/listinfo/aldor-l_aldor.org