depth first search

Stream: batteries

[Paige Thomas]

I translated a computable algorithm and proof of its correctness for depth first search from a paper I found in Isabelle. I'm planning on using it for the epsilon closure of nondeterministic state machines. If it may be of use, it is currently here.

[François G. Dorais]

What is your model for graphs?

[Paige Thomas]

/--
  The adjacency list representation of a graph.
-/
abbrev Graph
  (Node : Type) :
  Type :=
  List (Node × Node)

[Paige Thomas]

Is that what you mean?

[Paige Thomas]

If a pair of nodes is in the list, then there is a directed edge from the first node to the second node.

[Paige Thomas]

This allows for groups of nodes that are not connected to other groups of nodes. So the algorithm is basically to find the list of nodes that are all connected to a given list of nodes by some directed path.

[Shreyas Srinivas]

Once Vector is merged, I would like to suggest the following for finite graphs:

structure Graph (dataType : Type u) (n : Nat) where
    data : Vector dataType  n
     adj : Vector (Array  <| Fin n) n

[Paige Thomas]

What does (Array <| Fin n) mean?

[Paige Thomas]

What would the advantage be of this representation? (not saying there isn't one, just trying to understand)

[Chris Bailey]

a <| b x is a different way of writing a (b x) that doesn't require balancing parens. Some people prefer a <| b <| c <| d x to a (b (c (d x)))

[Chris Bailey]

A lot of syntactic items/notation have hover docs btw, including this one:

Haskell-like pipe operator <|. f <| x means the same as the same as f x,
except that it parses x with lower precedence, which means that
f <| g <| x is interpreted as f (g x) rather than (f g) x.

[Paige Thomas]

I see. So this would be an array of natural numbers each of which is less than n?

[Paige Thomas]

And then a vector of length n consisting of those?

[Paige Thomas]

I guess I'm not sure what this means as a representation.

[Paige Thomas]

Oh, is it https://en.wikipedia.org/wiki/Adjacency_matrix?

[Chris Bailey]

Oh sorry, I thought you were specifically asking about the syntax. Yes, it's an adjacency list. My guess is that the use of Fin n is just to show that the indices are all in-bounds as part of the type.

[Paige Thomas]

No, you were right, thank you. I was first asking about the syntax, and then trying to understand the semantics.

[Shreyas Srinivas]

The structure represents a graph of n vertices in adjacency list form (except I use arrays)

[Shreyas Srinivas]

The array entries are of type Fin n to indicate that the neighbours are also vertices. Also, I can use them as indices of adj_arr with no extra effort

[Shreyas Srinivas]

I am currently using the name FinGraph for this structure.

[Shreyas Srinivas]

Just wanted to add that for a different reason, I implemented an adjacency list based multigraph called fingraph with DFS and BFS: https://github.com/Shreyas4991/DGAlgorithms/blob/model_PN_shreyas/DGAlgorithms/Models/Fingraph.lean

Note : The decreasing_by proofs for the auxiliary functions are long, but I suspect these can be shortened.