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.
_______________________________________________
Axiom-developer mailing list
[email protected]
http://lists.nongnu.org/mailman/listinfo/axiom-developer
