Re: Major inconsistencies in Table 10.7 with unbounded intervals
Vincent
On 13 Feb 2015, at 12:10, Vincent Lefevre <vincent@xxxxxxxxxx> wrote:
> It seems that Table 10.7 has inconsistencies with unbounded intervals.
> For instance, consider a = [-inf,0] and b = [-inf,1]. What would the
> state be?
>
> It seems to work if the sets are compactified (i.e. by including -inf
> and +inf, only for the overlap(a,b) operation).
I think you are right, and it is a bit shameful we didn't pick this up before.
In fact:
- The "bound specification" is always OK, because it implicitly compactifies.
- The "set specification" breaks down when two bounds that may be infinite
are tested for equality, namely
starts, finishes, finishedBy, startedBy.
The "shrink to a point" situation can't happen when a bound is infinite.
- The cases
meets and metBy
are OK, because the bounds being tested must be finite.
If people agree that Vincent's suggestion solves the problem, I suggest to add to the paragraph "The “set” and “bound” columns in Table 10.7..." (p39/14) a sentence saying the sets are compactified in the relevant cases. Vincent, will you provide the text?
However is there another solution? Suppose we change the set definition of "starts" from
exists_a forall_b a\le b (aa has a lower bound for bb)
exists_b forall_a b\le a (bb has a lower bound for aa)
exists_b forall_a a<b (bb has a strict upper bound for aa)
by switching the quantifiers of the first two phrases, to
forall_b exists_a a\le b (bb has NO strict lower bound for aa)
forall_a exists_b b\le a (aa has NO strict lower bound for bb)
exists_b forall_a a<b (bb has a strict upper bound for aa)
and similarly for the other three offenders. Does that work? Maybe some help from a theorem-prover package would be useful. Nathalie?
John Pryce