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

[Waldek Hebisch]

C Y wrote:
> --- Waldek Hebisch <address@hidden> wrote:
> > 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?
>

If you start proving that expression are "undecidable" you get four
classes of expressions: provably zero, provably nozero, 
provably "undecidable" and the rest ("doubly undecidable").

There is a simple "algorithm" to prove that an expression is zero:
just start writing down all posible proofs. If the expression is
zero you will eventually find the proof. Similarly if an expression
is nonzero. I wrote algorithm in quotes because such procedure
finishes only if get the answer: if an expression is "undecidable"
the procedure will loop infintely long. Note that the problem is
really in recognizing that expression is "undecidable": if you
know that expression is "decidable" you can start enumerating
proofs and stop once you get one of the answers (zero or
nozero). You try to escalate: start another procedure that will
try to prove that expression is "undecidable" and stop once
you get one of the answers (zero, nozero or "undecidable")
but the point is that you will always have a part that
your procedure can not handle.

> > 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 math we have assumptions and consequences. Interesting theories
must be "open": if you add more assumptions you get more consequences.
More assumptions means higher risk that the assumptions are wrong...

I do not know what you mean by "might have a solution found, but not
by any algorithmic technique"? The only nonalgorithmic technique
of "solving" _algorithmic_ problem that I know is adding
assumptions. But in math we do not add assumptions lightly. In
fact, it is belived that all existing math may be handled inside
classical Zermelo-Frankel set theory (some theories want stronger
assumptions to allow more elegance and convenience, but less elegant
reformulations inside classical set theory should be possible). Also
a few attempts to extend Zermelo-Frankel theory failed (extended
theory contained contradiction).

Working with fixed assumptions you have a negative result: there
is no best algorithm. You have also a "positive" one: for each
algorithm there is a better one.

I think that one should have some distance to undecidability.
Implementer should know basic facts to avoid searching for
a simple "universal" algorithm. But already decidable
problems may require too much resources to solve. So one can
only handle "easy" cases of decidable problems. But if
you look at subcases of undecidable problem it also may have
easily decidable ones. For example deciding if a program ever
stops is hard, deciding if it stops in first million of steps is easy
(just run it and interrupt if it runs too long).

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

Related but different: if you have a subfieled L of complex numbers
and an irreducible polynomial P over L and a is a root of P, then
there is a smallest subfield of complex numbers (denoted by L(a))
containing both a and L. If you have two different roots a_1 and a_2
you get two different fields L(a_1) and L(a_2). But the two fields
are isomorphic. In other words, the internal structure of L(a)
is independent of the choice of root (it depends only on P). When
I talk about "abstract algebraic extension" I mean any field
isomorphic to L(a). There is an easy procedure (implemented in
Axiom) to build one such field and as long as you stay in a
single field the result remain valid for true L(a). The trouble
begin if you ask how a interacts with things outside L(a).
Theoreticaly this is not a big problem: you can replace multiple
algebraic extensions (say adding sqrt(2) and sqrt(3)) by a
single one. But Axiom can not decide if it should add sqrt(6)
or maybe -sqrt(6). Note that sqrt(2)*sqrt(3) problem is an easy
case which could be easily resolved within existing framework.
But already sqrt(x)*sqrt(x-1) is tough: if you take real
interpretation then sqrt(x-1) is undefined (or imaginary if you
prefer) for x < 1. So sqrt(x)*sqrt(x-1) is undefined (or negative
if you allow imaginaries) for negative x, but sqrt(x*(x-1)) is
well defined positive number for negative x.

Indeterminates can bridge the to words: single indeterminate
could represent all roots of a polynomial. For each posible
choice one could form apropriate algebraic extension and get
well defined result. At the end one should recombine all
choices into a single indeterminate representing final
answer.

-- 
                              Waldek Hebisch
address@hidden