Re: about emp (was: Motion 42: NO)
Le vendredi 08 février 2013 à 03:14 +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.
I don't see how the last example of 8.8.3 is relevant since it talks
about ill, which is the lowest decoration on the propagation order scale
of 8.8.6/26 and thus is not definitely not higher than the decoration of
the inputs.
Let me quote you the relevant parts of 8.8.6:
"w_dw = phi(v_dv)" where v_dv is a box "v_dv_1, ..., v_dv_k"
"w \subseteq Rge(phi | v)" (23)
"p_dv_0(phi,v)" (24)
"dw = min(dv_0,dv_1,...,dv_k)" (25)
"where the minimum is taken with respect to the propagation order dac >
def > trv > emp > ill" (26)
As you can see from (25) above, the decoration dw of the output can
never be improved so that it becomes higher than the decorations
dv_0, ..., dv_k of the inputs.
> > 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.
You are telling me that the implementation knows that the point function
being computed is not defined, but it still bothers to return a nonempty
interval for the interval function? That is just crazy.
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.
Best regards,
Guillaume