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

[William Sit]

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. 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.

> 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.  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.
Examples are the notations for differentiation and integration.  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. Computer programs can work correctly only if identifiers are scoped
correctly and such scoping should be transparent when identifiers are
overloaded.

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 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. A practical way to support the structure of
a ring requires these two separate notations. 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.

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

I think your ideal of avoiding "duplicate codes" (much like the ideal of sharing
dll libraries) is misplaced. 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.

I think a proper way to "allow" the kind of identification of underlying
mathematical structures that are the same is the concept of "isomorphism". For
isomorphisms between two domains in Axiom, this is approximated via facilities
called "map". In the ideal world, one should design code that can implement
inheritance via isomorphisms. However, it should be emphasized that implementing
isomorphisms involves extra code as well as duplicating code, but it will allow
flexibility in notations that is the facilitator of all mathematics thinking
(and in contrast, it creates a tedious complexity in programming due to the
rigidity of computer languages).

However, there is a caveat. Isomorphisms between a category specification and an
actual domain in that category are meaningless, mathematically speaking. The
categorical specification has no default sample domain. So we need a simulated
isomorphism mechanism. The parameter passing method is one way to indicate an
isomorphism but for more complicated structures, this becomes very clumbersome. 
We need to figure out a way to indicate isomorphisms that will allow, as did the
parameter passing method, multiple isomorphisms involving the same domain (or
subdomains) and category constructor. Putting this aside for future discussions,
let's concentrate on the interpretation for just a single isomorphism. 

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. 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. Those derived operations that are not generically implemented
will be handled like the defining operations except that their identifiers will
not be changed.  Finally, the properties of the defining operations must also be
translated, duplicated and inserted into the domain. The code in the category
should be restored afterwards.

Of course, in the cases where the default notations are used, none of the above
is necessary and thus using default notations gain efficiency over a new set of
notations. Moreover, when the notations are changed, even the properties of the
defining operations must be copied to the domain itself. This creates extra
search info in the database for the compiler and interpreter. Thus this
mechanism "duplicates" code, much like the templates in C++ classes. 

This mechanism is different from parameter passing in its details but not in
essense. The difference is that it emphasizes the role of isomorphisms and
suggests a way to retain default notations in the categorical definitions while
allowing new notations. The details also highlight some requirements for
implementation. As we shall see later, there are more.

A similar isomorphism mechanism already exists between two implementations of
the same mathematical object where the two data representations of objects in
the domains differ. The domains in POLYCAT are nothing but such and are viewed
as isomorphic using an extensive set of map facilities (which typically
translates by deconstructing a polynomial in one domain and then reconstructing
it in the other domain).  The different implementations of these domains are not
considered duplicated code for the mathematical structure of a polynomial ring,
and indeed are essential to the efficient implementation of certain algorithms
in polynomial rings. These map facilities need to be updated in case notations
for defining operations of the two domains are different.

> If the system does not let one do that, then the system is practically
> defective :-)

All systems have defects. Be realistic!
 
> | I think such constructs will make it more difficult for the
> | Interpreter to work since it would not be able look up the
> | appropriate signature from domains that have not been instantiated
> | during the session.
> 
> That depends on the *kind of lookup*.  For a system where all symbols
> are global with no proper scoping, then yes that is a problem.  But
> then, if the system is designed to write mathematical software it
> should have lookup rules that make that possible.  Said differently,
> the system should be designed to serve writing "natural" mathematical
> software.

These "look-up" rules are generated precisely by the isomorphisms discussed
above. However, to write "natural" mathematical software, we need to adopt the
"natural" mathematical notations accepted by the mathematical and scientific
community.

> | Of course, if the Interpreter  knows what to instantiate, that won't
> | be a problem. But how will the Interpreter be able to know?
> 
> By adequate scoping rules.

Scoping rules play a small part in the isomorphism mechanism. Scoping rules are
needed when the same identifiers (minus the prefixes or info used to aid proper
scoping) are used in different contexts (scopes).  Isomorphisms (as described
above) are needed to inherit properties when corresponding operators (between a
domain and its category, or between two domains) have different identifiers
(notatiosn) for the defining operations.  The Interpreter needs the duplicated
code in its database for domains which use a non-standard set of identifiers for
the defining operations. The non-standard set of identifiers are distinct from
the standard identifiers.
 
> |  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).

> | 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), there is
no ambiguity possible like the 3*4+5 above. 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.  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, duplicate, and insert 'square' in each domain so that
the Interpreter can find the translated defining operations and their
properties, or else you have to package call because the Interpreter has no way
to tell when you write 'square(5)' to which of the three monoids 5 would be in.
It would be all the more of a problem when all the three monoid structures
co-exist in the *same* domain (multiple inheritance). 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.  


There seems to be no good way to solve this multiple inheritance problem.
One way is for the compiler to tag each of the derived operations differently
for each instance of a category constructor, so we can have three different
'square', each replaced by a different identifier. But clearly, not only will
this destroy the very desirable overloading of operators, it will also destroy
the membership of the domain in the monoid category in each case.

