[Axiom-developer] Re: Questions of Simplification

[C Y]

--- Waldek Hebisch <address@hidden> wrote:

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


__________________________________________________
Do You Yahoo!?
Tired of spam?  Yahoo! Mail has the best spam protection around 
http://mail.yahoo.com