Re: Empty interval representations & Motion 13...
> From: "Nate Hayes" <nh@xxxxxxxxxxxxxxxxx>
> To: "John Pryce" <j.d.pryce@xxxxxxxxxxxx>,
> "P1788" <stds-1788@xxxxxxxxxxxxxxxxx>
> Subject: Re: Empty interval representations & Motion 13...
> Date: Tue, 4 May 2010 08:38:34 -0500
>
> John Pryce wrote:
> > Nate, Dan, P1788
> >
> > On 4 May 2010, at 07:32, Nate Hayes wrote:
> >> Nate Hayes wrote:
> >>> John Pryce wrote:
> >>>> Dan & P1788
> >>>>
> >>>> . . .
> >>>>
>
> > 2.
> > The set-theory definition of "aa strictLess bb" is open to debate,
> > but I am taking it to be the same as Vincent's "aa lessEqual bb" with
> > <= replaced by <.
> >
> > It then gives the same as "lessEqual" when aa or bb or both is/are
> > empty.
> >
> > In particular it gives
> > empty strictLess empty
> > is true, disagreeing with Nate's C++ guide. Nate, what does the guide
> > give as its definition of strictLess?
>
> The definition, literally, is:
>
> X strictLess Y :=
> ( X \not Empty ) and
> ( Y \not Empty ) and
> ( all x \in X )( exists y \in Y ) x < y and
> ( all y \in Y )( exists x \in X ) x < y
In all but one case the first two terms in this
formula are not necessary as the predicate as a
whole cannot be true unless there exist points
in both X & Y.
The exception is empty strictLess empty which is
made false by this construction & true without it.
>
> it then gives explicit endpoint-programming formula:
>
> X strictLess Y :=
> ( X \not Empty ) and
> ( Y \not Empty ) and ( inf(x) < inf(y) ) and ( sup(x) < sup(y) )
But if this is your TRUE formulation, I can see
why you might need to put the otherwise redundant
terms in the first predicate.
I have no guide, no principle, no intuition to
tell me which is correct so I don't know.
Dan
>
> The definitions for lessEqual are quite different, and there is a specific
> mention that empty lessEqual empty is supposed to be true.
>
> Although by the given definitions these results are perfectly logical,
> personally I find them to be counter-intuitive.
>
> Nate
>