Depth first search

We perform depth first search of a tree or graph, where the neighbours of a vertex are provided either by list α → List α or a lazy list α → MLList MetaM α.

This is useful in meta code for searching for solutions in the presence of alternatives. It can be nice to represent the choices via a lazy list, so the later choices don't need to be evaluated while we do depth first search on earlier choices.

partial def depthFirst' {m : Type u_1 → Type u_1} [Monad m] [Alternative m] {α : Type u_1} (f : Nat → α → m α) (n : Nat) (a : α) : m α

A generalisation of depthFirst, which allows the generation function to know the current depth, and to count the depth starting from a specified value.

def depthFirst {m : Type u_1 → Type u_1} [Monad m] [Alternative m] {α : Type u_1} (f : α → m α) (a : α) (maxDepth : optParam (Option Nat) none) : m α

Depth first search of a graph generated by a function f : α → m α.

Here m must be an Alternative Monad, and perhaps the only sensible values are List and MLList MetaM.

The option maxDepth limits the search depth.

Note that if the graph is not a tree then elements will be visited multiple times. (See depthFirstRemovingDuplicates)

Equations

• One or more equations did not get rendered due to their size.

def depthFirstRemovingDuplicates {m : Type u → Type u} [Monad m] {α : Type u} [BEq α] [Hashable α] (f : α → MLList m α) (a : α) (maxDepth : optParam (Option Nat) none) : MLList m α

Variant of depthFirst, using an internal HashSet to record and avoid already visited nodes.

This version describes the graph using α → MLList m α, and returns the monadic lazy list of nodes visited in order.

This is potentially very expensive. If you want to do efficient enumerations from a generation function, avoiding duplication up to equality or isomorphism, use Brendan McKay's method of "generation by canonical construction path".

Equations

• One or more equations did not get rendered due to their size.

def depthFirstRemovingDuplicates' {α : Type u_1} [BEq α] [Hashable α] (f : α → List α) (a : α) (maxDepth : optParam (Option Nat) none) : List α

Variant of depthFirst, using an internal HashSet to record and avoid already visited nodes.

This version describes the graph using α → List α, and returns the list of nodes visited in order.

Equations

• depthFirstRemovingDuplicates' f a maxDepth = Option.get! (MLList.force (depthFirstRemovingDuplicates (fun (a : α) => MLList.ofList (f a)) a maxDepth))