Martin Glauer
email: martin.glauer@ovgu.de

Till Mossakowski
email: till.mossakowski@ovgu.de

Institutions for SQL Database Schemas and Datasets

Keywords: databases, SQL, category theory, institutions, queries, derived signature morphisms

Databases and the query language SQL play a major role in modern applications. In this paper we present an institution-based formalisation of relational databases that uses structures close to those used in SQL. This is the essential difference to other category-theoretical formalisations of databases, which often depart quite far from the SQL standard. We also study SQL queries, using institutional monads, and prove cocompleteness and amalgamation results for the institution.

Introduction

Database techniques have a long tradition in computer science and build the foundation for numerous modern applications. The Structured Query Language (SQL) [11] forms the fundamental specification for most state-of-the-art query languages for many database systems. 1 Near to all applications that rely on databases use some query language that conforms to the SQL specification, e.g. MySQL or PostgreSQL. This central role made SQL an essential building block of modern database technology that can not be replaced by other languages easily. Thus, formal approaches towards databases should focus this existing standard rather than develop a rivalling query language.

The diversity and heterogeneity of data needed for one specific application raises the need for frictionless interaction and migration between different database schemas. The growing role of Linked Open Data underlines this need. As a result there this a vast landscape of formal approaches towards databases and data migration, including many category-theoretical approaches. The relational make-up of many database schemas makes it natural to model them as categories and yields the intuitive notion of a schema merge as pushouts of functors. In [START_REF] Schultz | Algebraic model management: A survey[END_REF][START_REF] Schultz | Algebraic data integration[END_REF][START_REF] Schultz | Algebraic databases[END_REF] tables are represented as categories and values and relations between tables are functors. The Functorial Query Language yields functionalities to query those structures. A similar approach towards schema integration was defined for the first time in an institutional setting in [START_REF] Alagić | A model theory for generic schema management[END_REF]. Institutions were defined in [START_REF] Goguen | Institutions: Abstract model theory for specification and programming[END_REF] as a framework to cover the vast, heterogeneous landscape of logical formalisms used in computer science. The benefits of a categorical or institutional formalisation are 1) better tools for database structuring, 2) database integration can be achieved via colimits and 3) the possibility of heterogeneous integration of databases with logical languages.

However, previous approaches to category-theoretic formalisation of databases do not well integrate with actual practice of SQL databases. The reasons are that the defined structures are not close to actual relational database structures, the logic is not three-valued as in SQL 2 , data tables cannot contain duplicates, the operators are not exactly those of SQL, and more (see also [START_REF] Schultz | Algebraic model management: A survey[END_REF] for differences between algebraic and relational databases). Therefore, in this work, we aim at formalising an SQL institution that comes as close as possible to the SQL standard. This means there should be a simple and obvious correspondence between SQL database schemas and theories in the institution. This is particularly important for tool support via the Heterogeneous tool set (Hets) [START_REF] Mossakowski | The Heterogeneous Tool Set[END_REF], which provides a software interface for institutions. Only with an institution supporting SQL directly, Hets can read in standard SQL database schemas. If needed, these can then be translated to other institutions. The formalisation presented in this paper can be seen a first step towards institution based logical reasoning on relational databases and their heterogeneous integration with logical theories. For example, in [START_REF] Schorlemmer | Institutionalising ontology-based semantic integration[END_REF], using institutions, (a simplified form of) a database schema is heterogeneously integrated with an ontology formulated in the description logic OWL, via a first-order theory playing the role of a bridge theory. Our work will enable the use of real-world SQL database schemas in such heterogeneous integration scenarios.

An Institution for Databases

There is a vast landscape of different logics with varying expressiveness, complexity and purpose. Yet, most logics define syntactical entities like signatures (vocabularies) and sentences, as well as concepts of model and satisfaction (of a sentence in a model). Goguen et al defined institutions in [START_REF] Goguen | Institutions: Abstract model theory for specification and programming[END_REF] as an overarching, abstract framework that covers all those concepts and thus integrates them into a common structure.

M | σ |= I Σ ϕ ⇔ M |= I Σ σ(ϕ) .
Definition 2. A semi-institution (Sign, Mod) (called specification frame in [START_REF] Ehrig | Functorial theory of parameterized specifications in a general specification framework[END_REF]) consists of a signature category Sign and a model functor Mod I : (Sign I ) op → Cat (that is, it is an institution without sentences and satisfaction relation).

In this section we will define our institution for relational SQL databases. The general structure is as follows: Each object of the signature category defines the schema of a relational database (e.g. tables, their columns and sorts) as well as the building blocks for expressions (i.e. function and predicate symbols). Sentences represent constraints on these tables (e.g. foreign key constraints) that the data in the database must conform to. The data stored in the database are objects of the model category and morphisms amongst these models represent multiset inclusion. Finally, the satisfaction relation checks whether the data the database (i.e. a model) conforms to a specified constraint (i.e. a sentence). As a guidance all parts of the institution will be explained using the following example tables for persons and employees. Both tables feature a primary key that is an integer. The employee table contains a foreign key reference to the person table, with an according constraint (i.e. the pid of an employee always must be the id of a person). Moreover, the employee table contains a check constraint ensuring that the salary of an employee cannot negative. The database schema describes the general structure of a database. It includes information about all tables in the database, which columns belong to a specific table and their respective datatype. Information about the structure of a database is expressed in the Data Definition Language (DDL). Many basic components (e.g. datatypes, operators) of a database are fixed by the underlying database system. Similarly, the SQL Institution is parameterised over (DΣ, DM ) consisting of a datatype signature DΣ, which is a many-sorted first-order signature DΣ = (S DΣ , F DΣ ) such that An extension for the database PostgreSQL (which also features geometrical datatypes, for geo databases) might look as follows: spec P o s t g r e s q l _ d a t a t y p e s = Mysql_datatypes then sorts Point , Line , Polygon . . .

Both signatures can be interpreted with a model in a standard way, following the SQL conventions for datatypes and their built-in operations.

For a given pair (DΣ, DM ) of a data type signature and a data type model, we now define an institution SQL(DΣ, DM ) as follows.

A signature in SQL(DΣ, DM ) defines the tables the database contains as well as the corresponding columns and their datatypes.

Definition 3 (Signatures). An object Σ of the category of signatures Sign consists of:

a set of table names (or short: tables)

T Σ , -for each table t ∈ T Σ , a set col Σ (t) of columns, -a function τ (•, •) : {(t, c)|t ∈ T Σ , c ∈ col Σ (t)} → S DΣ
assigning sorts (of the datatype signature) to columns in tables, and for each table t ∈ T Σ , a primary key pk Σ (t) ⊆ col Σ (t). Note pk Σ (t) = ∅ is possible, which expresses, in SQL terms, the absence of a primary key.

We include primary keys into signatures (instead of considering them to be sentences) because for each table there may be at most one primary key.

Definition 4 (Signature Morphisms

Σ (σ T (t)) = σ col,t (pk Σ (t)) if pk Σ (t) = ∅ Example 3.
A signature Σ for the tables shown in Example 1 is as follows:

-T Σ = {Employee, Person} -col Σ (Employee) = {id, salary, pid} -col Σ (Person) = {id, fname, lname} -τ Σ (Employee, .) = {id → Int, salary → Int, pid → Int} -τ Σ (Person, .) = {id → Int, fname → Text, lname → Text} -pk Σ (Person) = {id} -pk Σ (Employee) = {id}
The database schema described above yields means to structure data in tables with little limitations regarding the actual content of the data. In order to ensure data integrity, the SQL defines several types of constraints that may be placed on a table. The sentences of the presented institution formulate the most common types of constraints (NOT NULL, UNIQUE, FOREIGN KEY and CHECK) specified in the SQL standard.

Definition 5 (Sentences). Given a signature Σ, a sentence ϕ t is a constraint on a table t ∈ T Σ of one of the following forms:

-A non-null constraint notnull(t.c) (c ∈ col(t)) -A unique constraint un(t.c 1 , . . . , t.c n ) (c 1 , . . . , c n ∈ col(t)) -A foreign-key constraint fk((t.c 1 , u.d 1 ), . . . , (t.c n , u.d n )) for some a table u ∈ T Σ and c i ∈ col(t), d i ∈ col(u) for i = 1, . . . , n -A check constraint ck t (ϕ)
, where ϕ is a term of sort Bool over the signature DΣ (extended with logical connectives ¬, ∨, ∧ as operations on Bool) and variables from the set V ar(t) = {t.c | t ∈ col(t)}.

Definition 6 (Sentence Translation). Given a signature morphism

σ : Σ → Σ , a constraint ϕ t on a table t ∈ T Σ is translated along σ to σ(ϕ t ) depending on its structure -σ(un(t.c 1 , . . . , t.c n )) = un(σ T (t).σ col,t (c 1 ), . . . , σ T (t).σ col,t (c n )) -σ(fk((t.c 1 , u.d 1 ), . . . , (t.c n , u.d n ))) = fk( (σ T (t).σ col,t (c 1 ), σ T (u).σ col,t (d 1 )), • • • (σ T (t).σ col,t (c n ), σ T (u).σ col,t (d n ))) -σ(ck t (ϕ)
) is obtained by mapping all variable names along σ, i.e. the variable c.t is replaced with σ col,t (c).σ T (t).

Example 4. Primary keys are already part of the signature. Thus, there are only two constraints remaining in Example 1 that can be formulated as sentences:

-The foreign key linking Employees to Persons fk((Employee.pid,Person.id))

-The constraint that the salary of an employee must not be negative ck t (Employee.salary >= 0)

The signature fixes the structural make-up of the database and its tables. A model represents the data that may be stored in a database w.r.t. to the existing tables, columns and their datatypes. Note that in the interpretation of a table in a model, the same row may appear several times. Thus, tables are interpreted as multisets (also called bags) of rows. The use of multisets may seem overly complicated, because normalised databases cannot have duplicate rows. However, note that not all databases are normalised, and moreover duplicate rows can easily occur within views generated by queries.

For a set X, let ℘ multi (X) be the set of finite multisets over X. A finite multiset B ∈ ℘ multi (X) can be understood as a map B : X → N such that B(x) > 0 only for finitely many x ∈ X. For x ∈ X and B ∈ ℘ multi (X), let B#x be the multiplicity of x in B. We write x ∈ B for the fact that B#x > 0. Moreover, we use the abbreviation

∃!x ∈ B. ϕ(x) for ϕ(x) B#x = 1
i.e. there exists a unique x in B satisfying ϕ(x), and this x has multiplicity 1. Furthermore, addition on finite multiset is defined element-wise:

(B 1 + B 2 )#x = B 1 #x + B 2 #x.

Finally, inclusion of multisets is defined as

A ⊆ B iff for all x ∈ X, A#x ≤ B#x.

Definition 7 (Models). Given a signature Σ, an object of the model category Mod(Σ) is a function mapping tables to multisets of functions that map columns to elements of the datatype model, formally

M : t ∈ T Σ → ℘ multi (c ∈ col(t) → DM τ (t,c) ), such that for each t ∈ T Σ with pk Σ (t) = {c 1 , . . . , c n } = ∅ -r(c i ) = null DM for each row r ∈ M (t) and i = 1, . . . , n, and -for all rows r 1 ∈ M (t), ∃!r 2 ∈ M (t). r 1 (c 1 ) = r 2 (c 1 ) ∧ • • • ∧ r 1 (c n ) = r 2 (c n )
Note that in presence of the satisfaction relation introduced below, these conditions could be rephrased as

-M |= {notnull(t.c 1 ), . . . , notnull(t.c n )} -M |= un(t.c 1 , . . . , t.c n )
Morphisms in the category of models represent inclusion of data multisets.

Definition 8 (Model Morphisms). Given a signature Σ, the model category Mod(Σ) is a partially ordered set, where

M 1 ≤ M 2 iff for each t ∈ T Σ , M 1 (t) ⊆ M 2 (t).

Definition 9 (Model Reducts). Given a signature morphism

σ : Σ → Σ and a Σ -model M and a table t ∈ T Σ , a row r : (c ∈ col(σ T (t))) → DM τ (σ T (t),c ) ) can be reduced to a row r | σ : (c ∈ col(t)) → DM τ (t,c) ) by defining r | σ (c) = r (σ col,t (c)) for c ∈ col Σ (t). Then M | σ , the reduction of M against σ, is defined by ∀t ∈ T Σ , M | σ (t)#r = r |σ=r M (σ T (t))#r ( 1
)
for all r : (c ∈ col(t)) → DM τ (t,c) ). Note that M | σ (t)#r = 0 in case there is no r ∈ M (σ T (t)) with r | σ = r.
From M satisfying the primary key and not-null constraints of Σ , it is straightforward to see that M | σ satisfies those of Σ.

