Model Transformations as Free Constructions

Abstract

Hartmut Ehrig was an active researcher in Algebraic Specifications on the one hand and Graph and Model Transformations on the other hand. We demonstrate that these two research fields are closely connected, if we consider generating graph transformations only and use partial algebras instead of total algebras as the underlying category.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

In the last two decades, algebraic graph transformations became popular as a visual specification method for model transformations [8, 9]. There are two major reasons for that: Graph transformations use a graphical notation and are rule-based. A graphical notation is adequate, since many modern modelling techniques are graphical themselves, like for example use case, class, state, or activity diagrams in the Unified Modelling Language UML [15] or process specifications in Business Process Model and Notation BPMN [14]. And a rule-based mechanism avoids explicit control structures. Thus, it opens up the chance for massively parallel transformations.

Model transformations define the mapping between artefacts in possibly different modelling languages. Examples are the mapping of Petri-Nets [20] to State Charts [17], entity relationship diagrams [4] to relational database schemata, XML-schemata [6] to UML class diagrams [15], or arbitrary UML class diagrams to UML class diagrams without symmetric associations and multiple inheritance¹. In all these situations, model transformations are generators: given a model in the source language, the transformation process step by step generates a model in the target language together with a mapping that records the correspondence between the original items in the source to the generated items. Every model generation of this type must satisfy the following general requirements:

 

Termination.:

The generation process terminates for every finite source model.

Uniqueness.:

It produces a uniquely determined target for every source model.²

Persistence.:

The target generation does not change the source model.

 

These three requirements suggest that model transformations can be understood as some sort of (persistent) free construction from a suitable category of source models to a suitable category of target models.³ In this paper, we provide such an interpretation. For this purpose, we do not have to introduce any new definitions or results in terms of theorems and mathematical proofs. Instead, we interpret the available results in a slightly adjusted environment:

• 1. We restrict the well-known algebraic graph transformations to generating rules, i.e. to rules that do not delete or copy any items.

• 2. For the underlying category, we pass from total unary algebras⁴ to arbitrary partial algebras.

The first adjustment leads to a special case of graph transformations, in which the three different algebraic approaches to graph transformation, namely the double-pushout [12], the single-pushout [18], and the sesqui-pushout approach [7] coincide. This is due to the fact that generating rules are simple morphisms $L\overset{r}{\rightarrow }R$. For rules of this format, the direct derivation at a match $m:L\rightarrow G$ is a simple pushout construction of r and m in all three algebraic approaches.

The second adjustment provides a simple encoding of a “growing” correspondence between items in the source model and generated items in the target model, namely by partial mappings that are getting more and more defined within the transformation process.⁵ And, in partial algebras, the generation of elements, the creation of definedness for predicates, and the production of equivalences can be controlled by the same simple mechanism, namely Horn-type formulae.⁶

The rest of the paper is structured as follows. Section 2 introduces a typical example of a model transformation scenario, namely the generation of relational database schemata for object-oriented class diagrams. This example has also been used as a running example in [9].⁷ We show by the example, that even complex model transformation tasks can be modelled by purely generating rules. Section 3 presents the rich theory of generating transformations in a very general categorical framework. Especially, we show in Sect. 3.2 that special generating transformation systems can be interpreted as specifications defining epi-reflective sub-categories of the underlying category. Section 4 presents the basic theory for algebraic specifications of partial algebras as a concrete syntax for transformation rules. In this framework, the sample transformation rules in Sect. 2 obtain a formal semantics, which allows a detailed review of all samples in Sect. 5. The analysis results in substantial improvements that, on the one hand, simplify the transformations from the practical point of view and, on the other hand, turn all of them into free constructions.

2 Sample Transformations – from Classes to Relations

A typical model transformation scenario is the generation of relational schemata for object-oriented class diagrams. In this section, we present transformation rules for all three patterns that are useful to cope with inheritance, namely Single Table Inheritance (ST), Class Table Inheritance (CT), and Concrete Class Table Inheritance (CCT) [13].⁸ The presentation in this section stays on the intuitive level and trusts in the suggestive power of the rule visualisations as graphs with significant icons. Section 4 presents the necessary formal underpinning for a precise semantics which is described in Sect. 5.

Fig. 1.

Handling of classes, attributes, and associations in ST and CT

In this section, we use the same mapping from class diagrams to relational schemata which has been used in Example 3.6 of [9]: Classes are mapped to tables, attributes are mapped to columns, and associations are mapped to junction tables. The corresponding three rules for Single Table Inheritance and Class Table Inheritance are depicted in Fig. 1.⁹ For each class, the rule c2t generates a new table together with a column of numeric type (int) that is marked as key column¹⁰. That a class has been mapped is stored by a (partial) map indicated by the dotted arrow. The rule that generates columns in tables for class attributes is at2co. It is applicable to each attribute the class of which possesses an assigned table, possibly generated by an application of rule c2t. In order to simplify the presentation in this paper, we suppose that the set of base types (int, bool, string etc.) is identical in class models and relational schemata. Finally, associations between classes are mapped to junction tables by rule as2jt. This rule presupposes that the two classes at the ends of the association possess an assigned table with a primary key column each, which have possibly been generated by two applications of rule c2t. To each association, it assigns (dotted arrow) a new table with two columns that both are marked as foreign keys.¹¹ The foreign keys reference the keys that have been found by the match. For the sake of simplicity, we suppose that the type of a foreign key column is implicitly set to the type of the referenced key column.

Fig. 2.

Handling of inheritance in ST and CT

The handling of inheritance relations between classes is different in ST and CT. Figure 2 depicts the corresponding rules i4ST respectively i4CT which have the same left-hand side. The ST-pattern puts a complete inheritance hierarchy into a single table. This effect is implemented by the rule i4ST which merges the tables and keys for the super- and the sub-class of an inheritance relation and maps the relation itself to the same table, compare upper part of Fig. 2.¹² $^{,}$ ¹³

Figure 3 depicts a sample transformation sequence for a small composite class diagram in the single-table scenario. In the first step, rule c2t is applied three times and produces a table with primary key column for each class in the start object. The second step (2 $\times$  at4co) handles the column generation for the two given attributes. The third step (2 $\times$  i4ST) merges the three tables that have been generated before and ensures that there is only one table for the complete inheritance hierarchy. Finally, the fourth step applies the rule as2jt once which adds the junction table for the given association.

Fig. 3.

Sample transformation sequence

