A relation-algebraic approach to the “Hoare logic” of functional dependencies

• This paper expresses functional dependencies using binary relation algebra.
• It shows that functional dependency calculus is similar to Hoare logic.
• This is based on reasoning about the degree of injectivity of a relation.
• Applications are given for query optimization and lexicographic sorting.
• The optimizations are obtained by point-free calculations.

Abstract algebra has the power to unify seemingly disparate theories once they are encoded into the same abstract formalism. This paper shows how a relation-algebraic rendering of both database dependency theory and Hoare programming logic purports one such unification, in spite of the latter being an algorithmic theory and the former a data theory.The approach equips relational data with functional types and an associated type system which is useful for database operation type checking and optimization.The prospect of a generic, unified approach to both programming and data theories on top of libraries already available in automated deduction systems is envisaged.