POPL Paper—Formalising Graph Algorithms with Coinduction
New paper: “Formalising Graph Algorithms with Coinduction”, by myself and Nicolas Wu, will be published at POPL 2025.
The preprint is available here.
The paper is about representing graphs (especially in functional languages). We argue in the paper that graphs are naturally coinductive, rather than inductive, and that many of the problems with graphs in functional languages go away once you give up on induction and pattern-matching, and embrace the coinductive way of doing things.
Of course, coinduction comes with its own set of problems, especially when working in a total language or proof assistant. Another big focus of the paper was figuring out a representation that was amenable to formalisation (we formalised the paper in Cubical Agda). Picking a good representation for formalisation is a tricky thing: often a design decision you make early on only looks like a mistake after a few thousand lines of proofs, and modern formal proofs tend to be brittle, meaning that it’s difficult to change an early definition without also having to change everything that depends on it. On top of this, we decided to use quotients for an important part of the representation, and (as anyone who’s worked with quotients and coinduction will tell you) productivity proofs in the presence of quotients can be a real pain.
All that said, I think the representation we ended up with in the
paper is quite nice. We start with a similar representation to the one
we had in our ICFP
paper in 2021: a graph over vertices of type a is
simply a function a -> [a] that returns the neighbours
of a supplied vertex (this is the same representation as in this post). Despite the
simplicity, it turns out that this type is enough to implement a decent
number of search algorithms. The really interesting thing is that the
arrow methods (from Control.Arrow)
work on this type, and they define an algebra on graphs similar to the
one from Mokhov (2017). For example, the
<+> operator is the same as the overlay
operation in Mokhov (2017).
That simple type gets expanded upon and complicated: eventually, we
represent a possibly-infinite collection as a function that takes a
depth and then returns everything in the search space up to that depth.
It’s a little like representing an infinite list as the partial
application of the take function. The paper spends a lot of
time picking an algebra that properly represents the depth, and figuring
out coherency conditions etc.
One thing I’m especially proud of is that all the Agda code snippets in the paper are hyperlinked to a rendered html version of the code. Usually, when I want more info on some code snippet in a paper, I don’t really want to spend an hour or so downloading some artefact, installing a VM, etc. What I actually want is just to see all of the definitions the snippet relies on, and the 30 or so lines of code preceding it. With this paper, that’s exactly what you get: if you click on any Agda code in the paper, you’re brought to the source of that code block, and every definition is clickable so you can browse without having to install anything.
I think the audience for this paper is anyone who is interested in graphs in functional languages. It should be especially interesting to people who have dabbled in formalising some graphs, but who might have been stung by an uncooperative proof assistant. The techniques in the second half of the paper might help you to convince Agda (or Idris, or Rocq) to accept your coinductive and quotient-heavy arguments.