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

[Waldek Hebisch]

Martin Rubey wrote:

> Waldek Hebisch <address@hidden> writes:
> > P.S. AFAICS the problem is that the full list of kernel contains both
> > transcendental and algebraic kernels. goodCoef is relevant only for
> > transcendental kernels and got cofficients as a vector corresponding to
> > transcendental kernels. However, the list passed to goodCoef still contain
> > algebraic kernels, so goodCoef gets confised, and tries to eliminate wrong
> > kernel.
> 
> Yes, that's the same what I believe. However, I noticed that goodCoef is 
> called
> only in two functions, namely taneval and expeval. 
> 
> Here is expeval:
> 
>     expeval(f, lk, k, v) ==
>       y   := first argument k
>       fns := toY lk
>       g := y - +/[qelt(v, i) * z for i in minIndex v .. maxIndex v for z in 
> fns]
>       (rec := goodCoef(v, lk, "exp"::SY)) case "failed" =>
>         expnosimp(f, lk, k, v, fns, exp g)
>       v0 := retract(inv qelt(v, rec.index))@Z
>       lv := [qelt(v, i) for i in minIndex v .. maxIndex v |
>                                                  i ^= rec.index]$List(Q)
>       l  := [kk for kk in lk | kk ^= rec.ker]
>       h :F := */[exp(z) ** (- retract(a * v0)@Z) for a in lv for z in toY l]
>       h := h * exp(-v0 * g) * (k::F) ** v0
>       [eval(f, [rec.ker], [h]), [rec.ker], [h]]
> 
> 
> What I find a bit surprising is that goodCoef is not called as (roughly)
> 
>   goodCoef(v, fns, "exp"::SY)
> 
> fns would have to be coerced to the right type, of course. I thought that
> (formally), goodCoef
> 
>     goodCoef(v, l, s) ==
>       for i in minIndex v .. maxIndex v for k in l repeat
>         is?(k, s) and
>            ((r:=recip(qelt(v,i))) case Q) and
>             (retractIfCan(r::Q)@Union(Z, "failed") case Z)
>               and gdCoef?(qelt(v, i), v) => return([i, k])
>       "failed"
> 
> checks whether there is a kernel in l of "type" s, that has a coefficient 
> whose
> inverse is an integer, and such that all other coefficients are multiples of
> this coefficient. So, v and l should really be of the same length. Looking at
> deprel
> 
>     deprel(ker, k, x) ==
>       is?(k, "log"::SY) or is?(k, "exp"::SY) =>
>         qdeprel([differentiate(g, x) for g in toY ker],
>                  differentiate(ktoY k, x))
>       is?(k, "atan"::SY) or is?(k, "tan"::SY) =>
>         qdeprel([differentiate(g, x) for g in toU ker],
>                  differentiate(ktoU k, x))
>       is?(k, NTHR) => rootDep(ker, k)
>       comb? and is?(k, "factorial"::SY) =>
>         factdeprel([x for x in ker | is?(x,"factorial"::SY) and x^=k],k)
>       [true]
> 
> I have the feeling that the coefficients in v really correspond to the lists
> toY (for exp) and toU (for tan).
>

Yes, exactly.  But toY (and toU) transform kernels while goodCoef needs to
look at original (untransformed) kernel, so we would have to produce
a separate list.
 
> Altogether, it seems to me that the code could need a bit cleaning up. Does
> anybody know whether sumit contains equivalent functionality?
> 
> I must admit that I do not understand your patch. I assume that it also fixes
> the correspondence between the vector of coefficients v and the list of 
> kernels
> l. Why doesn't it fix that rather in expeval and taneval?
> 

I really do not "fix the correspondence": I detect when there is a
possible mismatch and return "failed" in this case.  The

     not (h = (maxIndex(v) - minIndex(v) + 1)) => "failed"

line is doing that.

Please understand that the patch is a compromise.  There are other
bugs when using EFSTRUC but at least one problem really affect most
of algebra.  Namely, rischNormalize can get into infinite loop:
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. 

You may think that simplification is a separate problem, but I
think that Bronstein added algebraic cases to rischNormalize
only because default simplifier was inadequate for his examples.
If you remove algebraic simplifications from rischNormalize then
the bug would go away.

Concerning my patch: EFSTRUC needs more fixes and restructuring it
may be a good idea.  However, such restructuring may require changes
in function signatures which currently requires rather lengthy
bootstrap procedure.  Also, I my tests I hit problems which looks
like compiler bugs (remember nested function thread).

So, I decided to do a minimal patch just fixing one problem. I tried
to keep changes localized -- putting change in expeval and taneval
would duplicate code.  To say the truth, fix for your problem is
a byproduct -- I simply did not want goodCoef to do wrong things
when a simple test could prevent it.

-- 
                              Waldek Hebisch
address@hidden