[Axiom-developer] Re: Questions of Simplification

[Waldek Hebisch]

C Y wrote:
> I know in general simplification and comparisons of equality are hard
> problems, but I'm afraid I'm not familiar with the formal mathematical
> results that demonstrate this.  Practically the problem is obviously
> difficult, and I have heard on many occasions that equality of two
> expressions is undecidable in general, but I'm curious if these
> questions have some "formal" mathematical analysis behind them.
> Can someone recommend some resources on automatic simplification,
> discussions of what "simplification" means, and issues related to
> undecidable equality cases?  My motivation is this - for some cases
> equality is undecidable, for some it is undecidable in reasonable time,
> for others is is solvable (4^a=2^(2a) being the example in issue 191).
> If equality cannot be decided in general, perhaps there is a way to
> categorize expressions so that it is "decidable if the question is
> decidable", so to speak.  I suppose the question is not terribly
> interesting from a theoretical mathematical standpoint, but if it
> should happen to be possible it would be very useful in CAS work.
> 
> Maybe there isn't any way in general to make this systematic, but if
> not I would like to understand why that's the case.  Any pointers
> appreciated.

I have a web page where I put references to some basic literature
about symbolic computations:

http://www.math.uni.wroc.pl/~p-wyk4/malgo/literat.html

For your question fundamental result is Richardson 1968, where he
proved that when expresion are build from arithmetic operations,
polynonials and trigonometic functions then already the problem
of finding out if a given expression in zero is undecidable.

Note that sound algorithm should _prove_ that expression is zero.
For some expressions we can show that there is no proof that
the expression is zero, but also no proof that the expression is
nonzero. Naive idea would be to classify expression into
provably zero, provably nonzero and and "undecidable". The catch
is that proving that an expression is "undecidable" is even
harder problem that proving that it is zero. So in constructive
direction we are trying to find out large classes of decidable
expressions, but without any hope of completeness (more effort
is likely to give bigger class).

In constructive direction there is again result of Richardson 
(How to recognize zero) where he proposes a method which
hopefully can decide equality of elementary numbers (numbers
produced using algebraic operations, exponential and trigonometric
functions). For elementary functions (functions build from polynomials,
exponential and trigonometric functions using composition and algebraic
operations -- absolute value is excluded) there is Risch (1979) structure
theorem which reduces the problem to constansts.

Axiom problem is that its notion of equality is inconsitent: Axiom
sometimes treats roots (in particular square root) as multivalued,
but in other places assumes that expressions form a field which
requires building abstract algebraic extension (or choosing a single
value). This dual notion of equality is responsible for bug 290:
Risch algorithm requires a field, but since Axion do not apply
simplification to roots we in fact get ring with zero divisors.

-- 
                              Waldek Hebisch
address@hidden