Entity Modelling

www.entitymodelling.org - entity modelling introduced from first principles - relational database design theory and practice - dependent type theory

The mathematics of dependent types, category theory and entity modelling

The mathematical notions of (a) Contextual Categories and (b) Generalised Algebraic Theories encapsulate the idea of types dependent on contexts which in turn are constructed from types1,2 . Now types of things are equally concepts and (c) Entity Modelling as described here is about modelling the types of things of interest in a particular situation or or as part of a particular endeavour (the chosen perspective); in an entity model, composition relationships model dependencies between types of things. (a), (b) and (c) are therefore closely related. An introduction to types that vary (aka dependent types) is given here: TypesThatVary.pdf.

Two mathematical papers follow. Firstly, here are some relatively recent notes on the generalised algebraic theory of contextual categories: theGATofCCs.pdf. I wrote these after having learnt of the definition of C-system given by Vladimir Voevodsky.

Secondly, here is a recent write up of some work that I did at the time of my thesis, basically it is a variation on contextual categories — in brief, meta-GAT algebras are to a contexual category as a clones are to Lawvere theories. I wrote these notes suspecting, as was subsequently confirmed, that Voevodsky was producing a paper describing similar structures to my meta-GAT algebras (he calls them B-systems): MetaGAT and MetaGAT algebras.pdf.

One of my ongoing projects is to produce confluent rewriting systems for both of the above theories and to prove equivalence automatically.

Another ongoing project is to find a generalisation of contextual category which explicitly includes conjunctive dependencies such as we find them in entity modelling and as described here in section conjunctive dependencies. So far this has proved elusive. If such can be found then it would give a more practical diagramming approach than contextual categories for the depiction of concepts. A paper I published on this in 19861 called "Formalising the Network and Hierarchical Data Models " is quite a long way off the mark.

1 Cartmell, John. Generalised algebraic theories and contextual categories. PhD thesis, Generalised algebraic theories and contextual categories. University of Oxford, 1978.
2 Cartmell, John. Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32(0):209 - 243, 1986.
3 Cartmell, John. Formalising the network and hierarchical data models - an application of categorical Logic. In Pitt, David and Abramsky, Samson and Poigné, Axel and Rydeheard, David, editor, Category Theory and Computer Programming, volume 240, Lecture Notes in Computer Science, 466-492, Springer Berlin Heidelberg, 1986.