Representing Relational Databases in a Logical Framework
@kohlhase @twiesing
There is a very elegant embedding of relational databases into MMT.
- We write a theory D that declares all the basic datatypes (integers, string, products, etc.) of the database language.
- A table schema is represented as a theory S with meta-theory D. The constants of S correspond to the columns of the table.
- Local consistency conditions (which are often omitted in relational databases) are represented as axioms in S.
- A table entry in S is represented as a morphism S -> D, i.e., entries are records whose fields are given by S.
- A join is represented as a pushout. For example, the join of S with S' where the field f of S should be equal to the field f' of S', is the pushout of {f} -include-> S and {f} -{f=f'}-> S'. The entries of the join are the set of universal morphisms out of the pushout for every pair (e,e') of entries for which the respective diagram commutes.
- A database view providing a table S backed by a table T are MMT morphisms m is represented as a morphism S -> T. As a special case, include morphisms represent the selection of some columns from a table. The entries of the view are the morphisms m;e for all entries e of T.
- A writable view providing S backed by T allows modifying an entry of T if the change can be propagated back to the corresponding entry of T. If T is a declared theory, this is possible if m is a renaming/inclusion. If m is a view or join, this is more complicated.
The goal of this topic is to
- work out the details of the above
- investigate the propagation of changes along writable views in general
- determine how these representations can be used to provide added value to database applications
In particular, we could represent the schema of a database in MMT (as sets of theories and views). The entries would be stored in an actual database. The theory D can use high-level datatypes, which MMT's codecs translate to the concrete types of the database. Queries (like joins, selections, and views) can be formulated in MMT and translated to relational queries; conversely, entries can be translated back to MMT views.