Re: about emp (was: Motion 42: NO)
Guillaume, Vincent, P1788
On 8 Feb 2013, at 02:14, Vincent Lefevre wrote:
> On 2013-02-07 19:07:11 +0100, Guillaume Melquiond wrote:
>> Le jeudi 07 février 2013 à 16:11 +0100, Vincent Lefevre a écrit :
>>> On 2013-02-07 15:07:27 +0100, Guillaume Melquiond wrote:
>>>> Le jeudi 07 février 2013 à 14:50 +0100, Vincent Lefevre a écrit :
>>>> As I understand it, decorations propagate from inputs to output and you
>>>> can never get an output with a stronger decoration than an input.
>>>
>>> IIRC, in our discussions it was allowed to improve a decoration
>>> if the condition associated with the property was satisfied.
>>
>> According to 8.8.6/25, this is not allowed. (And I am perfectly fine
>> with it not being allowed. I think it is the only way of defining it
>> correctly.)
>
> No, the implementation can use additional knowledge to provide a
> different decoration. See the last example of 8.8.3, for instance.
>
>> Just to clear any potential misunderstanding, I was not saying that
>> empty is only allowed to have the trv decoration. What I was saying is
>> that the emp decoration is redundant with the trv decoration: there is
>> no situation that I can think of where empty_emp could not be encoded by
>> empty_trv, and since nonempty_emp does not make sense, that does not
>> leave any purposeful meaning for decoration emp.
>
> 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". As Guillaume said (8 Feb 2013, at 06:05)
> Either the implementation knows that the point function being computed
> is not defined and it returns empty_emp or empty_ill, or it does not and
> it returns [0,0]_trv or any superset. Any other behavior is meaningless.
Guillaume's point (maybe written tongue in cheek) seems equally unsatisfactory that x*x might actually be x*y:
On 13 Feb 2013, at 10:05, Guillaume Melquiond wrote:
> Le lundi 11 février 2013 à 03:07 +0100, Vincent Lefevre a écrit :
>> Because when considering decorations (and only in this case), reasoning
>> is based on the *point functions*, not their interval version. The point
>> function is here f(x) = sqrt(-x*x-1).
>
> You do not know that! Who said that the point function was f(x) =
> sqrt(-x*x-1)? Is there anything in the motion that prevents the point
> function from being f(x,y) = sqrt(-x*y-1)? In that case, the domain is
> definitely not empty.
>
> Do not forget about this fundamental principle of modern programming
> languages, "referential transparency"...
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 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.
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.
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?
- In particular what about sqrt(-a[i]*a[j]-1) where it
cannot be determined statically whether i and j are equal?
But IMO these are to do with language semantics, and not our business.
Anyone willing to propose (*) with (**) as a motion? Anyone able to shoot it down in flames?
John Pryce