The multiresolution analysis of flow graphs

TL;DR

This paper explores the multiresolution analysis of flow graphs in computer programs, using category theory to establish natural definitions and foundational results for understanding control transfer structures.

Contribution

It introduces and proves fundamental results on graph-theoretic notions relevant to multiresolution analysis of flow graphs from a category-theoretical perspective.

Findings

Basic results on flow graph notions established

Category-theoretical framework applied to flow graphs

Natural definitions for multiresolution analysis provided

Abstract

We introduce and prove basic results about several graph-theoretic notions relevant to the multiresolution analysis of flow graphs that represent the transfer of control in computer programs. We take a category-theoretical viewpoint to demonstrate that our definitions are natural and to motivate particular incarnations of related constructions.

Equations

$$f_{(m)}{\circ }_{\ell }{g}_{(n)}:=f({\cdot }_1,\dots ,{\cdot }_{\ell -1},g({\cdot }_{\ell },\dots ,{\cdot }_{\ell +n-1}),{\cdot }_{\ell +n},\dots ,{\cdot }_{m+n}).$$

$$\circ :P(n)\times P(k_1)\times \cdots \times P(k_n)$$

$$(G,G_1,\dots ,G_n)$$

$${\varphi }_G(j):=\{\begin{array}{ll}s(e^{+})& \text{if }j=s(e_s)\\ t(e^{+})& \text{if }j=t(e_s)\\ & \text{or }t(e_s)=s(e_t)\text{ and }j=t(e_t)\\ s(e^{-})& \text{if }t(e_s)\ne s(e_t)\text{ and }{e}_s\ne e_t\text{ and }j=s(e_t)\\ t(e^{-})& \text{if }t(e_s)\ne s(e_t)\text{ and }{e}_s\ne e_t\text{ and }j=t(e_t)\\ j& \text{otherwise}\end{array}$$

$$G\otimes G^{\prime }:=G\bigsqcup G^{\prime }/\sim ,$$

$$(j,0)\sim (j,0)$$

$$(j^{\prime },1)\sim (j^{\prime },1)$$

$$(j,0)\sim (k,0)$$

$$(j^{\prime },1)\sim (k^{\prime },1)$$

$$(j,0)\sim (j^{\prime },1)$$

$$(f\otimes f^{\prime })(k):=\{\begin{array}{ll}[(f(j),0)]& \text{if }k=[(j,0)]\\ [(f^{\prime }(j^{\prime }),1)]& \text{if }k=[(j^{\prime },1)]\end{array}$$

$${\alpha }_{G,G^{\prime },G^{\prime \prime }}:\{\begin{array}{ll}[([(j,0)],0)]& \mapsto [(j,0)]\\ [([(j^{\prime },1)],0)]& \mapsto [([(j^{\prime },0)],1)]\\ [(j^{\prime \prime },1)]& \mapsto [([(j^{\prime \prime },1)],1)]\end{array}$$

$$\begin{array}{c}[([([(w,0)],0)],0)]\\ [([([(x,1)],0)],0)]\\ [([(y,1)],0)]\\ [(z,1)]\end{array}\mapsto \begin{array}{c}[([(w,0)],0)]\\ [([([(x,0)],1)],0)]\\ [([([(y,1)],1)],0)]\\ [(z,1)]\end{array}\mapsto \begin{array}{c}[(w,0)]\\ [([([(x,0)],0)],1)]\\ [([([(y,1)],0)],1)]\\ [([(z,1)],1)]\end{array}\mapsto \begin{array}{c}[(w,0)]\\ [([(x,0)],1)]\\ [([([(y,0)],1)],1)]\\ [([([(z,1)],1)],1)]\end{array}.$$

$$\begin{array}{c}[([([(w,0)],0)],0)]\\ [([([(x,1)],0)],0)]\\ [([(y,1)],0)]\\ [(z,1)]\end{array}\mapsto \begin{array}{c}[([(w,0)],0)]\\ [([(x,1)],0)]\\ [([(y,0)],1)]\\ [([(z,1)],1)]\end{array}\mapsto \begin{array}{c}[(w,0)]\\ [([(x,0)],1)]\\ [([([(y,0)],1)],1)]\\ [([([(z,1)],1)],1)]\end{array}.$$

Full text

1 Introduction

The notion of a “flow graph” is central to the analysis and compilation of computer programs, encompassing constructs that represent the transfer of control and data [7, 22, 23]. As the complexity of software increases, so does the scale of the corresponding flow graphs: accordingly, a framework for the analysis of flow graphs at multiple resolutions is desirable. Such a framework was originally presented in [16], based on a hierarchical representation of input/output structure called the program structure tree (PST).

For an illustration of this framework, consider the simple imperative program “skeleton” and associated control flow graph in Figure 1. The result of “stretching” it à la §0.B and the PST of the result are shown in Figure 2. Iterating the process of pruning each leaf of the PST à la §5 leads to “coarsened” control flow graphs such as those in Figure 3.

The utility of this framework is enhanced by [31], which shows how to restructure the control flow graph of a program in such a way that subroutines can be identified as programs in their own right using the control flow graph alone. This feeds naturally into a “multiresolution analysis” of recursively composing (resp. decomposing) a program from (resp. into) subprograms in a way that can help with building, understanding, and modifying large programs.

This paper extends the work of [16] while correcting both an error of definition (for interiors of single-entry/single-exit regions) found in [3], and another subtler error in the original proof of Theorem 3.1, by unifying and formalizing several natural concepts relevant to the decomposition and construction of flow graphs. This has several benefits: as the most basic example, we provide a definition of flow graph that is slightly different than its other usual variants but that is mathematically more natural and well-behaved. This in turn leads to a simpler analogue of the “refined process structure tree” of [24, 30] and natural category-theoretic constructions. These include multiresolution operations that approximate and/or refine flow graphs at multiple scales, as well as series and parallel operations that respectively embody sequential execution and if/else constructs in control flow.

While most of the results of this paper are conceptually straightforward and many are at least latent in the literature, few of them have been simultaneously formulated explicitly and mathematically. Indeed, the practical motivation for this paper is simply to show that the “right” definition of a flow graph entails all the obvious desiderata, particularly for treating subroutines as programs in their own right. As §7 highlights, the precise ability to compose flow graphs in category-theoretically nice ways is novel (though it is obvious that such a thing should be possible somehow): the unit object presents the principal difficulty, and much of our effort is focused on this issue for the case of parallel composition. This compositionality can inform the internal representation of graphical data structures and techniques for their manipulation in binary program analysis platforms such as [5] and program synthesizers [13] as well as compilers.

In particular, constraining the notion of a valid control flow graph to the one considered in the paper could confer an advantage from the point of view of precompilation or reuse/modification: our results give a recipe for inserting and combining precompiled code in a convenient way. In a similar vein, we may want to understand a disassembled binary by synthesizing a similar or equivalent program. After restructuring the control flow graph along the lines of [31] and performing some straightforward normalizations (see §0.B), we could construct the PST and attempt program synthesis for each of the subroutines corresponding to a leaf node. In particular, we could generate inputs and observe outputs to each of these subroutines, so that program induction is a viable fallback at each point. Recursively going up the PST, we (attempt to) get such a globally synthesized program, and our results indicate precisely how synthesized/induced programs of intermediate scale can be maintained and reasoned over.

In other words, the constructions of the paper can inform tools that blur the lines between compilation and decompilation. In particular, the central results of §5 and §6 contain the technical details necessary to have confidence that intermediate representations of programs can be (de)composed in a mathematically principled way, offering a firm foundation for future tools. Although superficial errors in [16] and hitherto unrecognized categorical structure in the PST have hindered its use, 111 To illustrate this point, we quote liberally from [3]: “Unfortunately, we discovered an error in the aforementioned proof regarding SSI [static single information] form…we discovered that this mistake had been made in an earlier paper as well, and that other mistakes had been made in several papers that built on SSI form. The goal of this article, therefore, is to clear up the mistakes to the greatest possible extent…The key mistake was…made by Johnson et al. [1994], who introduced a data structure called the program structure tree (PST), which attempted to represent the structure of a control flow graph hierarchically.”

we believe that tools based on it can and should be built.

The paper is organized as follows: we discuss dominance relations in §2; flow graphs, single-entry/single-exit regions, and the PST in §3; we introduce the structure of a category on flow graphs in §4 (this delay is to connect the paper to prior work most clearly); we discuss multiresolution transformations on flow graphs in §5; and in §6 we discuss series and parallel composition of flow graphs in the context of formal tensor product structures. §7 discusses two-terminal graphs before our concluding remarks in §8. §0.A contains proofs and §0.B sketches a “stretching” operation that enhances the applicability of our constructions.

We remark at the outset that all graphs (and related objects) are assumed finite throughout this paper. By convention, digraphs are allowed to have loops from a vertex to itself. Given a vertex $v$ in a digraph, let $d^{+}_{0}(v)$, $d^{-}_{0}(v)$, and $d^{0}(v)$ respectively denote the number of incoming edges excluding any loop, the number of outgoing edges excluding any loop, and the number ($\leq 1$) of loops at $v$. A vertex $v$ is a source iff $d^{+}_{0}(v)=0$ and a target iff $d^{-}_{0}(v)=0$, i.e., loops have no bearing on these properties.

2 Dominance relations

Let $G$ be a digraph and $j,k\in V(G)$. We say that $j$ dominates $k$, written $j\text{ dom }k$, iff every path from a source $s$ in $G$ to $k$ passes through $j$ [7, 22]. Define $D_{jk}=1$ if $j\text{ dom }k$ and $D_{jk}=0$ otherwise. Similarly, let $D^{\dagger}:=D(G^{*})$, where $G^{*}$ is the reversal or adjoint of $G$ with adjacency matrix $A^{*}$ and corresponding dominance relation dom†. If $D^{\dagger}_{jk}=1$, i.e., if j\text{ dom{}^{\dagger} }k, write $k\text{ pdom }j$ and say that $k$ postdominates $j$. Both the dominance and postdominance relations extend to edges. The following two lemmas are straightforward.

Lemma 1

For distinct edges $\{e_{j}\}_{j=1}^{3}$ in a digraph $G$, if $e_{1}\text{ dom }e_{3}$ and $e_{2}\text{ dom }e_{3}$, then either $e_{1}\text{ dom }e_{2}$ or $e_{2}\text{ dom }e_{1}$. Similarly, if $e_{1}\text{ pdom }e_{2}$ and $e_{1}\text{ pdom }e_{3}$, then either $e_{2}\text{ pdom }e_{3}$ or $e_{3}\text{ pdom }e_{2}$. ∎

Lemma 2

If $e_{1}\text{ dom }e_{2}$ and $e_{1}\text{ pdom }e_{2}$ with $e_{1}\neq e_{2}$, then a path from a source to a target that traverses $e_{2}$ contains a cycle of the form $(e_{1},\dots,e_{2},\dots,e_{1})$. ∎

We use Lemma 2 to fix a subtle (and minor) error in a proof of Theorem 3.1 that was originally presented by [16]. This helps us to rescue the framework of [16] in its entirety from the problems raised by [3].

3 Flow graphs, single-entry/single-exit regions, and the program structure tree

A flow graph $G$ is a digraph with exactly one source and exactly one target, such that there is a unique (entry) edge from the source and a unique (exit) edge to the target, and such that identifying the source of the entry edge with the target of the exit edge yields a strongly connected digraph. (We do not require the entry and exit edges to be distinct, e.g., if $|V(G)|=2$.) 222NB. One sometimes sees variants of the definition and naming of this particular sort of concept, for the latter most typically as “flowgraph”, “flowchart”, or “flow chart”. Some concepts with the same name are technically quite different but “spiritually” viewed in a similar context, as, e.g., in the work of Manin [8, 20].

A single entry/single exit (SESE) region in a digraph $G$ is defined as an ordered pair of edges $(e_{1},e_{2})$ satisfying each of the following conditions [16]: $e_{1}\text{ dom }e_{2}$, $e_{2}\text{ pdom }e_{1}$, and a cycle in $G$ contains $e_{1}$ iff it contains $e_{2}$. See Figure 5 for examples. Note first that $(e_{1},e_{1})$ is a degenerate SESE region, 333NB. Degenerate SESE regions $(e_{1},e_{1})$ are excluded by the original definition of [16]. We allow such regions to make the series tensor product of §6.1 work nicely.

and second that a nondegenerate SESE region $(e_{1},e_{2})$ (i.e., a SESE region with $e_{1}\neq e_{2}$) unambiguously corresponds to the ordered vertex pair $(t(e_{1}),s(e_{2}))$, where $s(\cdot)$ and $t(\cdot)$ respectively denote the source and target of an edge. We may use either the edge or vertex pairs above to specify a nondegenerate SESE region. Note also that in a DAG the third condition above is trivial. Finally, note that the edges $e_{s}$ from the source and $e_{t}$ to the target of a flow graph $G$ together define a SESE region and vice versa. With this in mind, write either $G$ or $(e_{s},e_{t})$ for the flow graph or the equivalent SESE region.

We give a few simple results (the first is straightforward enough that we omit a proof) before moving on to a fundamental theorem.

Lemma 3

If $(e_{1},e_{2})$ and $(e_{2},e_{3})$ are SESE regions, then so is $(e_{1},e_{3})$. ∎

Lemma 4

If $(e_{1},e_{2})$ and $(e_{1},e_{3})$ are SESE regions with $e_{2}\neq e_{3}$ and $e_{2}\text{ dom }e_{3}$, then $(e_{2},e_{3})$ is a (nondegenerate) SESE region.

Corollary 1

If $(e_{1},e_{2})$ is a SESE region with $e_{2}\neq e_{3}$ and $e_{2}\text{ dom }e_{3}$, and $(e_{2},e_{3})$ is not a SESE region, then $(e_{1},e_{3})$ is also not a SESE region. 444A useful restatement of this is that if $(e_{1},e_{2})$ is a SESE region with $e_{2}\neq e_{3}$ and $e_{2}\text{ dom }e_{3}$, then $(e_{1},e_{3})$ is not a SESE region unless $(e_{2},e_{3})$ is a SESE region. ∎

The interior $G^{\circ}$ of $G\equiv(e_{s},e_{t})$ is the set of vertices that are each on at least one path starting from $t(e_{s})$ that does not encounter $t(e_{t})$. Critically, this definition differs slightly from Definition 6 of [16], wherein the interior of a SESE region $(e_{s},e_{t})$ is defined as $\{j\in V:e_{s}\text{ dom }j\land e_{t}\text{ pdom }j\}$. An example in §5 of [3] and reproduced in Figure 4 illustrates the difference between these definitions.

A nondegenerate SESE region $(e_{1},e_{2})$ is called canonical if for any SESE region $(e_{1},e^{\prime}_{2})$ it is the case that $e_{2}\text{ dom }e^{\prime}_{2}$ and if for any SESE region $(e^{\prime}_{1},e_{2})$ it is the case that $e_{1}\text{ pdom }e^{\prime}_{1}$. Our definition of the interior of a SESE region enables the following corrected version of Theorem 1 of [16] (cf. [3]).

Theorem 3.1

Interiors of distinct canonical SESE regions are disjoint or nested.

Therefore canonical SESE regions are also minimal, so we may use the two terms interchangeably: we generally prefer and use the latter. The inclusion relation on minimal SESE regions induces a tree—viz., the PST. An example of this nesting behavior and the corresponding PST are depicted in Figure 5.

Lemma 5

A nondegenerate SESE region $(e_{0},e_{\infty})$ decomposes as $(e_{0},e_{\infty})=\bigcup_{j=1}^{m}(e_{j-1},e_{j})$, where $e_{m}\equiv e_{\infty}$ and $(e_{j-1},e_{j})$ are minimal SESE regions.

Define an edge-indexed matrix $S$ by $S_{e_{1},e_{2}}=1$ if $(e_{1},e_{2})$ is a nondegenerate SESE region and $S_{e_{1},e_{2}}=0$ otherwise. Then $S$ is the adjacency matrix of a digraph whose weakly connected components correspond to the situation in Lemma 5. We therefore obtain the following lemma.

Lemma 6

Each weakly connected component of the digraph corresponding to $S$ is a transitive tournament, hence has a unique source, target, and a path of length 1 from source to target defining a locally maximal SESE region. ∎

A closely related construction is the subject of §5.

4 The category of flow graphs

The principal goal of this section is merely to motivate and justify the details of the sequel. The key points are the introduction of the category ${\bf Dgph}$ of digraphs, and of its full subcategory ${\bf Flow}$ whose objects are flow graphs.

It is natural to attempt to regard transformations of mathematical objects as morphisms in an appropriate category [19]. Unfortunately, in many if not most cases involving digraphs, such an attempt is complicated by technicalities that commonly arise from loops [4]. The basic problem is that while identifying vertices should induce a graph morphism, such a morphism should also preserve edges. In particular, the morphism should preserve any edges between the vertices to be identified, necessarily inducing a loop. Insofar as we want loops in a coarse-grained control flow graph to correspond to actual loops in the atomic control flow, this is highly undesirable.

The common way around this problem is to treat loops on a separate footing. Following [4], define the category ${\bf Dgph}$ as follows. An object of ${\bf Dgph}$ is a reflexive digraph $G=(U,\alpha,\omega)$ given by a set $U$ and head and tail functions $\alpha,\omega:U\rightarrow U$ satisfying $\alpha\circ\omega=\omega$ and $\omega\circ\alpha=\alpha$. Meanwhile, for $G^{\prime}=(U^{\prime},\alpha^{\prime},\omega^{\prime})$, a morphism $f\in{\bf Dgph}(G,G^{\prime})$ is a function $f:U\rightarrow U^{\prime}$ satisfying $f\circ\alpha=\alpha^{\prime}\circ f$ and $f\circ\omega=\omega^{\prime}\circ f$.

The vertices of $G=(U,\alpha,\omega)$ are the (mutual) image $V\equiv V(G)$ of $\alpha$ and $\omega$; the loops are the set $L\equiv L(G):=\{u\in U:\alpha(u)=\omega(u)\}$ (so that $V\subseteq L$), and the edges are the set $E\equiv E(G):=U\backslash L$. 555 The usual notion of a digraph is recovered by considering $\alpha\times\omega$ and its appropriate restrictions on $U^{2}$, $L^{2}$, and $E^{2}$: e.g., we can abusively write $E=(\alpha\times\omega)(E^{2})$, where the LHS and RHS respectively refer to usual and reflexive notions of digraph edges.

Thus a morphism $f:U\rightarrow U^{\prime}$ restricts to $f|_{V}:V\rightarrow V^{\prime}$, $f|_{L}:L\rightarrow L^{\prime}$, and $f|_{E}:E\rightarrow U^{\prime}$. In particular, morphisms are only partially specified by their actions on vertices, and the following definition is essentially a convention about how to treat vertex identification by default.

We define ${\bf Flow}$ to be the full subcategory of ${\bf Dgph}$ whose objects are (combinatorially realized as) flow graphs. 666 As pointed out by D. Spivak, it would be desirable to describe flow graphs in terms of ${\bf Dgph}$, e.g. as algebras for some monad.

5 Coarsening flow graphs

We begin this section with intuition: the coarsening of a flow graph $G$ is obtained by taking each leaf of its PST and absorbing the interior of the corresponding sub-flow graph into its source. (See Figure 6.) The details are below.

For $G\in{\bf Dgph}$, define the absorption of $k$ into $j$ to be the morphism in ${\bf Dgph}$ (or the morphism’s image, depending on context) which corresponds to identifying $k$ with $j$, and in the case $k\neq j$ subsequently annihilating any loop at $j$ (by mapping it to the vertex $j$). It is clear that first absorbing $k$ and then $m$ into $j$ is equivalent to first absorbing $m$ and then $k$ into $j$. Consequently, for $U\subseteq V(G)$ we may define the absorption of $U$ into $j$ in the obvious way. 777 Failing to make fixed choices about whether to preserve or annihilate loops from, or formed at, absorbed and absorbing vertices amounts to a context-driven decision about the absorption process that is unlikely to be of any utility and need not be considered. Therefore, we proceed here to consider the space of such possible fixed choices. In the context of control flow graphs, a loop corresponds closely to a do-while construct. With this in mind, preserving such a construction under absorption corresponds to inserting additional computations into a do-while loop, or forming a new do-while loop around existing computations, altering the control flow. Meanwhile, annihilating loops corresponds to embedding the do-while construct within a larger sequence of computations, preserving the control flow. This is prima facie cause to restrict consideration to the definition of absorption introduced above.

For $G,H\in{\bf Flow}$ with $H\subset G$, define the absorption of $H$ to be the result of absorbing the interior of $H$ into its source (considered as a vertex in $G$). This amounts to replacing $H$ with a single edge between its source and target. Finally, define the coarsening $\circledcirc G$ of $G$ to be the result of absorbing all of the sub-flow graphs corresponding to leaves of the program structure tree of $G$. The fact that $\circledcirc G$ is well-defined follows from [16] (cf. the “prime subprogram parse” of [28]) along with the preceding considerations. In particular, the definitions of absorption and coarsening yield the following technical lemma.

Lemma 7

Let $G\in{\bf Flow}$ and let $\circledcirc G$ result from absorbing the vertex sets $L_{k}$ into $k$ for all $k\in K$ (so that $L_{k}$ corresponds to a leaf of the program structure tree and $k\not\in L_{k}$). Let $L:=\cup_{k\in K}L_{k}$ (this set should not be confused with the set of loops in $G$) and $J:=V\backslash(K\cup L)$, so that $V=J\cup K\cup L$ and $J,K,L$ are mutually disjoint. Let $j,j^{\prime}\in J$; $k,k^{\prime}\in K$ with $k\neq k^{\prime}$, and $\ell,\ell^{\prime}\in L$. Finally, write $L_{k}^{+}:=\{k\}\cup L_{k}$ and let $g\in V$. Then the adjacency matrix of $\circledcirc G$ w.r.t. the vertex set of $G$ is $A^{\prime}$, where $A^{\prime}_{jj^{\prime}}=A_{jj^{\prime}}$, $A^{\prime}_{jk^{\prime}}=\bigvee_{\ell^{\prime}\in L_{k^{\prime}}^{+}}A_{j\ell^{\prime}}$, $A^{\prime}_{kj^{\prime}}=\bigvee_{\ell\in L_{k}^{+}}A_{\ell j^{\prime}}$, $A^{\prime}_{kk^{\prime}}=\bigvee_{\ell\in L_{k}^{+},\ell^{\prime}\in L_{k^{\prime}}^{+}}A_{\ell\ell^{\prime}}$, and $A^{\prime}_{kk}=A^{\prime}_{g\ell^{\prime}}=A^{\prime}_{\ell g^{\prime}}=0$. ∎

The real matter of substance in coarsening a flow graph is producing the sets $J$, $K$, and $L$ referred to just above (it turns out to be easier to construct the $L_{k}$ from $L$ than to go in the opposite direction).

Theorem 5.1

Using the notation of the preceding lemma, define a matrix $M$ as follows. For each leaf $(e_{1},e_{2})$ of the program structure tree, let $(e_{1},e_{2})^{\circ}$ denote its interior, and for all $j\in(e_{1},e_{2})^{\circ}$ set $M_{j,s(e_{1})}=1$. Then $M$ is the adjacency matrix of a DAG (in fact, a forest) whose weakly connected components have vertex sets $L_{k}^{+}$ and corresponding targets $k$.

Having considered coarsening flow graphs, we note that the appropriate mathematical formalization in the opposite direction—i.e., of inserting one flow graph into another 888Note that we are not explicitly considering the insertion of loops in this setting.—is captured by the assertion that flow graphs form a (symmetric) operad [18, 21, 27] (cf. [25, 26]). At a high level, an operad is a collection of objects that “plug into each other” like maps $f_{(m)}:X^{m}\rightarrow X$ à la

[TABLE]

Let $P(n)$ denote the set of flow graphs with $n$ ordered edges and define the following family of maps

[TABLE]

by replacing, for each $1\leq j\leq n$, the $j$th edge in $G$ with $G_{j}$ in the obvious way. Writing $k_{0}\equiv 0$, the edge ordering on $G\circ(G_{1},\dots,G_{n})$ is obtained by assigning edges $\sum_{i=0}^{j-1}k_{i}+1,\dots,\sum_{i=0}^{j}k_{i}$ to $G_{j}\hookrightarrow G\circ(G_{1},\dots,G_{n})$ in the same order as the edges of $G_{j}$, i.e., the edge ordering is inherited from its local components.

Definition-checking or direct comparison to other insertion operads (e.g. the little $d$-disks or $d$-cubes operads in ${\bf Top}$) yields the following

Theorem 5.2

The triple $\{e,\{P(n)\}_{n=1}^{\infty},\circ\}$, where $e$ denotes the flow graph with one edge, forms an operad (in ${\bf Set}$). ∎

Thus the operadic composition $\circ$ and coarsening $\circledcirc$ operations are not only natural, but complementary, and we readily obtain the following lemma.

Lemma 8

If $G\in P(n)$ and $\circledcirc G_{j}=e\neq G_{j}$, then $\circledcirc(G\circ(G_{1},\dots G_{n}))=G$. ∎

6 Tensoring flow graphs

6.1 Tensoring in series

There is an essentially trivial tensor product on ${\bf Flow}$. The idea is simply to identify the exit edge of the first flow graph with the entry edge of the second flow graph, i.e., to combine flow graphs in series. The reason that this tensor product structure is interesting and useful is that it allows us a way to model additional structure in an enriched category. Specifically, this leads to the ${\bf Flow}$-category ${\bf SubFlow}_{G}$ of sub-flow graphs of a flow graph $G$.

We provide a quick sketch of the details here. Let $f\in{\bf Flow}(G,G_{f})$ and $f^{\prime}\in{\bf Flow}(G^{\prime},G^{\prime}_{f^{\prime}})$ with $V(G)\cap V(G^{\prime})=\varnothing$. Define $G\boxtimes G^{\prime}$ to be the flow graph obtained by identifying the exit edge of $G$ and the entry edge of $G^{\prime}$, and define $f\boxtimes f^{\prime}$ to be the morphism in ${\bf Flow}(G\boxtimes G^{\prime},G_{f}\boxtimes G^{\prime}_{f^{\prime}})$ obtained by identifying the output of $f$ on the exit edge of $G$ with that of $f^{\prime}$ on the entry edge of $G^{\prime}$.

The following lemmas are straightforward.

Lemma 9

${\bf Flow}$* is a monoidal category with tensor product given by $\boxtimes$, and with unit object the flow graph $e$ consisting of a single edge. ∎*

Lemma 10

For a generic flow graph $G$, we can form a category ${\bf SubFlow}_{G}$ enriched [17] over ${\bf Flow}$ as follows:

• •

${\bf SubFlow}_{G}:=E(G)$; 999In particular, loops and reflexive self-edges are not included here, though the former may be accommodated without substantial changes.

• •

for $e_{s},e_{t}\in{\bf SubFlow}_{G}$, the hom object ${\bf SubFlow}_{G}(e_{s},e_{t})\in{\bf Flow}$ is the (possibly empty) flow graph with entry edge $e_{s}$ and exit edge $e_{t}$;

• •

the composition morphism is induced by $\boxtimes$;

• •

the identity element is determined by the flow graph $e$ with one edge. ∎

An important advantage of ${\bf SubFlow}_{G}$ over the path category of $G$ is that the former is finite (and the preceding sections essentially detail its construction), whereas the latter is infinite whenever there is a cycle in $G$.

6.2 Tensoring in parallel

In this section we show that ${\bf Flow}$ carries a nontrivial monoidal structure (i.e., there is a tensor product operation that coherently combines flow graphs “in parallel” and not merely “in series” [6]). While the concept is rather obvious, the details are technical and we consequently make them explicit. In particular, although ${\bf Flow}$ is conceptually rather similar to the categories of $n$-cobordisms or tangles, the disjoint union only yields a tensor product in the latter cases: here, it must be modified to account for flow graphs whose entry and exit edges are identical or adjacent.

Let $s(e^{+}),t(e^{+}),s(e^{-}),t(e^{-})$ be four fixed distinct points not contained in the vertex set of any graph already under consideration, so that $e^{\pm}:=(s(e^{\pm}),t(e^{\pm}))$ may be regarded as two separated abstract edges. If $G$ is a flow graph with entry edge $e_{s}$ and (possibly adjacent or even identical) exit edge $e_{t}$, define a ${\bf Dgph}$-morphism (i.e., the image may not be a flow graph) $\phi_{G}$ by the vertex/loop map

[TABLE]

along with the extension to edges determined by not sending edges to (diagonal/reflexive edges or) loops.

Intuitively, if the entry and exit edges of $G$ are neither identical nor adjacent, then $\phi_{G}$ maps them respectively to $e^{+}$ and $e^{-}$: otherwise, $\phi_{G}$ maps the entry edge to $e^{+}$ and everything else (vertices and edges to the vertex; loops to a loop) to $t(e^{+})$. The rationale for the latter case is that it is the only really generic and consistent way for us to complete the definition of such a nontrivial ${\bf Dgph}$-morphism from a flow graph, and in fact this sort of definitional guidance is perhaps the primary rationale for invoking category theory ab initio.

The following lemma is straightforward.

Lemma 11

With $j,k\in V(G)$ with $j\neq k$ and $j^{\prime},k^{\prime}\in V(G^{\prime})$ with $j^{\prime}\neq k^{\prime}$, $\phi_{G}(j)=\phi_{G}(k)\Rightarrow\{j,k\}=\{t(e_{s}),t(e_{t})\}$; similarly, $\phi_{G^{\prime}}(j^{\prime})=\phi_{G^{\prime}}(k^{\prime})\Rightarrow\{j^{\prime},k^{\prime}\}=\{t(e^{\prime}_{s}),t(e^{\prime}_{t})\}$. ∎

If $V(G)\cap V(G^{\prime})=\varnothing$, we define

[TABLE]

where the equivalence relation on the disjoint (graph) union is determined, for $j,k\in V(G)$ with $j\neq k$ and $j^{\prime},k^{\prime}\in V(G^{\prime})$ with $j^{\prime}\neq k^{\prime}$, by

[TABLE]

where we use the shorthands $\star:=(t(e^{\prime}_{s})\neq s(e^{\prime}_{t}))\wedge(e^{\prime}_{s}\neq e^{\prime}_{t})$; $\star^{\prime}:=(t(e_{s})\neq s(e_{t}))\wedge(e_{s}\neq e_{t})$; $\star[j]:=(t(e_{s})=s(e_{t}))\wedge(j\in\{t(e_{s}),t(e_{t})\})\Rightarrow\star$, and $\star[j^{\prime}]:=(t(e^{\prime}_{s})=s(e^{\prime}_{t}))\wedge(j^{\prime}\in\{t(e^{\prime}_{s}),t(e^{\prime}_{t})\})\Rightarrow\star^{\prime}$, with an obvious extension to edges. (Here $e^{\prime}_{s}$ and $e^{\prime}_{t}$ denote the entry and exit edges of $G^{\prime}$.)

Lemma 12

(6.2) indeed defines an equivalence relation.

The following lemma is straightforward.

Lemma 13

If $G$ and $G^{\prime}$ are flow graphs, then so is $G\otimes G^{\prime}$. Furthermore, if $e$ denotes the flow graph with a single edge, then $G\otimes e\cong e\otimes G\cong G$. ∎

Thus in particular we have inclusions $i_{G}:\phi_{G}(G)\hookrightarrow G\otimes G^{\prime}$ and $i^{\prime}_{G^{\prime}}:\phi_{G^{\prime}}(G^{\prime})\hookrightarrow G\otimes G^{\prime}$ given respectively by $i_{G}(\phi_{G}(j))=[(j,0)]$ and $i^{\prime}_{G^{\prime}}(\phi_{G^{\prime}}(j^{\prime}))=[(j^{\prime},1)]$, where as per usual practice $[\cdot]$ indicates an equivalence class under $\sim$. $G\otimes G^{\prime}$ is a flow graph formed by identifying the entry edges of $G$ and $G^{\prime}$, and identifying the respective exit edges if this does not affect the interiors of the factors, and otherwise collapsing the smaller factor in a way that sufficiently extends the identification of entry edges.

Meanwhile, for $f\in{\bf Flow}(G,G_{f})$ and $f^{\prime}\in{\bf Flow}(G^{\prime},G^{\prime}_{f^{\prime}})$, we define $f\otimes f^{\prime}\in{\bf Flow}(G\otimes G^{\prime},G_{f}\otimes G^{\prime}_{f^{\prime}})$ as follows (see also Figure 7):

[TABLE]

along with the implied extension to edges.

Lemma 14

(5) is well-defined.

Theorem 6.1

${\bf Flow}$* is a monoidal category with tensor product $\otimes$ given by (3) and (5), and with unit object the flow graph $e$ consisting of a single edge.*

Corollary 2

$({\bf Flow},\otimes)$* is a symmetric monoidal category. ∎*

6.3 Remarks

The series and parallel tensor operations described above are very similar in spirit to the composition operations encountered in the study of so-called series-parallel graphs [2, 10] (cf. [9]). While the category-theoretical analysis of series and parallel tensor operations in the context of something like a system or wiring diagram has a very long history [1], a precise treatment appropriate to our development does not appear to be present in the literature.

7 Two-terminal graphs

Many of the considerations of the present paper have obvious analogues in the case of two-terminal graphs (TTGs). In particular, [28, 30] describes a multiresolution decomposition of TTGs (cf. [11]) that is a more granular version of the PST. This refined process structure tree reduces via a straightforward graph transformation (similar to that in §0.B) to constructing the SPQR tree [24].

Unfortunately, computing SPQR trees is a notoriously intricate exercise: indeed, a correct linear time algorithm was not actually implemented until 2000 [14], though an incorrect version of the same algorithm was first described in 1973 [15]. Today there is still not a completely explicit description of the correct linear time algorithm in the literature: for such an account it is necessary to refer to one of the two known publically available implementations in the C++ OGDF 101010http://www.ogdf.net/ and the Java jBPT 111111https://code.google.com/archive/p/jbpt/ frameworks. 121212An alternative algorithm is in [29], but we are not aware of an implementation. 131313For acyclic TTGs it is not hard to see that the analogue of SESE regions are vertex pairs $(j,k)$ s.t. $D_{jk}D^{\dagger}_{jk}-\delta_{jk}=1$, but the cyclic case is much harder.

While the computation and properties of the fundamental decomposition for TTGs are more involved than the PST, some analogues of the constructions detailed in this paper are simpler since TTGs are defined to omit loops. On the other hand, one minor complication relative to flow graphs that informs notions of coarsening and inclusion operads for TTGs is that some TTGs can have their sources and targets swapped. A more significant (and perhaps surprising) complication is that it is not clear how to define a canonical parallel tensor operation for TTGs: the principal difficulty is the unit object. Lacking such an operation would be a significant shortcoming relative to the framework for flow graphs, as parallel tensoring in ${\bf Flow}$ corresponds to introducing an if/else statement in control flow.

8 Conclusion

Besides applications to understanding and manipulating programs mentioned in §1, our particular notion of a flow graph naturally yields an interesting category that readily admits explicit representations and manipulations in (and of!) software. While some of the constructions involved are somewhat delicate and inelegant (for example, much of §6.2), this is due to properly accounting for degenerate cases that are of little practical concern but that nevertheless constrain practical and principled techniques for representing, reasoning about, and composing program artifacts.

Put another way, requiring that flow graphs exhibit category-theoretical desiderata places strong but satisfiable restrictions on them that can usefully inform the architecture of program analysis platforms, program synthesizers, compilers, etc. More generally, category theory allows us to address corner cases in the construction and manipulation of data structures whose resolution is not obvious.

Acknowledgements

We thank Brendan Fong, Artem Polyvyanyy, and David Spivak for helpful comments.

Appendix 0.A Proofs

Proof (Lemma 4)

The only thing to show is that $e_{3}\text{ pdom }e_{2}$. It must be the case that either $e_{2}\text{ pdom }e_{3}$ or $e_{3}\text{ pdom }e_{2}$, so assume the former. Since $e_{2}\text{ dom }e_{3}$ also, we must have that any source-target path traversing $e_{3}$ contains a cycle of the form $(e_{2},\dots,e_{3},\dots,e_{2})$ by Lemma 2; deleting all cycles from this path yields a source-target path traversing $e_{2}$ but not $e_{3}$. Reversing this path yields a contradiction to the assumption that $e_{2}\text{ pdom }e_{3}$. ∎

Proof (Theorem 3.1)

[Although our definition of the interior of a SESE differs in a slight but critical way from from [16], the proof is a mostly straightforward adaptation of the original attempt. That said, we also fix a minor gap of the original attempt for case ii).]

Let $(e_{1},e_{2})$ and $(e^{\prime}_{1},e^{\prime}_{2})$ be distinct canonical SESE regions whose interiors are not disjoint, and let $v$ be in their intersection. Since $e_{1}\text{ dom }v$ and $e^{\prime}_{1}\text{ dom }v$, it must be that either $e_{1}\text{ dom }e^{\prime}_{1}$ or $e^{\prime}_{1}\text{ dom }e_{1}$: assume the former w.l.o.g. Similarly, since $e_{2}\text{ pdom }v$ and $e^{\prime}_{2}\text{ pdom }v$, either $e_{2}\text{ pdom }e^{\prime}_{2}$ or $e^{\prime}_{2}\text{ pdom }e_{2}$: in the former case, $(e^{\prime}_{1},e^{\prime}_{2})\subset(e_{1},e_{2})$ and we are done, so assume the latter case. We now have three cases to consider: i) $e_{2}=e^{\prime}_{1}$; ii) $e_{2}\neq e^{\prime}_{1}$ and $e^{\prime}_{1}\text{ dom }e_{2}$; and iii) $e_{2}\neq e^{\prime}_{1}$ and $e^{\prime}_{1}$ does not dominate $e_{2}$. We shall show that each case leads to a contradiction.

