On February 27, 2006 10:37 AM Tim Daly (root) wrote: > ... > 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 semantics 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. >
Right on! I agree completely with both your analysis and your conclusion. > 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. Of course not all mathematics is inherently ambiguous and there are usually several different ways in which the ambiguity can be resolved. I would like to suggest (of course I can't prove it, yet. :) that the current approach to many mathematical subjects in terms of formal category theory provides a way of reducing the ambiguities in a way that is largely compatible with Axiom. For example, it seems to me that the formal definition given by Ralf Hemmecke in this email thread of a polynomial in terms of a graded sum is of this sort. That is the reason why Axiom's behaviour seems much less anomalous when described in this way. >... > 'semantic context' is really an 'extended 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". > I agree. My point of view is that as designers of computer algebra systems we need to be sensitive to the way that mathematics is actually done. We want a system that is easy to approach for someone with at least the usual non-specialist undergraduate experience in math - one that they will find immediately useful for at least some of things they want to do. But that does not mean that we need to be "held hostage" to only certain ways of doing mathematics. Where it seems an advantage, a system like Axiom needs to be free to present it's own method for formalizing and solving mathematical problems. In this case the user might need to learn something new in order to use Axiom even though they may have an advanced level of understanding of their subject in conventional mathematical terms. More than just the mechanical assistance that Axiom provides in solving a problem, it is this new formality that I think is the real value added by Axiom. This means that in some cases Axiom's way of doing things needs to be very carefully and completely documented. Unfortunately we do not have much documentation of this type for Axiom. > the compiler will let you keep the two domains separate and will > force you to merge the domains when you want that behaviour. 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). I agree. And again this is largely a function of the quality of the available documentation. I think the existing Axiom interpreter has it's good and bad points. Each of these needs to be understood without having to endure a long period of learning by trial and error. Good user interface design is a large and still largely un-solved problem. So there is still a lot of room for improvement. But changes to a complex existing system like Axiom need to be done very carefully because even simple changes can potentially have large and unexpected consequences for some applications and some ways of using Axiom. But at the same time this might provide sufficient motivation to continue the development of alternate user interfaces such as proposed in the B# project. > > 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. > I think you are right. In fact, I would say that the point is not so much that we should agree, but rather that we need to understand how it is possible to accommodate several different points of view even though they might appear at first to be contradictory. I think we need to focus *first* on documenting clearly what Axiom actually does, rather than trying to judge whether what Axiom does is "right or wrong". Because Axiom is open source software, if necessary, we can actually read the source code itself to determine this exactly. And we can demonstrate our understanding with actual experiments in Axiom. So far, I think we are doing a pretty good job of this. But it still needs to be distilled into useful documentation that can be read by non-specialists. Second, we need to try to explain *why* Axiom does what it does. This is harder and it might be difficult to get full agreement. Some parts of Axiom were clearly the result of experiments that were part of the overall research project. Some of these experiments where more successful than others and unfortunately we do not have very much documentation of this original research. My point of view is that where necessary we should try to create models that are (perhaps only largely) consistent with Axiom but motivated by contemporary methods in mathematics. This is where I see category entering. Since category theory is now also a fairly well accepted tool in programming language semantics, I think we are in a good position here. Third, we can consider changes to Axiom that would make it more self-consistent and that would make it conform more closely to the models that we have developed above, in brief: to make Axiom more categorical. Regards, Bill Page. _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
