Pointfree foundations for (generic) lossless decomposition

Abstract

This report presents a typed, “pointfree” generalization of relational data depen- dency theory expressed not in the standard set-theoretic way, “a` la Codd”, but in the calculus of binary relations which, initiated by De Morgan in the 1860s, is the core of modern algebra of programming. Contrary to the intuition that a binary relation is just a particular case of an n- ary relation, this report shows the effectiveness of the former in “explaining” and reasoning about the latter. Data dependency theory, which is central to relational database design, is addressed in pointfree calculational style instead of reasoning about (sets of) tuples in conventional “implication-first” logic style. It turns out that the theory becomes more general, more structured and sim- pler. Elegant expressions replace lengthy formulæ and easy-to-follow calculations replace pointwise proofs with lots of “· · ·” notation, case analysis and natural lan- guage explanations for “obvious” steps. In particular, attributes are generalized to arbitrary (observation) functions and the principle of lossless decomposition is established for arbitrary such functions. The report concludes by showing how the proposed generalization of data dependency theory paves the way to interesting synergies with other branches of computer science, namely formal modeling and transition systems theory. A number of open topics for research in the field are proposed as future work.