Case i). Since in this case $e_{2}=e^{\prime}_{1}$, we have that $e_{2}\text{ dom }v$ and $e_{2}\text{ pdom }v$, so it must be that any path from the source to the target that traverses $v$ must contain a cycle of the form $(e_{2},\dots,v,\dots,e_{2})$ by Lemma 2. But this means that $v$ cannot be in the interior of $(e_{1},e_{2})$, a contradiction: hence case i) cannot hold.

Case ii). Since in this case $e^{\prime}_{1}\text{ dom }e_{2}$ and generically $e_{1}\text{ dom }e^{\prime}_{1}$, we may decompose any path $\gamma_{02}$ from the source to $e_{2}$ (using an obvious notation) as $\gamma_{02}\equiv\gamma_{01}\gamma_{11^{\prime}}\gamma_{1^{\prime}2}$. Meanwhile since $e_{2}\text{ pdom }e_{1}$, we may decompose any path $\gamma_{1\infty}$ from $e_{1}$ to the target as $\gamma_{1\infty}\equiv\gamma_{12}\gamma_{2\infty}$. Taken together, these decompositions imply that we can decompose any path from the source to the target that traverses $e^{\prime}_{1}$ as $\gamma_{01}\gamma_{11^{\prime}}\gamma_{1^{\prime}2}\gamma_{2\infty}$, so that $e_{2}\text{ pdom }e^{\prime}_{1}$ and $e^{\prime}_{1}\text{ pdom }e_{1}$.

