[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

    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.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]