←Return to chapter

4.2. Preliminaries and simplifying assumptions

For simplicity, we will throughout consider minIR graphs that admit a type system $\Sigma$, though most of the results can also be adapted to other graph domains. We will write $T$ for the types of $\Sigma$ (i.e. its values) and $\Gamma$ for the operation types (i.e. its edges).

Linear paths and operation splitting #

An operation type $\nu \in \Gamma$ in the type system $\Sigma$ is a hyperedge. Its endpoints

are strings of data types that define the input and output signature of the operation $\nu$. We can refer to the set of all hyperedge endpoints of $\nu$ using the string indices $\mathrm{Idx}(\cdot)$ ($\sqcup$ denotes the disjoint set union):

Fix a partition of $P_\nu$ into disjoint pairs

where the last set of the partition may be a singleton if $|P_\nu|$ is odd. For every $\nu \in \Gamma$, we then define $f = \lceil |P_o| / 2 \rceil$ new split operation types $\nu_1, \dots, \nu_f$, each with two endpoints: the $i$-th operation type $\nu_i$ has endpoints $p_i$ and $p_i'$ in $P_\nu$. For every operation $o \in E$ of type $\nu$, we can then split $o$ into $f$ operations $o_1, \dots, o_f,$ each of arity 1 or 2 and of types $\nu_1, \dots, \nu_f$ respectively. We will refer to the graph transformation that replaces an operation $o$ in a minIR graph with the operations $o_i$ for $1 \leqslant i \leqslant f$ as operation splitting.

It is important to note that the splitting of an operation $o$ is unique and given by the type of $o$, and thus invariant under (typed) morphisms: there is a morphism $P \to G$ of a pattern into a graph if and only if there is a morphism $P' \to G'$ from the split pattern $P'$ into the split graph $G'$.

The endpoint partitions $P_\nu$ also define linear paths. Two values $v, v'$ in a minIR graph are on the same linear path if there are values $u_1, \dots, u_k$ with $v = u_1$ and $v' = u_k$ such that $u_i$ is connected to $u_{i+1}$ through an operation $o$ and they correspond to the same pair of endpoints in the endpoints partition (i.e. the indices of $P_{type(o)}$ correspond to values $u_i$ and $u_{i+1}$ in $\textit{src}(o) \sqcup \textit{tgt}(o)$).

Linearity assumption and rigidity #

Recall that in Definition ., $V_\textit{src}$ and $V_\textit{tgt}$ refer to the subset of values that are within the domain of definition of $\textit{src}$ and $\textit{tgt}$ respectively. For this chapter, we will assume $V_\textit{src} = V_\textit{tgt} = V$; in other words, minIR graphs are IO-free (this is w.l.o.g., see discussion after Proposition .) and all values are linear¹ (this is definitely not w.l.o.g.!).

As a result of this assumption, the subcategory of minIR graphs that we consider forms a rigid category, as introduced by Danos et al. Danos, 2014Vincent Danos, Reiko Heckel and Pawel Sobocinski. 2014. Transformation and Refinement of Rigid Structures. The definition, which we reproduce here, is given in terms of morphisms that intersect all components of the codomain. We refer to Danos, 2014Vincent Danos, Reiko Heckel and Pawel Sobocinski. 2014. Transformation and Refinement of Rigid Structures for the precise definition of that notion: in the context of linear-valued minIR graphs, this is equivalent to requiring that the image of the graph homomorphism intersects every connected component of the codomain.

In other words, there is a unique way to extend a morphism $A \xrightarrow{g} C$ to a morphism $B \xrightarrow{f} C$, if it exists. If we interpret $A$ and $B$ as graph patterns that we are interested in matching with $A \subseteq B$, then rigidity guarantees that there is (at most) a unique way to extend a match morphism $A \to G$ into a match morphism on the larger pattern $B \to G$.

The linearity assumption also has other useful consequences. Every linear value has exactly one use and one definition. As a result, all linear paths are disjoint and form a partition of the values of the graph. They correspond to the paths that form the connected components of the fully split graph, i.e. the graph obtained by splitting every operation. We call the number of linear paths (and hence the number of connected components in the fully split graph) the circuit width, written $width(G)$. We also use the linear path decomposition to define circuit depth, written $depth(G)$, as the longest linear path in $G$.