Moreover, if there is a cycle that traverses $e_{1}$, it also traverses $e_{2}$ and vice versa, so we may write such a cycle as $\omega_{12}\equiv\gamma_{12}\gamma_{21}$, where $\gamma_{12}\equiv\gamma_{11^{\prime}}\gamma_{1^{\prime}2}$ as above. Hence such a cycle $\omega_{12}$ must traverse $e^{\prime}_{1}$. Similarly, if there is a cycle that traverses $e^{\prime}_{1}$, it also traverses $e^{\prime}_{2}$ and vice versa, so we may write such a cycle as $\omega_{1^{\prime}2^{\prime}}\equiv\gamma_{1^{\prime}2^{\prime}}\gamma_{2^{\prime}1^{\prime}}$, where $\gamma_{1^{\prime}2^{\prime}}$ traverses $e_{2}$ since $e^{\prime}_{2}\text{ pdom }e_{2}$. Hence such a cycle $\omega_{1^{\prime}2^{\prime}}$ must traverse $e_{2}$. It follows that $(e^{\prime}_{1},e_{2})$ is a SESE region.

Since both $(e_{1},e_{2})$ and $(e^{\prime}_{1},e^{\prime}_{2})$ are canonical SESE regions, we have that $e_{1}\text{ pdom }e^{\prime}_{1}$ and $e^{\prime}_{2}\text{ dom }e_{2}$. At the same time, $e^{\prime}_{1}\text{ pdom }e_{1}$, so it must be that $e_{1}=e^{\prime}_{1}$. It follows that $(e_{1},e^{\prime}_{2})$ is also a SESE region, and therefore also that $e_{2}\text{ dom }e^{\prime}_{2}$, so it must be that $e_{2}=e^{\prime}_{2}$. This contradicts the hypothesis that $(e_{1},e_{2})$ and $(e^{\prime}_{1},e^{\prime}_{2})$ are distinct: hence case ii) cannot hold.

