Proving Termination for Standard Algorithms on Finite Graphs

Stream: general

[Andrew Wells]

I did Advent of Code in Lean (https://github.com/andrewmw94/2024_advent_of_code) and one difficulty I ran into repeatedly was proving termination of standard graph algorithms (DFS, BFS or Dijkstra's) on finite graphs. I just used sorry and am now coming back to try to prove termination for these. My approach is to use a set of unvisited nodes (so the complement of the typical set) and prove that set decreases. I got this working (ignoring the needed LawfulBEq and LawfulHashable proofs) here: https://github.com/andrewmw94/2024_advent_of_code/blob/main/aoc_day6/AocDay6/Thm.lean

I'm unhappy with this for two reasons:
1) Building the unvisited set could take a lot of time / memory that shouldn't really be needed.
2) I can imagine some problems where I know the graph is finite, but enumerating every node isn't tractable.

Am I approaching this wrong? How would you prove termination if you know the graph is finite but don't know the number of nodes?

For a stand-alone example, I have f1 which needs the same sort of proof, so you can just look at the first 38 lines.

[pandaman]

You can track the set of visited nodes instead and have (total nodes in graph) - visited.size as the termination_by clause.

[pandaman]

Here is my DFS reachability code. It uses a custom set type, but the idea about the termination is the same. It also uses a stack to make the implementation tail-recursive, which prevents stack overflow.
https://github.com/pandaman64/lean-regex/blob/main/RegexCorrectness/VM/EpsilonClosure/Basic.lean#L24

[Mitchell Lee]

If the unvisited set is only used in the termination proof and not the computation itself, then it won't use any time or memory at all. Proofs are ignored when compiling Lean code into an executable.

[Andrew Wells]

Thanks for the pointer! I like this; especially that it could be expanded to take a proof that there are N unique states (each corresponding to a node) for a problem like mine. If I understand correctly, measure is defined as def measure (s : SparseSet n) : Nat := n - s.count, so you would need to know the size of the set. Any ideas for proving termination if you know the graph is finite but not the number of nodes?

[pandaman]

Usually, we assume the number of nodes in a graph is known beforehand when writing a graph algorithm.

If it's not the case (like discovering possible moves as we search through the states), I think you would need to know an upper bound of n (from the fact that the search space is finite). For example, I can imagine we can define a function like def traverse {n : Nat} (visited : Std.HashSet Nat) (bound : visited.size < n) with termination_by => n - visited.size. Hopefully, the calculation of n on the caller would be erased.

[Markus Himmel]

I wrote something similar to the traverse you're describing a while ago:

import Std.Data.HashMap

open Std

theorem HashMap.size_le_fin (m : Std.HashMap (Fin n) β) : m.size ≤ n := by
  suffices ∀ k : Nat, k ≤ n → (∀ x ∈ m, x < k) → m.size ≤ k from this n (Nat.le_refl _) (fun x _ => x.2)
  intro k
  induction k generalizing m with
  | zero => simp [← Std.HashMap.isEmpty_iff_forall_not_mem, Std.HashMap.isEmpty_eq_size_eq_zero]
  | succ k ih =>
    intro hm hl'
    have := ih (m.erase ⟨k, by omega⟩) (by omega) (by
      simp only [HashMap.mem_erase, beq_eq_false_iff_ne, ne_eq, and_imp]
      intro ⟨x, hx⟩ hx' hx''
      have := hl' _ hx''
      simp_all; omega)
    have := HashMap.size_le_size_erase (m := m) (k := ⟨k, by omega⟩)
    omega

def dfs {n : Nat} (graph : Fin n → List (Fin n)) (start : Fin n) : HashMap (Fin n) Nat :=
  visit start ∅
where
  visit (cur : Fin n) (seen : HashMap (Fin n) Nat) :
      { s : HashMap (Fin n) Nat // seen.size ≤ s.size } := Id.run do

    if h : cur ∈ seen then
      return ⟨seen, Nat.le_refl _⟩
    else
      let mut curSeen : { s : HashMap (Fin n) Nat // seen.size < s.size } :=
        ⟨seen.insert cur seen.size, by simp [HashMap.size_insert, h]⟩

      for next in graph cur do
        have : n - curSeen.val.size < n - seen.size := have := HashMap.size_le_fin curSeen.val; by omega
        curSeen := ⟨visit next curSeen, Nat.lt_of_lt_of_le curSeen.property (visit next curSeen).property⟩

      ⟨curSeen.val, Nat.le_of_lt curSeen.property⟩
  termination_by n - seen.size