Just that = is not computatble doesn't mean that it's not existent.
Thus, associativity in MartinMonoid guarantees that
(a*b)*c and a*(b*c)
will be equal, but it does not mean that FriCAS can prove this
equality.
OK, what you mean is that you have a "virtual function" (let's call it
EqUaL) which us use in the axioms and which behaves like the
mathematical equality. (I abbreviate now MMon ==> MartinMonoid.)
"associativity in MMon" means then that every domain D that implements
MMon must be such that the relation EqUaL((a*b)*c, a*(b*c)) holds for
every elements a,b,c in D.
You know, we have something similar in aldor-combinat. Just suppose that
D is the domain containing all species. Ufff, no, we couldn't claim
MMon, because our implementation of * is neither commutative nor
associative.
But for PowerSeries you might even succeed to claim associativity.
FriCAS does that with CommutativeRing. Clearly an uncomputable property
for infinite domains, but if something claims to be of category
CommutativeRing (or MMon) then it is the task of the programmer to
really implement that claim. (Actually, it would be even better to
deliver a proof that the implementation is doing as claimed.---In fact,
that proof would be equivalent to this (named) category CommutativeRing.
In particular, any algorithm for a MartinMonoid can rely on
associativity.
... and on uniqueness of the unit 1? Can you claim that for PowerSeries?
That's actually interesting. Look at my powerseries implementation in
aldor-combinat. 0 and 1 are constant series and they are known to be
finite. If you'd ask zero?(0) you'd get a definite 'true' in finite
time. But for z := exp(x) - exp(x), all I can do is to compute the
powerseries up to a certain order. Asking zero?(z) would be an infinite
process. Strictly speaking, in my implementation 0 and z are different.
But now if you use EqUaL as your relation for deciding uniqueness, then
I bet EqUaL(0, z) should be true. The 0 is unique, but it's not
effectively checkable. Of course, I can live with such concepts and they
might even be useful, but one should clearly adapt/design the category
hierarchy for that and have everything properly specified.
I think the determinant for power seris example is quite useful:
I don't say otherwise. I just ask what you mean by "determinant"? Is it
defined by the alternating sum of products formula?
http://en.wikipedia.org/wiki/Determinant#n-by-n_matrices
Then for sure you can have this. And if you impose an explicit order on
the summands and multiplicants, you could define "determinant" even for
structures where neither * nor + is commutative. To put it to the
extreme, you can define such a determinant expression even if neither *
nor + is associative.
But what can you then do with this definition of determinant?
Sure for TaylorSeries we could ask whether the determinant is 0 up to a
certain given order. But you probably have other use cases.
we have to distinguish between commutative rings where zero can be
detected and commutative rings where it cannot.
Sure, that makes sense. And it should be reflected in the category
hierarchy.
But in both cases we can compute the determinant!
Sure, I agree.
> (Although with a significant difference concerning performance.)
Efficiency is another problem.
However, we have to rely on commutativity.
Why?
Ralf
--
You received this message because you are subscribed to the Google Groups "FriCAS -
computer algebra system" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/fricas-devel?hl=en.