Case iii). Since in this case $e^{\prime}_{1}$ does not dominate $e_{2}$, there is a path $\gamma_{02}$ from the source to $e_{2}$ that avoids $e^{\prime}_{1}$. Suppose that $e^{\prime}_{1}$ does not postdominate $e_{2}$, i.e., suppose that there is a path $\gamma_{2\infty}$ from $e_{2}$ to the target that avoids $e^{\prime}_{1}$. Then since $e^{\prime}_{2}\text{ pdom }e_{2}$, $\gamma_{2\infty}$ must traverse $e^{\prime}_{2}$. But since $e^{\prime}_{1}\text{ dom }e^{\prime}_{2}$ and the concatenated path $\gamma\equiv\gamma_{02}\gamma_{2\infty}$ from the source to the target traverses $e^{\prime}_{2}$, it must be that $\gamma_{2\infty}$ traverses $e^{\prime}_{1}$, contradicting the assumption that $e^{\prime}_{1}$ does not postdominate $e_{2}$. Therefore since $e^{\prime}_{1}\text{ pdom }e_{2}$ and $e_{2}\text{ pdom }v$, we have that $e^{\prime}_{1}\text{ pdom }v$. Moreover, $e^{\prime}_{1}\text{ dom }v$, so any path from the source to the target that traverses $v$ must contain a cycle of the form $(e^{\prime}_{1},\dots,v,\dots,e^{\prime}_{1})$ by Lemma 2. But this means that $v$ cannot be in the interior of $(e^{\prime}_{1},e^{\prime}_{2})$. By contradiction, case iii) cannot hold. ∎

