Re: [Hol-info] Different bug/feature in REAL_SOS

[John H. <Joh...@cl...>]

Hi Steve,

| Okay, so I'm stubborn, but this time I've got the bug/feature of REAL_SOS
| that I'd earlier tried to argue was different from the
| embed-the-naturals-in-the-reals problem _SOS that I'd identified still
| earlier.

This is indeed a different one. But it's not exactly a bug in the sense
of a local mistake, but a consequence of the general algorithmic
approach.

Generally speaking, the SOS functions do much better refuting a
conjunction of non-strict (<= or >=) inequalities. The prototypical
example that works well is:

 p_1 >= 0 /\ ... /\ p_n >= 0 ==> q > 0

since it is proved by refuting

 p_1 >= 0 /\ ... /\ p_n >= 0 /\ -q >= 0

and this is done by finding polynomials such that:

 m_1 + ... + m_k + s_1^2 + ... + s_l^2 = -1

where each m_i is a product of distinct input polynomials and a
nonnegative rational number. This leads to a contradiction since
the LHS by hypothesis must be negative.

However, as soon as you have a strict inequality (p_i > 0) and/or
inequality ~(p_i = 0), the refuting identity searched for becomes
significantly more complicated, since there may be no certificate of the
above form. This leads to the counterintuitive behaviour that making the
hypotheses stronger (from p_i >= 0 to p_i > 0) or even adding redundant
hypotheses (p_i > 0 and ~(p_i = 0) together) can make the behaviour
worse. The degree of parametrization increases significantly, which may
mean that the necessary search depth is greater, or just that the
numerical issues in floating-point conversion are more likely to
become an obstacle.

Of course, I would like to investigate alternative approaches to the
handling of strict inequalities. There are many interesting ideas to
pursue, but it would take a lot of experimentation to come up with
the right method. Do please keep collecting cases where SOS works
badly as well as cases where it works well, since these will be very
useful in such experimentation.

John.