Generic framework that allows simple traversals of DAGs.
Suppose we have a representation of some finite DAG, but it is encoded in such a way that it isn't obvious that it's acyclic. E.g., perhaps our representation is an alist mapping each node to its list of successors. We then want to do some traversal of the graph. The challenge is to prove that our traversal function terminates.
One typical way to do this is to record the nodes we've already traversed to ensure that we don't re-traverse them; then, an appropriate measure for termination is the count of nodes that we haven't yet traversed. Writing functions in this style is doable, but passing around the record of nodes we've already seen complicates reasoning about the function.
This framework helps to streamline a different approach. In this approach, we define
(mutual-recursion (defun traverse-node (node graph) (declare (xargs :guard (loopfree-p node graph) :measure (node-measure node graph))) (if (mbt (loopfree-p node graph)) (do-something node (traverse-list (successors node graph) graph)) (fail))) (defun traverse-list (nodelist graph) (declare (xargs :guard (loopfreelist-p nodelist graph) :measure (node-list-measure list graph))) (if (atom nodelist) (end-val) (combine (traverse-node (car nodelist) graph) (traverse-list (cdr nodelist) graph)))))
The framework is generic as to how the successors of a node are determined; e.g., they could be stored in an alist and extracted with assoc, or generated by some arbitrary function. It expects the successor function to produce a list of nodes. If the successors are not conveniently encoded as a list of nodes, you might still be able to work with this framework with some extra proof work. Another way in which the framework is not completely generic is that it uses an underlying traversal function that stores seen nodes in a fast alist. If this isn't the right encoding for your problem, you may again need to do some extra proofs to use this framework.
The following example shows how to use the macro
(def-dag-measure algraph :graph-formals (graph) :successors-expr (cdr (assoc-eq x graph)) :nodes-expr (strip-cars graph) :guard (and (alistp graph) (symbol-list-listp (strip-cdrs graph))) :node-guard (symbolp x) :node-list-guard (symbol-listp x))
In the above example:
This produces the following functions:
An example of how to use these functions to admit a simple node-count function is also provided by the macro, and reproduced here:
(mutual-recursion (defun algraph-count (x graph) (declare (xargs :measure (algraph-measure x graph) :guard (and (alistp graph) (symbol-list-listp (strip-cdrs graph)) (symbolp x) (algraph-loopfree-p x graph)))) (if (mbt (algraph-loopfree-p x graph)) (+ 1 (algraph-count-list (cdr (assoc-eq x graph)) graph)) 0)) (defun algraph-count-list (x graph) (declare (xargs :measure (algraph-list-measure x graph) :guard (and (alistp graph) (symbol-list-listp (strip-cdrs graph)) (symbol-listp x) (algraph-loopfreelist-p x graph)))) (if (atom x) 0 (+ (algraph-count (car x) graph) (algraph-count-list (cdr x) graph)))))