It is easily seen that reducts preserve the partial order on models; hence they are functorial.

∨ T U F T T T T U T U U F T U F ∧ T U F T T U F U U U F F F F F ¬ T F U U F T
-M |= Σ notnull(t.c) iff r(c) = null DM for each row r ∈ M (t) -M |= Σ un(t.c 1 , . . . , t.c n ) iff for all rows r 1 ∈ M (t), ∃!r 2 ∈ M (t). r 1 (c 1 ) = r 2 (c 1 ) ∧ • • • ∧ r 1 (c n ) = r 2 (c n ) -M |= Σ fk((t.c 1 , u.d 1 ), . . . , (t.c n , u.d n )) iff for all r 1 ∈ M (t) there is exactly one r 2 ∈ M (u) such that r 1 (c i ) = r 2 (d i ) for i = 1, ..., n -M |= Σ ck t (ϕ) iff for all r ∈ M (t), ϕ M ν(r) ∈ {T, U}, where for r ∈ M (t), ν(r) is the valuation defined by ν(t.c) = r(c) for all c ∈ col(t).
Here, ϕ DM ν is the evaluation of the term ϕ in the model DM using a valuation ν of the free variables, defined inductively in a standard way, where Boolean connectives are interpreted as shown in Fig. 1

. Note that since ϕ DM ν is of sort Bool, ϕ DM ν ∈ {T, F, U}.
While internally, our institution SQL(DΣ, DM ) uses a three-valued logic for the semantics of integrity constraints, ultimately, it is a two valued logic. This is achieved by considering sentences evaluating to T or U (the designated truth values, in standard many-valued logic terminology [START_REF] Rosser | Many-valued logics[END_REF]) to hold, and considering those evaluating to F as not to hold. (When eliminating U in the first place, one would obtain a different logic.) Further note that for conditions in queries, SQL takes T as the only designated truth value, see Sect. 3 below. This means that queries impose a stricter regime than integrity constraints, which is pragmatically motivated: missing data should not lead to violation of an integrity constraint, while in queries, all mentioned data should be present.

Proposition 1 (Satisfaction condition).

Let σ : Σ → Σ be a signature morphism between two database signatures. For all Σ -models M and Σ-constraints ϕ the following holds:

M | σ |= ϕ ⇔ M |= σ(ϕ)
Proof. Let M be a Σ -model and ϕ a Σ-sentence. The satisfaction follows directly from the fact that model reducts do not alter the data contained in the tables, apart from altering table and column names:

case ϕ = notnull(t.c): M | σ |= notnull(t.c) ⇔ ∀r ∈ M | σ (t) : r(c) = null DM Eq.1 ⇔ ∀r ∈ M (σ T (t)) : r | σ (c) = null DM ⇔ ∀r ∈ M (σ T (t)) : r (σ col,t (c)) = null DM ⇔ M |= σ(notnull(t.c)) case ϕ = un(t.c 1 , . . . , t.c n ): M | σ |= un(t.c 1 , . . . , t.c n ) ⇔ ∀r 1 ∈ M | σ (t) : ∃!r 2 ∈ M | σ (t) : i=1,...,n r 1 (c i ) = r 2 (c i ) Eq.1 ⇔ ∀r 1 ∈ M (σ T (t)) : ∃!r 2 ∈ M (σ T (t)) : i=1,...,n r 1 | σ (c i ) = r 2 | σ (c i ) ⇔ ∀r 1 ∈ M (σ T (t)) : ∃!r 2 ∈ M (σ T (t)) : i=1,...,n r 1 (σ col,t (c i )) = r 2 (σ col,t (c i )) ⇔ M |= σ(un(t.c 1 , . . . , t.c n )) case ϕ = fk((t.c 1 , u.d 1 ), . . . , (t.c n , u.d n )): M | σ |= fk((t.c 1 , u.d 1 ), . . . , (t.c n , u.d n )) ⇔ ∀r ∈ M | σ (t)∃!s ∈ M | σ (u) : ∀i ∈ {1, ..., n} : r(c i ) = s(d i )
Eq.1

⇔ ∀r ∈ M (σ T (t))∃!s ∈ M (σ T (u)) : ∀i ∈ {1, ..., n} : r| σ (c i ) = s| σ (d i ) ⇔ ∀r ∈ M (σ T (t))∃!s ∈ M (σ T (u)) : ∀i ∈ {1, ..., n} : r(σ col,t (c i )) = s(σ col,u (d i )) ⇔ M |= σ(fk((t.c 1 , u.d 1 ), . . . , (t.c n , u.d n ))))
Concerning check constraints, one can prove by induction over ϕ that

ϕ DM ν(r|σ) = σ(ϕ) DM ν(r)
From this, the satisfaction condition for check constraints follows using Eq. 1.

This completes the definition of the institution SQL(DΣ, DM ).

Queries and Views

Our institution SQL(DΣ, DM ) provides a formalisation of SQL database schemas as logical theories in that institution. Now an important feature of SQL is of course the Data Query Language (DQL). Queries cannot be directly represented as logical formulas in the institution, because as an answer, they deliver data and not just logical truth values. Therefore, formalisations for dealing with Prolog-style queries in an institutional setting usually use generalised substitutions [START_REF] Diaconescu | Herbrand theorems in arbitrary institutions[END_REF][START_REF] Diaconescu | Institution-independent Model Theory[END_REF] or derived signature morphisms. The latter are a generalised version of signature morphisms that may map signature symbols not only to other such symbols, but also to complex terms and expressions [START_REF] Mossakowski | What is a derived signature morphism?[END_REF][START_REF] Sannella | Foundations of Algebraic Specification and Formal Software Development[END_REF]. Then Prolog-style queries can be formalised as open sentences and their answer substitutions as derived signature morphisms 4 . However, it turns out that queries in SQL are different from Prolog-style queries. Indeed, SQL queries do not provide answer substitutions that map variables to terms, and so they cannot naturally be extended to a translation of sentences either. This is because SQL queries have a rich syntax, which in general cannot be reflected in SQL sentences (constraints). Instead, SQL queries provide a mapping of databases, i.e. models (see also Table. 1). Compared of abstract substitutions [START_REF] Diaconescu | Herbrand theorems in arbitrary institutions[END_REF][START_REF] Diaconescu | Institution-independent Model Theory[END_REF], the syntactic half of the structure is missing. This means we would need to use abstract semi-substitutions. However, we follow a slightly different path. Namely we use Kleisli morphisms in an institutional monad as an institution-independent formalisation of derived signature morphisms. Queries can then be formalised as such Kleisli morphisms, and materialised views (answer to queries) are reducts against these. Moreover, Kleisli composition gives a means to compose queries, which is also called query unfolding in database terminology [START_REF] Doan | Principles of Data Integration[END_REF].

query answer

Prolog-style open sentence derived signature morphism database-style derived signature morphism reduct against derived signature morphism Table 1. Different types of queries

The notion of institutional monad [START_REF] Mossakowski | What is a derived signature morphism?[END_REF] has been introduced for formalising the notion of derived signature morphism in an arbitrary institution; we weaken it here to the notion of semi-institutional monad, based on the notion of institution semi-morphism. We first recall the latter. Institution semi-morphisms relate two institutions by relating their signatures and models, while sentences are not related. This is useful if the institutions are semantically related, but differ too much in their sentences to have a full institution morphism between them.

Definition 11 ([10]

). Given institutions I and J , an institution semimorphism µ = (Φ, β) : I -→ J consists of a functor Φ : Sign I -→ Sign J and a natural transformation β : Mod I -→ Φ op ; Mod J .

Definition 12 ([5]). Given two institution semi-morphisms µ

1 , µ 2 : I -→ J with µ i = (Φ i , β i ), a (discrete) institution semi-morphism modification τ : µ 1 -→ µ 2 is a natural transformation τ : Φ 1 -→ Φ 2 such that Φ op 1 ; Mod J Φ op 2 ; Mod J τ op * Mod J o o Mod I β1 e e β2 9 9
commutes.

Definition 13 (Semi-institutional monad). Let I be an institution. A semi-institutional monad (T, η, µ) consists of -An institution semi-morphism T : I → I -A institution semi-morphism modification η : id → T (the unit of the monad) -A institution semi-morphism modification µ : T T → T (the multiplication of the monad)