Proof (Lemma 5)

Suppose w.l.o.g. that $(e_{0},e_{\infty})$ is not minimal. Then at least one of the following is true: i) there exists a nondegenerate SESE region $(e_{0},e_{1})$ such that $e_{\infty}$ does not dominate $e_{1}$; ii) there exists a nondegenerate SESE region $(e_{-1},e_{\infty})$ such that $e_{0}$ does not postdominate $e_{-1}$. Consider case i), and assume w.l.o.g. that $(e_{0},e_{1})$ is minimal (otherwise, we have at least one of case i) or ii) again). Then $e_{1}\text{ dom }e_{\infty}$, so $(e_{1},e_{\infty})$ is a nondegenerate SESE region and we can write $(e_{0},e_{\infty})=(e_{0},e_{1})\cup(e_{1},e_{\infty})$. Exactly similar reasoning informs case ii), and an induction establishes the lemma. ∎

Proof (Theorem 5.1)

Let $(e_{1},e_{2})$ be a leaf of the PST. If $s(e_{1})$ is in the interior of some other leaf $(e_{1}^{\prime},e_{2}^{\prime})$ of the PST, then $e_{1}=e_{2}^{\prime}$. Therefore, $M_{s(e_{2}^{\prime}),s(e_{1}^{\prime})}=1$ and any other vertices $j$ with $M_{j,s(e_{1}^{\prime})}=1$ correspond to the remaining elements of $(e_{1}^{\prime},e_{2}^{\prime})^{\circ}$, which are leaves in the digraph $G_{M}$ with adjacency matrix $M$. On the other hand, if $s(e_{1})$ is not in the interior of some other leaf of the PST, then it is a target in $G_{M}$. The result follows. ∎