The CT-pattern realises inheritance relations by foreign key references. Therefore, the rule i4CT maps an inheritance relation to a foreign key, compare lower part of Fig. 2. The key column of the table for the sub-class is simultaneously used as a foreign key reference to the key of the table for the super-class. This strategy requires coordinated key value generation for all tables “in an inheritance hierarchy” but provides unique object identity for all “parts” of the same object in different tables.

The CCT-pattern generates tables for all concrete classes only and “copies” all inherited attributes and associations to these tables. For the control of this copying process, we need a relation that provides all direct and indirect (transitive) sub-classes for a super-class. Figure 4 shows the rules, that “compute” the reflexive ($\mathtt {t^{0}}$) and transitive ($\mathtt {t^{*}}$) closure of the given inheritance relation ($\mathtt {t^{1}}$).

Fig. 4.

Reflexive/transitive closure of inheritance

Since tables are generated for concrete classes only, we distinguish between abstract and concrete classes. Concrete classes are visualised by the annotation {c}. The rule cc2t in Fig. 5 generates tables and keys in the CCT-pattern.¹⁴

Fig. 5.

Handling of classes, attributes, and associations in CCT

A single attribute can result in several columns, compare rule cat2co in Fig. 5: For an attribute a of type T in class c, a column of type T is generated into every table for a concrete class $c'$ that is a sub-class of c. Thus, the attribute mapping gets indexed by the concrete sub-classes of the owner class of the attribute, compare dotted circle in the visualisation of rule cat2co in Fig. 5.¹⁵

The handling of associations in CCT is even more complex. They cannot be mapped to one foreign key pair, since rows from several “unconnected” tables can be linked by instances of an association in this pattern. For an accurate mapping of the class model semantics, we need orthogonal combinations of foreign keys into the tables for all concrete sub-classes of the association’s source class with foreign keys into the tables for all concrete sub-classes of the association’s target class. The generation of these foreign keys is prepared by rule as2t in Fig. 5. It provides the table for all foreign key columns that are generated for an association.

The rules s2co and t2co in Fig. 6 generate these columns together with the foreign key references to the corresponding tables. These two rules are almost identical; s2co handles all concrete sub-classes of the association’s source and t2co all concrete sub-classes of the association’s target class. As in the case of the attribute mapping, the two mappings that store the correspondence between items in the class model and items in the relational schema are indexed by the concrete sub-class either on the source or the target side, compare the two dotted circles in Fig. 6.

Fig. 6.

Foreign keys for associations in CCT

For an accurate representation of the semantics of the class model, in each row of the “multi-junction table” exactly one foreign key on the source side and exactly one foreign key on the target side must be not null.¹⁶ Thus, we need foreign key columns that allow null values. This sort of foreign keys is depicted by a foreign key icon that is decorated by a $\bot$-symbol in Fig. 6.

3 Generating Transformations and Epi-Reflections

The samples in the preceding section show that model transformations can be specified by generating rules. This special case of transformation rules and transformation systems is presented in this section. We show that there is a rich theory especially wrt. parallel and sequential independence and parallel rule application. We assume an underlying category $\mathcal {C}$ with all small co-limits.¹⁷ $^{,}$ ¹⁸

3.1 Generating Transformation Systems

A rule is a morphism $r:L\rightarrow R$, a match for rule $r:L\rightarrow R$ in object G is a morphism $m:L\rightarrow G$, and a direct transformation with rule r at match m is defined by the pushout $\left( r\left\langle m\right\rangle :G\rightarrow r@m,m\left\langle r\right\rangle :R\rightarrow r@m\right)$ of the pair (r, m).¹⁹ The derivation result is denoted by r@m, the morphisms $r\left\langle m\right\rangle$ is called the trace of the direct derivation, and the morphism $m\left\langle r\right\rangle$ the co-match.²⁰ The result r@m is unique up to isomorphism, since pushouts are.

A transformation system $\mathbb {R}$ is a set of rules. The class $\mathbb {R}^{\rightarrow }$ of $\mathbb {R}$ -transformations is the least class of morphisms which (i) contains all isomorphisms, (ii) contains all traces $r\left\langle m\right\rangle$ for all rules in $r\in \mathbb {R}$ and all suitable matches m, and (iii) is closed under composition. By $\mathbb {R}_{G}^{\rightarrow }=\{h\in \mathbb {R}^{\rightarrow }\mid \mathrm {domain}(h)=G\}$, we denote the $\mathbb {R}$-transformations starting at object G. An object G is final wrt. a transformation system $\mathbb {R}$, if all $h\in \mathbb {R}_{G}^{\rightarrow }$ are isomorphisms.²¹ A system $\mathbb {R}$ is

 

terminating:

if, for any infinite sequence $(t_{i}:G_{i}\rightarrow G_{i+1}\,\in \mathbb {R}^{\rightarrow })_{i\in \mathbb {N}}$, there is $n\in \mathbb {N}$, such that $G_{n}$ is final,

confluent:

if, for any two $\mathbb {R}$-transformation $t_{1}:G\rightarrow H_{1}$ and $t_{2}:G\rightarrow H_{2}$, there are $\mathbb {R}$-transformations $t_{1}':H_{2}\rightarrow K$ and $t_{2}':H_{1}\rightarrow K$, and

functional:

if it is terminating and confluent.

 

Fig. 7.

Strong confluence

