Graph transformation in minIR

3.4. Graph transformation in minIR

As discussed in section 3.2, computation graphs with linear values, such as minIR, must adopt strict graph transformation semantics to ensure that linear constraints are satisfied at all times. In this section, we use the minIR graph category presented in the previous section to define transformation semantics that lean on the double pushout (DPO) Ehrig, 1976Hartmut Ehrig and Hans-Jörg Kreowski. 1976. Parallelism of manipulations in multidimensional information structures and sesqui-pushout (SqPO) Corrad., 2006Andrea Corradini, Tobias Heindel, Frank Hermann and Barbara König. 2006. Sesqui-Pushout Rewriting. In Graph Transformations, Berlin, Heidelberg. Springer Berlin Heidelberg, 30--45. doi: 10.1007/11841883_4 semantics in adhesive categories Lack, 2005Stephen Lack and Pawel Sobocinski. 2005. Adhesive and quasiadhesive categories. RAIRO - Theoretical Informatics and Applications 39, 3 (July 2005, 511--545). doi: 10.1051/ITA:2005028.

Adhesivity of hypergraph categories #

The natural place to start this section is by studying which of the categories defined in section 3.3 are adhesive. From adhesivity follows that transforming graphs using DPO and SqPO constructions is well-defined and unique, at least in the regimes of interest to us.

A category is said to be adhesive if it has all pullbacks and pushouts along monos, as well as some compatibility conditions between them, the so-called “Van Kampen squares”. We refer to the literature (e.g. Lack, 2005Stephen Lack and Pawel Sobocinski. 2005. Adhesive and quasiadhesive categories. RAIRO - Theoretical Informatics and Applications 39, 3 (July 2005, 511--545). doi: 10.1051/ITA:2005028) for a complete definition. For our purposes, the following two results are sufficient:

Every presheaf topos $[\mathbb C, \mathrm{Set}]$ is adhesive (Corollary 3.6 in Lack, 2005Stephen Lack and Pawel Sobocinski. 2005. Adhesive and quasiadhesive categories. RAIRO - Theoretical Informatics and Applications 39, 3 (July 2005, 511--545). doi: 10.1051/ITA:2005028);
Every full subcategory $\mathbb D \subseteq \mathbb C$ of an adhesive category is adhesive if the pullbacks and pushouts in $\mathbb C$ of objects in $\mathbb D$ are again in $\mathbb D$ (a simple result; if the Van Kampen squares commute in $\mathbb C$ , they must commute in $\mathbb D$ ).

A first result immediately follows from the first result:

Proposition 3.1Adhesivity of directed hypergraphs

The category

\mathbb H

of directed hypergraphs is adhesive.

Proof

It is a presheaf.

This does not immediately generalise to $\textrm{lin-}\mathbb H$ , as unlike $\mathbb H$ , Definition 3.2 imposes that $E$ be a coproduct. However, the result still holds:

Proposition 3.2Adhesivity of hypergraphs with linearity constraints

The categories

\textrm{lin-}\mathbb H

and

\textrm{lin-}\mathbb H_\textrm{type}

are adhesive.

Proof

$\textrm{lin-}\mathbb H$ is a full subcategory of the adhesive category $[\textrm{lin-}\mathbb C, \mathrm{Set}]$ . We must show the existence of pullbacks and pushouts along monos in $\textrm{lin-}\mathbb H$ .

Pullbacks. Consider a pullback $A \xleftarrow{p_a} P \xrightarrow{p_b}$ of $A \xrightarrow{a} C \xleftarrow{b} B$ in $[\textrm{lin-}\mathbb C, \mathrm{Set}]$ , with $A, B, C \in \textrm{lin-}\mathbb H$ . We must show that $P$ is in $\textrm{lin-}\mathbb H$ . Colimits are computed pointwise in presheaves, so we know that $P(E)$ is the pullback of $A(E) \to C(E) \leftarrow B(E)$ in $\textrm{Set}$ . If we can show that $P(E)$ is the coproduct of $P(E_{st})$ for $s, t \in \mathbb{N}$ , then we are done.

