Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.bipartite-matching

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

AHoF Maximum Bipartite Matching (augmenting-path / Hungarian tree method): find the largest set of edges with no shared endpoints in a bipartite graph -- the model for job/worker assignment, scheduling, and network routing. Each left vertex is matched by finding an AUGMENTING PATH: it can claim a right neighbor v when v is currently FREE, or when v's current match can itself be re-matched elsewhere (recursively). So a left vertex can be matched to v when: can-match? v-free? partner-reassignable? = v-free? OR partner-reassignable? over booleans. Proved native and axiom-free: the augment test as the boolean DISJUNCTION of 'the neighbor is free' and 'its current partner can move' (via logic/if-data over Bool); that a free neighbor is immediately matchable; that a reassignable partner also yields a match (the augmenting path); and that a match fails only when the neighbor is taken AND its partner cannot move. The DFS/BFS for augmenting paths is executable; what is proved is the per-neighbor augment decision, whose repetition (once per left vertex) yields a maximum matching. 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.bipartite-matching` prints this classification.

bipartite-matching/can-match? :
  (x₁ x₂ : data/Bool)
  → data/Bool

bipartite-matching/free-neighbor-matchable :
  → bipartite-matching/can-match? data/true data/false = data/true

bipartite-matching/reassignable-partner-matchable :
  → bipartite-matching/can-match? data/false data/true = data/true

bipartite-matching/taken-stuck-partner-fails :
  → bipartite-matching/can-match? data/false data/false = data/false