Rachid Echahed

Dominique Duval, Rachid Echahed

This paper introduces sketch-oriented databases, a categorical framework that encodes database paradigms as finite-limit sketches and individual databases and schemas as set-valued models. It illustrates the formalism through graph-oriented paradigms such as quivers, RDF triplestores and property graphs. It also shows how common graph features such as labels, attributes, typing, and paths, are uniformly captured by sketch constructions. Because paths play an important role in queries, we propose inference rules formalized via localizers to compute useful paths lazily; such localizers are also useful for tasks like database type conformance. Finally, the paper introduces stuttering sketches, whose aim is to facilitate modular composition and scalable model growth: stuttering sketches are finite-limit sketches in which relations are specified by a single limit instead of two nested limits, and the paper proves that finite unions of models of a stuttering sketch are pointwise colimits.

Thierry Boy de la Tour, Rachid Echahed

We address the problem of defining graph transformations by the simultaneous application of direct transformations even when these cannot be applied independently of each other. An algebraic approach is adopted, with production rules of the form $L\xleftarrow{l}K \xleftarrow{i} I \xrightarrow{r} R$, called weak spans. A parallel coherent transformation is introduced and shown to be a conservative extension of the interleaving semantics of parallel independent direct transformations. A categorical construction of finitely attributed structures is proposed, in which parallel coherent transformations can be built in a natural way. These notions are introduced and illustrated on detailed examples.

Jon Haël Brenas, Rachid Echahed, Martin Strecker

We consider a dynamic extension of the description logic $\mathcal{SROIQ}$. This means that interpretations could evolve thanks to some actions such as addition and/or deletion of an element (respectively, a pair of elements) of a concept (respectively, of a role). The obtained logic is called $\mathcal{SROIQ}$ with explicit substitutions and is written $\mathcal{SROIQ^σ}$. Substitution is not treated as meta-operation that is carried out immediately, but the operation of substitution may be delayed, so that sub-formulae of $\mathcal{SROIQ}^σ$ are of the form $Φσ$, where $Φ$ is a $\mathcal{SROIQ}$ formula and $σ$ is a substitution which encodes changes of concepts and roles. In this paper, we particularly prove that the satisfiability problem of $\mathcal{SROIQ}^σ$ is decidable.

Dominique Duval, Rachid Echahed, Frederic Prost et al.

Copying, or cloning, is a basic operation used in the specification of many applications in computer science. However, when dealing with complex structures, like graphs, cloning is not a straightforward operation since a copy of a single vertex may involve (implicitly)copying many edges. Therefore, most graph transformation approaches forbid the possibility of cloning. We tackle this problem by providing a framework for graph transformations with cloning. We use attributed graphs and allow rules to change attributes. These two features (cloning/changing attributes) together give rise to a powerful formal specification approach. In order to handle different kinds of graphs and attributes, we first define the notion of attributed structures in an abstract way. Then we generalise the sesqui-pushout approach of graph transformation in the proposed general framework and give appropriate conditions under which attributed structures can be transformed. Finally, we instantiate our general framework with different examples, showing that many structures can be handled and that the proposed framework allows one to specify complex operations in a natural way.