December 8
Michael Benedikt,
Oxford University
Nested Data, Views, and Gaifman Coordinatization
I will begin with an overview of how implicit definition, and variations of Beth's definability theorem, arise in relational databases, particularly in the context of view rewriting.
We then turn from relational databases to nested relational databases, a model of hierarchical data - 'objects' - where tables can contain tuples whose components are again tables. There is a standard transformation language for this data model, the Nested Relational Calculus (NRC). We show that a variant of Gaifman's coordinatization theorem plays a role in lieu of Beth's theorem, allowing one to generate NRC transformations from several kinds of implicit specifications. We discuss how to generate transformations effectively from specifications, which requires the development of proof-theoretic methods for implicit definability over nested sets.
This is joint work with Ceclia Pradic and Christoph Wernhard.