Every generating transformation system is strongly confluent as the following argument demonstrates. Consider Fig. 7 which depicts two arbitrary direct derivations with rules $r_{1}$ and $r_{2}$ at matches $m_{1}$ and $m_{2}$ respectively, i.e. sub-diagrams (1) and (2) are pushouts. Composing the original match of one rule with the trace induced by the other rule provides the two residual matches $m_{1}'=r_{2}\left\langle m_{2}\right\rangle \circ m_{1}$ and $m_{2}'=r_{1}\left\langle m_{1}\right\rangle \circ m_{2}$. Applying rule $r_{1}$ at that residual match $m_{1}'$ leads to the pushout $\left( r_{1}\left\langle m_{1}'\right\rangle :r_{2}@m_{2}\rightarrow r_{1}@m_{1}',m_{1}'\left\langle r_{1}\right\rangle :R_{1}\rightarrow r_{1}@m_{1}'\right)$. Since sub-diagram (1) is a pushout and $\left( r_{1}\left\langle m_{1}'\right\rangle \circ r_{2}\left\langle m_{2}\right\rangle \right) \circ m_{1}=r_{1}\left\langle m_{1}'\right\rangle \circ m_{1}'=m_{1}'\left\langle r_{1}\right\rangle \circ r_{1}$, we obtain the unique morphism from $r_{1}@m_{1}$ to $r_{1}@m_{1}'$, which we call $r_{2}\langle m_{2}'\rangle$, satisfying $r_{2}\langle m_{2}'\rangle \circ m_{1}\left\langle r_{1}\right\rangle =m_{1}'\left\langle r_{1}\right\rangle$ and $r_{2}\langle m_{2}'\rangle \circ r_{1}\left\langle m_{1}\right\rangle =r_{1}\left\langle m_{1}'\right\rangle \circ r_{2}\left\langle m_{2}\right\rangle$. Since pushouts decompose, the sub-diagram (3) in Fig. 7 is a pushout, i.e. the pair $\left( r_{2}\langle m_{2}'\rangle ,r_{1}\langle m_{1}'\rangle \right)$ is pushout of $\left( r_{1}\langle m_{1}\rangle ,r_{2}\langle m_{2}\rangle \right)$. Since pushouts compose, the sub-diagrams (2) and (3) together constitute a pushout, i.e. the pair $\left( r_{1}\langle m_{1}'\rangle \circ m_{2}\langle r_{2}\rangle ,r_{2}\langle m_{2}'\rangle \right)$ is pushout of $r_{2}$ and $r_{1}\langle m_{1}\rangle \circ m_{2}=m_{2}'$. Therefore $r_{2}\langle m_{2}'\rangle$ is the trace of the direct derivation with rule $r_{2}$ at match $m_{2}'$ and $r_{1}\langle m_{1}'\rangle \circ m_{2}\langle r_{2}\rangle$ is the co-match $m_{2}'\langle r_{2}\rangle$. Combining these results, we obtain:

$$\begin{aligned} r_{1}@\left( r_{2}\langle m_{2}\rangle \circ m_{1}\right)= & {} r_{2}@\left( r_{1}\langle m_{1}\rangle \circ m_{2}\right) \,\mathrm {and}\\ r_{2}\langle m_{2}'\rangle \circ r_{1}\langle m_{1}\rangle= & {} r_{1}\langle m_{1}'\rangle \circ r_{2}\langle m_{2}\rangle . \end{aligned}$$

Thus, the system is strongly confluent, which implies that it is confluent and, furthermore, that it is functional, iff it is terminating. That every generating transformation system is strongly confluent has some further direct positive consequences, especially wrt. sequential independence and parallel transformations.

Two composable traces $r_{2}\left\langle m_{2}\right\rangle \circ r_{1}\left\langle m_{1}\right\rangle$ are sequentially independent, if there is a match $m_{2}'$ for the rule $r_{2}$ such that $m_{2}=r_{1}\left\langle m_{1}\right\rangle \circ m_{2}'$. In the case of sequential independence, the order of rule application can be interchanged, i.e. $r_{2}\left\langle m_{2}\right\rangle \circ r_{1}\left\langle m_{1}\right\rangle =r_{1}\left\langle r_{2}\left\langle m_{2}'\right\rangle \circ m_{1}\right\rangle \circ r_{2}\left\langle m_{2}'\right\rangle$. The proof for this result is a simple reduction to strong confluence, compare Fig. 7.

Given two rules $r_{1}\!:\!L_{1}\!\rightarrow \!R_{1}$ and $r_{2}\!:\!L_{2}\!\rightarrow \!R_{2}$, we can construct the parallel rule $r_{1}\!\!+\!r_{2}\!:\!L_{1}\!\!+\!\!L_{2}\rightarrow R_{1}\!\!+\!\!R_{2}$ as the unique co-product morphism, where $\left( i_{L_{1}}:L_{1}\rightarrow L_{1}\!\!+\!\!L_{2},\,i_{L_{2}}:L_{2}\rightarrow L_{1}\!\!+\!\!L_{2}\right)$ is the co-product of the rule’s left-hand sides, $\left( i_{R_{1}}:R_{1}\rightarrow R_{1}\!\!+\!\!R_{2},\,i_{R_{2}}:R_{2}\rightarrow R_{1}\!\!+\!\!R_{2}\right)$ is the co-product of the rule’s right-hand sides, and $r_{1}\!+r_{2}$ satisfies $i_{R_{1}}\!\circ \left( r_{1}\!+r_{2}\right) =r_{1}\circ i_{L_{1}}$ and $i_{R_{2}}\!\circ \left( r_{1}\!+r_{2}\right) =r_{2}\circ i_{L_{2}}$. Having two matches $m_{1}$ and $m_{2}$ in the same object for $r_{1}$ and $r_{2}$ respectively, the parallel match $m_{1}\!+m_{2}$ is uniquely determined by $\left( m_{1}\!+m_{2}\right) \circ i_{L_{1}}=m_{1}$ and $\left( m_{1}\!+m_{2}\right) \circ i_{L_{2}}=m_{2}$. Since any co-limit construction of the same situation in any order results in the same object (up to isomorphism), we immediately obtain: $r_{1}\!+r_{2}\left\langle m_{1}\!+m_{2}\right\rangle =r_{2}\langle r_{1}\left\langle m_{1}\right\rangle \circ m_{2}\rangle \circ r_{1}\langle m_{1}\rangle =r_{1}\langle r_{2}\left\langle m_{2}\right\rangle \circ m_{1}\rangle \circ r_{2}\langle m_{2}\rangle .$

This result provides a good (maximal parallel) strategy for the search of a final object for a start object o in a system $\mathbb {R}$, compare Algorithm 1. If the system is terminating, the algorithm finds the final object for all start objects. Unfortunately, most systems are not terminating as the following argument shows.

