Notes

2022-11-16

Say you are given two integer ranges [a, b) where a is inclusive and b is exclusive. We would like to write a function that returns whether the two ranges overlap or not. I suggest you try it out before reading the rest of the note.

We are now going to take a viewpoint on the problem which I hope you will find original. Formally, the two intervals overlap if and only if they have (at least) one element in common. So we would like to decide if the following formula holds:

F := ∃x. x ∈ [a₁, b₁( && x ∈ [a₂, b₂( 

However, programming languages are really only subsets of the mathematical language, and most of them won't let us express the existential quantification. What we would like to find is a formula Fx that is equivalent to F but free of constructs that cannot be used in typical programming languages. In particular, Fx must be free of the existential quantifier.

It so happens that this business of eliminating quantifiers is a cornerstone of automated reasoning, where it goes by the unsurprising name of "quantifier elimination". Quite often the idea behind these procedures is to eliminate quantified variables by forming a conjunction of all the implicands. Let's see how this would work on our formula:

0: F := ∃x. x ∈ [a₁, b₁( && x ∈ [a₂, b₂( 
1:  <=> ∃x. (a₁ ≤ x && x < b₁) && (a₂ ≤ x && x < b₂) 
2:  ==> a₁ < b₁ && a₁ < b₂ && a₂ < b₂ && a₂ < b₁

In the last step we considered all pairs (a,b) that sandwich the variable x and formed the inequalities a < b. By construction, and by transitivity of ≤,<, the resulting conjunction is a consequence of our original formula F. In other words, if the two ranges overlap, then the formula on line 2 must hold. Interestingly for integers, and in fact for any total order, the formula on line 2 is equivalent to F (take x to be max(a₁,a₂)). That's one thing we can easily formally verify using HOL Light:

prove
 (`(?(x:int). (a1 <= x /\ x < b1) /\ (a2 <= x /\ x < b2)) <=>
   a1 < b1 /\ a1 < b2 /\ a2 < b2 /\ a2 < b1`,
  EQ_TAC THENL [ARITH_TAC; ALL_TAC] THEN STRIP_TAC THEN
  EXISTS_TAC `max (a1:int) a2` THEN ASM_ARITH_TAC);;

Finally, note that the two conjuncts a₁ < b₁ and a₂ < b₂ are simply saying that the two input ranges are non-empty. If the two ranges are known to be non-empty, then the check degenerates to a₁ < b₂ && a₂ < b₁.