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
removeDuplicatesBy? maintains an RBSet of previously visited nodes; otherwise if the graph is not a tree nodes may be visited multiple times.

We begin by defining a best-first queue of MLLists. This is a somewhat baroque data structure designed for the application in this file (and in particularly for the implementation of rewrite_search). If someone would like to generalize appropriately that would be great.

We want to maintain a priority queue of MLList m β, each indexed by some a : α with a priority. (One could simplify matters here by simply flattening this out to a priority queue of pairs α × β, with the priority determined by the α factor. However the lazyness of MLList is essential to performance here: we will extract elements from these lists one at a time, and only when they at the head of the queue. If another item arrives at the head of the queue, we may not need to continue calculate the previous head's elements.)

To complicate matters, the priorities might be expensive to calculate, so we instead keep track of a lower bound (where less is better) for each such a : α. The priority queue maintains the MLList m β in order of the current best lower bound for the corresponding a : α. When we insert a new α × MLList m β into the queue, we have to provide a lower bound, and we just insert it at a position depending on the estimate. When it is time to pop a β off the queue, we iteratively improve the lower bound for the front element of the queue, until we decide that either it must be the least element, or we can exchange it with the second element of the queue and continue.

A BestFirstQueue prio ε m β maxSize consists of an RBMap, where the keys are in BestFirstNode prio ε and the values are MLList m β.

A BestFirstNode prio ε consists of a key : α and an estimator ε : key. Here ε provides the current best lower bound for prio key : Thunk ω. (The actual priority is hidden behind a Thunk to avoid evaluating it, in case it is expensive.)

We ask for the type classes LinearOrder ω and ∀ a : α, Estimator (prio a) (ε a). This later typeclass ensures that we can always produce progressively better estimates for a priority. We also need a WellFounded instance to ensure that improving estimates terminates.

This whole structure is designed around the problem of searching rewrite graphs, prioritising according to edit distances (either between sides of an equation, or from a goal to a target). Edit distance computations are particularly suited to this design because the usual algorithm for computing them produces improving lower bounds at each step.

With this design, it is okay if we visit nodes with very large edit distances: while these would be expensive to compute, we never actually finish the computation except in cases where the node arrives at the front of the queue.