As discussed in section 3.4, minIR rewrites are instantiated from transformation rules by minIR match morphisms $m: P \to G$. Restricting our considerations to linear-valued minIR graphs has the further implication that all such match morphsisms $m$ will be injective. We call $m$ an embedding and write it using greek letters and a hooked arrow

Finding such embeddings $P \hookrightarrow G$ is the pattern matching problem that we are solving. This problem is equivalent to finding minIR subgraphs $H \subseteq G$ of $G$ such that $H$ is isomorphic to the pattern $P \simeq H$.

Convexity #

According to Proposition ., a necessary condition for a subgraph $H$ to define a valid minIR rewrite is convexity. In this chapter we weaken this requirement and propose a condition based on circuit width:

In this chapter, whenever we define a subgraph $H \subseteq G$ of a graph $G$, we will assume that $H$ satisfies the above weakened convexity condition.

The converse of Proposition ., however, is not true. The pattern-matching technique presented below will find a strict superset of convex embeddings. To restrict considerations to convex embeddings, it suffices to filter out the non-convex ones in a post-processing step.

Ignoring minIR Hierarchy #

So far, we have omitted discussing one part of the minIR structure: the nested hierarchy of operations. Syntactically, the hierarchy formed by $parent$ relations between minIR operations can be viewed as just another value type that operations are incident to: parent operations define an additional output that children operations consume as additional input. Because of the bijectivity requirement of minIR morphisms on parent-child relations of Definition ., these parent-child relations behave, in fact, like linear values – and hence do not violate the linearity assumption we have imposed.

However, by treating them as such, we have further weakened the constraints on pattern embeddings. We do not enforce that boundary values must be in the same regions or that parent-child relations cannot be boundary values. Similarly to convexity, we defer checking these properties to a post-processing step.

Further assumptions (harmless) #

We will further simplify the problem by making presentation choices that do not imply any loss of generality. First of all, we assume that all patterns have the same width $w$ and depth $d$, are connected graphs and have at least 2 operations. These conditions can always be fulfilled by adding “dummy” operations if necessary. Embeddings of disconnected patterns can be computed one connected component at a time.

We will further assume that all operations are on at most two linear paths (and thus in particular, have at most 4 endpoints). Operations on $\Delta > 2$ linear paths can always be broken up into a composition of $\Delta-1$ operations, each on two linear paths as follows:

This transformation leaves circuit width unchanged but may multiply the graph depth by up to a factor $\Delta$.

We furthermore define the set of all port labels

so that we can associate every operation endpoint in a minIR graph $G$ with a port label from the set $P_{all}$. We further endow the labels $P_{all}$ with a total order (for instance, based on the string index values). The total order on $P_{all}$ then induces a total order on the paths $v_1\cdots v_k \in V^\ast$ in $G$ that start in the same value $v_1$: the paths are equivalently described by the sequence of port labels of the operations traversed. These form strings in $P_{all}^\ast$, which we order lexicographically. Given a root value $r$, for every value $v$ in $G$ there is thus a unique smallest path from $r$ to $v$ in $G$². This path is invariant under isomorphism of the underlying graph (i.e. relabelling of the values and operations but preserving the port labels). With this we conclude the discussions of the specificities of minIR graphs related to typing, linearity and hierarchy, and the related assumptions that we are making.

To summarise, minIR graphs as they are considered in this chapter are hypergraphs (Definition .) that satisfy the following properties

• every vertex (value) is incident to exactly two hyperedges (operations). It is the target of one hyperedge (its definition) and the source of another one (its use),
• every hyperedge is incident to at most four vertices,
• every hyperedge can be split in a unique way (and invariant under isomorphism) into at most two split operations, with each at most two endpoints.

When modelling subgraphs of IO-free minIR graphs (typically patterns for pattern matching), some hyperedge connections at the boundary of the subgraph will be missing. We say a value is open if a use or define operation is missing (i.e. it is a boundary value in a minIR subgraph).

We will simplify refer to hypergraphs that satisfy the above assumptions as graphs. In the unique instance of this chapter where a graph that does not satisfy this construction is referred to, we will specifically call it a simple graph.

We conclude with the following notable bound on circuit width.

←Return to chapter