such that the usual laws of a monad are satisfied:

T T T T T T = η T T η µ µ T T T T T T T T = µ T T µ µ µ
The semi-institutional monad for the SQL data query language can now be sketched as follows. The institution semi-morphism (Φ, β) : SQL(DΣ, DM ) → SQL(DΣ, DM ) of the semi-institutional monad maps a signature Σ to Φ(Σ), which extends Σ with tables q, where q is an SQL query over Σ. The tables q are also called views, because the table resulting from a query represents a new view on the database. Resulting in such a view, an SQL query naturally has an associated set of (result) columns (=materialised view), this will act as q's set of columns in Φ(Σ). q will not have a primary key. β maps an SQL-model (aka database) M into the model β Σ (M ) which interprets each query q as the multiset of solutions of q over M . The monad unit η Σ is simply the inclusion of Σ into Φ(Σ). The monad multiplication µ Σ maps queries over queries to normal SQL queries. This is straightforward, because SQL allows to insert queries in positions where tables can occur (after all, views are special forms of tables), which is a form of query composition.

Since SQL is a rich language, the detailed formalisation of the complete SQL query language along the lines sketched above is beyond the scope of this paper. Instead, we concentrate on one particular form of SQL query, involving select, where and join. In a system, information is often distributed amongst multiple tables in order to prevent redundancies. In order to retrieve distributed data multiple tables can be joined into a view, using a query. When employing this restriction on queries, the above sketched semi-institutional monad can be detailed as follows, where the monad action given by the institution semi-morphism is denoted as T = (Φ, β):

-The signature functor Φ : Sign SQL → Sign SQL extends a signature Σ by tables of form

t 1 × • • • × t n | ϕ1,...,ϕ k → c 1 e 1 ,
col(t 1 × • • • × t n | ϕ1,...,ϕ k → c 1 e 1 , . . . , c m e m ) = {c 1 , . . . , c m }.
Sorts of columns are set w.r.t to the column expressions:

τ (t 1 × • • • × t n | ϕ1,...,ϕ k → c 1 e 1 , . . . , c m e m , c i ) = s i
where s i is the result type of e i . β Σ (M ) preserves the models behaviour on tables from Σ, i.e. β Σ (M )(t) = M (t) for t ∈ T Σ . In order to construct the interpretation of the new tables in Φ(Σ), we define e i (r 1 , . . . , r n ) as the evaluation of an expression e i (i = 1, . . . , m) w.r.t. to rows r 1 , . . . , r n , i.e.

e i (r 1 , . . . , r n ) := (λ(c 1 1 , . . . , c 1 m1 , . . . , c n 1 , . . . , c n mn ).t)(r 1 (col(t 1 )), . . . , r n (col(t n ))) Each of the constructed rows has to conform to the constraints specified in ϕ 1 , . . . , ϕ k . This can be easily guaranteed by checking whether the model M r1,...,rm satisfies the set of constraints (ϕ 1 , . . . , ϕ k ) where M r1,...,rn contains just the row r i for each table t i (i = 1, . . . , n) and no data for other tables. For a table

t = t 1 × • • • × t n | ϕ1,...,ϕ k → c 1 e 1 , .
. . , c m e m we construct the dataset as the evaluations of the corresponding column expressions:

β Σ (M )(t) = {r| r(c i ) = e i (r 1 , . . . , r n )(i = 1, . . . , m), r 1 ∈ M (t 1 ), . . . , r n ∈ M (t n ), ϕ j M r 1 ,...,rn ν r(ϕ j ) = T (j = 1, . . . , k)}
Here ν r(ϕj ) is the valuation determined by the unique row r i in table t i , where t i is the table over which ϕ j has been formulated. As stated above (after Def. 10), for constraints in queries, T is the only designated truth value.

η Σ is the inclusion µ Σ maps tables by collapsing an (outer) query over (inner) queries into a simple query. The result is the outer query, modified by substituting λterms for the inner queries into the column variables in λ-terms and check constraints of the outer query, and adding check constraints of the inner queries.

Example where e 1 = λp_id, p_fname, p_lname, e_id, e_salary, e_pid.e_salary e 2 = λp_id, p_fname, p_lname, e_id, e_salary, e_pid.e_fname e 3 = λp_id, p_fname, p_lname, e_id, e_salary, e_pid.e_lname

In the sequel, we work with an arbitrary but fixed semi-institutional monad (T, η, µ) over an institution I (with T = (Φ, β)). We can define several derived notions: Definition 14 (Kleisli semi-institution, adapted from [START_REF] Mossakowski | What is a derived signature morphism?[END_REF]). The Kleisli signature category has a objects I-signatures, and its morphisms

Σ 1 → Σ 2 are I-signature morphisms Σ 1 → Φ(Σ 2 ). Kleisli composition is defined by Σ 1 σ1 / / Φ(Σ 2 ) ; Σ 2 σ2 / / Φ(Σ 3 ) = Σ 1 σ1 / / Φ(Σ 2 ) Φ(σ2) / / Φ(Φ(Σ 3 )) µ Σ 3 / / Φ(Σ 3 )
Model categories are inherited from I. Model reduct against σ :

Σ 1 → Φ(Σ 2
) is given by β Σ2 ; Mod I (σ). This gives a semi-institution in the sense of Def. 2.

Due to the "semi"-nature of the monad, we do not have sentence translations along Kleisli signature morphisms. This reflects the fact that queries use a much more powerful language than constraints, and constraints are not closed under queries.

Queries are just Kleisli signature morphisms: Definition 15 (Query). A query is a signature morphism q : Σ Q → Φ(Σ).

Here, Σ Q typically is a "small" or "singleton" signature. In the case of SQL(DΣ, DM ), Σ Q will typically consist of a single table only, providing a name and column types for the result of the query. The query itself is then given by q(Σ Q ), which singles out one particular query in the space Φ(Σ) of all Σ-queries. The semantics of a query q as above is given by the Kleisli reduct β Σ ; Mod I (q), mapping Σ-models (aka Σ-databases) to Σ Q -models (aka materialised views of signature Σ Q ).

Two queries q 1 , q 2 : Σ Q → Φ(Σ) are equivalent [START_REF] Doan | Principles of Data Integration[END_REF] if their semantics agree, i.e. β Σ ; Mod(q 1 ) = β Σ ; Mod(q 2 ). q 1 is contained in 5Next, we consider composition of queries, also known as query unfolding, which is an important tool for data base integration [START_REF] Doan | Principles of Data Integration[END_REF]. Given two queries q 1 :

q 2 if for each M ∈ Mod(Σ), there is a model monomorphism β Σ (M )| q1 → β Σ (M )| q2 .
Σ Q 1 → Φ(Σ 1 ) and q 2 : Σ Q 2 → Φ(Σ 2 )
, we cannot compose them directly. Rather, we have (assuming the existence of signature coproducts) to assume that the first query is built over the second database enriched with the result of the second query, i.e. that Σ

1 = Σ Q 2 + Σ 2 .
Then we can pair the second query with η and take the Kleisli composition

Σ Q 1 q1 / / Φ(Σ 1 ) ; Σ 1 = Σ 2 + Σ Q 2 [η,q2] / / Φ(Σ 2 )
We can also obtain a semi-substitution from a query. Substitutions have been introduced in [START_REF] Diaconescu | Herbrand theorems in arbitrary institutions[END_REF][START_REF] Diaconescu | Institution-independent Model Theory[END_REF]. They run between variable sets that are represented as signature morphisms (extending a base signature with some constants playing the role of variables). We weaken the notion as follows: Definition 16. Given two signature morphisms ("variable sets")

χ 1 : Σ → Σ 1 and χ 2 : Σ → Σ 2 , a Σ-semi-substitution ψ : χ 1 → χ 2 is a functor Mod(ψ) : Mod(Σ 2 ) → Mod(Σ 1 )
such that the following diagram commutes:

Mod(Σ 1 ) Mod(χ1) & & Mod(Σ 2 ) Mod(χ2) x x Mod(ψ) o o

Mod(Σ)

For a query q : Σ Q → Φ(Σ), we consider the coproduct injection ι 1 : Σ → Σ + Σ Q as "variable set", and define the semi-substitution ψ :

ι 1 → 1 Σ via Mod(ψ) = β Σ ; Mod I (Σ + Σ Q [η Σ ,q] / / Φ(Σ)) .
Commutativity of the above diagram for semi-substitutions is ensured by the modification property of η (see Def. 12).

Another view on (general) Kleisli morphisms is that they correspond to (complex) schema mappings [START_REF] Schultz | Algebraic model management: A survey[END_REF], because they map table names to queries. This means that we can compose schema mappings, and also (via the Kleisli model functor) compute their semantics.

Database Integration via Colimits

The formalisation of SQL databases as an institution allows the use of colimits for database integration.

|I t | = {(i, u) | u ∈ T D(i) , (µ i ) T (u) = t},
i.e. the set of tables that are mapped (by some colimit injection) to t. I t has a morphism m : (i, u 1 ) → (j, u 2 ) whenever m : i → j ∈ I and D(m) T (u 1 ) = u 2 . The diagram functor D t : I t → S DΣ -Set acts on objects as

D t (i, u) = col D(i) (u),
which is S DΣ -sorted using τ D(i) (u, •), and on morphisms as

D t (m : (i, u 1 ) → (j, u 2 )) = D(m) col,u1 : col D(i) (u 1 ) → col D(j) (u 2 )
Let (C t , (θ t (i,u) ) (i,u)∈|It| ) be the colimit of D t in S DΣ -Set (recall that colimits in comma categories are constructed component-wise). Then C t is the sorted set of columns of table t in Σ. The column translation of µ i : D(i) → Σ is given by

(µ i ) col,u = θ (µi) T (u) (i,u) (u ∈ T D(i) ).
Finally, the primary key of C(t) is determined as (µ i ) col,u (pk D(i) (u)) for any (i, u) ∈ |I t | with pk D(i) (u) = ∅. Since any two such (i, u) are connected via a zigzag path in I t , the assumption about spans in I together with preservation of primary keys along signature morphisms ensures that this is independent of the choice of (i, u). This completes the construction of the colimit (Σ, (µ i : D(i) → Σ) i∈|I| ). Its universal property follows from the universal properties of the colimits involved in its construction. Here, signature morphisms are inclusions.

An integration of tables can be achieved using pushouts:

Example 7.

Address(name:string,address:string)

) ) Person(name:string) < < " " Person1(name:string,address:string,dob:date) Birthdate(name:string,dob:date)

