Gaby, I have a few questions at the end of this email, but first can I check if I have understood correctly:
As I understand it, in the existing 'catdef.spad.pamphlet': Categories that inherit from SemiGroup use '*' as the main operation *: (%,%) -> % Categories that inherit from AbelianSemiGroup use '+' as the main operation +: (%,%) -> % So we can get ring and field-like categories by inheriting from both. So the commutative axiom is bound up with function names and inheritance details when it might be more flexible if they were independent concepts. The code in the Yue Li sandbox works differently from this in that it uses a generalised mapping op: Mapping(T, T, T) which can be mixed and matched in a more general way. I get the impression that the new 'assume' syntax is intended to allow this more generalised approach to be applied to the categories in 'catdef.spad.pamphlet'. I get the impression that each of these mappings would have a category and a domain like this: category BINOPC BinaryOperatorCategory domain BINOP BinaryOperation So my questions are: q1) Are my above assumptions correct? q2) How do you plan to meld this new structure into catdef.spad.pamphlet? Do you plan to replace existing categories one-by-one or build the new structure in parallel with the existing. q3) Would all categories in catdef.spad.pamphlet, that represent a single operation over set, also have a domain? q4) How would you code a ring-like category to combine two single operation categories? q5) Would these new domains add any run-time overhead? q6) How to convert logic/rules into axioms/quantifiers, for instance in CancellationAbelianMonoid: c = a+b <=> c-b = a q7) Or in EntireRing: ab=0 => a=0 or b=0 q8) Or in EntireRing: not(1=0) q9) Or in OrderedSet: a<b and b<c => a<c q10) How would you handle "Conditional attributes" such as in EuclideanDomain: multiplicativeValuation Size(a*b)=Size(a)*Size(b) q11) How would you handle constraints like in Field: a*(b/a) = b | (a not 0) I Have drawn a diagram (by hand) of all the existing categories in catdef.spad.pamphlet about half way down on this page: http://www.euclideanspace.com/maths/standards/program/axiomsInAxiom/ This is just a start, it really needs to be optimised to clarify these issues. Perhaps if I understood the answers to the above questions better I might be able to change it to reflect the proposed new structure? Martin ------------------------------------------------------------------------------ Precog is a next-generation analytics platform capable of advanced analytics on semi-structured data. The platform includes APIs for building apps and a phenomenal toolset for data science. Developers can use our toolset for easy data analysis & visualization. Get a free account! http://www2.precog.com/precogplatform/slashdotnewsletter _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