Another way will be to ask the compiler to create the missing (NN,+).NRLIB and
the other two. Then (NN, +, *, max) will have three imported 'square' functions
and each will have to be package called. Not a big deal, yet. However, there is
then the danger of first too many NRLIBs and second there will be need for
multiple copies of (NN, +).NRLIB, one for each time (NN, +) becomes a subdomain,
and since the + may mean different operations (it is only an identifier, not a
distinguished identifier), each will in turn need to be tagged by their
superdomain! That will quickly become a nightmare.



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

> 
> | By allowing renaming of operations (even just all binary operations), the
> | categorical notation for * or + no longer exists and it would be
> | impossible for the Interpreter to search for a suitable signature in
> | a categorical manner --- only on a specific domain by domain (and
> | for instantiated domains only for that matter) basis.
> 
> I don't see what "renaming" has to do with this; from what I see, it
> can only lead to greater confusion.

Renaming is really setting up an isomophism using the identity map (if the
underlying sets are the same set, or the vacuous map if between a category and a
domain). This is similar to the renaming of ? to x for the main variable in
domains like UP(x, INT). The current renaming mechanism is too simplistic and
superficial and in my opinion, is the cause for errors. In your idealized
version of a monoid definition, the monoid operation should have no name, like a
?, because it is abstracted. But in any real monoid (domain), the operation must
have a name, just like a polynomial in UP needs a name for the main variable
(which is passed as a parameter). Without a name categorically, there can be no
search categorically. The way the Interpreter currently matches ? in UP(x, INT)
can easily be made to say x = y when they are distinct variables.

x:=variables (2*x::UP(x,INT));
y:=variables (2*y::UP(y,INT));
t:Boolean:= x=y

would return 'true'.

> However, passing the operation as a parameter to the structure is a
> first approximation of a viable solution.

The entire 'with' clause in constructors is to pass operations as parameters.
But their identifiers cannot be changed! (see SandBoxMonoid). It is not how to
specify an isomorphism that is the problem, it is how the compiler will
interpret and act on that specification that is the problem.
 
> | I do recognize some limitations for having two monoid categories
> | structured on two different operator notations. For example, there
> | is no commutative monoid with * as the multiplication and these are
> | needed (if one wants to look at the set of monomials in several
> | variables as a multiplicative monoid). However, it is far easier to
> | have say, AbelianAdditiveMonoid and AbelianMultipicativeMonoid
> | categories (cf. one AbelianMonoid where the operator must be "+")
> | than to implement all operators used in algebras as parameters.
> 
> I beg to differ.  Having to write duplicate codes is known to be a nightmare
> and fruitful source of bugs.  It does not really encourage
> abstractions. 

I said it is far easier, not that it is the correct solution. However, I don't
agree duplicated code should be the reason for objection to the easier way out.
Code efficiency is the least of our problems.

> 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 :-) You
can teach them about isomorphisms. Also, tell your students life is always a
compromise.

> | 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. 

Regarding uniformity, I am not totally satisfied with the isomorphism mechanism.
For example,  the domain that uses a new set of notations "belongs" to the
category in a way slightly different from another one that uses the default
notations. This non-uniformity may be a problem. But to uniformize would require
one to abandon the notion of default notations.

Coherence, if I understand what you meant by that, requires confluence in
rewriting rules. As far as I know, this property has not been proven with the
coercion system. So I don't know how you propose to improve this aspect (Axiom
is not coherent at this time).

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? :-)

> How can we explain
> the that concepts we clearly and unambiguously explained to the
> students or engineering cannot translate directly to code in a
> mathematically-oriented system?  

Indeed, computer programming and even mathematics, have their (different degrees
of) limitations (google theories by Godel, Turing, and Chaitain).

Humans can learn abstraction, the computer cannot. Natural languages do not
express abstractions well (otherwise, we don't need lawyers). It takes a human
being to interpret between the lines to understand abstraction. We *understand*
abstractions by making jumps in our logic system (the brain).


> How can we convince the engineer that
> he has to duplicate code, when he knows from practice that it is a
> source of disaster?

(with a million dollars dangling over their heads?)

Code duplication is a fact of programming life. The difference is simply whether
it is done automatically or manually. If a little bit of manual duplication can
be used to avoid a lot of automatic duplications, I'll choose the former, and do
it and monitor it VERY CAREFULLY. It is a temporary solution, until better
times.

 
> | 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). An abelian monoid IS also a
monoid and hence it will work! (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).  Axiom chooses to allow different notations for the monoid
operation, to distinguish between the commutative case using the more common +
notation. The problem as the system stands is due to the rigidity of the
computer programming languages in general, which does not exist in mathematical
abstractions.

> From a practical point of view, the system does
> not support a direct mapping from design to codes.  

