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

[Gabriel Dos Reis]

William Sit <address@hidden> writes:

| Hi Gabe:
| 
| Gabriel Dos Reis wrote:
| > William Sit <address@hidden> writes:
| > 
| > |  "Bill Page" <address@hidden> writes:
| > |
| > | > | I don't think there is any essential reason why SemiGroup and
| > | > | Monoid could not be implemented in the way you suggest. For
| > | > | example:
| > | > |
| > | > | )abbrev category SGROUP SemiGroup
| > | > | SemiGroup(m:Symbol): Category == SetCategory with
| > | > |       m: (%,%) -> %    ++ returns the product of x and y.
| > | > |       associative(m)
| > | > |
| > | > | )abbrev category ABELSQ AbelianSemiGroup
| > | > | AbelianSemiGroup(m:Symbol): Category == SemiGroup(m) with
| > | > |       abelian(m)
| > | > |
| > |
| > | Yes, there are no theoretical reasons, but there are plenty of
| > | practical ones.
| 
| > In fact, practicality dictates that the implementations in Axiom/Aldor
| > closely follow the mathematical structures.  
| 
| You probably misread my response to Bill. 

After re-reading the long thread that followed, I do not believe so.

I think I correctly read your answer and I correctly deduced a fundamental
mismatch between your conception of what a monoid is and should be
written and the demand of writing a computer program to express
mathematical structure.

| I was saying there are plenty of practical reasons NOT to implement
| in the way suggested, but no theoretical reasons NOT to implement
| the goal you suggested, in some way. 

Sorry, none of the reasons you enumerated were "practical".
They look to me as a choice that "looked good a the time", but turned
out to be broken but a heartily desire to stick to it instead of
evolving.   It looks to me more ideological than practical.  

It negates practice.

| > 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.  That is
| > the least I expect from a non-mathematically-oriented system.
| 
| Agreed in theory, not in practice. 

Wrong; I'm talking of practical issues.

| We should distinguish two issues: (1)
| derived  operations that depend only on the defining operations should be
| generically implemented and inherited, and (2) how to handle the notations
| (equivalently, identifiers in computer science terminology) for the defining
| operations and derived operations.  Notations (resp. identifiers) are 
extremely
| important in mathematics(resp. computer programming). Mathematics can only
| progress and make strides when good notations are invented AND agreed to.

notation is important, and so is semantics.  When syntax takes precedence over
semantics, the result is empty sophism and boring rethorics.

| Examples are the notations for differentiation and integration. 

Sorry, they do not illustrate in a anyway why a AbelianMonoid is not a
Monoid. 

| A software system that deviates from the universally accepted
| mathematical notations, even if for the sake of valid ideals,  will
| not be usable and at best be hardly usable.

Is it more important to derive from alleged universal notation (when
in fact the notation is highly ambiguous, and the universality is just
mirage) than derive from universal semantics?  Which mathematical
authority do know and universally agreed on that do not recognize an
Abelian monoid as a monoid?

| Computer programs can work correctly only if identifiers are scoped 
| correctly and such scoping should be transparent when identifiers are
| overloaded.

That is what you claim, and yet we have no evidence that Axiom/Aldor
have "correctly scoped identifiers".  Furthermore, we have to see
evidence of why it is desired that such "scoping should be transparent
when identifiers are overloaded."  As a matter of fact, we have
examples (in this thread) that suggest that the transparency is far
from being what we need.

| The concept of a ring is almost omnipotent in all branches of
| mathematics, and the standard notations for the multiplication (*)
| and addition (+) are adopted. 

You are missing an important fact: most of the mathematical texts use
notation invented when computer programs were not the primary focus of
the discourse when where context helped *humans* to automatically
disambiguate when more operations are involved.

| You may almost forget about that a ring is a monoid wrt to * and an
| abelion monoid wrt + because what is important to a ring is the two
| together, how they interact via the distributive laws.

No, you're wrong: I did not forget that.

| A practical way to support the structure of a ring requires these
| two separate notations.

Wrong: a practical way to support them is not to prejudge of syntax in 
more general contexts, and stick to the *algebraic structure* being
modeled. 

| Even in the simple case of your example for repeated operation
| (which you called "power"), the two operations * and + will produce
| (and should produce) outputs in two different notations: x^n (power)
| and n*x (multiple). In this case, the repeated operations in fact
| occur both in an *abelian* submonoid setting even if multiplication is
| non-commutative.

Well, unless you're a proposing a new mathematics you reduction is
again wrong -- because you're prejudging semantics.  Again take

    f (x, y) = x * y + x + y

on integers with usual addition and multiplication, then (N, f, 0) is
another Abelian monoid structure.  Computing the repeated operation
does not yield n * x or x^n.  Please stop confusing syntax with the
*structure*. 

The medium is not the message.  


| So I hope we need not argue a third issue: (3) maintaining standard
| notations for the defining operations in common algebraic structures.

but standard notation of what?  Computer programs have very different
requirements from free mathematical discourse.

| I think your ideal of avoiding "duplicate codes" (much like the
| ideal of sharing dll libraries) is misplaced.