The application of a rule r at a match m is idempotent, i.e.  $r\left\langle r\left\langle m\right\rangle \circ m\right\rangle$ is an isomorphism, if and only if the trace $r\left\langle m\right\rangle$ is an epimorphism. For the proof, consider Fig. 7 again and let $r_{1}=r_{2}$ as well as $m_{1}=m_{2}$. For the if-part, let $r_{1}\left\langle m_{1}\right\rangle$ as well as $r_{2}\left\langle m_{2}\right\rangle$ be epic. Then $r_{1}\left\langle m_{1}'\right\rangle$, and $r_{2}\left\langle m_{2}'\right\rangle$ are epic, since pushouts preserve epimorphisms. Since pushouts are unique up to isomorphism, there is an isomorphism $i:r_{1}@m_{1}\rightarrow r_{2}@m_{2}$ such that $i\circ r_{1}\left\langle m_{1}\right\rangle =r_{2}\left\langle m_{2}\right\rangle$. Since (3) is pushout, we obtain $j:r_{1}@m_{1}'\rightarrow r_{2}@m_{2}$ with $j\circ r_{1}\left\langle m_{1}'\right\rangle =\mathrm {id}$ and $j\circ r_{2}\left\langle m_{2}'\right\rangle =i$. Thus, $r_{1}\left\langle m_{1}'\right\rangle$ is section and epic, which means that it is isomorphism. For the only-if-part, suppose the application is idempotent, i.e. $r_{1}\left\langle m_{1}'\right\rangle$ is isomorphism and $r_{2}\left\langle m_{2}'\right\rangle$ is isomorphism with inverse morphism j. Then $r_{1}\left\langle m_{1}\right\rangle$ is epic: $h\circ r_{1}\left\langle m_{1}\right\rangle =k\circ r_{1}\left\langle m_{1}\right\rangle$ implies $h\circ r_{1}\left\langle m_{1}\right\rangle =k\circ r_{1}\left\langle m_{1}\right\rangle =k\circ j\circ r_{2}\left\langle m_{2}'\right\rangle \circ r_{1}\left\langle m_{1}\right\rangle =\left( k\circ j\circ r_{1}\left\langle m_{1}'\right\rangle \right) \circ r_{2}\left\langle m_{2}\right\rangle$. Since $\left( r_{1}\left\langle m_{1}'\right\rangle , r_{2}\left\langle m_{2}'\right\rangle \right)$ is pushout, there is unique morphism u such that $u\circ r_{1}\left\langle m_{1}'\right\rangle =k\circ j\circ r_{1}\left\langle m_{1}'\right\rangle$ and, since $r_{1}\left\langle m_{1}'\right\rangle$ is isomorphism, (i) $u=k\circ j$ as well as $u\circ r_{2}\left\langle m_{2}'\right\rangle =h$ and, since j is inverse of $r_{2}\left\langle m_{2}'\right\rangle$, (ii) $h\circ j=u\circ r_{2}\left\langle m_{2}'\right\rangle \circ j=u$. Now (i) and (ii) imply that $h\circ j=k\circ j$ and $h=k$ since j is isomorphism.

Therefore, a single non-epic trace $r\left\langle m\right\rangle$ in a system prevents termination, since the rule r can be applied over and over again at residuals of m with “new results”. Thus, a necessary condition for termination is that all traces in the system are epic. Since pushouts preserve epimorphisms, this property can be guaranteed, if we restrict rules to epimorphisms. Such systems consisting of epic rules only possess another important property as the next sub-section demonstrates.

3.2 Transformation Systems as Epi-Reflections

Every generating transformation system $\mathbb {R}$ in the sense of Sect. 3.1 which consists of epic rules only, can be interpreted as a specification of an epi-reflective sub-category of the underlying category $\mathcal {C}$. This section recapitulates the construction of this epi-reflection.²²

Every epic transformation rule $r:L\twoheadrightarrow R$ can be interpreted as a constructive axiom.²³ It is finite or of Horn-type, if it satisfies the following condition: For every chain of morphisms $\left( m_{i}:O_{i}\rightarrow O_{i+1}\right) _{i\in \mathbb {N}}$ with the co-limit $\left( C,\left( c_{i}:O_{i}\rightarrow C\right) _{i\in \mathbb {N}}\right)$, every morphism $p:L\rightarrow C$ into the co-limit object factors through an object in the chain, i.e. there is $i\in \mathbb {N}$ and a morphism $p_{i}:L\rightarrow O_{i}$ with $c_{i}\circ p_{i}=p$.

A morphism $m:L\rightarrow A$ solves axiom $r:L\twoheadrightarrow R$ in object A, written $m\models r$, if there is morphism $m^{r}:R\rightarrow A$ such that $m^{r}\circ r=m$.²⁴ An object A satisfies axiom r, written $A\models r$, if every morphism $m:L\rightarrow A$ solves r. An object A satisfies a transformation system $\mathbb {R}$ of epic rules, written $A\models \mathbb {R}$, if $A\models r$ for all $r\in \mathbb {R}$. The full sub-category of $\mathcal {C}$ which contains all objects satisfying $\mathbb {R}$ is denoted by $\mathcal {C}_{\mathbb {R}}$. Every such sub-category turns out to be an epi-reflection of $\mathcal {C}$.

Given an object A and a transformation system $\mathbb {R}$ of epic rules,

$$\begin{aligned} A_{\mathbb {R}}=\left\{ A\overset{m}{\longleftarrow }L_{m}\overset{r_{m}}{\longrightarrow }R_{m}\mid \left( r:L\twoheadrightarrow R\right) \in \mathbb {R},m:L\rightarrow A\right\} \end{aligned}$$

denotes the diagram of all occurrences of the left-hand sides of all rules in the transformation system in A.²⁵ In that diagram, for every morphism $m:L\rightarrow A$, the morphism $r_{m}:L_{m}{\rightarrow }R_{m}$ is a “copy” of $r:L\twoheadrightarrow R$. The co-limit of $A_{\mathbb {R}}$ is denoted by $A^{\mathbb {R}}=\left( A^{\mathbb {R}},r_{A}^{*}:A\rightarrow A^{\mathbb {R}},\left( m^{r_{m}}:R_{m}\rightarrow A^{\mathbb {R}}\right) _{\left( A\overset{m}{\longleftarrow }L_{m}\overset{r_{m}}{\longrightarrow }R_{m}\right) \in A_{\mathbb {R}}}\right)$ and we have $r_{A}^{*}\circ m=m^{r_{m}}\circ r_{m}\mathrm {\,\,\,for\,\,all\,}\left( A\overset{m}{\longleftarrow }L_{m}\overset{r_{m}}{\longrightarrow }R_{m}\right) \in A_{\mathbb {R}}$. The morphism $r_{A}^{*}$ is an epimorphism, since the equation (i) $h\circ r_{A}^{*}=k\circ r_{A}^{*}$ implies, for all $\left( A\overset{m}{\longleftarrow }L_{m}\overset{r_{m}}{\longrightarrow }R_{m}\right) \in A_{\mathbb {R}}$, $h\circ m^{r_{m}}\circ r_{m}=h\circ r_{A}^{*}\circ m=k\circ r_{A}^{*}\circ m=k\circ m^{r_{m}}\circ r_{m}$ and, since rules are epimorphisms, (ii) $h\circ m^{r_{m}}=k\circ m^{r_{m}}$. Since $A^{\mathbb {R}}$ is co-limit, (i) and (ii) imply $h=k$.

