Re: about emp (was: Motion 42: NO)
On 2013-02-17 14:32:31 +0000, John Pryce wrote:
> On 8 Feb 2013, at 02:14, Vincent Lefevre wrote:
> > nonempty_emp makes sense for sqrt(-x*x-1) with x = [-1,1]. As an
> > expression on intervals, sqrt(-x*x-1) = sqrt(-[-1,1]-1) = sqrt([-2,0])
> > = [0,0], so that the computed result must contain [0,0]. In general,
> > one would get [0,0]_trv. But if the implementation can determine that
> > for the point function sqrt(-x*x-1), the result is not defined for any
> > input of [-1,1], then it could improve the decoration to emp.
>
> I find something very unsatisfactory about what I call Vincent's
> "let's do half the job" argument that the returned value yy_dy in
> the last paragraph may have dy=emp, yet should (or shall) have
> yy=[0,0] "because we can't be sure what the user intended".
I recall that this is *not* "let's do half the job". There are good
reasons why an implementation may choose to behave that way, as I've
already explained.
> P1788 does not formally define the meaning of "expression", but in
> the forthcoming Draft 7.x, part of Ch 1 says semi-formally some
> things that an expression is, and is not, as guidance. I propose
> that it should also include this:
> (*)
> +---------------------------------------------+
> |An implementation SHOULD treat an arithmetic |
> |expression as meaning exactly what it says. |
> +---------------------------------------------+
This can be very ambiguous (examples could be included to say what can
be done and what can't, but remember that examples are just informative,
so ideally they shouldn't be needed).
> This would imply, for us, that
> (**)
> +---------------------------------------------+
> |The standard's design decisions shall assume,|
> |where relevant, that this is the case. |
> +---------------------------------------------+
>
> That is, any section of code (possibly part of a larger expression)
> that defines an arithmetic expression f(x_1,...,x_n) in distinct
> code variables x_1,...,x_n, SHOULD be regarded as defining the real
> function of those variables in the naive way.
>
> This should resolve many of the above arguments. In particular:
> - No way can sqrt(-x*x-1) be regarded as possibly being
> the 2-argument function sqrt(-x*y-1).
> - It should be unconditionally valid within *interval* code for
> an implementation to replace x*x by sqr(x).
> - Similarly it should be valid to replace a*x+b*x by
> (a+b)*x in cases where a,b are constants and a+b can be
> represented exactly, including x-x being 0; etc.
>
> No obligation for an implementation to do such optimisation, and
> there shall be ways of turning it on and off.
> Thus the user who wants sqrt(-x*x-1) with x=[-1,1] to give [0,0]
> shall be able to ensure this.
This is important. But I wouldn't call the above an optimization as
it changes the behavior.
> But if he is so perverse as also to want the decoration emp
> returned, he must run the code twice: with optimisation off, and
> with it on.
Of course, someone who is interested in the computation as a range
computation (by regarding variables as representing intervals, not
real numbers) wouldn't care about the decorations.
> There must be caveats to (*). E.g.
> - What about sqrt(-x*y-1) where variables x and y are
> aliases for the same memory location?
I don't think the memory location should matter[*]. But how the
variables are computed matters. For instance, if one has
y = x;
in the code, they may be regarded as having the same value.
[*] Even in C, two pointers having the same value, and even the same
bit-representation, are not always interchangeable. For instance, see
the following article:
http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1637.pdf
"Subtleties of the ANSI/ISO C standard", by Robbert Krebbers and
Freek Wiedijk (BTW, they give reference to a mail by Nick Maclaren
in 2001). This also shows that a language can have its own rules
on how to interpret an expression.
> - In particular what about sqrt(-a[i]*a[j]-1) where it
> cannot be determined statically whether i and j are equal?
I don't think there can be an ambiguity here, because no special
treatment could be done in such a case (except by generating code
with a test i == j).
> But IMO these are to do with language semantics, and not our business.
Agreed.
--
Vincent Lefèvre <vincent@xxxxxxxxxx> - Web: <http://www.vinc17.net/>
100% accessible validated (X)HTML - Blog: <http://www.vinc17.net/blog/>
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)