[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: David Casperson
Subject: [Axiom-math] Re: [Aldor-l] Hopf Algebra = Group + Monad
Date: Thu, 7 Aug 2008 09:10:08 -0700 (PDT)
User-agent: Alpine 1.00 (OSX 882 2007-12-20)

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.

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"

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

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.

Bill Page.

Aldor-l mailing list

reply via email to

[Prev in Thread] Current Thread [Next in Thread]