Stream: math-comp users

Topic: graph algorithms in Graph Theory project

Karl Palmskog (Jun 02 2020 at 09:35):

@Christian Doczkal so it seems like Graph Theory could be the place for a lot of proof-oriented graph theory. For example, do you think the work on strongly connected components (https://github.com/CohenCyril/tarjan) would fit there after some adaptation? Or how do you want to scope the project?

Karl Palmskog (Jun 02 2020 at 09:36):

personally, I would find it useful to only have to depend on MC + Graph Theory for work in this direction (e.g., when writing practical verified code using topological sorts and the like)

Christian Doczkal (Jun 02 2020 at 12:47):

One, lightly depressing, observation has been that the verification of graph algorithms (in particular the verification of intricate algorithms for easy to define concepts) does not profit much from a graph theory library. There often is little graph-theory knowledge required.

Christian Doczkal (Jun 02 2020 at 12:50):

Moreover, the specific paper you mention chooses to verify the algorithm at the level of the original Why3 proof, not necessarily making the best use of the higher-order nature of Coq (or Isabelle). I had a chat with Stephan Merz about this, when they presented the paper.

Karl Palmskog (Jun 02 2020 at 13:43):

OK, so you think the best way the community could maintain graph algorithm formalizations would be as a separate project?

Christian Doczkal (Jun 02 2020 at 18:20):

I wouldn't state it in those absolute terms. It depends on the algorithm. If the existence of an algorithm is not completely obvious and the verification requires some graph theory insights, then there may well be a case do develop the algorithm on top of the graph theory library or even within.

My example would be a function computing a minimum-width tree-decomposition for a graph. Currently there is no lemma in the library that allows things like "let (T,B) be a minimum-width tree decomposition", because the existence of such a decomposition is not entirely obvious (and was so far not needed).

Last updated: Apr 19 2024 at 16:01 UTC