For given object A and transformation system $\mathbb {R}$, consider $(r_{A_{i}}^{*}: A_{i}\twoheadrightarrow A_{i+1})_{i\in \mathbb {N}}$ as the chain of epimorphisms starting at $A_{1}=A$ and having $A_{i+1}=A_{i}^{\mathbb {R}}$. We denote the co-limit of this chain by $\left( \mathbb {R}(A),\left( a_{i}:A_{i}\twoheadrightarrow \mathbb {R}(A)\right) _{i\in \mathbb {N}}\right)$ and obtain $\left( a_{i+1}\circ r_{A_{i}}^{*}=a_{i}\right) _{i\in \mathbb {N}}.$ All these co-limit morphism are epimorphisms, since all morphisms in the chain are epic.

Furthermore $\mathbb {R}(A)\in \mathcal {C}_{\mathbb {R}}$: Let $\left( r:L\twoheadrightarrow R\right) \in \mathbb {R}$ and let $m:L\rightarrow \mathbb {R}(A)$. Since r is finite, there is $i\in \mathbb {N}$ and $m_{i}:L\rightarrow A_{i}$ with $a_{i}\circ m_{i}=m.$ Since $A_{i+1}=A_{i}^{\mathbb {R}}$, we obtain morphism $m_{i}^{r}:R\rightarrow A_{i+1}$ with $m_{i}^{r}\circ r=r_{A_{i}}^{*}\circ m_{i}.$ Putting all parts together provides: $\left( a_{i+1}\circ m_{i}^{r}\right) \circ r=a_{i+1}\circ r_{A_{i}}^{*}\circ m_{i}=a_{i}\circ m_{i}=m$, such that we found $a_{i+1}\circ m_{i}^{r}$ as the desired morphism $m^{r}:R\rightarrow \mathbb {R}(A)$ with $m^{r}\circ r=m$.

Finally, we get the following result: For a transformation system $\mathbb {R}$ and object A, $a_{1}:A\twoheadrightarrow \mathbb {R}(A)$ is the epi-reflector for A into $\mathcal {C}_{\mathbb {R}}$. The proof is straightforward: If $X\in \mathcal {C}_{\mathbb {R}}$ and $f:A\rightarrow X$ are given, we show by induction on i that there are morphisms $\left( f_{i}:A_{i}\rightarrow X\right) _{i\in \mathbb {N}}$ for all $\left( A_{i}\right) _{i\in \mathbb {N}}$ in the chain $\left( r_{A_{i}}^{*}:A_{i}\twoheadrightarrow A_{i}^{\mathbb {R}}\right) _{i\in \mathbb {N}}$ constructed above. Since $A_{1}=A$, the induction can start with $f_{1}:A_{1}\rightarrow X:=f:A\rightarrow X$. Now let, as induction hypothesis, $f_{i}:A_{i}\rightarrow X$ be given. By construction $A_{i+1}=A_{i}^{\mathbb {R}}$ and $A_{i}^{\mathbb {R}}$ is a co-limit object. Let $\left( r:L\twoheadrightarrow R\right) \in \mathbb {R}$ and $m:L\rightarrow A_{i}$ be a morphism to $A_{i}$, then $f_{i}\circ m:L\rightarrow X$ is a morphism to X. Since $X\models \mathbb {R}$, there is $\left( f_{i}\circ m\right) ^{r}:R\rightarrow X$ with $\left( f_{i}\circ m\right) ^{r}\circ r=f_{i}\circ m$. Thus, $f_{i}$ together with the family of these morphisms are a co-cone for the diagram that has been used to construct $A_{i+1}=A_{i}^{\mathbb {R}}$ from $A_{i}$. Since $A_{i}^{\mathbb {R}}$ is the co-limit of this diagram, we obtain the unique morphism $f_{i+1}:A_{i}^{\mathbb {R}}\rightarrow X$ that satisfies $f_{i+1}\circ r_{A_{i}}^{*}=f_{i}.$ This completes the induction. Now $\left( X,\left( f_{i}:A_{i}\rightarrow X\right) _{i\in \mathbb {N}}\right)$ is a co-cone for the chain $\left( r_{A_{i}}^{*}:A_{i}\twoheadrightarrow A_{i}^{\mathbb {R}}\right) _{i\in \mathbb {N}}$. Since $\mathbb {R}(A)$ is the limit of this chain, we get a morphism $f^{*}:\mathbb {R}(A)\rightarrow X$ that satisfies $\left( f^{*}\circ a_{i}=f_{i}\right) _{i\in \mathbb {N}}$ and, especially, $f^{*}\circ a_{1}=f_{1}=f$. Uniqueness of $f^{*}$ follows from $a_{1}$ being epic.

The co-limit construction for the chain $\left( r_{A_{i}}^{*}:A_{i}\twoheadrightarrow A_{i+1}\right) _{i\in \mathbb {N}}$ is superfluous, if $r_{A_{k}}^{*}$ is an isomorphism for some $k\in \mathbb {N}$. In this case, (i) $A_{k}\in \mathcal {C}_{\mathbb {R}}$, (ii) $r_{k+j}^{*}$ is isomorphism for all $j\in \mathbb {N}$, (iii) $A_{k+1}$ is the limit of the chain, and (iv) the reflector for A is given by $r_{A_{K}}^{*}\circ \,\cdots \,\circ r_{A_{1}}^{*}:A\twoheadrightarrow A_{k+1}$.

The presented approximation of the epi-reflector for a transformation system $\mathbb {R}$ with epic rules is an instance of Algorithm 1. Each approximation step $r_{A}^{*}:A\twoheadrightarrow A^{\mathbb {R}}$ is the trace of an application of a maximal parallel rule, compare diagram $A_{\mathbb {R}}$ above. And the approximation stops after finitely many steps, if and only if the computed object is final wrt. $\mathbb {R}$, i.e. admits isomorphic $\mathbb {R}$-transformations only. Thus, Algorithm 1 calculates the epi-reflector in $\mathcal {C}_{\mathbb {R}}$ for every start object o in a terminating transformation system $\mathbb {R}$ with epic rules.

4 Partial Algebras

