Stratification criteria and rewriting techniques for checking chase termination

The Chase is a fixpoint algorithm enforcing satisfaction of data dependencies in databases. Its execution involves the insertion of tuples with possible null values and the changing of null values which can be made equal to constants or other null values. Since the chase fixpoint evaluation could be non-terminating, in recent years the problem know as chase termination has been investigated. It consists in the detection of sufficient conditions, derived from the structural analysis of dependencies, guaranteeing that the chase fixpoint terminates independently from the database instance. Several criteria introducing sufficient conditions for chase termination have been recently proposed [9,8, 13, 12]. The aim of this paper is to present more general criteria and techniques for chase termination. We first present extensions of the well-known stratification conditions and introduce a new criterion, called local stratification (LS), which generalizes both super-weak acyclicity and stratification-based criteria (including the class of constraints which are inductively restricted). Next the paper presents a rewriting algorithm, whose structure is similar to the one presented in [10]; the algorithm takes as input a set of tuple generating dependencies and produces as output an equivalent set of dependencies and a boolean value stating whether a sort of cyclicity has been detected. The output set, obtained by adorning the input set of constraints, allows us to perform a more accurate analysis of the structural properties of constraints and to further enlarge the class of tuple generating dependencies for which chase termination is guaranteed, whereas the checking of acyclicity allows us to introduce the class of acyclic constraints (AC), which generalizes LS and guarantees chase termination.