98 Graph Theory — Reach
98.1 Overview
This module defines graph reachability over a list of weighted edges \((\mathtt{WEdge}\, n)\) using the reflexive–transitive closure of symmetric adjacency, and establishes its core structural properties: symmetry, monotonicity under edge-list inclusion, a cons-decomposition lemma, and lemmas relating total weight to list membership.
98.2 Declarations
Given a list of weighted edges \(\mathit{edges}\) on \(n\) vertices, \(\mathtt{SymAdj}\, \mathit{edges}\, u\, v\) holds when there exists an edge \(e \in \mathit{edges}\) whose endpoints are \(\{ u, v\} \) (in either order), i.e. \((e.u = u \wedge e.v = v) \vee (e.u = v \wedge e.v = u)\).
\(\mathtt{Reach}\, \mathit{edges}\) is the reflexive–transitive closure of \(\mathtt{SymAdj}\, \mathit{edges}\); that is, \(\mathtt{Reach}\, \mathit{edges}\, u\, v\) holds when \(u\) and \(v\) are connected by a path through edges in \(\mathit{edges}\).
The total weight of an edge list is the sum of the weights of all its edges: \(\mathtt{totalWeight}\, \mathit{edges} = \sum _{e \in \mathit{edges}} e.\mathit{weight}\).
\(\mathtt{SpansLike}\, F\, E\) holds when the edge list \(F\) is at least as connected as \(E\): for every pair of vertices \(u, v\), if \(u\) and \(v\) are reachable in \(E\) then they are also reachable in \(F\).
If \(\mathtt{SymAdj}\, \mathit{edges}\, u\, v\) then \(\mathtt{SymAdj}\, \mathit{edges}\, v\, u\).
If \(\mathtt{SymAdj}\, e_1\, u\, v\) and every edge of \(e_1\) also belongs to \(e_2\), then \(\mathtt{SymAdj}\, e_2\, u\, v\).
If \(\mathtt{Reach}\, \mathit{edges}\, u\, v\) then \(\mathtt{Reach}\, \mathit{edges}\, v\, u\).
If \(\mathtt{Reach}\, e_1\, u\, v\) and every edge of \(e_1\) also belongs to \(e_2\), then \(\mathtt{Reach}\, e_2\, u\, v\).
If \(e \in \mathit{edges}\) then \(\mathtt{Reach}\, \mathit{edges}\, e.u\, e.v\); that is, the two endpoints of any listed edge are immediately reachable from each other.
If every symmetric adjacency in \(\mathit{edges}\) implies reachability in \(\mathit{edges}'\), and \(\mathtt{Reach}\, \mathit{edges}\, u\, v\), then \(\mathtt{Reach}\, \mathit{edges}'\, u\, v\).
For a non-empty edge list \((g :: \mathit{rest})\), \(\mathtt{Reach}\, (g :: \mathit{rest})\, a\, b\) if and only if one of three cases holds: (1) \(\mathtt{Reach}\, \mathit{rest}\, a\, b\); (2) \(\mathtt{Reach}\, \mathit{rest}\, a\, g.u\) and \(\mathtt{Reach}\, \mathit{rest}\, g.v\, b\); or (3) \(\mathtt{Reach}\, \mathit{rest}\, a\, g.v\) and \(\mathtt{Reach}\, \mathit{rest}\, g.u\, b\).
If two edge lists \(l_1\) and \(l_2\) have the same elements (i.e. \(\forall x,\; x \in l_1 \leftrightarrow x \in l_2\)), then \(\mathtt{Reach}\, l_1\, a\, b \leftrightarrow \mathtt{Reach}\, l_2\, a\, b\).
\(\mathtt{totalWeight}\, ([] : \mathtt{List}\, (\mathtt{WEdge}\, n)) = 0\).
If \(e \in \mathit{edges}\) then \(\mathtt{totalWeight}\, \mathit{edges} = e.\mathit{weight} + \mathtt{totalWeight}\, (\mathit{edges}.\mathtt{erase}\, e)\).