Re: [Axiom-developer] Provisos

[root]

>>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