Ralf Hemmecke <[email protected]> writes: >> 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.)
The truth is: yes. I didn't dare to introduce that concept here on the list because I do not know enough about decidability etc. > "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. Why not? The question is: commutative with respect to which notion of equality. Of course, equality as implemented violates commutativity. (actually, I think that's my whole point: it's not the implementation of multiplication that violates commutativity, but rather the implementation of equality.) > ... and on uniqueness of the unit 1? Can you claim that for > PowerSeries? No. and there should be another assertion for that. In Sage-combinat they have UniqueRepresentation, in FriCAS we have things like unitscanonical or some such. There was some discussion about the meaning of that one (involving Waldek) some year or so ago. > 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? Again: not the implementation of * and + is bad. It's only equality that's failing. If we do not use equality, all is well. There are lot's of useful computations you can do without equality, in fact. For example, I could compute the determinant of a matrix of power series and then guess a closed form from what I get. >> However, we have to rely on commutativity. > > Why? I cannot think of an example where it matters right now, but I'm sure there are. (I should add: yes, there is an established definition for determinants in noncommutative rings. But I never worked with such beasts so far.) In any case, the current implementations of the determinant almost certainly only give the right result in the commutative case. Martin -- 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.