Section 3.2 shows that all generating transformation systems in which all rules are epimorphisms induce free constructions and possess useful properties like idempotent rule applications that facilitates the analysis with respect to termination. Unfortunately, all epimorphisms in categories of total algebras, which usually constitute the underlying category for most (graph) transformation frameworks, are surjective, i.e. are just able to generate new equalities. Therefore, frameworks based on total algebras must live with non-epic rules and need an additional machinery for termination, like negative application conditions [16], source consistence derivations in triple graph grammars [2], or artificial translation attributes as in [9], Sect. 7.4. The situation stays simple, if we pass from total to partial algebras [3, 19] as we recapitulate in this section.

A signature $\varSigma =(S,O)$ consists of a set of sorts S and a family of operations $O=(O_{d,c})_{d,c\in S^{*}}$. For $d,c\in S^{*}$ and $f\in O_{d,c}$, d is called the domain specification of f and c is called the co-domain specification. An (algebraic) system $A=\left( A_{S},O^{A}\right)$ for a given signature $\varSigma =(S,O)$ consists of a family $A_{S}=\left( A_{s}\right) _{s\in S}$ of carrier sets, and a family $O^{A}=\left( f^{A}:A^{d}\rightarrow A^{c}\right) _{f\in O_{d,c},d,c\in S^{*}}$ of partial functions.²⁶

This set-up allows functions that provide several results simultaneously, since co-domain specifications are taken from the free monoid over the sort set. Especially, operations with an empty co-domain specification are possible. They are interpreted as predicates in algebraic systems: If $p\in O_{d,\varepsilon }$ for $d\in S^{*}$, the function $p^{A}:A^{d}\rightarrow \{*\}$ maps to the one-element-set in every system A. Thus $p^{A}$ singles out the elements in $A^{d}$ for which it is defined, i.e. for which it is “true”.

Given two systems A and B with respect to the same signature $\varSigma =(S,O)$, a homomorphism $h:A\rightarrow B$, is given by a family of total mappings $h=\left( h_{s}:A_{s}\rightarrow B_{s}\right) _{s\in S}$ such that the following condition is satisfied:²⁷

$$\begin{aligned} \text {}&\forall d,c\in S^{*},f\in O_{d,c},x\in A^{d}\!:\text {if }f^{A}\left( x\right) \text {is defined, }f^{B}\left( h^{d}(x)\right) =h^{c}\left( f^{A}\left( x\right) \right) . \end{aligned}$$

(1)

The condition (1) means for the special case where $f\in O_{d,\epsilon }$, that $f^{B}$ must be defined for $h^{d}(x)$, if $f^{A}$ is defined for x. The concrete value of these functions is irrelevant, since there is a single value in $\{*\}$ and $h^{\varepsilon }=\mathrm {id}_{\{*\}}$. By $\mathsf {Sys}(\varSigma )$, we denote the category of all $\varSigma$-systems and all $\varSigma$-homomorphisms. For every signature $\varSigma$, $\mathsf {Sys}(\varSigma )$ has all small limits and co-limits for each signature $\varSigma$.²⁸

The most important property of $\mathsf {Sys}(\varSigma )$ for the purposes of this paper is, that epimorphisms are not necessarily surjective. This fact can be demonstrated by a simple example using the signature with one sort N and one unary operation s $\,\in O_{\mathtt {N},\mathtt {N}}$, the system $K=\left( K_{\mathtt {N}}=\{x\},\mathtt {s}^{K}=\emptyset \right)$, the system of natural numbers $N=\left( N_{\mathtt {N}}=\mathbb {N}_{0},\mathtt {s}^{N}::i\mapsto i+1\right)$, and the morphism $k:K\rightarrow N$ defined by $x\mapsto 0$. This morphism is epic, since N is generated by the function $\mathtt {s}^{N}$ starting at value $0=k(x)$.²⁹ However, the morphism $k':K\rightarrow N$ with $x\mapsto 1$ is not epic, since the value 0 is not reachable by function calls of $\mathtt {s}^{N}$ starting at 1.³⁰

For a general characterisation of epimorphisms in $\mathsf {Sys}(\varSigma =\left( S,O\right) )$, we need the following closure operations for a family of subsets $\left( B_{s}\subseteq A_{s}\right) _{s\in S}$ of a system A. For all sorts $s\in S$:

$$\begin{aligned}&B_{s}^{0}=B_{s}\cup \left\{ y\in A_{s}\,::\,f^{A}(*)=(p,y,q),\,f\in O_{\epsilon ,v}\right\} \\&B_{s}^{i+1}=B_{s}^{i}\cup \left\{ y\in A_{s}\,::\,f^{A}(x)=(p,y,q),\,f\in O_{w,v},\,x\in \left( B^{i}\right) ^{w},\,|w|\ge 1\right\} \\&B_{s}^{*}=\bigcup _{i\in \mathbb {N}_{0}}B_{s}^{i} \end{aligned}$$

A $\varSigma$ -morphism $h:A\rightarrow B$ is epic, if and only if $h(A)_{s}^{*}=B_{s}$ for all sorts $s\in S$, i.e. if and only if the system B is function-generated starting at the h -image of A in B.³¹ Therefore, a constructive axiom in the sense of Sect. 3.2 in a category $\mathsf {Sys}(\varSigma )$ of algebraic systems can generate new elements in the carriers (as long as they are operation generated), can generate new “truths” by defining new predicate instances, and can generate new equalities if it is not injective.

Constructive axioms are usually presented as finite implications, the elementary building blocks of which are formulae. Given signature $\varSigma =\left( S,O\right)$ and variable set $X=\left( X_{s}\right) {}_{s\in S}$, the set of formulae $\mathcal {F}^{\varSigma ,X}=\left( T_{s}^{\varSigma ,X}\right) _{s\in S}\cup F^{\varSigma ,X}$ is defined by:

$$\begin{aligned} x\in T_{s}^{\varSigma ,X}&\text { if }&x\in X_{s} \end{aligned}$$

(2)

$$\begin{aligned} f_{i}(t)\in T_{s_{i}}^{\varSigma ,X}&\text { if }&f\in O_{w,{s_{1}\ldots s_{k}}},\,t\in \left( T^{\varSigma ,X}\right) ^{w},1\le i\le k,k\ge 1 \end{aligned}$$

(3)

$$\begin{aligned} f(t)\in F^{\varSigma ,X}&\text { if }&f\in O_{w,\epsilon },\,t\in \left( T^{\varSigma ,X}\right) ^{w} \end{aligned}$$

(4)

$$\begin{aligned} l=r\in F^{\varSigma ,X}&\text { if }&l,r\in T_{s}^{\varSigma ,X},s\in S \end{aligned}$$

(5)

