Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.kosaraju

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/kosaraju.clj1 definitions, 3 theorems

AHoF Kosaraju's Algorithm: find the strongly connected components (SCCs) of a directed graph in O(V + E) via two depth-first passes -- one on the graph (recording finish order) and one on the TRANSPOSE (grouping by reachability in decreasing finish order). Two vertices lie in the same SCC exactly when each is reachable from the other: same-scc? u-reaches-v? v-reaches-u? = u-reaches-v? AND v-reaches-u? over booleans. Proved native and axiom-free: the same-component test as the boolean conjunction of the two directed reachabilities (via logic/if-data over Bool); that mutual reachability puts two vertices in one SCC; and that if EITHER direction is unreachable they are in different SCCs. The two DFS passes and the component labelling are executable; what is proved is the mutual-reachability SCC membership decision (the condensation of the graph is a DAG of these components). Requires data/Bool, logic/if-data (both in the D63 checkpoint). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.kosaraju` prints this classification.

kosaraju/same-scc? :
  (x₁ x₂ : data/Bool)
  → data/Bool

kosaraju/mutual-reach-same-scc :
  → cyk/rule-applies? data/true data/true = data/true

kosaraju/forward-unreachable-different :
  → cyk/rule-applies? data/false data/true = data/false

kosaraju/backward-unreachable-different :
  → cyk/rule-applies? data/true data/false = data/false