[Axiom-developer] Re: severe (!) bug in normalize

[Waldek Hebisch]

Martin Rubey wrote:
> Waldek Hebisch <address@hidden> writes:
> > rischNormalize (using Risch strucute theorem) can detect that some kernels
> > are algebraically dependent and forms an expression which is a constant.  
> > But
> > simplifier is unable to see that the expression is constant.  You have
> > written that simplifing is undecidable, but that happens even for "easily
> > decidable" classes.  The problem really is that various part of Axiom use
> > inconsistent conventions.  rischNormalize is sound _only_ when
> > sqrt(6)=sqrt(2)sqrt(3).  But simplifier refuses to do such simplifications
> > (they are invalid using default "real" convention) and things which
> > matematically are fields turn into rings with zero divisors.
> 
> Yes. This *really* needs cleaning up. In fact, I think we should consider to
> redesign the algebra to make use of axioms like canonicalUnitNormal and the
> like. Maybe Francois is heading in the right direction, too, when he tries to
> choose consistent simplification rules for EXPR. However, I think that he will
> need some help.
> 
> I guess that the main problem with EXPR and friends is, that it is not clear
> what the variables are. Do you know the assumptions needed for RischNormalize?
I do not know what problems with variables you see here (I am aware of
tread about Polynomial Expression Integer, but I think it is a separate
problem).  The problem I mention really boils down to definition of
roots (in praticular square root): some field computations
treat roots just as a particular case of field extension.  So root is
an abstract quantity fully characterized by its defining polynomial.
But numerical functions and some real algorithms do care which
of the roots is chosen.  
We should systematically distinguish both kinds of extensions. When
convertion from "real" extension to "agebraic" in may be wise to
keep extra info around so that we can convert back without loss
of information.  When converting from "agebraic" extension to a
"real" one we need to do a case split (here conditional expressions
would be usefull).

RischNormalize tries to implement Risch structure theorem:

------<start TeX>
\begin{theo}\label{rischstr1}
Let $K$ be a differential field with
derivative $D$ and field of constants $k$.  Assume that elements
$z_j\in K$, $y_j\in K$ satisfy ${{Dz_j}\over{z_j}} = Dy_j$,
$j = 1,\dots,n$.  Then either transcendental degree of
$k(x, y_1,\dots, y_n, z_1,\dots, z_n)$ is greater or equal to $n+1$
or elements $Dy_1,\dots, Dy_n$ are linearly dependent over
rational numbers.
\end{theo}


\begin{coro}\label{rischstr2}
Let $K$ be a differential field with $D$.  Assume that elements
$z_j\in K$, $y_j\in K$ satisfy ${{Dz_j}\over{z_j}} = Dy_j$,
$j = 1,\dots,n$ and that $K$ is algebraic over
$k(x, y_1,\dots, y_n, z_1,\dots, z_n)$. Also assume that
${{Dz_{n+1}}\over{z_{n+1}}} = Dy_{n+1}$ and $y_{n+1}\in K$.  Then
either $z_{n+1}$ is transcendental over $K$, or there are rational
numbers $q_j$ such that
$$Dy_{n+1} = \sum_{j = 1}^{n}q_jDy_j.$$
In the second case $z_{n+1} = c\prod_{j = 1}^{n}z_j^{q_j}$, where $c$
is a constant.
----<end TeX>

so basic assumption is that we are given a computable field of
constants.  But rischNormalize uses operations implemented by other
domains to perform actual computuations, so there are extra
assumptions.  One is that if an expression does not depend on a
kernel (which is checked using derivatives) simplifier should
eliminate this kernel from the expression.  For example
representing 'y' as 'x - x + y' is legal for computable fields,
but rischNormalize would not tolerate such representation.
Of course, since expressions are represented as rational functions
of kernels such simple problem can not happen in Axiom. But
(sqrt(2)*sqrt(3)-sqrt(6))*exp(x) already hints towards possible
problems.

-- 
                              Waldek Hebisch
address@hidden