RE: [Axiom-developer] Axiom in general

[Bill Page]

On September 13, 2005 6:51 AM Nicolas Doye wrote:

> For those that don't know remember my mini-intro some time
> back, I was one of James Davenport's PhD students charged 
> with finding a mathematical foundation for coercion in Axiom.
> 
> http://worldofnic.org/research/phd.ps
> 
> Chapter 2 of my thesis gave some introduction to the mathematical
> formulation of Categories in Axiom/Magma/OBJ.

Nicolas, I am glad to see you here! I discovered your thesis just
a few weeks ago and put a pdf version here in the Axiom portal
reference section:

http://page.axiom-developer.org/zope/Plone/refs/articles/doye-aldor-phd.
pdf/view

This might be useful for people who are "ps-challenged". Please
let me know if this is acceptible re copyright etc.

> 
> Chapter 3 talks about Category Theory.
> Chapter 4 talks about Order Sorted Algebra.
> (Both these chapters put these definitions in Axiom terms at
> the end).
>

Excellent! I am very interested in putting more category theory
in Axiom.

> Chapter 9 talks about where I'd like Axiom to go.
> 
> Some of my "ideas" in my thesis are wrong and I no longer stand
> by them. I was naive. Please ignore 9.7 and any assertions that
> Axiom should be written in Axiom. ;-)

But perhaps Axiom could/should be written in Aldor?

> 
> In some ways, it is far more useful to not think of Axiom in
> terms of Category Theory. Functors etc. are useful sometimes
> when thinking abstractly about Axiom, but Axiom's true roots
> are in Order Sorted Algebra.

I think it would be great to see an application of Goguen's
"Hidden Algegra" for correctness proofs in Axiom/Aldor:

http://www.cse.ucsd.edu/users/goguen/projs/halg.html

> 
> In axiom a Category is an Order Sorted Signature, but the order
> on the sorts is never explicitly defined and there are some
> difficulties in the definition of the operator symbols.
> 
> OBJ _is_ based on Order Sorted Algebra. It's main advantage over
> Axiom as I see it, is that it defines Theories. A Theory is an
> Order Sorted Signature with (and this is what Axiom misses) a set
> of  equations. This means that in Axiom we are free to say that
> MyDomain is in MyCategory, but certain assertions that we as
> mathematicians know about all Domains in MyCategory may not be
> true in MyDomain. Will literate programming help? Maybe. Will it
> enforce? Nope.
>

It is clear that what Axiom calls a "category" is not a category
in the sense of category theory. I think your approach to
understanding just what is a "category" in Axiom has a lot of
merit.

But of course this is a different objective than *implementing*
category theory in Axiom. This is simply a matter of the design
of appropriate algebra library code. From my point of view a
category (in the sense of category theory) in Axiom must end up
as one or more domains within some Axiom "category" of categories.

This is unfortunate terminology. From the point of view of the
mathematics it might be preferrable to refer to Axiom's concept
of category as a "class" but then that also has terminological
problems.

> Another fantastic advantage of OBJ is a view. In Axiom we can
> not say that MyDomain forms a Group over the operator * and the
> operator +, because the operator is hard-coded into the Group
> Category. This sucks. :-( Changing this behaviour is left as an
> exercise to the reader with time to rewrite almost all of Axiom.
> :-)
> 

We have time here given Tim's "thirty year horizon" ... :)

Do you have any ideas about how we might begin to apply OBJ
to Axiom and Aldor?

Regards,
Bill Page.