5 5
Here, signature morphisms map tables in the unique way and leave columns as they are. If table Person has primary key name, then this is also the primary key in the colimit. However, if Person does not have a primary key, but Birthdate and Address have one consisting of both of their respective columns, then the diagram does not have a colimit, because its primary key cannot be determined.

Since tables in one signature do not interact, the same effect can also be achieved with a coequaliser Example 8. So the coequaliser involves a coequaliser at the level of tables plus a pushout at the level of columns.

Address

The amalgamation property is a major technical assumption in the study of specification semantics [START_REF] Sannella | Specifications in an arbitrary institution[END_REF] and is important in many respects. For example, it allows the computation of normal forms for specifications [START_REF] Borzyszkowski | Generalized interpolation in CASL[END_REF], and it is a prerequisite for good behaviour w.r.t. parameterization [START_REF] Ehrig | Fundamentals of Algebraic Specification[END_REF] and conservative extensions [START_REF] Diaconescu | Logical support for modularisation[END_REF] and for soundness of proof systems for structured specification [START_REF] Mossakowski | A relatively complete calculus for structured heterogeneous specifications[END_REF]. Intuitively, amalgamation of databases is just a rearrangement of the (partially shared) tables.

Definition 17.

A cocone for a diagram in Sign I is called (weakly) amalgamable if it is mapped to a (Weak) limit under Mod I . This can be characterised in more elementary terms as follows: Given a diagram D : I -→ Sign I , a family of models

(M i ) i∈|I| is called D-consistent if M j | D(m) = M i for each m : i -→ j ∈ I.
Then a cocone (Σ, (µ i ) i∈|I| ) over the diagram in D : I -→ Sign I is weakly amalgamable if for each D-consistent family of models (M i ) i∈|I| , there is a Σ-model M with M | µi = M i (i ∈ |I|) (and moreover, an analogous condition holds for model morphisms). In case M is unique with these properties, the cocone is amalgamable.

An institution I admits (weak) finite amalgamation if all finite colimit cocones are (weakly) amalgamable. Proposition 3. For colimit cocones as in Prop. 2, SQL(DΣ, DM ) admits weak finite amalgamation, and if all diagram signatures have a primary key, then also finite amalgamation.

Proof. Let (Σ, (µ i ) i∈|I| ) be a colimit cocone as in Prop. 2. Moreover, let (M i ) i∈|I| a D-consistent family of models. We need to define its amalgamation M ∈ Mod SQL (Σ). Given t ∈ T Σ , consider the diagram D t : I t → S DΣ -Set defined in the proof of Prop. 2. Recall that col Σ (t) is the colimit of this diagram. The carrier sets of the model DM form an S DΣ -sorted set |DM |, and any row is an S DΣ -sorted map into |DM |. Hence, any compatible family of rows (r (i,u) ∈ M i (u)) (i,u)∈|It| is a cocone for D t , and by the colimit property of col Σ (t), it can be amalgamated to a row r : (c ∈ col(t)) → DM τ (t,c) . If all diagram signatures have a primary key, then let M (t)#r = 1 for any such r, and M is the unique amalgamation. If not, then proceed with the following algorithm (working on a copy of (M i ) i∈|I| that is modified):

1. initially, set all multiplicities M (t)#r to 0. 2. Choose a compatible family of rows (r (i,u) ∈ M i (u)) (i,u)∈|It| , and for its amalgamation r, increase M (t)#r by one. 3. Decrease the multiplicities M i (u)#r (i,u) by one. 4. Repeat steps 2 and 3 until all multiplicities M i (u)#r (i,u) are zero. By Eq. 1, all M i (u)#r (i,u) will reach zero simultaneously.

By very general results [START_REF] Goguen | Institutions: Abstract model theory for specification and programming[END_REF][START_REF] Sannella | Foundations of Algebraic Specification and Formal Software Development[END_REF], Props. 2 and 3 carry over from signatures to presentations, i.e. signatures equipped with axioms, e.g. foreign key constraints.

Conclusion

We presented an institutional approach towards a formalisation of relational databases and their integration via colimits and amalgamation. Building on a foundation of a many-sorted first-order structure, the signatures and sentences reflect SQL's Data Description Language, including tables, their columns and various constraints. The models of this institution capture the data that can be stored in those tables. Queries on a database can be formalised as a semiinstitutional monad. Syntactic and semantic components of this institution were designed to closely follow those used in SQL, which allows an easy application of this new formalisation to existing database-related tools.

Many other categorical approaches define a new query language (e.g. FQL [START_REF] Spivak | Relational foundations for functorial data migration[END_REF]). This limits the frictionless application of those approaches in real-world scenarios, as SQL is used in most software solutions that involve database communication. Therefore, we designed the presented institutional formalisation of databases to closely reflect the existing structures from the SQL specification.

Many open questions remain, e.g. whether model reducts have left and right adjoints as in [START_REF] Schultz | Algebraic model management: A survey[END_REF], or whether colimits can be expressed as queries. Also, the existence of colimits in the Kleisli category should be studied, because these correspond to database integrations using queries. Note that by the results of [START_REF] Mossakowski | What is a derived signature morphism?[END_REF], these colimits do not always exist.

Future work should also investigate the manipulation of data by insert and delete statements. Model morphisms could be used to capture a structure similar to those used in a categorical theory of patches [START_REF] Mimram | A categorical theory of patches[END_REF], which may yield a logical framework for version tracking of databases.

Operations that involve multiple tables are present in most database-related application. The introduction of a suitable institutional semi-monad (and its Kleisli morphisms) enhances the presented institution for databases with functionalities such as inner joins that combine multiple tables. Yet, the current formalisation allows only inner joins. Full formalisations of all different types of joins (e.g. left join, outer join) and other principles (e.g. aggregations, unions) are yet to be done. The introduction of other join types can be achieved by introducing multiple join operators with appropriate model interpretations. A similar approach could be chosen for unions. Aggregations will pose a tougher problem. They require an adaption of the notion of reduct of a Kleisli morphism, because a single row in a query result would stem from multiple rows of a single base table.

Institutions were defined as a framework that allows integration of different logics. Similarly, one may define institution comorphisms [START_REF] Goguen | Institution morphisms[END_REF] to different logics (including logics for algebraic databases) and thus open the doors for the vast and powerful landscape of logic reasoning tools. The Heterogeneous tool set (Hets) [START_REF] Mossakowski | The Heterogeneous Tool Set[END_REF] offers functionalities for reasoning and proving not only across logics, but also integrates languages like UML. The integration of the SQL-institution into this tool set can be a step towards a logics-founded approach for model-driven development for databases with automated checks for coherence. Integration of queries could be done by representing Kleisli morphisms6 , implementing their composition as well as checks for query containment and equivalence.

Definition 1 .

 1 An institution I = (Sign I , Sen I , Mod I , |= I ) consists of (i) a category of signatures Sign I and signature morphisms; (ii) a sentence functor Sen I : Sign I → Set (where Set is the category of sets), providing for each signature Σ a set of sentences Sen I (Σ) and for each signature morphism σ : Σ 1 → Σ 2 a sentence translation map Sen I (σ) : Sen I (Σ 1 ) → Sen I (Σ 2 ) (also written σ(-)); (iii) a contra-variant model functor Mod I : (Sign I ) op → Cat (where Cat is the category of categories 3 ), providing for each signature Σ a category of models Mod I (Σ) and for each signature morphism σ : Σ 1 → Σ 2 a model reduct functor Mod I (σ) : Sen I (Σ 2 ) → Sen I (Σ 1 ) (also written -| σ ); and (iv) a family of satisfaction relations |= I Σ ⊆ |Mod I (Σ)|×Sen I (Σ) indexed over Σ ∈ |Sign I |, such that the following satisfaction condition holds for every signature morphism σ : Σ → Σ in Sign I , every sentence ϕ ∈ Sen I (Σ) and for every Σ -model M ∈ |Mod I (Σ )|:

5 .

 5 a(= s ) DM b =      T a = b = null DM F null DM = a = b = null DM U otherwiseExample 2. A many-sorted first order signature for MySQL-datatypes may consist of the following components: logic CASL . FOL = spec Mysql_datatypes = sorts Bit , Bool , Int , Float , Text , Blob . . . ops 0 : Int ; null : Int ; null : Float ; null : Text ; . . . ops __ + __ , __ * __ : Int * Int -> Int ops is_null , is_not_null : Int -> Bool ; . . . ops __ = __ , __ >= __ Int * Int -> Bool ; . . . ops empty : Text -> Bool ; . . .

Fig. 1 .

 1 Fig. 1. Boolean operations in SQL's 3-valued logic

Example 6 .

 6 Coproducts put database tables side by side: Address(name:string,address:string) ) ) Address(name:string,address:string) Birthdate(name:string,dob:date) Birthdate(name:string,dob:date) 5 5

is_null DM is T for null DM , and F otherwise. 4. is_not_null DM is F for null DM , and T otherwise.

  1. there is a sort bool ∈ S DΣ 2. for each sort s ∈ S DΣ there is a constant null : s, unary predicates is_null : s and is_not_null : s, and a binary predicate = s : s × s.

	and of a datatype model DM , which is a DΣ-model such that
	1. DM bool = {T, F, U}. (Note that SQL builds upon a 3-valued logic in order
	do cope with the existence of null-values.)
	2. All operations are strict, i.e. they return null DM (or U, in case of operations
	with result sort bool) if any of the operands is null DM . The only exceptions
	to this rule are is_null and is_not_null.
	3.

). A signature morphism σ : Σ → Σ in the category of signatures Sign consists of -a table translation σ T : T Σ → T Σ , and -a family of column translations σ col,t : col(t) → col (σ T (t)) t∈T Σ , such that types of columns are preserved

	τ Σ (σ T (t), σ col,t (c)) = τ Σ (t, c)
	and for each table t ∈ T Σ , the primary key (if existing) is preserved
	pk

  . . . , c m e m written in SQL notation as SELECT e 1 AS c 1 , . . ., e m AS c m FROM t 1 JOIN . . . JOIN t n WHERE ϕ 1 AND . . . AND ϕ k where t 1 , . . . , t n ∈ T Σ , ϕ 1 , . . . , ϕ k are check constraints with the columns of t 1 , . . . , t n as variables, c 1 , . . . , c m are new column names, and each c i is attached with a λ-expression e i

