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

[Page, Bill]

On Monday, March 13, 2006 7:43 PM Gaby wrote:

> ...
> Bill Page writes:
> 
> > 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)
> 
> all that makes sense, except that -- upon reflection this a
> while -- not everything should be explicit parameter.
> 
> Basically, the idea is this.  When have (T, op, e) as a monoid,
> it is because the three elements together satisfy some relations.
> If I may borrow some loose analogy, it is like with implicit
> functions.  The above means that there are some redundancy in
> the triple.  Here, e is uniquely defined by op (maybe non-
> constructively, but when it exists it is unique).  Consequently
> the neutral element is a function of op and T.

No. This is an additional assumption that is not part of the
mathematical definition of a monoid. Normally in mathematics we
would say:

  Let 'M(T,op,e)' be an monoid.

Nowhere do we imply that 'op' uniquely determines 'e'. In addition
to the associativity of 'op', we only require that op(e,x)=op(x,e)
for all x in T.

At most we can say that 'M(T,op,e)' uniquely determines 'e',
but that is trivial.

In Axiom we would like to interpret such a declaration as a
specification of the substructure of some domain (e.g. Integer)
as being isomorphic to some monoid, e.g. M(Integer,+,0). As such
it inherits a binary operation '+' and a constant '0' plus some
(implicit) axioms about their relationship. Martin's construct
turns this around a little since for the sake of Aldor '+' and
'0' must be pre-defined in Integer. The 'extend' is merely adding
the implicit axioms and additional default (ie. monoid-dependent)
operations (if any).

> So I would write
> 
>      Integer has Monoid(Integer, *)
> 
>      extend Integer: Monoid(Integer, +) with {
>          neutral == 0;
>      }
> 

No.

The Axiom/Aldor "language constraints" that I was referring to
above prevent us from writing more simply:
 
   Integer has Monoid(*,1)
   extend Integer: Monoid(+,1)

where the domain % of '*' and '1' is to be understood from
context. See also my previous message re:

  Monoid(m:(%,%)->%, id:%): Category == with { }

Regards,
Bill Page.