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.

Deprecation

This material has been moved out of Mathlib to https://github.com/semorrison/lean-monadic-list.

@[deprecated]

partial def depthFirst' {α : Type u} {m : Type u → Type u} [Monad m] [Alternative m] (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.

@[deprecated]

def depthFirst {α : Type u} {m : Type u → Type u} [Monad m] [Alternative m] (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

• depthFirst f a (some d) = depthFirst' (fun (n : Nat) (a : α) => if n ≤ d then f a else failure) 0 a
• depthFirst f a = depthFirst' (fun (x : Nat) (a : α) => f a) 0 a

@[deprecated]

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.

@[deprecated]

def depthFirstRemovingDuplicates' {α : Type u} [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 = (depthFirstRemovingDuplicates (fun (a : α) => MLList.ofList (f a)) a maxDepth).force.get!