Re: about emp (was: Motion 42: NO)
Vincent, P1788
On 7 Feb 2013, at 13:50, Vincent Lefevre wrote:
> On 2013-02-06 22:07:15 +0100, Guillaume Melquiond wrote:
>> - Finally, the emp decoration seems superfluous to me. There is no point
>> in decorating a nonempty interval with an emp decoration (except maybe
>> for wreaking havoc in an interval library), so the emp decoration could
>> just as well be removed. An empty interval would then be decorated with
>> trv when it does not designate a NaI.
>
> IIRC, there can be problems with that. For instance, take zz = g(yy)
> where yy is Empty. Since g is defined and continuous on the empty set
> yy, one can return zz = (Empty,dac). But now assume that yy wasn't
> actually an input, but yy = f(xx) for some non-empty xx, e.g.
> sqrt([-2,-1]). So, one would get:
>
> (g o f)(xx) = (Empty,dac)
>
> which is wrong.
I am looking for arguments against Guillaume's proposal to abolish emp, but this isn't one IMO.
I stick to my view (draft 6.2 §8.8.4) that any yy_dy "must tell the truth about some conceivable evaluation of a function f over a box xx", and that def, hence dac and com, should include "xx is nonempty" in their definition. Hence Empty_d with d in {def, dac, com} is a contradiction.
So with Guillaume's proposal, a (non-NaI) Empty can only be decorated trv.
John P