Cartesian institutions with evidence: Data and system modelling with diagrammatic constraints and generalized sketches

TL;DR

This paper develops a formal framework for data constraints using category theory, focusing on diagrammatic constraints and their transformations across data schemas, enhancing safety assurance and interoperability.

Contribution

It introduces a generalized sketch framework within finitely complete categories to model data schemas and constraints, analyzing their transformation laws during schema evolution.

Findings

Formalizes data constraints using category theory and sketches.

Analyzes transformation laws of satisfaction relations during schema changes.

Provides a mathematical foundation for data interoperability and safety assurance.

Abstract

Data constraints are fundamental for practical data modelling, and a verifiable conformance of a data instance to a safety-critical constraint (satisfaction relation) is a corner-stone of safety assurance. Diagrammatic constraints are important as both a theoretical concepts and a practically convenient device. The paper shows that basic formal constraint management can well be developed within a finitely complete category (hence the reference to Cartesianity in the title). In the data modelling context, objects of such a category can be thought of as graphs, while their morphisms play two roles: of data instances and (when being additionally labelled) of constraints. Specifically, a generalized sketch $S$ consists of a graph $G_S$ and a set of constraints $C_S$ declared over $G_S$, and appears as a pattern for typical data schemas (in databases, XML, and UML class diagrams). Interoperability of data modelling frameworks (and tools based on them) very much depends on the laws regulating the transformation of satisfaction relations between data instances and schemas when the schema graph changes: then constraints are translated co- whereas instances contra-variantly. Investigation of this transformation pattern is the main mathematical subject of the paper