Proof (Lemma 12)

Since it is obvious from the structure of $\star[j]$ and $\star[j^{\prime}]$ that $(j^{\prime},1)\sim(j,0)\iff(j,0)\sim(j^{\prime},1)$, the only thing to show is transitivity. A (perhaps unnecessarily) mechanical proof consists of verifying each of the eight assertions $(\ell_{1,b_{1}},b_{1})\sim(\ell_{2,b_{2}},b_{2})\sim(\ell_{3,b_{3}},b_{3})\Rightarrow(\ell_{1,b_{1}},b_{1})\sim(\ell_{3,b_{3}},b_{3})$ for $(b_{1},b_{2},b_{3})\in\{0,1\}^{3}$ and $\ell_{1,b_{1}},\ell_{2,b_{2}},\ell_{3,b_{3}}$ distinct.

First, consider $(b_{1},b_{2},b_{3})=(0,0,0)$: we must show in this case that $(\phi_{G}(\ell_{10})=\phi_{G}(\ell_{20})=\phi_{G}(\ell_{30}))\wedge\star$ implies $(\phi_{G}(\ell_{10})=\phi_{G}(\ell_{30}))\wedge\star$, but this is trivial.

Next, consider $(b_{1},b_{2},b_{3})=(0,0,1)$. Here we must show that $(\phi_{G}(\ell_{10})=\phi_{G}(\ell_{20})=\phi_{G^{\prime}}(\ell_{31}))\wedge\star\wedge\star[\ell_{20}]\wedge\star[\ell_{31}]$ implies $(\phi_{G}(\ell_{10})=\phi_{G^{\prime}}(\ell_{31}))\wedge\star[\ell_{10}]\wedge\star[\ell_{31}]$. By Lemma 11, $\{\ell_{10},\ell_{20}\}=\{t(e_{s}),t(e_{t})\}$, so $t(e_{s})=s(e_{t})$ and $\star[\ell_{10}]$ is true, establishing the desired result.