λ(t 1 .c 1 , . . . , t 1 .c n1 , . . . , t n .c 1 , . . . , t n .c nm ).t that specifies the computation rules for this column depending on all columns of the joined tables. The type of t is called result type of e i . The columns of these tables are given as

  would correspond to the table in the monadPerson × Employee| Employee.pid = Person.id,Employee.salary >= 10000 → salary e 1 , fname e 2 , lname e 3

	5.
	The tables from Example 1. A query
	SELECT Person . salary AS salary ,
	Person . fname AS fname ,
	Person . lname AS lname
	FROM Person JOIN Employee
	ON Employee . pid = Person . id
	WHERE Employee . salary >= 10000;

Proposition 2 .

 2 Consider finite diagram D : I → Sign SQL , where for any span j i / / k in I with j = k and any t ∈ T D(i) , the following holds: D(m) T (t) and D(n) T (t) both have a primary key, then so does t. Then D has a colimit. Proof. Let a finite diagram D : I → Sign SQL with the above property be given. We construct its colimit signature Σ together with colimit injections (µ i : D(i) → Σ) i∈|I| as follows. Let D T be the projection of D to tables and table translations. Then let T Σ be the colimit of D T (in Set), and let (µ i ) T : T D(i) → T Σ (for i ∈ |I|) be the colimit injections. This gives us the table part of the colimit. Concerning the column part, let S DΣ -Set be the category of S DΣ -sorted sets, which is given by the comma category Set ↓ S DΣ . For a table t ∈ T Σ , we construct a diagram of S DΣ -sorted column sets as follows. The index category I t has objects

m o o n

  Here, signature morphisms leave columns as they are. For table Person, at the table level, we have the coequaliser (in Set)

	Person	/ / / / Address, Birthdate	/ / Person
	At the column level, we obtain a pushout
	name:string,address:string = =
		) )
	name:string	name:string,address:string,dob:date 5 5
		! !
	name:string,dob:date
	(name:string,address:string)
	Birthdate(name:string,dob:date) A A A A
	Person → Address
	Person → Birthdate
			& &
	Person(name:string)	Person(name:string,address:string,dob:date)

For big data applications, NoSQL databases play an important role, but even there, also SQL databases are used.

This also means that the subtle difference in the semantics of integrity constraints and that of where conditions in queries cannot be captured. We capture it: see our discussion on designated truth values below.

Strictly speaking, Cat lives in a higher set-theoretic universe, such that it is not member of itself.

This way of formalising queries also has been proposed in an informal annex within the DOL language standard[START_REF]Object Management Group: The distributed ontology, modeling, and specification language (DOL)[END_REF].

For SQL(DΣ, DM ) this means multiset inclusion; and query equivalence is the same as containment in both directions.

Note that the signatures Φ(Σ) are generally infinite and cannot be easily represented, but for a Kleisli morphism, only the mapped symbols need to be represented.


Jens Kosiol
email: kosiolje@mathematik.uni-marburg.de

Lars Fritsche
email: lars.fritsche@es.tu-darmstadt.de

Nebras Nassar
email: nassarn@mathematik.uni-marburg.de

Andy Schürr
email: andy.schuerr@es.tu-darmstadt.de

Gabriele Taentzer
email: taentzer@mathematik.uni-marburg.de

Constructing Constraint-Preserving Interaction Schemes in Adhesive Categories

Keywords: Algebraic Graph Transformation, Interaction Scheme, Graph Constraints, Correctness-by-Construction, Adhesive Categories

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Algebraic graph transformation [ ] has proved to be a suitable formal framework to reason about model transformations [ ]. In application scenarios like model generation and editing or refactoring of models, it is desirable that transformations preserve consistency with respect to a set of integrity constraints. Nested constraints [ ] allow to express first-order properties of graphs and a large subset of constraints formulated in OCL [ ] -a widespread constraint language in modeling -may be translated into those [ , ]. In the context of algebraic graph transformation, the standard approach to ensure the validity of results of transformations with respect to a constraint is to equip transformation rules with suitable application conditions. This approach is elaborated for arbitrarily nested constraints in ℳ-adhesive categories [ ] and has tool support for EMF model transformations [ ]. It comes in two variants: Given a constraint 𝑐 and a rule, one can construct a 𝑐-guaranteeing and a 𝑐-preserving application condition for the rule. The 𝑐-guaranteeing application condition ensures that the rules' application is possible if and only if the constraint 𝑐 is fulfilled afterwards. The 𝑐-preserving one is logically weaker: The constraint 𝑐 is only ensured to be fulfilled after a rule application if it already was before. Though sound from the formal point of view for every constraint, from the practical point of view the results are especially satisfactory in the case of negative constraints, which forbid a certain structure to exist. Then the new application conditions prohibit applications of the rule that would introduce this structure. However, for positive constraints requiring structures to exist, an application of a rule may be prohibited, e.g., because it creates a structure that necessitates another structure to exist that is not created likewise. In this way, frequently the application conditions stemming from positive constraints lead to rules which are applicable only rarely or are even inapplicable at all (see Sect. for a concrete example).

To supplement the approach described above, we develop an alternative construction. Given a positive constraint 𝑐, instead of using application conditions, our idea is to complement the action of a rule in such a way that 𝑐 holds after its application. Our construction works for monotonic rules, i.e., rules which only create structure, and positive atomic constraints. Some instance 𝐺 satisfies a positive atomic constraint -which may be compactly notated as ∀ (𝑃, ∃ 𝐶) where 𝑃 is a subobject of 𝐶 -if for all subobjects of 𝐺 that are isomorphic to 𝑃 there exists a subobject isomorphic to 𝐶 which includes the image of 𝑃 . Positive atomic constraints are highly relevant in practice, e.g., they occur frequently when translating OCL into graph constraints and the application conditions arising from them in the standard approach are often far too restrictive. The crucial idea of our approach is to calculate all possible ways in which the application of a rule 𝑟 may lead to a new match for the premise 𝑃 of a constraint 𝑐 = ∀ (𝑃, ∃ 𝐶). These are the different ways in which an application of 𝑟 may introduce a new violation of 𝑐. They can significantly differ from each other and thus require diverging actions to resolve the would-be introduced violation. Hence, for each such situation we derive a rule that includes 𝑟 as subrule but additionally creates structure that complements the new match for 𝑃 to a new match for 𝐶. All these rules are collected into an interaction scheme [ ] that is constraint-preserving: Applying an interaction scheme means to apply a common subrule -here 𝑟 -once and every other rule from the interaction scheme as often as possible but with fixed partial match given by the match of the common subrule (the common actions are only performed once). In this way, every image of 𝑃 that gets newly created by an application of 𝑟 is complemented to an image of 𝐶 by application of one of the rules of the interaction scheme and the validity of the constraint is preserved. Slightly extending this construction also gives a constraint-guaranteeing interaction scheme, i.e., an interaction scheme that additionally includes rules that "repair" already existing violations.

The original motivation for this research is to continue work from [ ]. There, multi-rules for triple graph grammars (TGGs) [ ] -a formalism for the declar-ative description of consistency relationships between two modeling languages with graph-like representations -have been developed. The exemplary multi-rules in [ ] serve to preserve consistency with (informally described) constraints but were developed "by hand". This has the disadvantage that preservation of the constraint is not ensured by construction and has to be checked on a case-by-case basis. Our work paves the way to automate the design of those multi-rules in a way that guarantees correctness by construction. Our restriction to monotonic rules corresponds to that motivation since TGGs are composed of those.

The main contribution of this paper is the introduction and formalization of constraint-preserving and -guaranteeing interaction schemes in the setting of adhesive categories [ ]. It is organized as follows. In Sect. we illustrate our results with an example. Section recalls relevant background. In Sect. we present our construction of interaction schemes while Sect. points out further possibilities to refine that construction. Section compares to related work before we conclude in Sect. . An extended version of this paper [ ] includes all proofs.

Introductory Example

We adapt the example from [ ] since, in a way, we continue the work of constructing multi-amalgamated rules for triple-graph grammars (TGGs). There, a TGG for co-evolution of a class diagram and a documentation structure is given. We use a simplified version of this example, namely a plain graph grammar. If an instance of that meta-model is to be understood as documentation structure for a class-diagram, it is reasonable, e.g., to expect owned Entries of referenced Docs to be referenced, too. This constraint is expressible as a positive atomic constraint. Doc that is already referenced by another one. Thus, the creatable instances and the order of possible rule applications are severely restricted. As an alternative, we will automatically derive so-called multi-rules like createEntry-multi depicted in Fig.

. Applying it as a so-called interaction scheme with kernel rule createEntry at a Doc still creates an Entry but additionally inserts a reference to this Entry from every Doc that references the chosen Doc. This is equivalent to applying its complement rule (Fig.

) at every possible match with fixed partial match induced by a precedent application of createEntry. Applying, e.g., the rule createEntry at is not applicable at that match, applying the rule createEntry-multi at it as interaction scheme leads to the valid instance depicted in Fig.

Preliminaries

In this section, we present some technical preliminaries. We conduct our work in the framework of adhesive categories [ ]. They have been introduced as a general setting for double pushout rewriting and can be understood as categories where pushouts along monomorphisms behave like pushouts along injective functions in the category of sets and functions. Here, we only recall rules and transformations in adhesive categories with a focus on multi-amalgamation after introducing positive atomic constraints.

To express properties of graphs in a way fitting to the algebraic approach to graph transformation, first graph predicates or graph conditions have been developed (being expressively equivalent to a first-order logic on graphs) and later been generalized to the setting of so-called ℳ-adhesive categories [ , ]. Our approach deals with a small but nonetheless in practice highly important fragment of that logic, namely positive atomic constraints [ ].

Definition (Positive atomic constraint).

In an adhesive category 𝒞, a positive atomic constraint 𝑐 is a monomorphism 𝑝 : 𝑃 ˓→ 𝐶 between two objects. We will write 𝑐 = ∀ (𝑃, ∃ 𝑝 : 𝑃 ˓→ 𝐶) or ∀ (𝑃, ∃ 𝐶) for short for such a constraint. We call 𝑃 the premise and 𝐶 the conclusion of the constraint.

An object 𝐺 satisfies a positive atomic constraint 𝑐, denoted by 𝐺 |= 𝑐, if for every monomorphism 𝑔 : 𝑃 ˓→ 𝐺 there exists a monomorphism 𝑞 : 𝐶 ˓→ 𝐺 such that 𝑔 = 𝑞 ∘ 𝑝.

Positive atomic constraints are the only kind of constraints we consider, so we will just call them constraints when this is not apt to introduce misunderstanding.

