Combining relation algebra and data refinement to develop rectangle-based functional programs for reflexive-transitive closures

摘要

We show how to systematically derive simple purely functional algorithms for computing the reflexive-transitive closure of directed graphs. Directed graphs can be represented as binary relations and we develop our algorithms based on a relation-algebraic description of reflexive-transitive closures. This description employs the notion of rectangles and instantiating the resulting algorithm with different kinds of rectangles leads to different algorithms for computing reflexive-transitive closures. Using data refinement we then develop simple Haskell programs for two specific choices of rectangles and show that one of them has cubic running time like Warshall's standard algorithm. Finally, we apply our approach to other standard operations of relation algebra and present graph theoretic applications of our developments.