For $(b_{1},b_{2},b_{3})=(0,1,0)$, we must show that $(\phi_{G}(\ell_{10})=\phi_{G^{\prime}}(\ell_{21})=\phi_{G}(\ell_{30}))\wedge\star[\ell_{10}]\wedge\star[\ell_{21}]\wedge\star[\ell_{30}]$ implies $(\phi_{G}(\ell_{10})=\phi_{G}(\ell_{30}))\wedge\star$. By Lemma 11, $\{\ell_{10},\ell_{30}\}=\{t(e_{s}),t(e_{t})\}$, so $t(e_{s})=s(e_{t})$ and $\ell_{10},\ell_{30}\in\{t(e_{s}),t(e_{t})\}$. Since in the present case both $\star[\ell_{10}]$ and $\star[\ell_{30}]$ are true by assumption and we have just shown their hypotheses true, their mutual conclusion $\star$ is also true here. This yields the desired implication. (NB. Although $\star[\ell_{21}]$ is true in this case, neither its hypothesis nor its conclusion are.)

By symmetry, the last case we need to consider is $(b_{1},b_{2},b_{3})=(0,1,1)$: we need to show here that $(\phi_{G}(\ell_{10})=\phi_{G^{\prime}}(\ell_{21})=\phi_{G^{\prime}}(\ell_{31}))\wedge\star[\ell_{10}]\wedge\star[\ell_{21}]\wedge\star^{\prime}$ implies $(\phi_{G}(\ell_{10})=\phi_{G^{\prime}}(\ell_{31}))\wedge\star[\ell_{10}]\wedge\star[\ell_{31}]$. By Lemma 11, $\{\ell_{21},\ell_{31}\}=\{t(e^{\prime}_{s}),t(e^{\prime}_{t})\}$, so $t(e^{\prime}_{s})=s(e^{\prime}_{t})$ and $\star[\ell_{31}]$ is true, so we are done. ∎