Let $v \in P(E)$ . Because $A(E)$ and $B(E)$ are coproducts in Set, i.e. a disjoint union, there must be $s, t, s', t' \in \mathbb{N}$ such that $p_a(v) \in A(E_{st})$ and $p_b(v) \in B(E_{st'})$ . By naturality of $a$ and $b$ , it follows that $a(p_a(v)) \in C(E_{st})$ and $b(p_b(v)) \in B(E_{s't'})$ . But by commutativity of the pullback diagram, $a(p_a(v)) = b(p_b(v))$ , and thus $s = s'$ and $t = t'$ . We conclude by unicity of the pullback that $v \in P(E_{st})$ and thus $P(E) = \bigsqcup_{st} P(E_{st})$ .

Pushouts. The same argument as for pullbacks also applies to pushouts: given a pushout $P$ of $A \xrightarrow{a} C \xleftarrow{b} B$ in $[\textrm{lin-}\mathbb C, \mathrm{Set}]$ with $A, B, C \in \textrm{lin-}\mathbb H$ , an element $v \in P(E)$ that makes the pushout square commute must have preimages in $A(E_{st}), B(E_{st})$ and $C(E_{st})$ for some $s, t \in \mathbb{N}$ . Thus the pushout distributes over the coproduct, and we can conclude that $P(E)$ is the coproduct of pushouts.

The same argument also applies to $\textrm{lin-}\mathbb H_\textrm{type}$ ¹.

Now to the spicy stuff:

Proposition 3.3Non-adhesivity of hierarchical hypergraphs

Whilst

\textrm{hier-lin-}\mathbb H_\textrm{type}

is adhesive, the category

\textrm{hier-lin-}\mathbb H

is NOT adhesive.

Proof

$\textrm{hier-lin-}\mathbb H_\textrm{type}$ is a presheaf – hence adhesive.

The following pushout square shows that $\textrm{hier-lin-}\mathbb H$ cannot be adhesive: the pushout square is valid in $[\textrm{hier-lin-}\mathbb C, \mathrm{Set}]$ , but the pushout at the bottom right is not in $\textrm{hier-lin-}\mathbb H$ , because the child regions cannot each be assigned a unique parent.

Double pushout semantics #

From Proposition 3.3, it follows that minIR graph transformations can be performed through the double pushout (DPO) construction Ehrig, 1976Hartmut Ehrig and Hans-Jörg Kreowski. 1976. Parallelism of manipulations in multidimensional information structures in the $[\textrm{hier-lin-}\mathbb C, \mathrm{Set}]$ category.

Definition 3.6Double pushout (DPO) transformation

A transformation rule $p$ in an adhesive category $\mathbb A$ is a span $L \leftarrow I \rightarrow R$ . For objects $G, H \in \mathbb A$ , we then write $G \xRightarrow{(p,m)} H$ or $G \xRightarrow{p} H$ if there is a matching morphism $m: L \to G$ and a context object $C$ along with morphisms $G \leftarrow C \to H$ and $I \to C$ such that the following diagram commutes and both squares are pushouts:

If the DPO transformation $G \xRightarrow{(p,m)} H$ exists for some rule $p$ and match $m$ , then we say $G \Rightarrow H$ is a valid DPO rewrite.

To ensure that a DPO rewrite is valid in minIR, we must impose certain conditions. Let $G$ be an IO-free minIR graph, i.e. $G \in \textrm{hier-lin-}\mathbb H$ , there is a morphism $G \to \Sigma$ in $\textrm{hier-lin-}\mathbb H_\textrm{type}$ for some type system $\Sigma$ and $I = O = \varnothing$ .

A DPO rewrite $G \Rightarrow H$ is a valid minIR DPO rewrite if there is a transformation $G \xRightarrow{p} H$ in $[\textrm{hier-lin-}\mathbb C, \mathrm{Set}]$ and

$p$ is left-mono, i.e. the morphism $I \to L$ is mono,²
the pushout complement $C$ and pushout $H$ also exist in the slice category $\textrm{hier-lin-}\mathbb H_\textrm{type} \searrow \Sigma$ ,
$H$ satisfies the hierarchy condition of Definition 3.3,
$H$ is IO-free.

Proposition 3.4

G

is a minIR graph and

G \Rightarrow H

is a valid minIR DPO rewrite, then

H

is a valid minIR graph.

Proof

We know by construction that $H \in [\textrm{hier-lin-}\mathbb C, \mathrm{Set}]$ . We must show that $H$ further satisfies the constraints to be an object in the full subcategory of minIR graphs.

The first condition is standard in DPO and guarantees that $C$ and $D$ are unique if they exist.

The third condition we impose on $H$ corresponds directly to the constraint that defines hierarchical graphs in $\textrm{hier-lin-}\mathbb H$ . The fourth condition ensures that valid minIR DPO rewrites map IO-free graphs to IO-free graphs.

Finally, the second condition is imposed to ensure well-typedness of $H$ . The functor $\textrm{hier-lin-}\mathbb H \to \textrm{hier-lin-}\mathbb H_\textrm{type}$ that forgets the $\textit{def}$ and $\textit{use}$ morphisms is a left adjoint (it possesses a right Kan extension defined pointwise), and thus preserves colimits. The images of $C$ and $H$ thus form pushout squares in $\textrm{hier-lin-}\mathbb H_\textrm{type}$ , and by unicity, must match the pushout squares in $\textrm{hier-lin-}\mathbb H_\textrm{type} \searrow \Sigma$ . Hence $H$ is well-typed.

The restriction to rewrites of IO-free graphs is not a restriction of generality: if we are interested in rewriting computations with inputs and outputs, we can always express them as IO-free graphs by adding input and output ops with the values in $I$ as outputs, respectively $O$ as inputs. We assign them dedicated types distinct from all other operations; these operations will never be matched by transformation rules and can be removed at the end of rewriting.

Generalising to sesqui-pushouts #

We restricted minIR rewrites to DPO transformations obtained form left-mono rules, to ensure that the construction is unique. This excludes rules that may identify two values in $G$ but split them into two different values in $H$ . Such rules allow for cloning values, which is a useful transformation in minIR for non-linear values. An example of a transformation rule that we would like to allow in minIR:

For this example we added a 2x operation that multiplies an angle value passed as input by two. The transformation rule replaces a rotation of angle $2\alpha$ by two rotations of angle $\alpha$ by cloning the input angle.

Such semantics are possible using the sesqui-pushout construction (SqPO) by Corradini et al. Corrad., 2006Andrea Corradini, Tobias Heindel, Frank Hermann and Barbara König. 2006. Sesqui-Pushout Rewriting. In Graph Transformations, Berlin, Heidelberg. Springer Berlin Heidelberg, 30--45. doi: 10.1007/11841883_4. We can reuse the same $\xRightarrow{(p,m)}$ notation: when DPO is restricted to left-mono rules as we have done, SqPO is a generalisation of DPO (i.e. the construction coincides whenever the DPO exists).

Definition 3.7Sesqui-pushout (SqPO) transformation

A transformation rule $p$ in an adhesive category $\mathbb A$ is a span $L \leftarrow I \rightarrow R$ . For objects $G, H \in \mathbb A$ , we then write $G \xRightarrow{(p,m)} H$ or $G \xRightarrow{p} H$ if there is a matching morphism $m: L \to G$ and a context object $C$ along with morphisms $G \leftarrow C \to H$ and $I \to C$ such that $C$ is the final pullback complement of $I \to L \xrightarrow{m} G$ and the right square is a pushout:

If the SqPO transformation $G \xRightarrow{(p,m)} H$ exists for some rule $p$ and match $m$ , then we say $G \Rightarrow H$ is a valid (SqPO) rewrite.

The left square is redundant in the diagram above, as it follows from the requirement that $C$ be the final pullback complement (FPC). It is kept to highlight the similarities to DPO. As the commuting diagram indicates, the final pullback complement (FPC) construction forms a pullback square. Furthermore, unlike pushout complements, the FPC is defined by a universality property that ensures uniqueness if it exists. We refer to Corrad., 2006Andrea Corradini, Tobias Heindel, Frank Hermann and Barbara König. 2006. Sesqui-Pushout Rewriting. In Graph Transformations, Berlin, Heidelberg. Springer Berlin Heidelberg, 30--45. doi: 10.1007/11841883_4 for the exact FPC construction.

With SqPO, we can define the set of valid minIR rewrites as given by the SqPO transformations $G \xRightarrow{p} H$ in $[\textrm{hier-lin-}\mathbb C, \mathrm{Set}]$ satisfying the relaxed set of conditions

the pushout complement $C$ and pushout $H$ also exist in the slice category $\textrm{hier-lin-}\mathbb H_\textrm{type} \searrow \Sigma$ ,
$H$ satisfies the hierarchy condition of Definition 3.3,
$H$ is IO-free.

We conclude this section with a discussion of some of the properties of minIR transformations using SqPO (referring again to Corradini Corrad., 2006Andrea Corradini, Tobias Heindel, Frank Hermann and Barbara König. 2006. Sesqui-Pushout Rewriting. In Graph Transformations, Berlin, Heidelberg. Springer Berlin Heidelberg, 30--45. doi: 10.1007/11841883_4 or König, 2018Barbara König, Dennis Nolte, Julia Padberg and Arend Rensink. 2018. A Tutorial on Graph Transformation. In Graph Transformation, Specifications, and Nets - In Memory of Hartmut Ehrig. Springer, 83--104. doi: 10.1007/978-3-319-75396-6_5 for a more detailed explanation of the concepts discussed):

Deletion in unknown context. A key difference between DPO and SqPO transformations is that SqPO transformations on graphs will delete edges attached to a vertex $v_d$ that is deleted by the transformation rule (i.e. $v_d \in L$ but $v_d \not\in R$ of the rule). The DPO transformation on the other hand is only well-defined when all edges incident to $v_d$ are in the image of $m$ and thus explicitly deleted (this is known as the dangling condition).

As minIR rewrites follow SqPO semantics, transformation rules such as the following are allowed:

Here $\times$ denotes the multiplication of angles and $\textsf{const(0)}$ the zero angle. Any operation that would be connected to the starred value on the left would be deleted by this rule. However such an implicit operation deletion only yields valid minIR graphs if all incident values are non-linear and none of the target values of the deleted operation are used.

Non-left-mono rules. As discussed in the introduction to SqPO, the cloning of values is allowed in minIR rewrites. However, linear values may never be cloned (the FPC or pushout will not exist in these cases). Thus any minIR transformation rule will be left-mono on linear values. It must further be left-linear on all (linear and non-linear) values in $I$ that are mapped to outputs in $R$ : if a value $w$ is produced by op applied to $v$ , then cloning $v$ and 'op will result in two definitions of $w$ .

Non-right-mono rules. Non-right-mono rules are allowed in both DPO and SqPO. They result in vertex merges. In minIR, the situation for right-mono is symmetric to left-mono: the map must be mono on linear values (otherwise the same value will have multiple uses or definitions) and it must be mono on all values in $I$ that are mapped to inputs in $L$ (otherwise a value in the rewritten minIR graph will have more than one value definition).

In fact, a much simpler argument applies: the category $\textrm{lin-}\mathbb H_\textrm{type}$ is isomorphic to the presheaf category $[\textrm{lin-}\tilde{\mathbb C}_\textrm{type}, \mathrm{Set}]$ , where $\textrm{lin-}\tilde{\mathbb C}_\textrm{type}$ is obtained from $\textrm{lin-}\mathbb C_\textrm{type}$ by removing the object $E$ . Adhesivity follows. ↩︎
This is often called left-linear in the literature. We avoid this term in this thesis to avoid confusion with the linearity property of values in minIR. ↩︎

←Return to chapter