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

[Bill Page]

On March 9, 2006 5:31 PM Ralf Hemmecke wrote:
> 
> On 03/09/2006 03:46 PM, Martin Rubey wrote:
> > I wouldn't want to ask "Integer has Monoid", since this 
> > doesn't make any sense to me. I'd like to ask "Integer
> > has Monoid(Integer, *)" or "Integer has Monoid(*)"
> ... 
> How would you mathematically express that the integers belong
> to the category of monoids? You would probably say that
> 
> F(Integer) is an object in the category of monoids
> 
> where F is a functor from the category of rings (or rather the
> category in which Integer really lives) that forgets every
> extra structure of a ring an just selects a monoid structure.
> Yes, the functor F decides whether you mean the additive or the
> multiplicative structure.
> 
> I hope, some category experts correct me, if I am wrong. I'm not
> so fluent in that language.
>

I think your description is correct.
 
> Anyway there is clearly something missing in the "has" 
> construction if that would have to be written mathematically.
> 

I agree with Martin. One should interpret:

  if Integer has Monoid(*,1)

as the question of whether F = (*,1) is a functor from the category
containing Integer to Monoid, the category of monoids.

Axiom/Aldor language constraints require us to write

  Integer has Monoid(Integer,*,1)

Martin has suggested a method using 'extend' in Aldor to make
such an assertion by:

  extend Integer: Monoid(Integer,+,1)

where Monoid is the category:

  Monoid(T:Type,m:(T,T)->,u:T): category == with { }
  ++ m(m(a,b),c) = m(a,m(b,c)) and m(a,u)=a and m(u,a)=a
  ++ for all a,b,c in T

and of course it is up to the programmer to verify that the
axioms are satisfied.

It is also possible to write a domain constructor such that
MonoidDomain(Integer,+,1) is a Monoid.

In the current version of Axiom with the Aldor interface installed
the 'extend' construct works for domains written in Aldor but not
for Axiom domains written in SPAD such as Integer above. This is
a known bug in the Aldor interface mentioned by Peter Broadbery
several months ago.

Regards,
Bill Page.