		Search-engine friendly clone of the ACL2 documentation.

Proof-automation

Def-dag-measure

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

a relatively fast, executable function that checks whether all paths from the current node through the graph are loop-free
a measure function that takes a node in the graph, where if node A is loop-free and has successor node B, then measure(B) < measure(A).

This combination allows traversal functions to be written in this style:

(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 provided by this book:

(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:

algraph is the base name that will be used for the functions produced
The :graph-formals are a list of extra arguments required in each function that operates on a graph.
:successors-expr and :nodes-expr describe the representation of the graph: :successors-expr is an expression that, given graph node x, returns the list of successors of x, and :nodes-expr is an expression that produces the full list of nodes of the graph.
:guard, :node-guard, and :node-list-guard specify guards for the functions.

This produces the following functions:

(algraph-loopfree-p x graph) and (algraph-loopfreelist-p x graph) return t if the portion of the graph reachable from (node, resp. node list) x is acyclic. These are guard-verified fast (?) executable functions that do a linear time and space traversal of the graph. Theorems are provided showing that if a node is loop free, then its successors are loop free.
(algraph-measure x graph) and (algraph-list-measure x graph) are measure functions that can be used as the node-measure and node-list-measure in mutual recursions such as traverse above.

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)))))