[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] Curiosities with Axiom mathematical structures
From: |
Ralf Hemmecke |
Subject: |
Re: [Axiom-developer] Curiosities with Axiom mathematical structures |
Date: |
Thu, 02 Mar 2006 23:34:50 +0100 |
User-agent: |
Thunderbird 1.5 (X11/20051201) |
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 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.
(Unfortunately, nothing in the Aldor code above says anything about
relations between 1 and *.)
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.
> | The point is that one speaks of a "category of rings, groups,
> | monoids, etc.), but not of a "category of rings(*, 1, +, -, 0)".
> | So defining those structures in Axiom without arguments would be
> | highly preferable.
> I profoundly disagree. Any respectable source on algebraic structures
> defines rings as tuples.
Did I say something else?
> When one colloquially says "take a monoid",
> one speaks of that tuple, and it is also understood that the
> components of that tuple are parameters, and as such will vary from
> one tuple to another.
I think we should not argue here, we all know what a monoid is.
But it seems that Aldor tries to fix a names for the functions f_1 and
f_2 (namely 1 and * in the definition of Monoid above) and doesn't allow
other names in Aldor-categories that inherit from Monoid.
But actually, only when a concrete monoid is constructed (i.e. an
Aldor-domain), then % becomes the name of the domain and the
placeholders f_1 and f_2 become concrete functions.
In some sense the Monoid from above is not a concrete monoid, but maybe
one can really see it as the "object" part of a mathematical category. I
cannot see the "morphisms", however.
Would be nice to learn something from the original designers of the
language. ;-)
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?
> | 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 object-oriented 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".
> In fact, practicality dictates that the implementations in Axiom/Aldor
> closely follow the mathematical structures. For example, the only
> assumption I need to define the power of an element is that its
> domain
> has a monoidal structure. From software engineering point of view,
> Practicality dictates that I should not have to write duplicate codes,
> one for additive operation, one for multiplicative operation when the
> underlying mathematical structure is the same.
Well, I don't think it is necessary to duplicate code very much. One
only has to do a little bit of work.
Take for example
MyBinaryPowering(
X: Type,
*: (X, X) -> X,
N: with {
zero?: % -> Boolean;
one?: % -> Boolean;
length: % -> MachineInteger;
bit?: (%, MachineInteger) -> Boolean;
}
): with {
binaryPower: (X, X, N) -> X; -- binaryPower(x,y,n)=x*y^n
} == add {
<<implementation: MyBinaryPowering>>
}
Well, it's a package, but by giving the operation * as a parameter, I
can do different things with it, for example,
P ==> MyBinaryPowering(Integer, +$Integer, Integer);
T ==> MyBinaryPowering(Integer, *$Integer, Integer);
binaryPower(5, 3, 2)$P; -- equals 5+3*2
binaryPower(5, 3, 2)$T; -- equals 5*3^2
BTW, assume for a moment we could espress something like [*]. In that
case it would not even help if I could write
MyBinaryPower(X: Monoid, N: with {...}): ...
because then it would not be clear what binaryPower would compute if the
parameter X has two Monoid structures at the same time.
Ralf
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, (continued)
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, William Sit, 2006/03/09
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/09
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, William Sit, 2006/03/10
- RE: [Axiom-developer] Curiosities with Axiom mathematical structures, Bill Page, 2006/03/08
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, William Sit, 2006/03/09
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, William Sit, 2006/03/14
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/02
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/02
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures,
Ralf Hemmecke <=
- 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, 2006/03/13