Re: Motions 20 and 21 on comparisons
P1788
Juergen and Arnold have recently spoken in favour of simplicity for P1788 comparisons. I agree.
Hence my gut feeling is that Dominique Lohez's BRA theory is elegant, and it should be used to help choose the most appropriate theoretical underpinning, but it should not be made executable (or even pre-process-able) as part of P1788. Therefore I expect to vote NO to the motion in section 5 of her position paper.
As for the motion 21 position paper (M21), I found Marco & Juergen's "overlapping(A,B)" function, whose range is the 13 states, more compelling -- until I looked at it in more detail. I may still be persuaded, but so far it has disappointed my expectations.
We have decided intervals are (a) subsets of the reals, (b) include Empty, and unbounded intervals. In M21 Table 1, which follows Allen's Temporal Logic ideas, A and B are assumed *nonempty*. Also significant for converting our intuitive ideas to quantified formal statements, they are assumed *compact* (closed and bounded).
I had hoped the quantified statements in Table 1 would prove to be "canonical", i.e. in some sense the best, most natural, way to express the given property formally. Then, by applying them when A or B is empty or unbounded, we would get a "canonical generalisation" of the overlapping() function to such A or B.
Alas this isn't so, see details below. I feel in its present form M21 adds neither conceptual simplicity nor practical simplicity, so I expect to vote NO to it as well.
At present I support Ulrich's 7 comparisons, but Arnold's minimalism "I never needed any comparison of intervals except for three" is very attractive.
Regards
John
---------------------
Two points about M21.
---------------------
1. Another symmetry.
Besides the symmetry of "meets" <-> "metBy", etc., there is a second symmetry one can usefully exploit. Namely, in Table 1
- change every < to > and <= to >=;
- change every a to b and vice versa;
- change every resulting u>v to v<u and u>=v to v<=u;
Then M21 Table 1 should be unchanged, modulo using
* logical "and" (\land) is commutative;
* bound variables can be renamed (if one removed all the "primes", whose purpose I still do not see, this would be unnecessary);
* adjacent \forall's commute, and adjacent \exists's commute.
The statement of "meets" is NOT invariant under this, but WOULD be if the middle term (\exists_a \forall_b ...) is changed to (\exists_a \exists_b ...). Namely an equivalent statement is
(\forall_a \forall_b a <= b) \land (\exists_a \exists_b a < b) \land (\exists_a \exists_b a = b) (1)
2. Lack of canonical-ness.
Consider "starts" which in M21 Table 1 is
(\exists_a \forall_b a <= b) \land (\exists_b \forall_a b <= a) \land (\exists_b \forall_a a < b) (2)
Using compactness one can see that, for nonempty compact intervals, this is equivalent to the result of swapping round each (\exists \forall ...), namely
(\forall_b \exists_a a <= b) \land (\forall_a \exists_b b <= a) \land (\forall_a \exists_b a < b) (3)
But these give different results when either A or B is empty. Namely (2) gives false, while (3) gives true.
Marco, Juergen: can you devise forms of the statements in Table 1, that are demonstrably canonical in some natural sense?