>>Do you know how this is different from the GUARDIAN package (Reduce) >>described in this ISSAC'97 paper? >> >> "Guarded Expressions in Practice" >> Andreas Dolzmann and Thomas Sturm >> >> http://portal.acm.org/citation.cfm?id=258851 > >I don't know. The comments I made were from my thesis work done prior >to this publication. I don't have access to that paper at the moment. >If you have a copy perhaps you could summarize the differences. >
Certainly the general case of combining provisos suffers from several problems, not the least of which is the zero-equivalence problem. Thus while it is not difficult to add constraints that split a computation, it is in general undecided if they can combine. That said, there is one likely difference. In the Axiom implementation, the provisos consisted of "constraint" objects which were over particular domains. Thus, [x > 0] is a strongly typed constraint from POLY(INT) (assuming x came from POLY(INT)). The logical operations were typed also, so given [x > 0] as a constraint from POLY(INT) and [x < 0] as a constraint from POLY(INT) then [x > 0] & [x < 0] uses a typed '&' operation from POLY(INT). Since the domain added the constraints, presumably the domain knows how to combine them. Any other paper or implementation I've seen uses untyped operations based on pure symbols. Thus given [x > 0] & [x < 0] the operation is some order-sorted algebra over naked symbols. The reasoning over these symbols knows nothing about the domains. This loses a lot of information that is carried in the types about how to combine the constraints. Thus they tend to fall back on either matching operations or unification operations. Tim _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
