Re: [Axiom-developer] Curiosities with Axiom mathematical structures

[Ralf Hemmecke]

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