Proof (Lemma 14)

We need to show that whenever $[(j,0)]=[(j^{\prime},1)]$ we also have $[(f(j),0)]=[(f^{\prime}(j^{\prime}),1)]$. An equivalent assertion is that whenever $\phi_{G}(j)=\phi_{G^{\prime}}(j^{\prime})$, we also have $\phi_{G_{f}}(f(j))=\phi_{G^{\prime}_{f^{\prime}}}(f^{\prime}(j^{\prime}))$. There are precisely four cases in which the hypothesis can hold, corresponding to the first four cases of (2) (note that the second case has four subcases). In the first case, both $[(f(j),0)]$ and $[(f^{\prime}(j^{\prime}),1)]$ must be the source of the entry edge in $G_{f}\otimes G^{\prime}_{f^{\prime}}$ since $f$ and $f^{\prime}$ are morphisms in ${\bf Flow}$; similarly, the other cases respectively give that both $[(f(j),0)]$ and $[(f^{\prime}(j^{\prime}),1)]$ must be the target of the entry edge, the source of the exit edge, and the target of the exit edge. ∎

Proof (Theorem 6.1)

We must establish two things: that $\otimes$ is a bifunctor, and that it satisfies the necessary coherence conditions.

To see that $\otimes$ is a bifunctor, first note that $(id_{G}\otimes id_{G^{\prime}})([(j,0)])=[(j,0)]=id_{G\otimes G^{\prime}}([(j,0)])$ by (5), and $(id_{G}\otimes id_{G^{\prime}})([(j^{\prime},1)])=[(j^{\prime},1)]=id_{G\otimes G^{\prime}}([(j^{\prime},1)])$, so that $id_{G}\otimes id_{G^{\prime}}=id_{G\otimes G^{\prime}}$. Now we must show that $(g\otimes g^{\prime})\circ(f\otimes f^{\prime})=(g\circ f)\otimes(g^{\prime}\circ f^{\prime})$. But this is easily seen since, again by (5), we have $(g\otimes g^{\prime})([(f(j),0)])=[(g(f(j)),0)]=((g\circ f)\otimes(g^{\prime}\circ f^{\prime}))([(j,0)])$ and similarly $(g\otimes g^{\prime})([(f^{\prime}(j^{\prime}),1)])=[(g^{\prime}(f^{\prime}(j^{\prime})),1)]=((g\circ f)\otimes(g^{\prime}\circ f^{\prime}))([(j^{\prime},1)])$. Since the action on edges follows trivially, $\otimes$ is indeed a bifunctor.

To see that the putative tensor product is coherent, we first note that the triangle equation turns out to be trivial, so we need only verify the pentagon equation, which we recall in Figure 8. The associator $\alpha_{G,G^{\prime},G^{\prime\prime}}:(G\otimes G^{\prime})\otimes G^{\prime\prime}\rightarrow G\otimes(G^{\prime}\otimes G^{\prime\prime})$ is given by

[TABLE]

along with the implied extension to edges. The explicit form of (6) makes it clear that the associator is bijective, and hence an isomorphism.

For notational convenience, let $W,X,Y,Z$ denote flow graphs with $(w,x,y,z)\in V(W)\times V(X)\times V(Y)\times V(Z)$. The three steps on the top of the pentagon are

[TABLE]

while the two steps on the bottom of the pentagon are

[TABLE]

The pentagon equation follows from the equality of the rightmost parts of (7) and (8), as does the theorem. ∎

Appendix 0.B Stretching flow graphs

By inserting new vertices and edges, we can transform many “approximate” flow graphs into bona fide sub-flow graphs that can then be captured by the PST.

Lemma 15 (“Sketch of stretch”)

Let $G$ be a flow graph. For each vertex $v\in G^{\circ}$, perform transformations indicated by the table below. The cumulative result of these transformations is well-defined; repeating them has no effect. ∎

[TABLE]

Call the result of the process sketched in lemma 15 the stretching of $G$. This construction is similar to the “normalization” of two-terminal graphs (see §7).

Corollary 3

There is a bijective correspondence between induced subgraphs with single sources and targets and SESE regions in a stretching. In particular, any loop corresponds to a minimal SESE region in a stretching. ∎

By considering the complete bipartite graph $K_{3,3}$, it is easy to show the following

Lemma 16

There exists a planar flow graph with a nonplanar stretching. ∎