RE: [Axiom-developer] Curiosities with Axiom mathematical structures

[Page, Bill]

Ralf,

I do hope that we are converging ... :)

On Tuesday, March 14, 2006 12:30 PM you wrote:
> ...
> I wrote: 
> > Category theorists purist do not like to write set membership
> > because it implies that categories are always sets.
> ... 
> 
> > They prefer to posit the existence of a functor.
> 
> Could you be more precise?

I think this is not so relevant to our goal -- this is all
just "categorical nonsense" ;) ... But "elements" in
category theory are usually abstracted as abstracted as
morphisms from the terminal object (source) to some other
object (target). Such morphisms are called elements of the
target object. The terminal object is abstracted from the
notion of a singleton set and can be defined generally as
a certain kind of "limit" etc. etc. In general the existence
of a morphism (or functor if the objects themselves are
categories) is equivalent to the existence of an element
of the target.

> ... 
> He? If you say "Monoid(Integer,*,1)" is "the particular object
> in Monoid" then why would I have to write
> 
>    Integer has Monoid(Integer, *, 1) ?

Because our objective is the say that Integer has a certain
relationship to this Monoid.

> 
> That also looks unnatural. What would be the meaning of
> "has" and what should be the types of its first and second
> argument?

  Integer has Monoid(Integer, *, 1)

is equivalent to writing

  F(Integer) = Monoid(Integer, *, 1)

in your notation. The types associated with 'has' are

  domain has category

Integer is a member of some category and Monoid(Integer,*,1)
is a member of another category.

> 
>  > Then the functor F maps Integer into Monoid(Integer,*,1):
> > 
> >     Integer |-> Monoid(Integer,*,1)
>

This is just another way to write:

    F(Integer) = Monoid(Integer, *, 1)
 
> It's hard to follow you. Let me tell you what I understood.
> 
> 1) There is a category Monoid whose objects are categories.
> (In that sense Monoid would be on the same type level as
> "Category" in Aldor.)

I don't think that is true. In Aldor we can not have categories
that are objects (elements or members) of other categories -
we can only have categories that are sub-categories of other
categories. Domains are objects of categories. This is
explained very well I think in the Aldor Users Guide, section
"7.5 Subtypes" and related chapters:

   Inheritance for domains from categories is analogous to
   class membership and inheritance between categories is
   analogous to class containment.

> I order to avoid confusion, lets call it MONOID.

I am not sure what to call it in Aldor except it syntactically
it looks like 'Monoid' in the expression

  Monoid(Integer, *, 1)

but we said this (whole thing) was a category, so 'Monoid'
is something else - I guess a "category constructor".

> 
> 2) Monoid(Integer, *, 1) would be a category.
>    I hope you _don't_ mean the category structure that comes
>    from the fact that any monoid can be considered as a
>    category. But than I cannot interpret what the objects
>    and arrows in that category would be.

No, I mean

    Monoid(Integer, *$Integer, 1$Integer)

is a category with object 'Integer', composition '*$Integer' and
identity '1$Integer'.

> 
> 3) For me "Monoid(Integer,*,1)" looks more like the universal
> algebra given by the carrier set {0,1,-1,...} and operations
> * and 1 together with the monoid axioms.
> ...

I think that is probably a good alternative to category theory
when trying to formally express the semantics of Aldor programs.
But maybe it is too general and I think therefore less interesting
mathematically. Category theory has been so successful at
capturing and unifying a very wide range of mathematical concepts.
I would like to have some assurance that my chosen computer
algebra system has a similar "power" to represent such a wide
range of mathematics.

> ... 
> What would be different to
> 
>    Integer has with {*:(%,%)->%;1:%}
> 
> ?? Only that "Monoid" appears?
> 

I think it is important to understand what the Aldor Users
Guide means when it says:

   Note that Aldor is constructed so that a domain is only
   a member of a named category if it explicitly inherits
   from the category -- not if it merely exports the same
   collection of (explicit) declarations1.

This is what we mean in Axiom when we say domains satisfy
named categories by *assertion*.

    Integer has with {*:(%,%)->%;1:%}

does not say anything about the relationship between the
operations * and constant 1 except that they occur in Integer.
This does not make Integer a monoid but the result is true.

On the other hand

    define Monoid:Category == with {*:(%,%)->%;1:%}
    ++ a*(b*c)=(a*b)*c and a*1 = 1*a = a

gives a "name" to the category and adds some comments. The
result of

    Integer has Monoid

is false. Note that the only difference is the 'Monoid' is
a named category instead of a category constant. 'Integer'
only satisfies such a category if we explicitly say that
it does like this:

   extend: Integer: Monoid == add;

Now 

    Integer has Monoid

is true. We can use this fact in the program code to treat
(Integer,*,1) as a mathematical monoid. But this is only
a convention that we might or might not implement.

In fact we don't even need the 'with' clause if all we need
is an "axiom"

    define Monoid2:Category == with
    extend: Integer: Monoid2 == add;

The only thing that has been added to Integer is the assertion
that it satisfies Monoid2. This is just like in Axiom where
we can use this sort of category to represent some property.
(Axiom allows such axioms to be defined implicitly but Aldor
does not.) What we **do** with such a property is entirely up
to the programmer.

Regards,
Bill Page.