←Return to chapter

3.5. MinIR rewriting, operationally

The previous section proposed to view minIR rewrites as the result of a (DPO or SqPO) graph transformation. This yields valid rewriting semantics elegantly (and with little effort!). However, the conditions that must be imposed on the transformation to be valid, along with the fact that pushouts may not exist mean that the existence of a rewrite given a transformation rule and a match is not guaranteed.

In this section, we address this by considering a more restricted notion of minIR rewriting, for which the existence of the right-hand side of the rewrite is guaranteed. In addition, in place of the categorical presentation of the last section, we express the rewriting operation operationally, i.e. as data and a procedure on sets that translates directly into an algorithmic implementation.

We find that this rewrite definition is sufficient in practice. We conclude the section with an example of how more complex rewrites can be achieved by composition of simpler rewrites that can be expressed in this framework.

Graph glueings and rewrites #

Throughout, we consider graph glueings on disjoint vertex and (hyper)edge sets. To underline this, we will use the $\sqcup$ symbol to denote disjoint set unions.

As we will be working exclusively with vertex and edge sets in this section (as opposed to the objects in the indexing category), we will drop the bold typeface for sets, writing e.g. $V$ instead of $\mathbf V$ for the set of vertices of a hypergraph.

Finally, all minIR graphs in this section are IO free.

We define local graph rewrites in terms of graph glueings. Consider first the case of two arbitrary graphs $G_1 = (V_1, E_2)$ and $G_2 = (V_2, E_2)$, along with a relation $\mu\ \subseteq V_1 \times V_2$. Let $\sim_\mu \ \subseteq (V_1 \sqcup V_2)^2$ be the equivalence relation induced by $\mu$, i.e. the smallest relation on $V_1 \sqcup V_2$ that is reflexive, symmetric and transitive, and satisifes for all $v_1 \in V_1$ and $v_2 \in V_2$,

Then, we can define

• $V = (V_1 \sqcup V_2)/\sim_\mu$ is the set of all equivalence classes of $\sim_\mu$, and
• for $v \in V_1 \sqcup V_2$, $\alpha_\mu(v) \in V$ is the equivalence class of $\sim_\mu$ that $v$ belongs to.

In other words, the glueing is the disjoint union of the two graphs, with identification (and merging) of vertices that are related in $\mu$.

This allows us to define a rewrite on a graph $G$:

A graph rewrite per this definition can always be generated by a single pushout (SPO) transformation Löwe, 1991Michael Löwe. 1991. Extended algebraic graph transformation. Retrieved from http://d-nb.info/910935696.

• define $L$ as the graph $(V^-, E^-)$. Then the injection $L \subseteq G$ is the match morphism $L \to G$;
• the partial map $\mu$ maps a subset of $V^-$ to vertices in the replacement $R = G_R$. By injectivity of the match morphism, it also defines a partial map $L \rightharpoonup R$.

We opted for SPO-like semantics in this definition, as they are the simplest to write in set-theoretic terms and coincide with DPO and SqPO in our restricted domain of interest.

The result of the rewrite is computed by gluing the right-hand side $G_R$ to the context subgraph $G_C = (V_C, E_C)$ of $G$ given by

The partial function $\mu$ is a special case of a glueing relation $\mu \subseteq V_C \times V_R$, and thus defines a glueing of $G_C$ with $G_R$. The rewritten graph resulting from applying $r$ to $G$ is $$r(G) = (G_C \sqcup G_R) / \sim_\mu.$$

An example of a graph rewrite is given in the next figure. This is equivalent to an SPO transformation with the graph induced by $V^-$ on the left-hand side, the graph $G_R$ on the right-hand side and the partial map $L \hookrightarrow R$ given by $\mu$.

When there are no edges between $V \smallsetminus V^-$ and $V^- \smallsetminus dom(\mu)$ (purple in the example above), this definition corresponds to graph rewrites that can be produced using DPO transformations (see discussion in section 3.4). Otherwise, such edges are deleted.

The notions of graph glueing and graph rewrite can straightforwardly be lifted to hypergraphs and, by extension, to minIR graphs. Notice that in this case, values are glued together, not operations (the former were defined as the graph’s vertices, the latter as its hyperedges).

However, the glueing of two valid minIR graphs – and the result of applying a valid rewrite – may not be a valid minIR graph. Glueing two values of a linear type, for instance, is a sure way to introduce multiple uses (or definitions) of it. Thus, we must be careful to only consider glueings and rewrites of minIR graphs that preserve all the constraints we have imposed in Definition 3.4.

