Best first search

We perform best first search of a tree or graph, where the neighbours of a vertex are provided by a lazy list α → MLList m α.

We maintain a priority queue of visited-but-not-exhausted nodes, and at each step take the next child of the highest priority node in the queue.

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.

Options:

• maxDepth allows bounding the search depth
• maxQueued implements "beam" search, by discarding elements from the priority queue when it grows too large
• removeDuplicates maintains an RBSet of previously visited nodes; otherwise if the graph is not a tree nodes may be visited multiple times.

def bestFirstSearchAux {m : Type u → Type u} {α : Type u} [Monad m] [Alternative m] [Ord α] (f : Nat → α → MLList m α) (maxQueued : optParam (Option Nat) none) : Std.RBMap α (Nat × MLList m α) compare → m (Std.RBMap α (Nat × MLList m α) compare × List α)

Auxiliary function for bestFirstSearch, that updates the internal state, consisting of a priority queue of triples α × Nat × MLList m α. We remove the next element from the list contained in the best triple (discarding the triple if there is no next element), enqueue it and return it.

def bestFirstSearch {m : Type u → Type u} {α : Type u} [Monad m] [Alternative m] [Ord α] (f : α → MLList m α) (a : α) (maxDepth : optParam (Option Nat) none) (maxQueued : optParam (Option Nat) none) (removeDuplicates : optParam Bool true) : MLList m α

A lazy list recording the best first search of a graph generated by a function f : α → MLList m α.

We maintain a priority queue of visited-but-not-exhausted nodes, and at each step take the next child of the highest priority node in the queue.

The option maxDepth limits the search depth.

The option maxQueued bounds the size of the priority queue, discarding the lowest priority nodes as needed. This implements a "beam" search, which may be incomplete but uses bounded memory.

The option removeDuplicates keeps an RBSet of previously visited nodes. Otherwise, if the graph is not a tree then nodes will be visited multiple times.