| Thread Links | Date Links | ||||
|---|---|---|---|---|---|
| Thread Prev | Thread Next | Thread Index | Date Prev | Date Next | Date Index |
On 08/17/2011 03:43 AM, Vincent Lefevre wrote: [in: Motion 26: NO]
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.
Note that (as already discussed last year) before any function evaluation with decorations, domain must be called to set the correct initial decorations, which is designed to take care of situations with some empty input. Thus the specification is OK.
Is it possible to define piecewise functions in this theory?
Yes, see example 2 on page 24 of 20110805Decs+FTDIAproof.pdf On 08/17/2011 01:53 PM, Vincent Lefevre wrote: > > Now, see my mail about my vote. There seems to be another > contradiction. And the motion doesn't make it clear that there > are no other ones. > The proof of the FTDIA guarantees that there are no errors (unless the proof is faulty). So please inspect the proof. Arnold Neumaier