Please, if you want to discuss shared dll libraries, let's do that in
a different thread.  The issue at hand is too important to be left
diluted in questionable analogies. 

| In order to avoid duplicating code due to the dual use of * and + in
| the monoid structures, one will have to, as admitted throughout
| these discussions by everyone, ADD tons of code and in the end
| making writing software for a ring more difficult, not less. Not
| only that, I doubt if the experts here could agree to how that
| additional code should be written, even if everything were started
| from scratch. 

Please, what are you tlaking about?

| I think a proper way to "allow" the kind of identification of underlying
| mathematical structures that are the same is the concept of
| "isomorphism".

But not all structrures are isomorphic, even in the same
(mathematical) category.  We do not need to recover from yet another
set of misguided and misplaced isomorphims.

[...]

| Let's say in Monoid, I used & for the defining monoid operation. If I want to
| form a monoid domain with set Integer and operation #, (Integer, #), I would
| have to specify to the compiler an isomorphism.  The compiler would have to
| execute this isomorphism by replacing each occurrence of '&' by '#' in the
| category definition temporarily before matching the domain
| signatures with the category signatures. This necessitates that in
| the category definition of a monoid, and in the domain code of an
| actual monoid, we can identify and separate the defining operations
| from the derived operations -- which is currently not the
| case. Let's assume this is done nonetheless. 

You are using confusing terminologies to say exactly what I'm proposing.

| Then the generic code of derived operations (such as 'square' or
| 'power'), if available, will have to be translated, duplicated, and
| inserted in the domain for correct signatures and implementation.

I disagree.  There is no inherent reason why they should be
duplicated.  The operation '&' is a parameter!  Whether the
instantiation should be through copy-and-build or sharing is a
completely different issue.

[...]

| > If the system does not let one do that, then the system is practically
| > defective :-)
| 
| All systems have defects. Be realistic!

No kidding.  

I just release one last week.

[...]

| > |  Indeed, how is a user to know what symbol was used, say, for the
| > | operations? What if the user instantiates Integer with both * and +
| > | for the same operations in two instances?
| > 
| > When both will be in scope.  If the user uses * with Integer, the
| > system knows that (*, Int) is a monoidal structure.  Same if
| > (+, Int).
| 
| I meant using * for multiplication of integer in one instantiation,
| and using + for multiplication of integer in another instantiation,
| two notations for the same set and operation. (I am not advocating
| this! see original message for the context, please).
|  
| > | Can a compiler or interpreter catch this?
| > 
| > Yes, definitely.
| 
| Really? The two copies of the multiplicative monoid of integers are
| compiled at different times and instantiatiated in the SAME
| interpreter session. Can the interpreter execute something like
| 3*4+5 correctly and give 60 (without package calls)? What if we have
| two copies of the ring of integers where in one the notations for *
| and + are interchanged? When this sort of arbitrary notations is
| allowed, every function call need to be a package call or else it
| would be a nightmare to explain all the "strange" answers. (The
| isomorphism mechanism does not seem to solve this problem).

Well, programming languages have been dealing with such issues for
long time now.  Either, you permit nonsensical uses (because in
general you can't prevent all of them and yet remain useful); or you
do minimal checking when same operations should be defined
consistently (programming languages like C++ calls it the "One
Definition Rule", and do not require compilers to diagnose all of
them, but there are known systems in production use that have
implemented them for the vast majority part of it and can handle such
cases). 

| > | If not, it would be a nightmare of bug reports.
| > 
| > It would be a nightmare only if one takes the rules that a type has a
| > unique algebraic structure.  That is both theoretically and practically
| > false.  See the examples (+, NN), (*, NN), (NN, max) I gave earlier.
| 
| Quite the contrary. When a type has a unique algebraic structure (I
| presume you meant only default notations for its defining operators
| are allowed), 

No, please do take note that I'm distinguishing structure from syntax.

| there is no ambiguity possible like the 3*4+5 above.

Utimately, you have to agree that a symbol resolves to what it
implements -- even mroe so in your OO-centric view of mathematical structures.


| I don't disagree this state is non-optimal, but the proposed state
| has its problems. Your examples show three *different* binary
| operations with three *different* identifiers.

Again, identifiers are not algebraic structures.  

The proposed change certainly has its set of problems -- but nothing of
what you said above is about them.  To start with, the proposal is not
complete :-)

| If you want to inherit say the function 'square' for each, you need
| to, as explained above, establish three isomorphisms to the
| fictitious domain % in the categorical definition and translate,

Please do notice that 'square' implicitly depends on the monoid
operation passed as parameter to the monoid structure.  Consequently,
if I wanted to have different *instances* of it simultaneously in the
same scope, then I need to give different names to those *instances*
If I want to have them simultaneously in the *same scope*, then
obviously I need to give different names to their *instances*, e.g.

     doublePlus == Monoid(T, +).square
     doubleTime == Monoid(T, *).square

[...]

| It would be all the more of a problem when all the three monoid structures
| co-exist in the *same* domain (multiple inheritance).

