Last August, we finally published an article based on an idea I proposed back in 2022 and contributed to implementing over the following years. This idea is not explicitly stated in the article itself, but here is the gist of it.
In type theory, the most general representation of a directed graph is usually considered to be the function A → A → U, where A is the type of graph vertices and U is the universe (“type of types”), i.e., a homogeneous binary predicate. Using the classical equivalence (see, for example, HoTT book, 4.8.3) ∑[T:U] (T → A) ≃ (A → U), we can transform the definition of a graph into a pair { edge : A → U, adj : (from : A) → edge from → A }. This is a representation as an adjacency map, which maps the initial vertices to edge constructions and can extract the terminal vertex from them. By specializing this construction for finite graphs and data structures, we obtain the classical representations of an adjacency matrix/list.
So the idea behind the article is that such a representation is convenient for working at the logical level as well, at least for algorithms that behave as depth-first search, i.e., start from one vertex and recursively traverse all edges from it. In particular, since we can squeeze the directed graph into a finite map, it can be used as a partial commutative monoid (PCM) in separation logic. The (partial) operation of a monoid is defined as the disjoint union of maps with non-intersecting domains. For this to work, we have to assume that graphs can be partial, i.e., allow hanging edges where the initial vertex lies in the desired subgraph and the terminal vertex potentially lies outside it. When combining partial graphs, dangling edges are resolved into regular edges by sticking to their terminal vertices.
In classical separation logic, a PCM of heaps is typically the main one. Once we have a second PCM, we can consider mappings (morphisms) between them, as well as endomorphisms on the graphs themselves. In this case, a morphism is a function that preserves the monoidal operation, f(γ₁∙γ₂) = fγ₁∙fγ₂. This allows us to extend the concept of framing to graphs — in the article, we call this “contextual localization.” In other words, morphisms allow us to extract a piece of a graph, perform some operation on it, and then automatically glue it back to the unaffected remaining part, which greatly simplifies a number of proofs. In particular, high-level combinators over the encoding of graphs as finite maps are morphisms — map, filter, as well as more ad-hoc functions such as sinks, extracting a set of terminal vertices. Graph reachability is not a morphism in itself, but it interacts conveniently with the filter morphism, allowing us to “cut out” fragments of reachable components.
We use this apparatus to create a library for working with graphs in Hoare Type Theory and to construct two formal proofs of the imperative of Schorr-Waite algorithm (marking a binary graph where the traversal stack is stored in the graph itself through edge inversion, without allocating separate memory) and union-find (constructing disjoint equivalence classes). The proofs turned out to be quite compact (110 lines for Schorr-Waite, 49 for union-find).
The limitation of the described technique stems from the original idea: it is natural for algorithms that explore a graph by following edges. Algorithms that work with edges more “globally” (for example, https://en.wikipedia.org/wiki/Kruskal%27s_algorithm) will likely require other representations.