Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.edmonds-karp

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

AHoF Edmonds-Karp Algorithm: compute the maximum flow through a network in O(V*E^2) by repeatedly finding a SHORTEST augmenting path (by BFS) in the residual graph and pushing flow along it, until none remains -- a concrete polynomial realization of Ford-Fulkerson. The BFS may traverse an edge only while it has RESIDUAL CAPACITY (its current flow is below its capacity, i.e. residual = capacity - flow > 0): has-residual? residual = decide (1 <= residual) over exact-rational (integer) residual capacities. Proved native and axiom-free: the residual test; that an edge with positive residual can carry more flow (it is part of the residual graph the BFS explores); the certificate that a usable edge's residual is at least one unit (native nnrat/at-most); and that a saturated edge (zero residual) is unusable. The BFS, augmentation, and residual bookkeeping are executable; what is proved is the residual-capacity decision, whose repetition yields the max flow (equal to the min cut). Requires nnrat/at-most, audit/decide-nnrat-at-most, nnrat/decide-at-most-true-sound (all 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.edmonds-karp` prints this classification.

edmonds-karp/has-residual? :
  (x₁ : ℚ≥0)
  → data/Bool

edmonds-karp/positive-residual-usable :
  → edmonds-karp/has-residual? 3 = data/true

edmonds-karp/usable-residual-at-least-one :
  → 1 ≤ 3

edmonds-karp/saturated-edge-unusable :
  → edmonds-karp/has-residual? 0 = data/false