Rules are a declarative way to define transformations of objects. They consist of a left-hand side 𝐿, a right-hand side 𝑅, and an interface 𝐾. Informally, in the category of graphs, the application of a rule to a graph 𝐺 means to delete the elements of 𝐿 and create those of 𝑅 while preserving the elements stemming from the interface 𝐾. A match identifies the "location" in 𝐺 where this is done. Formally and more generally in adhesive categories, a transformation can be defined using two pushout diagrams.

Definition ((Monotonic) Rule. Transformation).

Given an adhesive category C, a rule 𝑝 consists of three objects 𝐿, 𝐾, and 𝑅, called left-hand side (LHS), interface, and right-hand side (RHS), and two monomorphisms 𝑙 : 𝐾 ˓→ 𝐿, 𝑟 : 𝐾 ˓→ 𝑅. Its inverse rule is the rule

𝑝 -1 = (𝑅 ←˒ 𝐾 ˓→ 𝐿). A rule 𝑝 = (𝐿 ←˒ 𝐾 ˓→ 𝑅) is called monotonic (or non-deleting) if 𝑙 : 𝐾 ˓→ 𝐿 is an isomorphism.
In that case we just write 𝑟 : 𝐿 ˓→ 𝑅. Given a rule 𝑝 = (𝐿 ←˒ 𝐾 ˓→ 𝑅), an object 𝐺, and a monomorphism 𝑚 : 𝐿 ˓→ 𝐺, called match, a (direct) transformation 𝐺 ⇒ 𝑝,𝑚 𝐻 from 𝐺 to 𝐻 via 𝑝 at match 𝑚 is defined by the diagram to the right where both squares are pushouts.

𝐿 𝐾 𝑅

𝐺 𝐷 𝐻 𝑙 𝑟 𝑚 𝑛

A rule 𝑝 is called applicable at match 𝑚 if the first pushout square above exists, i.e., if 𝑚 ∘ 𝑙 has a pushout complement.

Since we exclusively consider monotonic rules in this paper, we will just call them rules and give the following definition for the monotonic case only. Subrules and their multi-rules have a twofold purpose. First, the application of a rule, then called a multi-rule, may be equivalently split into the application of a subrule followed by one of a complement rule with respect to that subrule. The construction of such a complement rule is not unique; a quite involved one can be found in [ ]. For a simpler one for monotonic rules, also used in [ ], we refer to the extended version of this paper [ ]. An example is displayed in Fig. .  This decomposition of a rule application allows for important extensions in two directions: coordinated parallelism and a for-each like syntax. A subrule may capture the common behavior of several multi-rules and thus serve as a kernel to amalgamate their respective actions into application of a single multi-amalgamated rule. Secondly, often a subrule is intended to be applied once followed by as many applications of the complement rule as possible. Interaction schemes unify both ideas into one concept: An interaction scheme consists of a bundle of multi-rules for the same kernel rule. Its application is defined by applying the kernel rule once and each of the complement rules of the multi-rules as often as possible with the fixed partial match given by application of the kernel rule.

Definition

(Subrule. Multi-rule. Interaction scheme. Application). A subrule or kernel rule 𝑟 0 of a rule 𝑟 1 : 𝐿 1 ˓→ 𝑅 1 is a rule 𝑟 0 : 𝐿 0 ˓→ 𝑅 0 with kernel morphism 𝑠 1 : 𝑟 0 ˓→ 𝑟 1 consisting of the monic components 𝑠 1,𝐿 : 𝐿 0 ˓→ 𝐿 1 and 𝑠 1,𝑅 : 𝑅 0 ˓→ 𝑅 1 such that the arising square in the diagram to the right is a pullback. The rule 𝑟 1 is then called a multi-rule for 𝑟 0 .

𝐿 0 𝑅 0 𝐿 1 𝑅 1 𝑟0 𝑠 1,𝐿 𝑠 1,𝑅

𝑟1

An interaction scheme is a finite set ias = {𝑠 1 , . . . , 𝑠 𝑛 } of kernel morphism from a kernel rule 𝑟 0 to different multi-rules 𝑟 1 : 𝐿 1 ˓→ 𝑅 1 , . . . , 𝑟 𝑛 : 𝐿 𝑛 ˓→ 𝑅 𝑛 of 𝑟 0 . The application of the interaction scheme ias to an object 𝐺 with kernel match 𝑚 0 : 𝐿 0 ˓→ 𝐺 is defined as follows: A maximal matching 𝐽 for ias is computed, i.e., a family of matches (𝑚 𝑗 : 𝐿 𝑗 ˓→ 𝐺) 𝑗∈𝐽 with 𝐿 𝑗 ∈ {𝐿 1 , . . . , 𝐿 𝑛 } for all 𝑗 ∈ 𝐽 that is (i) consistent, i.e., 𝑚 0 = 𝑚 𝑗 ∘ 𝑠 𝑗,𝐿 for all 𝑗 ∈ 𝐽 and (ii) maximal, i.e., no further match for one of the LHSs 𝐿 1 , . . . , 𝐿 𝑛 can be added to the family of matches such that it still is consistent.

Then, the (multi-)amalgamated rule 𝑟 𝑠 : 𝐿 𝑠 ˓→ 𝑅 𝑠 , that is the rule arising by computing the colimits 𝐿 𝑠 of the family of morphisms (𝑠 𝑗,𝐿 ) 𝑗∈𝐽 and 𝑅 𝑠 of the family of morphisms (𝑠 𝑗,𝑅 ) 𝑗∈𝐽 with 𝑟 𝑠 being induced by the universal property of 𝐿 𝑠 , is applied.

Remark . In adhesive categories, for every finite family 𝐽 of matches the colimits exist (as iterated pushouts along monomorphisms), the morphism 𝑟 𝑠 is a monomorphism, and all rules 𝑟 𝑗 are subrules of the resulting multi-amalgamated rule 𝑟 𝑠 [ ]. In practical applications, e.g., when working with finite graph-like structures, this property is automatically fulfilled.

For formalizing our intended construction, we need a way to express the difference between objects in the setting of adhesive categories. The concept of initial pushouts [ ] allows for this.

Definition (Initial pushout).

Given a morphism 𝑒 : 𝐸 → 𝑃 , an initial pushout over 𝑒 is a pushout (0) as in the left square below such that 𝑏 𝑃 is a monomorphism and the pushout (0) factors as a pushout (1) uniquely through every pushout (2) over 𝑒 where 𝑏 ′ 𝑃 is a monomorphism as in the right diagram below. Given an initial pushout (0) over 𝑒, 𝐵 𝑃 is called the boundary object and 𝐶 𝑃 the context object with respect to 𝑒.

𝐵 𝑃 𝐸 (0) 𝐶 𝑃 𝑃 𝑏 𝑃 𝑒 𝑐 𝑃 𝐵 𝑃 𝐴 1 𝐸 (1) (2) 𝐶 𝑃 𝐴 2 𝑃 𝑏 ′ 𝑃 𝑏 * 𝑃 𝑏 𝑃 𝑒 𝑐 * 𝑃 𝑐 𝑃 𝑐 ′

𝑃

In the category of sets, if the morphism 𝑒 : 𝐸 → 𝑃 is injective, the set 𝐵 𝑃 is empty and 𝐶 𝑃 is isomorphic to 𝑃 ∖𝑒(𝐸). In the category of graphs, if 𝑒 is injective, 𝐶 𝑃 is the graph arising by adding to 𝑃 ∖ 𝑒(𝐸) those nodes from 𝐸 necessary to complete it to a graph and 𝐵 𝑃 consists exactly of those boundary nodes. Thus, 𝐵 𝑃 consists of those nodes of 𝐸 which get mapped to a node with an adjacent edge in 𝑃 that has no preimage in 𝐸. Thus, we will often use 𝑃 ∖ 𝐸 instead of 𝐶 𝑃 to denote the context object in an initial pushout over a monomorphism.

Constraint-Preserving Interaction Schemes

In this section, we develop our construction of constraint-preserving and -guaranteeing interaction schemes. We prove the construction to be well-defined, i.e., it results in a family of multi-rules, and present sufficient conditions for the desired preservation property of the arising interaction schemes.

The central idea of the construction of a constraint-preserving interaction scheme is to identify each way in which the application of a rule may introduce a violation of a given positive atomic constraint 𝑐 = ∀ (𝑃, ∃ 𝐶). These are the different ways in which the rule can create a new occurrence of 𝑃 . For each such situation we derive a multi-rule that additionally amends this new 𝑃 to 𝐶. Applying the such arising interaction scheme instead of the original rule preserves the validity of the constraint (if the multi-rules themselves do not introduce new violations again). Slightly extending this strategy additionally provides rules that repair already existing violations of the constraint, i.e., enable to not only preserve but guarantee consistency.

We first introduce compatible rule-constraint intersections to classify the ways in which a rule 𝑟 : 𝐿 ˓→ 𝑅 may introduce an image of the premise 𝑃 of a constraint ∀ (𝑃, ∃ 𝐶). Assuming a transformation 𝐺 ⇒ 𝑟,𝑚 𝐻 to be given, the co-match is an embedding of 𝑅 in 𝐻. If there is an image of 𝑃 in 𝐻, it intersects with that image of 𝑅 in 𝐻 (maybe emptily). This intersection restricts to an intersection between the images of 𝐿 and 𝑃 in 𝐻 as well. Thus, we introduce compatible intersections as monomorphisms 𝜄 : 𝐷 ˓→ 𝐸 where 𝐸 is a subobject of 𝑅 and 𝑃 and 𝐷 is a subobject of 𝐿 and 𝑃 in a compatible way. The intuition is that 𝐷 is that part of 𝑃 already matched by the rule and 𝐸 ∖ 𝐷 is the part the rule's application created anew. This suggests that if 𝜄 is an isomorphism, a situation is captured where the rule only matches some part of an image of 𝑃 without creating a part of it (compare Lemma ). We only need to consider those intersections that actually stem from applications of rules. Thus, calculating all such intersections gives all conceivable different ways in which an application of the rule might introduce a new subobject (isomorphic to) 𝑃 . depicts a compatible rule-constraint intersection for rule createEntry and the constraint PropagationOfEntries. It is the only compatible intersection for them where 𝜄 is not an isomorphism. Only intersecting the node of type Entry from the rule's RHS with the one from the constraint's premise (inducing an empty intersection between the LHS and the premise) leads to a pair of intersections that satisfy the first two properties of Definition but not the third one: It is not possible that an application of createEntry only creates the node of type Entry of an occurrence of the premise but not its corresponding incoming edge of type ownedEntry as this would imply that the edge existed without a target node before the application of the rule createEntry which is not allowed in a graph. In the example above, the node doc is a (in fact the only) boundary element: When deleting 𝐸 from 𝑃 , this node needs to be added to the result again for it to become a graph (so that the edge of type refDoc is not dangling). This signifies that this node must have existed before application of the rule and is one of the places (here even the place) at which 𝐸 and 𝑃 ∖ 𝐸 are glued to receive a complete copy of 𝑃 . Hence, this node needs to be matched by the rule application to create 𝑃 and, thus, is already part of 𝐷, the intersection of 𝐿 and 𝑃 . The next lemma states that this generalizes, i.e., the boundary object 𝐵 𝑃 is always a subobject of 𝐷 and the existence of this inclusion morphism is vital for our construction.

