[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] Curiosities with Axiom mathematical structures
From: |
Ralf Hemmecke |
Subject: |
Re: [Axiom-developer] Curiosities with Axiom mathematical structures |
Date: |
Tue, 07 Mar 2006 06:35:36 +0100 |
User-agent: |
Thunderbird 1.5 (X11/20051201) |
Dear William,
On 03/04/2006 05:31 PM, William Sit wrote:
Hi Gabe:
Gabriel Dos Reis wrote:
William Sit <address@hidden> writes:
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.
By (1) you probably mean to say something like
define PrimitiveType: Category == with {
=: (%, %) -> Boolean;
~=: (%, %) -> Boolean;
default { (a:%) ~= (b:%):Boolean == ~(a = b); }
}
I must say that I liked this idea of "default implementations" when I've
encountered it. But it also introduces all the complications with
multiple inheritance.
For example, assume we have
define ContainerType(T: Type): Category == with {
bracket: Tuple Type -> %; -- constructor
generator: % -> Generator T; -- yields all the elements
#: % -> Integer; -- size
default {
#(x: %): Integer == {
n: Integer := 0;
for element in x repeat n := n + 1;
}
return n;
}
}
define FixedArrayType(n: Integer, T: Type): Category == with {
ContainerType(T);
default {#(x: %): Integer == n;}
}
Theoretically, there is no difference in the two # functions, but
practically, one would prefer the second one for FixedArray's since it
is a little bit faster.
Now, assume I have some other category MyFancyCat that inherits from
ContainerType, but not from FixedArrayType. Then I create
define MyFixedCat(n: Integer, T: Type): Category == with {
MyFancyCat T;
FixedArrayType(n, T);
}
Of course, MyFixedCat also inherits defaults, but which one? (The
current compiler takes the first one.) Changing the order of the
categories results in more efficient code. However, think of a second
default function that could be implemented in both categories, but the
more efficient one in ContainerType. Then you can choose any order for
MyFixedCat and get always only one efficient default.
When I started with Aldor, I used defaults a lot, but I encountered
exactly the above scenario and then removed the defaults in almost all
places and shifted it to the actual domains. Default implementations
should be used with great care.
Computation time is never an issue in mathematics, but one should not
(totally) neglect it in computer algebra.
Your (2) from above refers to the idea of renaming operators. Currently,
apart from the "renaming during inheritance", we are restricted anyway
quite a bit. For example, I would like my multiplication sign to look
like \times or \circ. Well, Aldor does not (yet) handle Unicode. But
even if it did, I would probably have to disambiguate certain
mathematical expressions so that they become Aldor programs.
But actually that is another issue: How to write a good user interface
(notations) that maps nice looking expressions to the right underlying
algorithm. Maple and Mathematica know already quite a bit of such user
interfaces. However, they don't have the beauty of types.
There is Chapter 9 of Doye's PhD thesis
http://portal.axiom-developer.org/refs/articles/doye-aldor-phd.pdf
which deals in part with the renaming.
From what I understand, it simply makes two mathematically distinct
things (operator symbols and operator names) distinct in the programming
language. (Though I don't quite like the syntax.)
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.
It would certainly make sense to print "a + a" as "2*a", but how an
element of a domain is printed is decided by the domain.
If we have
define MyMonoid: Category == with {
1: %;
*: (%, %) -> %;
power: (%, Integer) -> %;
}
-- and (now fancy notation with renaming)
define MyTimesPlus: Category == with
MyMonoid;
MyMonoid where {
0: % == 1;
+: (%, %) -> % == +;
ntimes: (%, Integer) -> % == power;
}
}
Then MyTimesPlus has 6 different signatures.
If one removes the line "ntimes" then it would be only 5 and "power"
would correspond to the multiplication (or (more correctly) to the
actual implementation of it in a corresponding domain).
So, operator symbols and operator names agree as long as they are not
renamed.
And one could also build
MyInteger1: MyTimesPlus == add {
Rep == Integer;
0: % == per 0;
1: % == per 1;
...
}
MyInteger2: MyTimesPlus == add {
Rep == Integer;
0: % == per 1;
1: % == per 0;
(x: %) + (y: %): % == per (rep x * rep y);
(x: %) * (y: %): % == per (rep x + rep y);
...
}
Now, clearly, it can easily be figured out what 0, 1, +, etc. mean if
MyInteger1 or MyInteger2 is in scope. If both are in scope then nobody
can infer what "0 + 1" should return. In fact, constructing
implementations like that is also currently possible without renaming.
So I hope we need not argue a third issue: (3) maintaining standard notations
for the defining operations in common algebraic structures.
Hmmm, don't some people use \cdot, \times, \circ, \odot, etc to denote
multiplication? ;-)
But let's continue with MyInteger1/2.
If I now ask
MyInteger1 has MyMonoid
then that refers to the multiplicative structure. I have, however, to say
macro MyAdditiveMonoidMacro == {
MyMonoid where {
0: % == 1;
+: (%, %) -> % == +;
ntimes: (%, Integer) -> % == power;
}
}
MyInteger1 has MyAdditiveMonoidMacro
So what do I gain by a "renaming feature"? Not much, since now I must
add the corresponding "with respect to addition" or create another category.
(Isn't that very similar to the case when Monoid and AbelianMonoid are
totally unrelated?)
In fact, if I now define a new category
define MyAdditiveMonoidCategory == {
MyMonoid where {
0: % == 1;
+: (%, %) -> % == +;
ntimes: (%, Integer) -> % == power;
}
}
and ask
MyInteger1 has MyAdditiveMonoidCategory
then this should (and must) return false since MyInteger1 is not
explicitly declared to be a member of that category.
Ralf
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, (continued)
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/01
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, William Sit, 2006/03/02
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/02
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/04
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/03
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, William Sit, 2006/03/04
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures,
Ralf Hemmecke <=
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, William Sit, 2006/03/07
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/08
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/09
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/09
- [Axiom-developer] BINGO, Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/09
- Re: [Axiom-developer] BINGO,Curiosities with Axiom mathematical structures, William Sit, 2006/03/09
- Re: [Axiom-developer] BINGO, Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/10
- Re: [Axiom-developer] BINGO,Curiosities with Axiom mathematical structures, William Sit, 2006/03/10
- Re: [Axiom-developer] BINGO, Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13
- RE: [Axiom-developer] BINGO, Curiosities with Axiom mathematical structures, Bill Page, 2006/03/09