Ensuring rewrite validity: interfaces #

As a sufficient condition for valid minIR rewrites, we introduce minIR interfaces, a concept closely related to the “hypergraph with interfaces” construction of Bonchi, 2017Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Paweł Sobociński and Fabio Zanasi. 2017. Confluence of Graph Rewriting with Interfaces or the supermaps of quantum causality Hefford, 2024James Hefford and Matt Wilson. 2024. A Profunctorial Semantics for Quantum Supermaps. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, July 2024. ACM, 1--15. doi: 10.1145/3661814.3662123. We eschew the presentation of holes as a slice category in favour of a definition that fits naturally within minIR and is sufficient for our purposes.

Let $G$ be a $\Sigma$-typed minIR graph with data types $T$ and linear types $T_L \subseteq T$. Consider type strings $S, S' \in T^\ast$. We define the index sets

corresponding respectively to the set of all indices into $S$ and the subset of indices of linear types. For any $i \in \mathrm{Idx}(S)$, we denote by $S_i$ the type at position i in $S$.

We define a partial order $\preccurlyeq$¹ on $T^\ast$ where $S \preccurlyeq S'$ and say that $S'$ can be coerced into $S$ if there exists an index map $\rho: \mathrm{Idx}(S) \to \mathrm{Idx}(S')$ such that

• types are preserved: $S_i = S'_{\rho(i)}$, and
• $\rho$ is well-defined and bijective on the restriction to indices of linear types
  $$\left.\rho\right|_{\mathrm{Idx}_L(S)}: \mathrm{Idx}_L(S) \to \mathrm{Idx}_L(S').$$

We can define the interface associated with an operation $o$ in a minIR graph $G$ by considering the values used and defined by $o$. Calling $\tau$ the type morphism on $G$ and assuming $o \in E_{st}$ to be an operation in $G$ with $s$ inputs and $t$ outputs, we define the interface of $o$ in $G$ as the pair of strings in $T^\ast$

Similarly, we can assign interfaces to subgraphs of minIR graphs:

Note that $B_U$ is exactly the set of inputs $I$ in the non-IO free minIR graph given by the subgraph $(V_H, E_H)$ of the minIR graph. $B_D$ is a superset of the outputs $O$ of $H$: it includes all linear values in $H$ that do not have a use in $H$, but also any non-linear value that has a use outside of $H$.

Unlike interfaces, subgraph boundary values are not ordered. An ordering of $B \subseteq V$ is a string $S \in V^\ast$ along with a bijective map

If there are strings $S_U, S_D \in V^\ast$ and orderings of $B_U$ and $B_D$

then we can set $\textit{src}_i\,(H) = (S_U)_i$ and $\textit{tgt}_i\,(H) = (S_D)_i$ in complete analogy to operations. We will write $\textit{src}(H)$ and $\textit{tgt}(H)$ for the strings $\textit{src}_1(H)\cdots\textit{src}_{|S_U|}(H)$ and $\textit{tgt}_1(H)\cdots\textit{tgt}_{|S_D|}(H)$ respectively. We say that the subgraph $H$ implements the interface

where the type morphism $\tau$ was extended element-wise to strings $V^\ast$.

Remark, though, that unlike operations, the same subgraph may implement more than one interface as a result of various choices of orderings $\textrm{ord}_U$ and $\textrm{ord}_D$.

As mentioned, the subgraph $H$ forms a non-IO free minIR graph. We can always construct an IO-free minIR graph from $H$ by adding two operations $o_{in}$ and $o_{out}$ in the root region respectively in $E_{0, |S_U|}$ and $E_{|S_D|, 0}$ inputs-outputs, defined by

We call the resulting graph $\bar{H}$ an interface graph. It implements the interface $I_H$ if $H$ implements $I_H$. Calling to mind the illustrations of section 3.3, $\bar{H}$ looks like one of the nested regions within regiondef operations that we were considering.

MinIR operation rewrite #

Consider

• an operation $o$ in a minIR graph $G$ with values $V,$
• an interface graph $\bar{H}$ with values $V_H$ and its associated subgraph $H \subseteq \bar{H}$, such that $H$ implements an interface $I(o) \triangleleft I_H,$
• the index maps $\rho: \mathrm{Idx}(\textit{src}(H)) \to \mathrm{Idx}(\textit{src}(o))$ and $\sigma: \mathrm{Idx}(\textit{tgt}\,(o)) \to \mathrm{Idx}(\textit{tgt}\,(H))$ that define the generalisation $I(o) \triangleleft I_H$ (per Definition 3.10).

We can define a glueing relation $\mu_o \subseteq V \times V_H$

This is almost enough to define a rewrite that replaces the operation $o$ in $G$ with the values and operations of $H$ – the interface compatibility constraint $I(o) \triangleleft I_H$ that we have imposed ensures that the resulting minIR graph is valid. Unfortunately, $\mu_o$ is not a partial function as required by Definition 3.4.

This is resolved in the following proposition:

The definition of the rewrite of $o$ into a graph $H$ behaves as one would expect – the only subtleties relate to handling non-linear (i.e. copyable) values at the boundary of the rewrite. The following example illustrates some of these edge cases.

When the index maps $\rho$ and $\sigma$ are not injective (yellow and green dots), values are merged, resulting in multiple uses of the value (i.e. copies). This is why the index maps must be injective on linear values (dots in shades of blue). Value merging also happens when a value is used multiple times in $o$ (yellow and red dots). This will never happen with linear values (as they can never have more than one use in $o$), nor with any value definitions (the same value can never be defined more than once). Finally, values not in the image of $\rho$ or $\sigma$ (purple dot) are discarded. This case is also excluded for linear values by requiring surjectivity.

Arbitrary minIR rewrites #

We have so far defined rewrites of single operations into graphs $H$. We can generalise these rewrites to rewrite subgraphs $P \subseteq G$, provided the minIR subgraphs satisfy some constraints. We require for this a notion of convexity, as discussed in Bonchi, 2022Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski and Fabio Zanasi. 2022. String diagram rewrite theory II: Rewriting with symmetric monoidal structure. Mathematical Structures in Computer Science 32, 4 (April 2022, 511--541). doi: 10.1017/s0960129522000317.

As usual, let us consider a minIR graph $G$ with values $V$, linear values $V_L \subseteq V$, edges $E$, the incidence maps $\textit{src}_i$ and $\textit{tgt}_j$ as well as their inverses $\textit{use}$ and $\textit{def}$. Consider further a subgraph of $G$ that we will now call $P = (V_P, E_P) \subseteq G$, to distinguish from $H$.

Let us further define the partial $parent$ morphism that maps a value $v \in V$ to the parent of the region of $v$.

Define the sets of boundary values $B_U, B_D$ and $B = B_U \cup B_D$, as in (2); then fix the boundary orderings $\textit{src}(P)$ and $\textit{tgt}\,(P)$ as in (3). The subgraph $P$ implements the interface

Consider an interface graph $\bar{H}$ that implements $I_H$ such that $I_P \triangleleft I_H$. Instead of defining a gluing relation from values of an operation $o$ to values of $H$, we replace the interface $I(o)$ with $I_P$. This generalises the definition of $\mu_o$ from (4) to a glueing $\mu\subseteq B \times V_H$ defined as

With the set of boundary operations defined as²

we are able to define minIR rewrites in their most general form.

This simple and limited graph transformation framework captures a remarkably large set of minIR program transformations. It may seem at first that the restriction to boundary values within a single region of Definition 3.11, as well as the convexity requirements of Definition 3.12 represent significant limitations on the expressivity of the rewrites. In practice, however, the semantics of minIR operations can be used to decompose more complex rewrites into a sequence of simple rewrites to which Proposition 3.6 applies.

Consider minIR graphs with a type system that includes regiondef and call operations as discussed in examples of the previous section – respectively defining a code block by a nested region and redirecting control flow to a code block defined using a regiondef. Then all constraints that we impose on rewriting can be effectively side-stepped using the region outlining and value hoisting transformations.

Region outlining moves a valid minIR subgraph into its own separate region, and replaces the hole left by the subgraph in the computation by a call operation to the newly outlined region.

Value hoisting moves a value definition within a region to its parent region and passes the value down to the nested region through an additional input. In case of linear values, we can similarly hoist the unique use of the value to the parent region.

Using these transformations, non-convex subgraphs can always be made convex by taking the convex hull and outlining any parts within it that are not part of the subgraph. Outlined regions can then be passed as additional inputs to the subgraph. Step 1 of the figure below illustrates this transformation. Similarly, a subgraph that includes operations without their parent can be extended to cover the entire region and its parent, outlining any parts of the region that are not part of the subgraph.

Finally, whenever a boundary value $v$ belongs to a region that is not the top level region of the subgraph³, we can repeatedley hoist $v$ to its parent region until it is in the top level region. The value is then recursively passed as argument to descendant regions until the region that it is required in. Subgraphs can thus always be transformed to only have input and output boundary values at the top level region. Step 2 of the figure below illustrates this transformation.

←Return to chapter