A syntactical presentation $P_{X}=\left( X,P\subseteq \mathcal {F}^{\varSigma ,X}\right)$ of a $\varSigma$-system consists of a variable set X and a set of formulae P; it is finite, if X and P are finite sets. The presented system $\mathbf {A}^{P_{X}}=\mathbf {T}^{P_{X}}\!/\!_{\equiv }$ is constructed as follows. The carriers $\left( \mathbf {T}_{s}^{P_{X}}\right) _{s\in S}$ are inductively defined by:

$$\begin{aligned} x\in \mathbf {T}_{s}^{P_{X}}&\mathrm {\,if\,}&x\in {X_{s}}\mathrm {\,or\,}\left( x\in P\mathrm {\,and\,}x\in T_{s}^{\varSigma ,X}\right) \end{aligned}$$

(6)

$$\begin{aligned} f_{j}(x)\in \mathbf {T}_{s_{j}}^{P_{X}}&\mathrm {\,if\,}&f_{i}(x)\in \mathbf {T}_{s_{i}}^{P_{X}},f\in O_{w,s_{1}\dots s_{k}},1\le i,j\le k\end{aligned}$$

(7)

$$\begin{aligned} t_{j}\in \mathbf {T}_{s_{j}}^{P_{X}}&\mathrm {\,if\,}&f_{i}(t_{1},\dots t_{m})\in \mathbf {T}_{s_{i}'}^{P_{X}},f\in O_{s_{1}\dots s_{m},s_{1}'\dots s_{n}'},1\le j\le m,i\le n\end{aligned}$$

(8)

$$\begin{aligned} t_{j}\in \mathbf {T}_{s_{j}}^{P_{X}}&\mathrm {\,if\,}&p(t_{1},\dots t_{k})\in P,p\in O_{s_{1}\dots s_{k},\epsilon },1\le j\le k,k\ge 1\end{aligned}$$

(9)

$$\begin{aligned} l,r\in \mathbf {T}_{s}^{P_{X}}&\mathrm {\,if\,}&\left( l=r\right) \in P\mathrm {\,and\,}l,r\in T_{s}^{\varSigma ,X} \end{aligned}$$

(10)

For an operation $f\in O_{w,s_{1}\dots s_{k}}$ ($k\ge 1$) and a possible argument $x\in \left( \mathbf {T}^{P_{X}}\right) ^{w}$, $f^{\mathbf {T}^{P_{X}}}\!\!(x)=(f_{1}(x),\dots ,f_{k}(x))$, if $f_{j}(x)\in \mathbf {T}_{s_{j}}^{P_{X}}$ for all $1\le j\le k$. For a predicate $p\in O_{w,\epsilon }$ and a possible argument $x\in \left( \mathbf {T}^{P_{X}}\right) ^{w}$, $p^{\mathbf {T}^{P_{X}}}\!\!(x)$ is defined, if $p(x)\in P$. And the quotient relation $\equiv \,\,\subseteq \mathbf {T}^{P_{X}}\!\!\times \mathbf {T}^{P_{X}}$ is the smallest congruence containing $\left\{ (l,r)\mid \left( l=r\right) \in P\right\}$.³²

Since $\mathbf {T}^{P_{X}}$ is closed wrt. sub-terms, compare Eq. (8), and $\equiv :\mathbf {T}^{P_{X}}\rightarrow \mathbf {A}^{P_{X}}$ is surjective, $\mathbf {A}^{P_{X}}$ is generated by X which means, that there is an epimorphism $x^{P_{X}}:X\twoheadrightarrow \mathbf {A}^{P_{X}}$ mapping x to $[x]_{\equiv }$.³³ If we have two syntactical presentations $P_{X}=\left( X,P\subseteq \mathcal {F}^{\varSigma ,X}\right)$ and $C_{X}=\left( X,C\subseteq \mathcal {F}^{\varSigma ,X}\right)$ with the same variable set X such that $P\subseteq C$, then the kernel of $x^{P_{X}}$ is contained in the kernel of $x^{C_{X}}$ and we obtain an epimorphism $_{P_{X\!}C}^{\implies }:\mathbf {A}^{P_{X}}\twoheadrightarrow \mathbf {A}^{C_{X}}$ with $_{P_{X\!}C}^{\implies }\circ \,x^{P_{X}}=x^{C_{X}}$.³⁴

A Horn-type presentation $H=\left( X,P\subseteq C\subseteq \mathcal {F}^{\varSigma ,X}\right)$ of an axiom consists of a finite variable set X, a finite syntactical presentation $C\subseteq \mathcal {F}^{\varSigma ,X}$, called the conclusion, and a sub-presentation P of C, called the premise. The presented axiom is the uniquely determined epimorphism $_{P_{X\!}C}^{\implies }$. A system satisfies H, if it satisfies $_{P_{X\!}C}^{\implies }$, compare Sect. 3.2.

Specification 1 presents a formalisation CM of the class diagrams that we used in Sect. 2, i. e. class diagrams are CM-algebras. As an example, consider the class diagram which is the start object in Fig. 3. It is modelled by the following CM-algebra S: $S_{\mathtt {C}}\!=\!\{1,3,4\}$; $S_{\mathtt {B}}\!=\!\{$ int, bool, string $\}$; $S_{\mathtt {At}}\!=\!\{2,5\}$; $S_{\mathtt {As}}\!=\!\{6\}$; $S_{\mathtt {I}}\!=\!\{7,8\}$; $\mathtt {int}^{S}\!::*\mapsto$  int; $\mathtt {conc}^{S}\!=\!\{1,3,4\}$; $\mathtt {o}_{\mathtt {At}}^{S}\!::2\mapsto 1,5\mapsto 4$; $\mathtt {t}_{\mathtt {At}}^{S}\!::2\mapsto$ bool $,5\mapsto$  string; $\mathtt {o}_{\mathtt {As}}^{S}\!::6\mapsto 3$; $\mathtt {t}_{\mathtt {As}}^{S}\!::6\mapsto 1;$ $\mathtt {sub}^{S}\!::7\mapsto 3,8\mapsto 4$; $\mathtt {sup}^{S}\!::7\mapsto 1,$ $8\mapsto 1$; $\texttt {<=}^{S}\!=\!\{(1,1),(3,3),(4,4),(3,1),(4,1)\}$.

All underlined operation are implicitly required to be total. This requirement can be explicitly specified by very simple axioms. For example, the axiom for the operation o(wner):At $\rightarrow$ C is: x:At :: ==> o(x). The axioms (a1) – (a4) specify that inheritance is hierarchical, i.e. induces a partial order $\texttt {<=}$. The rules ${\mathtt {t^{0}}}$, ${\mathtt {t^{1}}}$, and ${\mathtt {t^{*}}}$ in Fig. 4 are picturesque visualisations of the epimorphisms presented by axioms (a1), (a2), and (a3) respectively.

5 Sample Transformations – Revisited

The informally introduced model transformation rules in Sect. 2 can be precisely formalised on the basis of the definitions in Sect. 4. Specifications 1 and 2 specify class models and relational schemata respectively. For the model transformation pattern “Single Table Inheritance (ST)”, we devise the partial operations depicted in the specification ST in the left part of Specification 3.³⁵ With this interpretation all rules in Fig. 1 and the rule i4ST in Fig. 2 depict morphisms in $\mathsf {Sys}(\mathtt {ST})$. As an example, consider the rule c2t in Fig. 1. Its left-hand side L is the following ST-algebra: $L_{\mathtt {C}}\!=\!\{1\}$; $L_{\mathtt {B}}\!=\!\{$ int, bool, string $\}$; $\mathtt {int}^{L}\!::*\mapsto$  int; $\mathtt {conc}^{L}\!=\!\{1\}$; $\texttt {<=}^{L}\!=\!\{(1,1)\}$; and all other components of L are empty. Its right-hand side is represented by the ST-algebra R: $R_{\mathtt {C}}\!=\!\{1\}$; $R_{\mathtt {B}}\!=\!\{$ int, bool, string $\}$; $\mathtt {int}^{R}\!::*\mapsto$  int; $\mathtt {conc}^{R}\!=\!\{1\}$; $\texttt {<=}^{R}\!=\!\{(1,1)\}$; $R_{\mathtt {T}}\!=\!\{2\}$; $R_{\mathtt {Co}}\!=\!\{3\}$; $R_{\mathtt {K}}\!=\!\{4\}$; $\mathtt {ta}^{L}\!::3\mapsto 2$; $\mathtt {t}_{\mathtt {Co}}^{L}\!::3\mapsto$  int; $\mathtt {c}_{\mathtt {K}}^{L}\!::4\mapsto 3$; $\mathtt {C2T}^{L}\!::1\mapsto 2$; and all other components of R are empty. The rule morphism $r:L\rightarrow R$ maps as follows: $r_{\mathtt {C}}::1\mapsto 1$; $r_{\mathtt {B}}::$ int $\mapsto$ int, bool $\mapsto$ bool, string $\mapsto$ string; and all other components of the morphism are empty.

Unfortunately, the corresponding transformation system is not terminating for almost all class models. This is due to the fact, that the rules c2t and as2jt are not epic and induce non-epic traces. Therefore, they are not idempotent.

This defect can be avoided by a simple reengineering of ST to the specification ST’ in the right part of Specification 3 together with the adapted rules in Fig. 8 and the adapted rule i4ST’ in Fig. 9 which are epimorphism and guarantee termination of the transformation system for finite class models, since all rules are idempotent and the specification ST’ does not contain any recursive function.

Fig. 8.

Epic handling of classes, attributes, and associations in ST (and CT)

From the practical point of view, ST’ allows more compact rules (compare Figs. 2 and 9.) and is a more precise description for the mapping of class model items to elements in a relational schema than ST: Classes are mapped to keys, since the only feature classes provide for their objects is object identity. Attributes are mapped to columns as before. And associations are mapped to foreign key pairs, since it is the key pair that enforces type conformance of the association’s links in the relational model.

From the theoretical point of view, ST’ and the corrected, now epic rules are better than the rules in Sect. 2, since they induce an epi-reflection, are idempotent, and, therefore, can easily be analysed wrt. termination.

Fig. 9.

Epic handling of inheritance in ST and CT

The two other patterns CT and CCT, discussed in Sect. 2, can also be turned into epi-reflections. The pattern CT differs from ST just by the handling of inheritance. The corresponding transformation rule is i4CT’ in Fig. 9. The necessary mapping of inheritance relations to relational schemata can be provided by a partial operation I2FK : Inheritance $\longrightarrow$ ForeignKey.

Specification 4 presents CCT as a parametric specification in the sense of [10].³⁶ The five rules for the transformation of class models into relation schemata are specified by the total operation As2T and the axioms (a5) – (a8). The semantics of such a specification is the free construction from $\mathsf {Sys}(\mathtt {Source})$ to $\mathsf {Sys}(\mathtt {Target})$ wrt. the obvious forgetful functor in the opposite direction. The point-wise construction of these free objects is described in Sect. 3.2.

It is obvious that the presentation of constructive axioms as Horn-formulae is not as suggestive as the presentation as visual transformation rules, compare for example Fig. 10 which graphically depicts the axioms (a7) and (a8) by rules s2co’ and t2co’ respectively. But as we have shown in this paper both variants are semantically equivalent, if the presented morphisms are epic.

Fig. 10.

Epic generation of foreign keys for associations in CCT

6 Summary

In this paper, we discussed the close connection between generating graph rules and the point-wise construction of epi-reflectors for finite constructive axioms. Constructive axioms turned out to be special cases of arbitrary generating rules. And a finite transformation from an arbitrary object o to a final one can be interpreted as the calculation of the epi-reflector of o, if all rules are epimorphisms.

In categories of partial algebras, constructive axioms can (operation-) generate new elements (e.g. rules in Fig. 10), can add new predicate definitions (e.g. rules in Fig. 4) and are able to identify items (e.g. rule i4ST’ in Fig. 9). Therefore, constructive axioms in categories of partial algebras are suitable for the application area of model transformations for two reasons.

First of all, model transformation rules are typically generating rules, compare for example Triple Graph Grammars (TGG) [2, 9], which have been proposed as a standard framework for model transformation. All rules in TGG are generating, especially all sets of derived rules that can be used for model transformation, i.e. forward, backward, source/target, and integration rules. Future research will investigate the connection between TGG and the framework proposed here.

Secondly, a model transformation produces the derived target model for a given source model, i.e. the target shall be uniquely determined (possibly up to isomorphism) for each source model and it shall be computable in a finite number of steps. If the computation is a calculation of an epi-reflector, uniqueness is for free. And, as we showed above, constructive axioms show better termination behaviour than arbitrary rules. We demonstrated these features in this paper by some typical examples. Future research, especially the elaboration of more and bigger transformation examples, will show, if epimorphisms are sufficient for model transformation.