Acyclicity and antisymmetry
Recently I worked out a graph-theoretic construction that Yun-Sheng needed in his project. Central to the correctness of the construction is the acyclicity of the intermediate graphs (which are directed), and since directed acyclic graphs are essentially partial orders (in particular, acyclicity is essentially antisymmetry), I wonder whether the construction can be described and reasoned about more cleanly if the construction is redone in relational calculus. This post experiments with the relational calculus approach on the first property appearing in the construction: an induced sub-graph of an acyclic directed graph is also acyclic. This property is rather intuitive — informally we can just say that any cycle in the sub-graph would be one in the original graph, which however doesn’t have cycles. Our aim is to formally reproduce the argument in relational calculus, which will be more detailed but ideally won’t be more complicated than the informal one. (But alas, my experiment result ends up being somewhat too complicated.)
A directed graph over a set $X$ of vertices is simply an endo-relation $R : X \leadsto X$ (which is my preferred notation for $R \subseteq X \times X$): there is an edge from $x : X$ to $x' : X$ exactly when $R$ relates $x$ to $x'$, which I write as $R\ x\ x'$.
If we want to talk about reachability in $R$, we can take its reflexive transitive closure $R^* : X \leadsto X$, so that to check whether $x'$ is reachable from $x$, we can simply ask whether $R^*\ x\ x'$. The reflexive transitive closure operation can be seen as the conversion of an endo-relation to the smallest preorder that contains the relation, so we can define the operation in terms of the Galois connection
$$ R^* \subseteq P \quad\Leftrightarrow\quad R \subseteq P $$
for all endo-relation $R$ and preorder $P$. Now if we want to say that $R$ has no cycle, the statement we need is exactly the antisymmetry of $R^*$
$$ R^* \cap {R^*}^\circ \subseteq \mathit{id} $$
(where $(^\circ)$ is the relational converse operation): given any potentially non-trivial cycle that leaves $x$ for some $x'$ (i.e., $R^*\ x\ x'$) and then goes back from $x'$ to $x$ (i.e., $(R^*)^\circ\ x\ x'$, which is just $R^*\ x'\ x$), $x$ must be equal to $x'$ (i.e., $\mathit{id}\ x\ x'$), that is, the cycle must be trivial; so any $x$ is reachable from itself only through the trivial cycle that doesn’t leave $x$ at all.
To deal with induced sub-graphs of $R$, we need to talk about subsets of $X$, and here we use the sub-object formulation from category theory (which may not be the right choice though, as we’ll see later). Given a subset $Y$ of $X$, there is an injection function $I_Y : Y \leadsto X$ (implicitly lifted to a relation); we’ll fix a particular $Y$ and omit the subscript $Y$ in $I_Y$ in the rest of this post. Being a total function, $I$ is simple (mapping every input to at most one output)
$$ I \cdot I^\circ \subseteq \mathit{id} $$
(where $(\cdot)$ is relational composition) and entire (mapping every input to at least one output)
$$ \mathit{id} \subseteq I^\circ \cdot I $$
which can actually be strengthened to
$$ I^\circ \cdot I = \mathit{id} $$
because $I$ is injective with $I^\circ$ as its left inverse. The sub-graph of $R$ induced by $Y$ is then $I^\circ \cdot R \cdot I : Y \leadsto Y$, where $I$ and $I^\circ$ are used to restrict the domain and codomain of $R$ to $Y$.
Our aim is to prove
$$ R^* \cap {R^*}^\circ \subseteq \mathit{id} \quad\Rightarrow\quad (I^\circ \cdot R \cdot I)^* \cap {(I^\circ \cdot R \cdot I)^*}^\circ \subseteq \mathit{id} $$
Intuitively, $I^\circ \cdot R \cdot I$ should be contained in $R$ since the former is a sub-graph of the latter, and then we could just invoke monotonicity:
\begin{equation} \text{‘}~ (I^\circ \cdot R \cdot I)^* \cap {(I^\circ \cdot R \cdot I)^*}^\circ \subseteq R^* \cap {R^*}^\circ \subseteq \mathit{id} ~\text{’} \label{conceptual} \end{equation}
But this is type-incorrect because in our formulation $Y$ is not necessarily a subset of $X$ — to be precise, $Y$ should be thought of as a set that’s used to index a subset of $X$, but $Y$ itself may have nothing to do with $X$. Therefore we need to wrap the leftmost relation of type $Y \leadsto Y$ in type-casts $I : Y \leadsto X$ and $I^\circ : X \leadsto Y$ to turn it to a relation of type $X \leadsto X$. These type-casts distribute into $(\cap)$ (via an inequality, which happily is the right direction for us):
\begin{equation} I \cdot ((I^\circ \cdot R \cdot I)^* \cap {(I^\circ \cdot R \cdot I)^*}^\circ) \cdot I^\circ \subseteq (I \cdot (I^\circ \cdot R \cdot I)^* \cdot I^\circ) \cap (I \cdot {(I^\circ \cdot R \cdot I)^*} \cdot I^\circ)^\circ \label{with-casts} \end{equation}
Comparing the right-hand side with Argument \ref{conceptual}, we see that it suffices to establish
\begin{equation} I \cdot (I^\circ \cdot R \cdot I)^* \cdot I^\circ \subseteq R^* \label{reachability} \end{equation}
which says that reachability in the sub-graph $I^\circ \cdot R \cdot I$ implies reachability in the original graph $R$, corresponding to our intuition. We can then properly formulate Argument \ref{conceptual},
\begin{align*} & I \cdot ((I^\circ \cdot R \cdot I)^* \cap {(I^\circ \cdot R \cdot I)^*}^\circ) \cdot I^\circ \\ \subseteq{} & \reason{Inequality \ref{with-casts}} \\ & (I \cdot (I^\circ \cdot R \cdot I)^* \cdot I^\circ) \cap (I \cdot {(I^\circ \cdot R \cdot I)^*} \cdot I^\circ)^\circ \\ \subseteq{} & \reason{Inequality \ref{reachability}; monotonicity of $(\cap)$ and $(^\circ)$} \\ & R^* \cap {R^*}^\circ \\ \subseteq{} & \reason{$R^*$ antisymmetric} \\ & \mathit{id} \end{align*}
which isn’t yet the antisymmetry of $(I^\circ \cdot R \cdot I)^*$ though. Fortunately, we can shunt the outermost $I$ and $I^\circ$ from the left to the right (by the simplicity and entirety of $I$),
$$ (I^\circ \cdot R \cdot I)^* \cap {(I^\circ \cdot R \cdot I)^*}^\circ \subseteq I^\circ \cdot I $$
and the right-hand side is again included in $\mathit{id}$ by the injectivity of $I$, establishing the antisymmetry.
It remains to verify Inequality \ref{reachability}. By shunting, the inequality is equivalent to
$$ (I^\circ \cdot R \cdot I)^* \subseteq I^\circ \cdot R^* \cdot I $$
It is tempting to use the Galois connection for $(^*)$; to do that we need to verify that $I^\circ \cdot R^* \cdot I$ is a preorder first, which isn’t difficult but isn’t completely trivial either — we’ll prove a generalisation later. Applying the Galois connection, we are left to verify
$$ I^\circ \cdot R \cdot I \subseteq I^\circ \cdot R^* \cdot I $$
which follows from
$$ R \subseteq R^* $$
This inequality is true but doesn’t look right however: it says that having an edge between some vertices $x$ and $x'$ implies that $x'$ is reachable from $x$, but this didn’t show up in our informal argument. What we expect is to have a simpler obligation like $I^\circ \cdot R \cdot I$ being included in $R$ (every edge of the sub-graph is an edge in the original graph), and then extend the obligation through the monotonicity of $(^*)$. To state this alternative obligation, again we insert type-casts:
\begin{equation} I \cdot I^\circ \cdot R \cdot I \cdot I^\circ \subseteq R \label{inclusion} \end{equation}
This is true because of the simplicity of $I$ (which says that $I \cdot I^\circ$ is coreflexive, so $I \cdot I^\circ : X \leadsto X$ acts as a predicate on $X$ picking out those vertices in $Y$). By the monotonicity of $(^*)$ the above is then extended to
$$ (I \cdot I^\circ \cdot R \cdot I \cdot I^\circ)^* \subseteq R^* $$
Comparing this with Inequality \ref{reachability}, we see that we’re done if we can establish
$$ I \cdot (I^\circ \cdot R \cdot I)^* \cdot I^\circ \subseteq (I \cdot I^\circ \cdot R \cdot I \cdot I^\circ)^* $$
This is in fact an equality, and can be proved by indirect reasoning: for all preorder $P$,
\begin{align*} & I \cdot (I^\circ \cdot R \cdot I)^* \cdot I^\circ \subseteq P \\ \Leftrightarrow{}& \reason{shunting} \\ & (I^\circ \cdot R \cdot I)^* \subseteq I^\circ \cdot P \cdot I \\ \Leftrightarrow{}& \reason{Galois connection for $(^*)$ (see below)} \\ & I^\circ \cdot R \cdot I \subseteq I^\circ \cdot P \cdot I \\ \Leftrightarrow{}& \reason{shunting} \\ & I \cdot I^\circ \cdot R \cdot I \cdot I^\circ \subseteq P \\ \Leftrightarrow{}& \reason{Galois connection for $(^*)$} \\ & (I \cdot I^\circ \cdot R \cdot I \cdot I^\circ)^* \subseteq P \end{align*}
In the middle, again to use the Galois connection for $(^*)$ we need to show that $I^\circ \cdot P \cdot I$ is a preorder (assuming that $P$ is), and here’s a quick proof: for reflexivity,
$$ \mathit{id} \subseteq I^\circ \cdot I \subseteq I^\circ \cdot P \cdot I $$
and for transitivity,
$$ (I^\circ \cdot P \cdot I) \cdot (I^\circ \cdot P \cdot I) \subseteq I^\circ \cdot P \cdot P \cdot I \subseteq I^\circ \cdot P \cdot I $$
Overall, the formal reasoning indeed mirrors our informal argument: from Inequality \ref{inclusion}, which says that edges of the sub-graph are also edges of the original graph, we get to Inequality \ref{reachability} saying that reachability in the sub-graph implies reachability in the original graph, and then all it takes to reduce acyclicity of the sub-graph to acyclicity of the original graph is just monotonicity. What complicate the formal reasoning are the type-casts, which make one wonder whether they can be dealt with more easily. Until then, while there’s certain elegance that can be seen in the relational calculus approach, the calculation is just too heavyweight for such a simple property.
