[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures
From: 
Gabriel Dos Reis 
Subject: 
Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures 
Date: 
02 Mar 2006 19:59:59 +0100 
[ 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 nonmathematicallyoriented 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
mathematicallyoriented 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 runtime.
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 wellknown, 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
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Francois Maltey, 2006/03/01
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/01
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, William Sit, 2006/03/02
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures,
Gabriel Dos Reis <=
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/04
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/03
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, William Sit, 2006/03/04
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/07
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, William Sit, 2006/03/07
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/08
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/09
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/09
 [Axiomdeveloper] BINGO, Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/09
 Re: [Axiomdeveloper] BINGO,Curiosities with Axiom mathematical structures, William Sit, 2006/03/09