Zulip Chat Archive
Stream: new members
Topic: Termination of BFS
Philipp (Jan 03 2024 at 21:57):
I was doing some Advent of Code to learn Lean (horrible code here: https://github.com/klockeph/AdventOfCode2023; I definitely see improvement over the days, whenever I found better (syntax) features).
So one recurring pattern is a kind of BFS over a 2D map (List (List Char))
. I was usually too lazy to parse that as a graph; instead I implemented a function getNext (Nat * Nat) -> List (Nat * Nat)
that returned all valid neighbors.
I repeated myself quite often (https://github.com/klockeph/AdventOfCode2023/blob/main/AdventOfCode/Day10.lean#L64, https://github.com/klockeph/AdventOfCode2023/blob/main/AdventOfCode/Day16.lean#L74 to name two)... and while I could fix that by hardcoding less and making e.g. getNext an argument of bfs, the main thing that bothers me is the partial
.
How would I prove termination of bfs over a finite graph? One idea I had is using Fin * Fin
as positions; would that be enough?
Another idea would be having a HashSet of all nodes and removing visited ones, instead of adding; then that HashSet is always decreasing (or empty). But it would require a pass over the Graph beforehand.
So what is the standard way of implementing bfs and proving that it terminates?
Last updated: May 02 2025 at 03:31 UTC