Functions as types or the "Hoare logic" of functional dependencies

TL;DR

This paper introduces an algebraic framework that treats data dependencies as types, enabling type checking and query optimization in databases, and relates it to logical systems like Hoare logic for program analysis.

Contribution

It presents a novel algebraic approach to data dependencies as types, unifying database theory with programming logic for improved type checking and optimization.

Findings

Algebraic treatment of data dependencies as types enhances database query analysis.

The approach aligns with logical systems like Hoare logic for program correctness.

Potential for automated deduction systems to improve database operation verification.

Abstract

Inspired by the trend on unifying theories of programming, this paper shows how the algebraic treatment of standard data dependency theory equips relational data with functional types and an associated type system which is useful for type checking database operations and for query optimization. Such a typed approach to database programming is then shown to be of the same family as other programming logics such as eg. Hoare logic or that of strongest invariant functions which has been used in the analysis of while statements. The prospect of using automated deduction systems such as Prover9 for type-checking and query optimization on top of such an algebraic approach is considered.