[Axiom-developer] Provisos

[daly]

Thanks for the reference to the Guarded Expression in Practice paper.

That's a really pretty piece of work they've done. I like it a lot.
I'll have to get a copy of REDLOG/GUARDIAN and try it. This is a very
readable paper and they make a lot of good points.

Instead of wandering off into the sorted-order logic wilderness
they did manage to stay algebraic in their approach. They did ask
the question:
   When designing a new CAS based on guarded expressions, how
   should the knowledge be distributed between the algebraic
   side and the logic side?

Their problems are similar to the ones I encountered and their
solutions are similar. 




The one glaring difference is that I spent a lot of time reducing
the expressions into interval notation. The interval notation for
   x <> 0 
becomes
   [x <> 0]
which can be expanded (by POLY(INT), since it is domain specific) to
   [x < 0]
   [x = 0]
   [x > 0]
Other domains, say one that has OnePointCompletion (that is, infinity),
might put further cases into play:
   [x = %minusInfinity]
   [x < 0]
   [x = 0]
   [x > 0]
   [x = %plusInfinity]





Another difference is that rather than using a global simplifier
and global quantifier eliminator, the process is distributed
across the category/domain hierarchy. The intervals are called
Constraints, which are collected into SuchThat clauses, and you 
would have signatures like:

   and(a:Constraint(POLY(INT)),b:Constraint(POLY(INT)) -> Constraint(POLY(INT))

so that POLY(INT) would get involved in simplifying expressions and
constraints which are over that domain. Expressions over other domains, e.g
   Constraint(POLY(COMPLEX(INT))))
would simplify based on knowledge from that domain instead. Thus each
domain would know special information that could be brought forward to
help the simplification.

But you would expect that kind of architecture decision in Axiom.

Major kudos to Dolzmann and Sturm.

Tim