ok, time for me to weigh in on this subject.... but i will do it at a meta-level.
i think it is important to distinguish between mathematics and computational mathematics. my experience is that written mathematics notation is very ambiguous. we don't normally notice this because we view each equation in the context of a given subject and, usually, in the context of a few paragraphs that contain the semantics. axiom attempts to capture the semantics and carry it in the type. if the sematics of the type fits your understanding of the equation then axiom works "correctly". if not, it appears to be a bug. (axiom is hardly bug-free but i'm focused on the DMP issue here) so what is the semantics of 2*x + 1/x? well, it's ambiguous. each of you have successfully argued your understanding of the semantics. and, in the context you've established, you are correct. but axiom has to assign a meaning that might not match your understanding. this is where the ambiguity becomes apparent. it is also where mathematics and computational mathematics part company. the 'solution' to this problem is to develop the computational idea of a 'semantic context'. essentially what is needed is the ability to say (at least in computer science terms): "i want 'x' to be globally scoped" or "i want 'x' to be locally scoped" but that isn't the best long-term approach. 'semantic context' is really an 'extented type' idea. that is, you want to be able to tell axiom what area of mathematics you are working in and have the type system adapt its meaning to that area. this is the section of the textbook where the author say things like: "i'm carefully distinguishing the Ring of coefficients from the variables in the polynomial" vs "this book explores polynomial arithmetic". the compiler will let you keep the two domains separate and will force you to merge the domains when you want that behavior. the interpreter is just guessing and you have to be careful to understand how and why it guesses. (which means we have to construct a model of the interpreter so we can formally state the coercion/conversion graph). in my world view a semantic context is another facet in the crystal. (but that's still long-term fantasy so we won't talk about it here). anyway, i don't see that it is possible to resolve this debate. you are all arguing from different semantic contexts. until you agree to use the same assumptions there is no resolution. t _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
