Re: Question on rewriting and program specification

Re: Question on rewriting and program specification

[Andrej Bauer]

Jacques Carette wrote:
> Of course, if you happen to know exactly
> which semi-decision procedures are being used, you can fool them and get
> the system to either go into an infinite loop or give a wrong answer.
> But that requires a huge amount of knowledge to do so.  The average user
> would be unable to manufacture such examples.

I have a rather unfortunate experience with "average users" who get
wrong answers from CAS's, namely our undergraduate math majors. In their
first-year analysis course they learn how to compute limits. Invariably,
they are given some limits which Mathematica gets wrong, e.g.:

Limit[((1 + 4 x^2)^(1/4) - (1 + 5 x^2)^(1/5))/(a^(-x^2/2) - Cos[x]),
      x -> 0]

The answer is 0, _except_ when the parameter a equals e, in which case
the answer is 6. Yes, this is a nasty limit pulled out of a hat, but it
is precisely the sort of thing we test our students on. It is rather
disappointing that Mathematica falls into exactly the same sort of trap
as the average student.

Another example is the use of l'Hospital rule, which is used by every
CAS. There is a side condition which is not checked by them, which makes
them give wrong answers. (The side condition is very nasty to check,
namely, whether the zero of a derivative is isolated.)

The situation is even worse when engineers and physicsts use CAS. They
trust them blindly (I suspect). One day they're going to build a nuclear
power plant based on a faulty limit computed by Mathematica or Maple.

Andrej Bauer

Computer Algebra weaknesses

[Jacques Carette]

I should have been more precise when I spoke of "decision procedures" in
the context of a CAS.  There are many semi-decision procedures for
non-parametric problems.  For parametric problems, these procedures
break down.  The issue is almost always the same: a theorem is applied
without properly checking side-conditions.  Frequently, the issue is one
of zero recognition in the presence of parameters, but there can be more
complex situations, such as the one Andrej points out.

CASes are typically very good at getting good answers at non-parametric
problems, and my comments were aimed mostly at that class.  Computer
Algebra implementers (and I used to be one) are typically very afraid of
combinatorial explosions, as a lot of computer algebra people are
``algorithms'' people.  Their mathematics background was often such that
they prefered a ``generic'' answer quickly than a thorough answer that
was a) a mess, and b) slow to get.  This is, in part, why I am now in
academia, as I want to ``fix'' that.

Andrej Bauer wrote:

>I have a rather unfortunate experience with "average users" who get
>wrong answers from CAS's, namely our undergraduate math majors. In their
>first-year analysis course they learn how to compute limits. Invariably,
>they are given some limits which Mathematica gets wrong, e.g.:
>
>Limit[((1 + 4 x^2)^(1/4) - (1 + 5 x^2)^(1/5))/(a^(-x^2/2) - Cos[x]),
>      x -> 0]
>
>The answer is 0, _except_ when the parameter a equals e, in which case
>the answer is 6. Yes, this is a nasty limit pulled out of a hat, but it
>is precisely the sort of thing we test our students on. It is rather
>disappointing that Mathematica falls into exactly the same sort of trap
>as the average student.
>
>
This is exactly the kind of parameter specialization problem where CAS
designers have ``chosen'' to ignore and return a generic answer.  This
has been documented since at least 1991 in a nice paper in the Bulletin
of the AMS.

>Another example is the use of l'Hospital rule, which is used by every
>CAS. There is a side condition which is not checked by them, which makes
>them give wrong answers. (The side condition is very nasty to check,
>namely, whether the zero of a derivative is isolated.)
>
>
I don't know about Mathematica, but Maple does NOT use l'Hospital's
rule.  Almost all limits are computed using one-sided asymptotic series
expansions, as l'Hospital's rule is just not very suitable to
large-scale computations.  If interested, I can provide various
published references to the algorithms involved.

Of course, one still needs to check that the leading term is non-zero.
For the limit above, observe (in Maple):
 > assume(a::real, x::real);
 > f := ((1 + 4*x^2)^(1/4) - (1 + 5*x^2)^(1/5))/(a^(-x^2/2) - cos(x)):
 > normal(series(f, x=0,5));

                             1        2       4
                       - ---------- x~  + O(x~ )
                         ln(a~) - 1


which clearly indicates that a=exp(1) is a problem point.  That the
limit is computed anyways is an instance of choosing the ``generic''
answer [whatever that means].

>The situation is even worse when engineers and physicsts use CAS. They
>trust them blindly (I suspect). One day they're going to build a nuclear
>power plant based on a faulty limit computed by Mathematica or Maple.
>
>

Engineers and physicists don't use CAS - they use Matlab.  The errors
you get there are both worse and better: worse because numerical
algorithms are so much more prone to giving (silent) nonsense, and
better because Matlab cannot phrase any problems which are parametric!

In Ontario (where I teach to Engineers), an Engineer who used either a
CAS or Matlab in a computation for their safety critical system and did
not check the correctness of the result, would be fully liable for any
ensuing problems on their design.  Thus, theoretically, Professional
Engineers are supposed to given full justifications for the answers of
the tools they use.  In practice, they trust the tools blindly a bit too
often.

Again in Ontario, I have some knowledge of the process used for
safety-critical software in nuclear power plants [I even have some grant
money associated to that].  Tools like Matlab or Maple would not be
allowed to give ``final'' answers, in any step of the process.  But this
is getting just a bit off-topic for the categories mailing-list...

Jacques