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

[Gabriel Dos Reis]

[ Woaw, I did not anticipate we would have so much fun with what I
think is a mistake in Axiom/Aldor :-)]


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

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

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

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

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

| Can a compiler or interpreter catch this?

Yes, definitely.

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

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

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

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

| 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.  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?  How can we convince the engineer that
he has to duplicate code, when he knows from practice that it is a
source of disaster? 

| 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.  From a practical point of view, the system does
not support a direct mapping from design to codes.  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.

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

| 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 :-((

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'm asking the question as someone interested in (mathematical)
software engineering teaching and someone interested in Axiom.

| 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 fear you did not see what I was talking about.

-- Gaby