Stream: Is there code for X?

Topic: Enumerating transitive closure / reachable nodes in a graph

Maximilian Vollath (Dec 20 2024 at 12:02):

I have a graph and need to, for every single node, enumerate all reachable nodes.

So essentially a verified implementation of this:

axiomatization f :: "('a × 'a) list ⇒ ('a × 'a) list" where
  f_prop: "set (f rel) = (set rel)⇧+"

(An alternative would be a function that finds all reachable nodes from one single node, I'm just kind of assuming it's going to be less efficient if I need to call it for all nodes.)

Mathias Fleury (Dec 20 2024 at 12:31):

Is efficiency really a criteria for you?

Mathias Fleury (Dec 20 2024 at 12:32):

Less efficient is rarely a good design criterion for proof writing

Mathias Fleury (Dec 20 2024 at 12:32):

Easier to write proofs is much more important

Fabian Huch (Dec 20 2024 at 12:52):

To add to that: Usually, when you want a verified efficient implemtation, you start from a simple abstract definition, and refine it down to more efficient code, e.g. via the Refinement framework in the AFP.

Maximilian Vollath (Dec 20 2024 at 18:16):

Efficiency is only a tiny bit important but tbh a simple factor of up to n won't matter. Enumerating all nodes from an initial node would be enough for me.

Last updated: Dec 21 2024 at 16:20 UTC