Formalising Graph Algorithms with Coinduction
summary
Formalisation in Cubical Agda treats graphs as coinductive functions V -> Neighbors V where neighbors are monus-weighted neighbors (possibly infinite multisets implemented with quotient/higher-inductive laws). Productivity problems from quotients are solved by defining neighbors as a dependent pair using semigroup actions plus a coherence condition, enabling guarded coinduction. Algebraic operators (taken from the Arrow library) give overlay and connection monoids and a semiring; search, transitive closure (Kleene star) and Dijkstra are encoded as graph-transformations with termination justified via completely iterative monads.
AI-written summary · about