Multi-amalgamated Transformations

Abstract

In this chapter, we introduce amalgamated transformations. An amalgamated rule is based on a kernel rule, which defines a fixed part of the match, and multi rules, which extend this fixed match. From a kernel and a multi rule, a complement rule can be constructed which characterises the effect of the multi rule exceeding the kernel rule. If multiple rules can be applied using the same kernel rule, as a first main result the Multi-amalgamation Theorem states that a bundle of s-amalgamable transformations is equivalent to a corresponding amalgamated transformation. An interaction scheme is defined by a kernel rule and available multi rules, leading to a bundle of multi rules that specifies in addition how often each multi rule is applied. Amalgamated rules are in general standard rules in $\mathcal{M}$-adhesive transformation systems; thus all the results follow. In addition, we are able to refine parallel independence of amalgamated rules based on the induced multi rules. If we extend an interaction scheme as large as possible we can describe the transformation for an unknown number of matches, which otherwise would have to be defined by an infinite number of rules. This leads to maximal matchings, which are useful for defining the semantics of models. For this chapter, we require an $\mathcal{M}$-adhesive category with binary coproducts as well as initial and effective pushouts (see Sect. 4.3). The theoretical results in this chapter are based on [GHE14].