[Axiom-developer] Re: Questions of Simplification (whoops)

[C Y]

Whoops - sorry about the blank reply.

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

Good list!  Thanks!

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

I'll see if I can dig that up at a college library.  It sounds like the
information in that paper should be part of the eventual Axiom literate
documentation on simplification.

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

Blegh.

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

Wait - if you can't prove that it is zero, isn't the only possible
proof one that it is undecidable?  You mean that an undecidability
proof in the case of an undecidable problem is more complex than a
proof that something is zero, when something can be proven to be 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).

So classes of undecidable problems might have a solution found, but not
by any algorithmic technique?

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

Interesting!  I also need to scare up the original Risch papers .
 
> 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.

Hmm. Is "abstract algebraic extension" similar to the discussion on
indeterminates?

Cheers, and thanks!

CY

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