axiom-developer
[Top][All Lists]

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

 From: Gabriel Dos Reis Subject: Re: [Axiom-developer] Curiosities with Axiom mathematical structures Date: 14 Mar 2006 01:26:09 +0100

```Ralf Hemmecke <address@hidden> writes:

[...]

| Yes, one has to rethink that quite a lot. The problem with your
| suggestion is the following
|
| 1) You cannot simply ask
|
|    Integer has Monoid
|
| because you have to give a parameter.

yes, that is alright.  The question

Integer has Monoid

is an underspecified question.

| 2) If you say something like
|
| MyMonoid(T: Type, m: (T, T) -> T): Category == with {
|    square: T-> T;
|    default {square(t: T): T == m(t, t)}
| }
|
| then it is perfect Aldor.
|
|    Integer has MyMonoid(Integer, *)
|
| and it will return true only if you have said
|
| extend Integer: MyMonoid(Integer, *) == add;
|
| somewhere.

That is fine! -- I don't expect Aldor to read my mind :-)

| (But probably you had something else in mind.)
|
| Although I don't really like that an AbelianMonoid is not a Monoid,
| and although I think that renaming during inheritance would be nearer
| to mathematics...

I still don't follow that path.  Please could you explain with more
examples?  The understanding of renaming I have causes more trouble
than it solves problem.

|  after all the discussion here, I somehow think that
| seen a clear case where renaming would be over-advantageous.
|
| I'd like to say
|
|    Integer has Monoid
|
|
|    Integer has Monoid(*, 1);
|    Integer has Monoid(+, 0);

I would not.  The question

Integer has Monoid

gives me no clue about what is going on.

In fact, in situations where when I ask the question

Integer has Group(op)

I'm more interested interested in retrieving the inverse operation and
neutral element of op, than just the mere question is it a Group.

Consider computing the nth "power" of x (of type T).  First of, one
can have a general (helper) implementation of "power" for a monoid (or
even just a semigroup or a magma) see page 99 of

http://www.stepanovpapers.com/notes.pdf

and onwards.  If n is negative and T is a group, then one can just
take the "positive" power of the inverse of x -- reuse known
abstraction.

| Simply think of a category Foo with hundreds of exported function,
| would you like to write
|
|    Dom has Foo(f1, f2, ..., f100)
|
| ??? That is not really handy.

quite; but I believe my first idea can be refined (as I did):  I doubt
all of the hundreds parameters for Foo are independent.  In pratice,
the number of indenpendent parameters for the algebraic structure does
nto exceed 5 or six.  However, many of the "exported" functions are
"functions" of those independent parameters.

-- Gaby

```