>>> 4) Axioms are operator specific and not for the whole category. For >>> instance the lattice category inherits a commutativity axiom for join >>> and another commutativity axiom for meet. There is not just one >>> commutativity axiom. For more 'numerical' categories I guess we would >>> assume a commutativity flag applies to * and that + is always >>> commutative but relying on assumptions like that does not seem to >>> generalise well. >> >> Would this be covered by the current mechanism (using 'if' as in: >> >> if $ has Monoid >> x ** y == exp(y * log x) >> >> Or perhaps we can re-think the 'if' and move the conditional cases >> into their own categories. This would have the benefit of >> simpliying the compiler and the inheritance machinery. It would >> have the down side of expanding the category lattice. > >When you are talking about the current mechanism is this: having an >empty category for each attribute? It seems to me that this would >require quite a lot of categories because we don't just need >commutativity but meet-commutativity, join-commutativity and so on.
Actually, there already is an empty category for each attribute. But I'm thinking of something slightly different. Instead of conditional exports where it says every? : ((S -> Boolean),%) -> Boolean if $ has finiteAggregate that we have a separate category so that the new category inherits from the prior category and unconditionally exports the additional signatures. This eliminates the need for runtime signature checking. It also makes it easier to attach axioms to categories because there are no conditional attachments. Tim _______________________________________________ Axiom-developer mailing list [email protected] https://lists.nongnu.org/mailman/listinfo/axiom-developer
