Dilian Gurov: Cartesian decomposition of n-ary relations: An exercise in fixed point theory

Recently I worked with Minko Markov on the problem of decomposing n-ary relations as the Cartesian product of smaller relations, essentially partitioning the set of attributes of the original relation into pairwise independent sets (intuitively meaning that there is no correlation between the sets of attributes). The problem arose from the domain of verification of software families (where each individual SW product consists of a collection of artefacts) by reusing the verification results as much a possible in order to avoid the individual verification of every single product of the family.

After attacking the problem from different angles we finally found that the story becomes clean and elegant when presenting it in terms of the lattice of attribute partitions, and fixed points of a basic transformation on this lattice. Several of the definitions and theorems we had worked out became redundant, due to the well-known Knaster-Tarski fixed point theorem for lattices. In particular, the theorem guarantees the existence of a least fixed point for monotone transformers (eliminating the need to define separately what we are looking for, namely a maximal decomposition), and gives an iterative construction to compute this fixed point (by starting from the bottom of the lattice and iteratively applying the transformer until stabilization).

I believe the talk to be of instructional (and aesthetic) value to graduate students that want to learn a bit about fixed points in computer science. I plan to give the talk following the above "story", and using the white board only.