[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
RE: [Axiom-developer] Curiosities with Axiom mathematical structures
From: |
Page, Bill |
Subject: |
RE: [Axiom-developer] Curiosities with Axiom mathematical structures |
Date: |
Mon, 13 Mar 2006 22:17:45 -0500 |
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.
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, (continued)
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/02
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/04
- RE: [Axiom-developer] Curiosities with Axiom mathematical structures, Bill Page, 2006/03/04
- RE: [Axiom-developer] Curiosities with Axiom mathematical structures, Page, Bill, 2006/03/13
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, William Sit, 2006/03/13
- RE: [Axiom-developer] Curiosities with Axiom mathematical structures, Page, Bill, 2006/03/13
- RE: [Axiom-developer] Curiosities with Axiom mathematical structures,
Page, Bill <=
- RE: [Axiom-developer] Curiosities with Axiom mathematical structures, Page, Bill, 2006/03/14
- RE: [Axiom-developer] Curiosities with Axiom mathematical structures, Page, Bill, 2006/03/14
- RE: [Axiom-developer] Curiosities with Axiom mathematical structures, Page, Bill, 2006/03/14