[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures
From: 
Gabriel Dos Reis 
Subject: 
Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures 
Date: 
14 Mar 2006 01:03:32 +0100 
Ralf Hemmecke <address@hidden> writes:
 On 03/02/2006 08:23 PM, Gabriel Dos Reis wrote:
 > "Bill Page" <address@hidden> writes:
 >  On February 27, 2006 11:08 AM Gabriel Dos Reis wrote:
 >  > Ralf Hemmecke <address@hidden> writes:
 >  >  Note that one would have to say something like
 >  >   >  define Monoid(
 >  >  *: (%, %) > %;
 >  >  1: %
 >  >  ): Category == ...
 >  >   >  define Group(
 >  >  *: (%, %) > %,
 >  >  inv: % > %,
 >  >  1: %
 >  >  ): Category == ...
 >  >   >  define Ring(.....): Category == with {
 >  >  Monoid(*, 1);
 >  >  Group(+, , 0);
 >  >  }
 >  >  > Ring should be both Monoid and Group, whether they shoud be
 >  > categories, I don't really know.

 > The reason I previously said I did not see why Monoid should be a
 > category is that the operation is already passed in as a parameter, so
 > there would nothing to implement "inside" in the Monoid.

 I had to read your statement several times until I got the point. I
Sorry about that.
 must admit that I probably have not thought clearly enough before I
 wrote down the code. But it's clear that als a (multisorted) universal
 algebra

 define Monoid: Category == with {
 1: %;
 *: (%, %) > %
 }

 can mathematically be seen as

 a Monoid is a tuple (%, (f_1, f_2)) where % is the underlying set,
 f_1 is the unit element and f_2 is multiplication.
Yes.
Furthermore, the monoid operation uniquely identifies the neutral
element; consequently I think the syntax can be minimized to
define Monoid(T: type, m: T x T > T) : Category with {
neutral : T;
}
Here, I don't expect neutral to be exported to the "global scope".
Rather it should be visible only through the member access operator,
e.g.
 (Unfortunately, nothing in the Aldor code above says anything about
 relations between 1 and *.)
I understand that, but I'm all for stepwise refinement. First, get
rid of the syntax that stands in the way, then more on "semantics",
e.g. more interesting stuff :)
 But although the operations are called 1 and * that should not
 matter. They should be just place holders for the actual name of the
 operation in the concrete monoid.
Exactly. And they should not be exported to the "global scope".
[...]
 > Indeed, there would be a redundancy in the system. The underlying type
 > and the operation suffice to uniquely define the structure. So that
 > means, the other parameters are somehow "function" of the essential
 > parameters. That implies that indeed Monoid will be a category which
 > domains will implement by supplying the value for the neutral element.
 > Same reasoning for Group where the type and the operation suffice to
 > define the inverse and the neutral element.

 Yes. The domain provides the value for the neutral element. And who
 provides the name for the neutral element? You know the domain Integer
 is both a Monoid with respect to addition and multiplication. You have
 just the identifier "1" in the category Monoid. How would I
 specify/name the additive unit element in Integer?
That problem is a nonproblem if you observe the following. The
neutral element is a function of the monoid operation. Furthermore,
each *instance* of monoid structure gives rise a unique neutral
element (for example, accessible through member access). So there is
no conflict between the neutral element of Monoid(N, +) and that of
Monoid(N, *). They are all (a priori) different. They matter only
when using generic function, but then by the time such functions are
called the particular monoid instance is already sealed so there is no
possible confusion.

 >  However, there is no way in Axiom to express that a Ring is a Monoid
 >  (SemiGroup if you like) "with respect to multiplication" and a Group
 >  (which is also a Monoid) "with respect to addition".
 >
 > I understand there is no way. My issue is *why*? E.g. is it
 > fundamental or just implementation details that shrine into the
 > interface? My suspected answer is that it is an artifact of the
 > used objectoriented technology.

 I cannot belief that this issue is fundamental, but I am not an expert
 in this field. I you could help to come up with a nice syntax that
 would allow a compiler to translate

 [*] a Ring is a SemiGroup "with respect to multiplication"
 and a Group (which is also a Monoid) "with respect to addition"

 into reasonable binaries, I would highly appreciate it, since it would
 make Aldor even more "mathematical".
define Magma(T: Type, m: T x T > T) : Category;
define SemiGroup(T: Type, m: T x T > T) : Join(Magma(T, m)) with {
Associative(T, m);
}
define Monoid(T: Type, m: T x T > T) : Join(SemiGroup(T, m)) with {
neutral : T;
}
define Group(T: Type, m: T x T > T) : Join(Monoid(T, m)) with {
inverse : T > T;
}
define AbelianGroup(T: Type, m: T x T > T) : Join(Group(T, m)) with {
Commutative(T, m);
}
define Ring(T: Type, a : T x T > T, m : T x T > T) :
Join(AbelianGroup(T, a), SemiGroup(T, m)) with {
Distributive(T, a, m);
}
the syntax is not right but I guess you get the idea.
 Gaby
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, (continued)
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/09
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, William Sit, 2006/03/10
 RE: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Bill Page, 2006/03/08
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, William Sit, 2006/03/09
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, William Sit, 2006/03/14
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/02
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/02
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/04
 RE: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Bill Page, 2006/03/04
 RE: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Page, Bill, 2006/03/13
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, William Sit, 2006/03/13
 RE: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Page, Bill, 2006/03/13
 RE: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Page, Bill, 2006/03/13
 RE: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Page, Bill, 2006/03/14