Building a Consensus: A Rectangle Covering Problem

Abstract

The other day, over a very pleasant lunch in the restaurant of Oxford's recently renovated Ashmolean Museum, Oege de Moor gave me a problem about rectangles. The problem is explained more fully later, but roughly speaking one is given a finite set of rectangles RS and a rectangle R completely covered by RS. The task is to construct a single rectangle covering R among the elements of a larger set of rectangles associated with RS, called the saturation of RS. The saturation of RS is the closure of RS under so-called consensus operations, a term coined in (Quine, 1959), in which two rectangles are combined in two distinct ways to form new rectangles. The rectangle problem is a simplified version of containment-checking, a crucial component in a type inference algorithm for Datalog programs (Schäfer & de Moor, 2010). 19 In the Schäfer-de Moor algorithm the problem is generalised to cubes in n-space rather than rectangles in two-space, the components of each cube are given by propositional formulae rather than by intervals on the real line, and certain equality and inhabitation constraints are taken into account. Oege felt that the central proof, Lemma 15 in (Schäfer & de Moor, 2010), deserved to be simplified so he posed the rectangle problem as a special case. This pearl was composed in response to the challenge.