Definition (Compatible rule-constraint intersection

Lemma (Covering of boundary elements).

Let 𝒞 be an adhesive category with initial pushouts, 𝑟 : 𝐿 ˓→ 𝑅 a rule, 𝑐 = ∀ (𝑃, ∃ 𝑝 : 𝑃 ˓→ 𝐶) a constraint in 𝒞, and (𝑑 : 𝐿 ←˒ 𝐷 ˓→ 𝑃, 𝑒 : 𝑅 ←˒ 𝐸 ˓→ 𝑃 ) with monomorphism 𝜄 : 𝐷 ˓→ 𝐸 a compatible rule-constraint intersection. Let 𝐵 𝑃 be the boundary object of the initial pushout over 𝑒 𝑃 : 𝐸 ˓→ 𝑃 . Then there exists a monomorphism 𝑥 : 𝐵 𝑃 ˓→ 𝐷 such that 𝜄∘𝑥 = 𝑏 𝑃 . In particular, 𝐵 𝑃 is a pullback object for the monomorphisms 𝜄 : 𝐷 ˓→ 𝐸 and 𝑏 𝑃 : 𝐵 𝑃 ˓→ 𝐸 (compare Fig. ).

Given a compatible rule-constraint intersection (𝑑, 𝑒), we use it to compute a multi-rule 𝑟 𝑑,𝑒 . Its RHS is just the join of 𝑅 and 𝐶 along 𝐸, thus completing a newly created 𝑃 to 𝐶. The multi-rule 𝑟 𝑑,𝑒 should match exactly in those cases where 𝑟 creates a new 𝑃 by adding 𝐸 ∖ 𝐷 to some already existing structure. Thus, 𝑃 has to exist except for the part 𝐸 ∖ 𝐷 before rule application and the multi-rule needs to match that structure. This is achieved by joining 𝐿 with the join of 𝑃 ∖ 𝐸 and 𝐷 along the boundary object 𝐵 𝑃 .

Construction (Constraint-guaranteeing and constraint-preserving interaction scheme). Let 𝒞 be an adhesive category with initial pushouts,

𝑟 : 𝐿 ˓→ 𝑅 a monotonic rule, and 𝑐 = ∀ (𝑃, ∃ 𝑝 : 𝑃 ˓→ 𝐶) a positive atomic constraint in 𝒞. For each (up to isomorphism) compatible rule-constraint intersection (𝑑 : 𝐿 The constraint-guaranteeing interaction scheme for 𝑟 with respect to 𝑐 consists of the arising multi-rules and is denoted with ias 𝑟,𝑐 . Its restriction ias 𝑝 𝑟,𝑐 consists of those multi-rules stemming from pairs of intersections (𝑑, 𝑒) where 𝜄 : 𝐷 ˓→ 𝐸 is not an isomorphism and is called constraint-preserving interaction scheme.

𝑑 𝐿 ← -˒ 𝐷 𝑑 𝑃 ˓-→ 𝑃, 𝑒 : 𝑅 𝑒 𝑅 ← -˒ 𝐸 𝑒 𝑃 ˓-→ 𝑃 )
Example . Given the rule createEntry and the constraint PropagationOfEntries, the constraint-preserving interaction scheme consists only of the kernel morphism that embeds createEntry into the multi-rule createEntry-multi as depicted in Fig.

. That is because the only possible choice for a compatible rule-constraint intersection that is not an isomorphism is the one presented in Example .

The constraint-guaranteeing interaction scheme additionally contains the multi-rules depicted in Fig. . The intersections from which they are arising are given by the two isomorphisms from the empty graph to itself and from one node of type Doc to itself, respectively. The node of type Doc then might by identified with each of the two nodes of type Doc occurring in the constraint. Remark . We introduced interaction schemes, as usual, as finite sets in Definition . For the construction of the amalgamated rule (Definition and Remark ) it is important that the set 𝐽 is finite -otherwise the colimits might not exist.

The most natural setting to guarantee that both the interaction schemes arising by the above construction and the number of matches in their maximal matchings are finite is that of finitary categories, i.e., categories where every object has only finitely many subobjects. Moreover, in finitary adhesive categories initial pushouts always exist [ , Fact . ] -thus they do not need to be required as additional precondition. But since, for the above construction, the number of compatible rule-constraint intersections is not relevant and the number of matches in a maximal matching might be finite even if the considered interaction scheme is not, we did not restrict ourselves to finitary categories.

Showing that this construction actually leads to multi-rules of the original rule exploits the van Kampen property of the cube in Fig. ; in this way the right front face is a pullback.

Theorem (Well-definedness of construction).

Let 𝒞 be an adhesive category with initial pushouts, 𝑟 : 𝐿 ˓→ 𝑅 a monotonic rule, and 𝑐 = ∀ (𝑃, ∃ 𝑝 : 𝑃 ˓→ 𝐶) a positive atomic constraint in 𝒞. Then for every compatible rule-constraint intersection (𝑑, 𝑒) the rule 𝑟 𝑑,𝑒 : 𝐿 𝑑,𝑒 ˓→ 𝑅 𝑑,𝑒 as introduced in Construction is a multi-rule of 𝑟 and the morphism 𝑟 𝑑,𝑒 is a monomorphism.

The next lemma states that compatible rule-constraint intersections are capable of distinguishing if an application of a rule 𝑟 first enabled a matching of 𝑃 in 𝐻 or if this match already restricts to a match in 𝐺 where 𝐺 ⇒ 𝑟 𝐻.

Lemma (Classification of compatible rule-constraint intersections).

Let 𝒞 be an adhesive category with initial pushouts, 𝑟 : 𝐿 ˓→ 𝑅 a monotonic rule, 𝑐 = ∀ (𝑃, ∃ 𝑝 : 𝑃 ˓→ 𝐶) a positive atomic constraint, and (𝑑 :

𝐿 𝑑 𝐿 ← -˒ 𝐷 𝑑 𝑃 ˓-→ 𝑃, 𝑒 : 𝑅 𝑒 𝑅 ← -˒ 𝐸 𝑒 𝑃
˓-→ 𝑃 ) with morphism 𝜄 : 𝐷 ˓→ 𝐸 a compatible rule-constraint intersection for the rule 𝑟 and the premise 𝑃 of the constraint 𝑐. Let 𝐻 be an object with monomorphisms 𝑛 1 : 𝑅 ˓→ 𝐻 and 𝑚 2 : 𝑃 ˓→ 𝐻 such that the induced square is a pullback and a pushout complement 𝐺 for 𝑛 1 ∘ 𝑟 exists. Then 𝑃 already embeds into 𝐺 in a way compatible to its embedding in 𝐻 if and only if 𝜄 : 𝐷 ˓→ 𝐸 is an isomorphism.

Intuitively, applying the original rule 𝑟 and the complement rules of the constructed interactions scheme afterwards, these complement rules supplement each currently existing image of the premise 𝑃 of the constraint with an image of its conclusion 𝐶. But it may happen that the application of such complement rules introduces new occurrences of 𝑃 which, by nature of our construction, are not supplemented. Consequently, it may happen that after applying the interaction scheme the constraint is violated, nonetheless. The next definition serves to be able to exclude situations like that rigorously and assumes familiarity with the concept of parallel independence [ ]. The subsequent theorem states that this condition of independence is a sufficient (not necessary) condition for the constructed interaction schemes to preserve (guarantee) consistency with respect to a constraint. Its proof uses this independence to show that occurrences of 𝑃 must stem from application of 𝑟 or have already existed before. Then one needs to check that each such situation is covered by a multi-rule which is done by showing the arising intersections to be compatible (see Definition ).

Definition (Complementable).

Given a monotonic rule 𝑟 : 𝐿 ˓→ 𝑅 and a positive atomic constraint 𝑐 = ∀ (𝑃, ∃ 𝐶), 𝑟 is called (strongly) complementable with respect to 𝑐 if for every multi-rule 𝑟 𝑑,𝑒 : 𝐿 𝑑,𝑒 ˓→ 𝑅 𝑑,𝑒 from the interaction scheme 𝑖𝑎𝑠 𝑝 𝑟,𝑐 (𝑖𝑎𝑠 𝑟,𝑐 ) the inverse of its complement rule and the constant rule 𝑃 ˓→ 𝑃 are parallel independent.

Theorem (Guarantee and preservation

Prospects and Future Work

This paper focuses on presenting the general idea behind the construction of constraint-preserving interaction schemes and proving their fundamental property. However, there are a lot of possible refinements and interesting future work:

In adhesive categories with strict initial object ∅, a constraint of the form ∃ 𝐶, which requires 𝐶 to be a subobject of 𝐺 to be valid for an object 𝐺, is semantically equivalent to ∀ (∅, ∃ ∅ ˓→ 𝐶), i.e., preservation or guarantee of those constraints is dealt with in our framework as well.

The general idea presented in this paper may be used for deleting rules 𝑟 = (𝐿 ←˒ 𝐾 ˓→ 𝑅) as long as it is not possible that an application of that rule deletes an occurrence 𝐶 of the relevant constraint ∀ (𝑃, ∃ 𝐶), e.g., always when 𝐿 ∖ 𝐾 and 𝐶 intersect emptily. The construction stays the same, in principle, with 𝐾 playing the role of 𝐿. The difference is that every arising multi-rule gets equipped with left-hand side 𝐿 𝑑,𝑒 arising as pushout of 𝐾 ˓→ 𝐿 and 𝐾 ˓→ 𝐾 𝑑,𝑒 .

The precondition of complementability that comes with Theorem is a severe restriction. There are examples, where this precondition is not met, but where recursively repeating our construction for the computed multi-rules again terminates (with no new multi-rules arising anymore) and where these multi-rules of multi-rules can be equivalently expressed as simple multi-rules of the original rule and the constraint is preserved by that extended interaction scheme. We give an example for this, namely a constraint requiring transitive closure over edges of a certain type, in the extended version of this paper [ ]. Investigating this possibility in more detail is future work.

We plan to further integrate application conditions into our approach. Another topic for future research is to support preservation or guarantee of more than one constraint simultaneously. It would be especially interesting to combine support for positive atomic constraints and negative ones of the form ¬∃ 𝐶, forbidding 𝐶 to be an subobject of 𝐺 to be valid for 𝐺. Our vision is to characterize those combinations of rules and constraints such that it is possible to preserve consistency with the whole set of constraints by incorporating the negative ones as application conditions into the rules and then constructing the preserving interaction schemes to support the positive atomic ones.

Related Work

As already discussed in Sect. and , our work can be seen as a continuation of [ ] and a supplement to [ ]. To the best of our knowledge, we are the first to suggest an automatable construction to alter a rule into an interaction scheme to preserve consistency with respect to a given constraint.

We are aware of two works, both with tool support, allowing for automatic construction of interaction schemes in the context of EMF model transformation, but none of them explicitly aims at preservation of constraints. In [ ], Alshanqiti et al. derive visual contracts from Java programs. They monitor the execution of programs and generate transformation rules describing the behavior of the program. The process supports the generation of interaction schemes. In contrast to our work aiming at preservation of constraints, their derived rules provide an abstract and visual representation of observed behavior.

Kehrer et al. [ ] allow a user to specify examples of how a transformation should (or should not) act and from that infer a rule subsuming the provided examples. Their tool is also able to derive interaction schemes. As above, the aim is not to preserve correctness of an explicitly given constraint, and a generated interaction scheme may or may not happen to do so (depending on the quality of the input of the user) or serve a completely different purpose.

There are two works, [ , ] and [ ], that derive repair programs from (graph) constraints. In both works, given a set of constraints, a set of rules and some control structure are derived such that applying the resulting program to an instance results in an instance satisfying those constraints. In neither case interaction schemes are derived, but by passing of parameters or marking and applying rules as often as possible, the same effects are achieved. The second work is done in the context of (labeled) graphs and supports quite a large class of graph constraints, though support for sets of constraints is limited. The first one is done in the context of EMF models and repairs violations of multiplicities while respecting the in-built constraints of EMF. Moreover, it is implemented [ ].

In [ ], Becker et al. propose a method to design consistency-preserving rulebased refactorings. Given such a refactoring and a constraint, an invariant checker provides the user with minimal counterexamples for situations in which the refactoring does not preserve consistency with respect to the constraint. The user may use this information to redesign the refactoring and iterate over this process. The class of supported constraints is slightly larger than ours (supporting also negative constraint). Refactorings are specified via graph transformation rules and though there is no explicit support for interaction schemes, it is possible to use marking and iterate the application of rules as often as possible, which can have the same effect. If a constraint-preserving specification of a refactoring is achieved, of course, depends on the user.

In [ ], Kehrer et al. automatically derive edit rules from meta-models. Starting with atomic operations, they revise rules such that elementary consistency constraints, necessary to be met for a model to be opened in a typical editor, are preserved on application of those roles. When viewing lower bounds of multiplicities of containment edges as positive atomic constraints and applying our construction to these constraints and their elementary rules for node creation, we receive exactly the rules they are using, too. In this case, however, the resulting rules actually not are multi-rules since the LHSs of the resulting multi-rules are the LHSs of the original rules again.

Conclusion

In the setting of adhesive categories, given a positive atomic constraint and a monotonic rule, we presented a construction of a constraint-preserving (or -guaranteeing) interaction scheme. We showed that our construction is welldefined and gave (sufficient) conditions under which the constraint is preserved (or guaranteed) when applying the resulting interaction schemes. With this approach, we are aiming at being able to replace the computation of constraintpreserving (or -guaranteeing) application conditions for rules in a situation where this has the often undesired effect of severely restricting the applicability of the rule. With our approach we are already able to automate the construction of multi-rules that had to be developed by hand before in [ ]. We pointed at promising directions of research to be able to generalize our construction, to overcome the precondition of complementability that was necessary for our main theorem to hold, and to increase the effectiveness of our method in practice.

  Fig. . Meta-model for documentation structures The meta-model in Fig. is a blueprint for simple documentation structures. They consist of Docs owning Entries. Moreover, Docs reference Docs and Entries. Figure presents a grammar allowing to create instances of the meta-model. Black elements have to exist for a rule to be applicable and green elements (additionally marked with ++) are newly created upon application. The rules allow for creation of a new Doc, creation of an Entry to an existing Doc, and insertion of the references, respectively.

  Fig. . Monotonic rules to create documentation structures

  Fig. . Constraint PropagationOfEntries

  Fig. . Rule createEntry with negative application condition (the crossed-out red elements are forbidden to exist)

  .

  Fig. . Example for an instance graph

Fig. .

 . Fig. . Construction of the multi-rule 𝑟 𝑑,𝑒

  Fig. . Compatible rule-constraint intersection for rule createEntry and constraint PropagationOfEntries (node names indicate the morphisms)

  Fig. . Additional multi-rules contained in the constraint-guaranteeing interaction scheme of rule createEntry and constraint PropagationOfEntries

  ). Let 𝒞 be an adhesive category, 𝑟 : 𝐿 ˓→ 𝑅 a monotonic rule, and 𝑐 = ∀ (𝑃, ∃ 𝐶) a positive atomic constraint in 𝒞. A compatible rule-constraint intersection for 𝑟 and 𝑐 is a pair of spans of monomorphisms 𝑑 : 𝐿

	𝑑 𝐿 ← -˒ 𝐷 monomorphism 𝜄 : 𝐷 ˓→ 𝐸 such that (compare Fig. ) 𝑑 𝑃 ˓-→ 𝑃 and 𝑒 : 𝑅	𝑒 𝑅 ← -˒ 𝐸	𝑒 𝑃 ˓-→ 𝑃 with
								𝐵𝑃								𝑥	𝐵𝑃
			𝑑 𝐿		𝐷						𝑑 𝐿		𝐷	𝑃 ∖ 𝐸
	𝐿	𝑟	(1) 𝑚1 𝑒 𝑅	𝐺	𝐸	𝜄	(4) 𝑏 𝑃 𝑑 𝑃 𝑒 𝑃	𝐵𝑃 (3)	𝑃 ∖ 𝐸	𝐿	𝑟	𝐿 𝑑,𝑒	𝐸	𝜄	𝐷 +𝐵 𝑃 𝑃 ∖ 𝐸 𝑝 ∘ 𝑒 𝑃
	𝑅	𝑛1	𝑔	(2)		𝑃	𝑐 𝑃	𝑅	𝑒 𝑅	𝑟 𝑑,𝑒		𝐶
					𝐻	𝑚2					𝑅 𝑑,𝑒
		Fig. . Compatible intersections

. 𝑑 𝑃 = 𝑒 𝑃 ∘ 𝜄, . the square (1) is a pullback, i.e., 𝜄 : 𝐷 ˓→ 𝐸 is a subrule of 𝑟, and . there exists an object 𝐻 and monomorphisms 𝑛 1 : 𝑅 ˓→ 𝐻 and 𝑚 2 : 𝑃 ˓→ 𝐻 such that the arising square (2) is a pullback and a pushout complement 𝐺 for 𝑛 1 ∘ 𝑟 exists (i.e., the rule 𝑟 -1 is applicable at 𝐻 with match 𝑛 1 ).

  with monomorphism 𝜄 : 𝐷 → 𝐸 for 𝑟 and 𝑐, compute the multi-rule 𝑟 𝑑,𝑒 : 𝐿 𝑑,𝑒 ˓→ 𝑅 𝑑,𝑒 in the following way (compare Fig. ): . Compute the LHS 𝐿 𝑑,𝑒 of 𝑟 𝑑,𝑒 as pushout of the morphisms 𝑑 𝐿 ∘ 𝑥 : 𝐵 𝑃 ˓→ 𝐿 and 𝐵 𝑃 ˓→ 𝑃 ∖ 𝐸. . Compute the RHS 𝑅 𝑑,𝑒 of 𝑟 𝑑,𝑒 as pushout of the morphisms 𝑒 𝑅 : 𝐸 ˓→ 𝑅 and 𝑝 ∘ 𝑒 𝑃 : 𝐸 ˓→ 𝐶. . The morphism 𝑟 𝑑,𝑒 : 𝐿 𝑑,𝑒 ˓→ 𝑅 𝑑,𝑒 is induced by the universal property of the pushout computing 𝐿 𝑑,𝑒 .

  ). Let an adhesive category 𝒞 with initial pushouts be given. Let 𝑟 : 𝐿 ˓→ 𝑅 be a monotonic rule, 𝑐 = ∀ (𝑃, ∃ 𝑝 : 𝑃 ˓→ 𝐶) a positive atomic constraint, and 𝑖𝑎𝑠 𝑟,𝑐 and 𝑖𝑎𝑠 𝑝 𝑟,𝑐 the constraint-guaranteeing and constraint-preserving interaction schemes from Construction , respectively. Let 𝑚 1 be a match for 𝑟 at an arbitrary object 𝐺 with maximal matchings 𝐽 and 𝐽 𝑝 for 𝑖𝑎𝑠 𝑟,𝑐 and 𝑖𝑎𝑠 𝑝 𝑟,𝑐 extending 𝑚 1 . . If 𝑟 is strongly complementable with respect to 𝑐 and 𝐽 is finite, then the object 𝐻 arising by application of 𝑖𝑎𝑠 𝑟,𝑐 with that matching satisfies the constraint 𝑐. . If 𝑟 is complementable with respect to 𝑐 and 𝐽 𝑝 is finite then the object 𝐻 arising by application of 𝑖𝑎𝑠 𝑟,𝑐 with that matching satisfies the constraint 𝑐.

Acknowledgments This work was partially funded by the German Research Foundation (DFG), projects "Triple Graph Grammars (TGG) . " and "Generating Development Environments for Modeling Languages". We thank Erhan Leblebici for many helpful remarks.

. Alshanqiti, A., Heckel, R., Kehrer, T.: Inferring visual contracts from Java programs.

Automated Software Engineering ( ), -( ) . Becker, B., Lambers, L., Dyck, J., Birth, S., Giese, H.: