We present a technique to calculate iterative, polynomial-time graph algorithms directly from the definition of the properties. We do this by fixed-point fusion of (1) a least fixed point expressing all finite paths through a directed graph and (2) Galois connections that capture the properties of interest. We demonstrate the technique by constructing three algorithms from the literature: a transitive closure algorithm, a dominance algorithm and an algorithm for the single-source shortest path problem. Furthermore we show how the transitive closure algorithm can be understood as an abstraction of a fourth iterative all-pairs shortest path algorithm. The approach illustrates that reasoning in the style of fixed-point calculus extends gracefully to the domain of graph algorithms. We thereby bridge common practice from the school of program calculation with common practice from the school of static program analysis, where fixed-point fusion is known as a complete abstraction, and build a novel view on iterative graph algorithms as instances of abstract interpretation.
分享
引用