Well, I doubt any system will ever do, at least not without adding on so much
baggage that most will shunt away.  Even if the isomorphisms mechanisms (in the
sense above) are fully implemented it still will not support the mapping from
design to codes because of problems discussed above. In a sense, we want the
input and output to be simple and ambiguous, but the computation to be exactly
what we have in our mind.

> And if I cannot
> directly see the design in the code, how do I know the code reflects
> the design and my intent.  If I have duplicate codes floating around,
> how do I know for sure that I've fixed the bugs I have identified
> through testing with some parameters?  If I do not have a direct
> mapping from design to code, how do evolve my software in a sound and
> controlled manner?  Those are practical questions.

Sure, these questions exist independent of the problem we are discussing here.
Recompiling the world may allow a well-designed system to propagate fixes
automatically while regenerating duplicated codes. For manually duplicated code,
we have to rely on documentation.

> | 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. If all you are
arguing is for absolutely avoiding manually duplicating code or maintaining it,
I'll say that is not a sound software engineering practice to begin with. Here
is a sound principle: Avoid duplication code if you can, but you do what you
have to do to make things work (and you better check the code and document it
well :-).

> | There is a certain degree of trust that users know what they are doing.
> 
> I understand that.  But that issue is different from what mine.
> 
> | Creating examples that deliberately violate these conventions and
> | implicit assumptions of the system and show the "weakness" or
> | "buggiess" of Axiom (or any other CAS) is not productive.
> 
> if you are talking about the issue I raised, then I believe you
> profoundly misunderstood it.
> And claiming it deliberately violates conventions and implicit
> assumptions of Axiom is very unproductive.  I'm deeply disappointed :-((

Sorry. Nothing personal and that was a general, misplaced, remark. 

I understand your points. There are many monoid structures in any algebraic
object because monoid is a very simple structure. Nothing I said disagrees with
your premise that (NN,+), (NN,*), (NN, max) are all abelian monoids. I agree
also that currently, you cannot tell Axiom that NN (Integer or even NNI) has all
three operations as monoid operators and that is a limitation due to the
rigidity of computer languages. To do that, you have to create something like
AbelianAdditiveMonoid (same as AbelianMonoid), AbelianMultipicativeMonoid, and
AbelianMaxMonoid, and that, while not entirely satisfactory, does not have the
problem discussed earlier.

Moreover, the three 'square' functions would produce x^2, 2*x, and x and the
three 'power' functions produce x^n, n*x, and x. Clearly, in (NN, max), the
'square' and 'power' functions are superfluous, but this automatic application
of the monoid construction will not simplify them. In AbelianMonoid, the
'square' function is simply not removed. So there are some simplification
possibilities when a categorical constructor is duplicated in cases with special
properties.

While manually duplicating this for the most common notations is not a problem,
I admit this can generalize  and we may have to duplicate a complicated
structure in more advanced mathematics.   An example would be Set(S), which is a
commutative ring (and a Boolean algebra) in two different ways at least. In such
case, the current practice would be to declare implictly the properties of a
Boolean algebra and use different notations for its operators. Since algebraic
properties of operations are only declarative, it is easy enough to state these
again. However, Set(S) will not inherit from CommutativeRing and so Matrix
Set(S) will not be a valid type construction. 

So my objections are not targeted to your proposal to find a way to allow such
inheritance. My objection is based on practical difficulties: not only is the
modifications proposed (even via isomorphism) very involved, they do not solve
all the problems. As far as I know, most standard higher algebraic structures
use well-established notations. (In fact, if a mathematical paper deviates
significantly from de facto notations, the paper will probably be rejected! Have
you seen ANY paper which interchanges the * and + notations in a commutative
ring?) This does not mean one cannot form a commutative ring with other
operators. To allow such inheritance needs a different yet undiscovered
mechanism, one which, like isomorphism, will likely require at least duplication
of code, albeit automatically.

> The issue is this:  *why* should one be forced to duplicate codes for
> an algorithms that work on the same mathematical structure.  The
> question arise from software engineering point of view, in general,
> and mathematical software in particular (I classified Axiom as a
> mathematical software).  If the reasons for that are not theoretical,
> I believe we need to improve over the situation.

I hope this long message provides some answers to *why*. But duplicating code is
not the main problem. The reasons are technical in nature, not theoretical. They
include the role identifiers play in inheritance, in multiple inheritance,
subdomains, the "un-overloading" of overloaded operators, and to some extent, in
scoping and the proliferation of libraries, as well as complexity in calling
sequences.
 
> I'm asking the question as someone interested in (mathematical)
> software engineering teaching and someone interested in Axiom.

Glad to know you. A rare combination.
 
> | One consequence of these examples is confusion of the real issues:
> | the lack of documentation on the conventions and implicit
> | assumptions, and real bugs.

I withdraw that comment, with apology.
 
> I fear you did not see what I was talking about.

Is this better? (Boy, I'm beginning to feel that I don't know what I was talking
about!)


William