it would be a problem only if one sticks to an ill-suited OO-centric
view.  Other models exist, and should be explored.


| Notice that while the domain (NN, +, *, max) exists, the domains
| (NN, +), (NN, *), and (NN, max) are transiently constructed during
| compilation only! There is no (NN, +).NRLIB for example. Besides,
| you can only have ONE signature 'square: % -> %' in the domain 
| (NN, +, *, max), not three.  This possibly is an important reasons why
| AbelianMonoid does not descend from Monoid.  

you're confusing the current ill-suited OO implementation with what
should happen.  If there is no theoretical reason why that should
happen, then you better off revise your implementation model.

| There seems to be no good way to solve this multiple inheritance problem.

Abandon, OO and that ill-suited multiple inheritance stuff, when not
helpful, -- e.g. here.

[...]

| Needless to add, such automated translation, duplication and insertion are
| simply not supported currently (see SandBoxMonoid).

No.  Please see above.

[...]

| > I wanted to use Axiom to teach generic programming here,
| > but I'm being forced to walk away from it :-((
| > How can I convince students of the value of the system when it does
| > not support their knowledge?
| 
| Your students should be able to learn the abstract concepts abstractly :-)

My students are better off not learning the abstraction at all, than
have their mind crippled with obfuscated ill-suited implementations.

| You can teach them about isomorphisms. Also, tell your students life
| is always a compromise.

my students are well aware that life is compromise -- do not of many
students that decide to take graduate courses and still believe
otherwise? 

| > | CAS to be practical, certain compromises are necessary.
| > 
| > 100% agreed.  However, uniformity and coherence should not be compromised.
| > The current approach does not even support the mathematical or
| > "categorial" approach we would like to recommend.  
| 
| The current approach does support, within the limits of the programming
| language. The Axiom designers are mathematicians and computer scientists and
| they must have thought about this before deciding on the
| compromise. Remember, that was in the 1970's and I think their
| compromise is quite reasonable and have served the community well
| for over 30 years.  

many systems were designed more than 30 years ago.  At the time, their
designers tried to do the best possible at their time.  Those who
refused to evolve died.  Since the 1970s advances have been made in
understanding type systems; it would be singular that Axiom refuses to
evolve and stick to OO-centric views we now know does not work well.
We can't require unreasonable degree of foresight from designers, but
it is unreasonable that the system refuses to evolve -- if it ever
wanted to survive.

[...]

| Coherence, if I understand what you meant by that, requires confluence in
| rewriting rules.

No, you misunderstood what I was saying.

[...]

| If you think now one can redo Axiom in a better way, we are all for
| it. What's your priorities? (in other words, when can you start? :-)

What about give me unrestricted access to Adlro compiler sources? ;-)
(and I'm serious)

[...]

| > | I do not question the theorectical advantage of rebuilding all
| > | algebra based on properties of operators (there is research in
| > | theory of operads which would support such a design) but I doubt
| > | their practicality, especially when the notation for the operators
| > | can only be known dynamically at run-time.
| > 
| > Well, I'm approaching the issue more from a *practical* point of view
| > than a theoretical point of view.  As the system currently stands, in
| > practice, I cannot simply and clearly write once a generic function
| > for monoidal structures and expect it to work for both for Abelian and
| > non Abelian monoids. 
| 
| This is not true. First, you don't mean non-Abelian monoids, you meant
| not-necessarily Abelian monoids (or simply monoids).

I meant what I said.

| An abelian monoid IS also a monoid and hence it will work!

Oh really?

| (You just need to redefine AbelianMonoid to use * instead of +,
| showing it is not an inherent weakness of the system but just a 
| matter of notations).  

You are displaying an incoherent attitude in this matter, and at this
pointI don't know how serious you're.

   f(x, y) = x * y + x + y

f uses both * and +.  Now, (N, f, 0) is an Abelian monoid, so you
propose that in the same session I rename f to *, * to + and + to ?
You're joking, right?

[...]

| > | As already well-known, with the current status, all properties of
| > | operators are declarative and not verified.
| > 
| > My problem is simpler than that.  I'm not asking for the definition of
| > the algebraic properties of operators.  I'm trying to have a way to
| > convince Axiom/Aldor to support sound software engineering practice.
| > Even better if I can take the standard library as an example.
| 
| No, you are not discussing "sound software engineering practice". You are
| arguing about how to inherit abstract algebraic properties.

No.  The ill-suited inheritance stuff is just one irritating
manifestation of "sound software engineering practice".  Don't shout
the messenger.

[...]

| I understand your points. There are many monoid structures in any algebraic
| object because monoid is a very simple structure.

No, the problem is not because it is a simple structure, it is because
it is a *structure* and the current system confuses structure with
syntax.  That is the root of the problem.

[...]

| Have you seen ANY paper which interchanges the * and + notations in
| a commutative ring?) 

That is beside the point.  The issue is not whether * should be
interchanged with +.  The issue is how to simply design the system so
that AbelianMonoid is indeed a Monoid.  

-- Gaby