Quantification in Double-Categorical Database Schemas

Abstract

Double-categorical database schemas are enriched with universal quantification in the form of right adjoints to substitution. This allows phrasing of the important query, relational division. It is shown that such right adjoints together with suitable tabulators interpret modal operators, provide cartesian closed structure, and, when combined with global cocartesian structure, interpret first-order predicate logic and thus description logic. These structures are applied throughout to querying and optimization. It is seen, for example, that Frobenius reciprocity and Beck-Chevalley hold in any suitably structured double database schema and that these provide pushdown optimization rules. Such optimization rules are thus provably error-free as a property of the schema. Likewise, negation queries are derived from cocartesian and local implication structure.