Changes http://wiki.axiom-developer.org/AldorLanguageRestrictions/diff
--
In Axiom and in Aldor's algebra library there are currently two categories
Monoid and AbelianMonoid. Due to language restrictions something of type
AbelianMonoid is not automatically a Monoid.
The reason is that (basically) the definition is as follows
(I add a prefix to avoid naming conflicts)::
\begin{aldor}
define MyMonoid: Category == with {
1: %;
*: (%, %) -> %;
}
define MyAbelianMonoid1: Category == with {
0: %;
+: (%, %) -> %;
}
\end{aldor}
It would be desirable simply to write::
\begin{aldor}
define MyAbelianMonoid2: Category == with {
MyMonoid;
-- ... some predicat logic expression (written in Aldor not as a
comment)
-- that states commutativity of *.
}
The additional expression is certainly not always computable, but the
information should be
formally there so theorem provers could use it.
Now we can define a ring
\begin{aldor}
define MyRing: Category == with {
MyMonoid;
MyAbelianMonoid1;
}
\end{aldor}
The definition of MyAbelianMonoid2 still uses "*" as the operation identifier.
So
\begin{aldor}
define MyRing: Category == with {
MyMonoid;
MyAbelianMonoid2;
}
\end{aldor}
is possible, but would lead to a category that basically exports "*" and "1".
So in order to define a Ring one would have to have a way to
rename "*" to "+" and "1" to "0" during the inheritance.
That is currently not possible in SPAD/Aldor.
See also a comment from
http://wiki.axiom-developer.org/[EMAIL PROTECTED]
\begin{latex}
\begin{verbatim}
>From WilliamSit Wed Mar 1 22:55:44 -0600 2006
From: William Sit
Date: Wed, 01 Mar 2006 22:55:44 -0600
Subject: Curiosities with Axiom mathematical structures
Message-ID: <[EMAIL PROTECTED]>
"Bill Page" <[EMAIL PROTECTED]> 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)
> |
\end{verbatim}
\end{latex}
Yes, there are no theoretical reasons, but there are plenty of practical ones.
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. Of course, if the Interpreter
knows what to instantiate, that won't be a problem. But how will the Interpreter
be able to know? 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? Can a compiler or interpreter catch this? If
not, it would be a nightmare of bug reports.
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 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. For CAS to be practical,
certain compromises are necessary. 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.
As already well-known, with the current status, all properties of operators are
declarative and not verified. There is a certain degree of trust that users know
what they are doing. 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. One consequence of
these examples is confusion of the real issues: the lack of documentation on the
conventions and implicit assumptions, and real bugs.
William
--------------------
Hmm, can you construct an example where the operation names would not be
available at compiletime? At the moment it is not even possible to treat
categories in a
truely first class manner.
How could the compiler type check the following?
\begin{aldor}
define Foo(b: Boolean): Category == {
if b then
with {foo: % -> %}
else
with {bar: % -> ()}
}
Dom(b: Boolean): Foo(b) == {
if b then
add {foo(x: %): % == x}
else
add {bar(x: %): () == {}}
}
\end{aldor}
But if the category is fixed, then a domain could tell the interpreter about
the function
names it exports without the need of being instantiated.
--
forwarded from http://wiki.axiom-developer.org/[EMAIL PROTECTED]
