Thread Links Date Links
Thread Prev Thread Next Thread Index Date Prev Date Next Date Index

Motion 26: NO



Though I like the theory, I currently vote NO.
Here are some comments.

In Theorem 5.2, I would prefer the notation (ff,d) = f(xx) because one
gets 2 data: ff and d. Writing ff_d = f(xx) is a bit misleading w.r.t.
usual notation with indices.

5.8.4 and 5.8.5 are very complicated and difficult to understand, and
without better explanations, I'm not convinced that they are correct.
Moreover 5.8.5 seems to be wrong on the following example:
  * xx = [-2,-1]
  * yy = Empty
  * f(x,y) = sqrt(x) + y
One gets:
  * The decoration of xx from domain(xx) is bnd.
  * The decoration of yy from domain(yy) is emp.
  * For zz = sqrt((xx,bnd)), p_emp(sqrt,xx) holds, so that one chooses
    e = emp. Thus d = min{emp,bnd} = emp.
  * For zz + yy, if one applies (Eval3) directly as said in 5.8.5:
    one chooses e = con. Then d = min{con,emp,emp} = emp. But since
    the box (xx,yy) is empty, according to (8), the decoration of
    f(xx,yy) must be > emp, leading to a contradiction. So, it seems
    that (Eval1) was necessary here.

5.8.6 (Examples) should have examples with empty intervals as input.
It may be better to give examples earlier, in order to illustrate the
contents of 5.8.4 and 5.8.5 and make them easier to understand.

The two orders (containment order and propagation order) look quite
artificial: the former because of the reversal of the containment
signs and the latter because the order seems more or less arbitrary.
The motion should explain the reason of these choices, more precisely
the choice of the set D and the propagation order. Actually this is
related to the following questions:

What about practical use (something important for a standard)?
Is there any algorithm that would be based on this motion,
showing that each of the properties can be useful?

Is it possible to define piecewise functions in this theory?

-- 
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 / Arénaire project (LIP, ENS-Lyon)