; Jared Davis ; ; Here is a script demonstrating the use of quantification and mapping ; over sets in order to create some basic concepts from Graph Theory. (in-package "ACL2") (include-book "sets/map") ; We will represent a graph as a set of edges. Each edge consists of ; ; - a start vertex, from(e) ; - an end vertex, to(e) ; ; We will allow vertices to be any arbitrary objects. (defun edgep (e) (declare (xargs :guard t)) (consp e)) (defun from (e) (declare (xargs :guard (edgep e))) (car e)) (defun to (e) (declare (xargs :guard (edgep e))) (cdr e)) ; We now introduce quantification functions for edgep. This allows us to ask ; if, e.g., every element in a set is an edgep (all). (SETS::quantify-predicate (edgep x) :in-package-of edgep) ; I'll go ahead and represent graphs as simple sets of edges. (defun graphp (g) (declare (xargs :guard t)) (and (SETS::setp g) (all g))) ; We can construct a graph's vertex set from its edge set. To do so, we'll ; simply union the mappings of the "from" and "to" functions across the edge ; set. (SETS::map-function (from edge) :in-package-of edgep :set-guard ((all ?set)) :list-guard ((all-list ?list)) :element-guard ((edgep a))) (SETS::map-function (to edge) :in-package-of edgep :set-guard ((all ?set)) :list-guard ((all-list ?list)) :element-guard ((edgep a))) (defun vertices (g) (declare (xargs :guard (graphp g))) (SETS::union (map g) (map g))) ; Here are some examples, to get a feel for how these functions actually ; look. By the way, all of our quantification is done constructively, so ; we can execute these functions. (graphp '( (a . b) (b . c) (c . d) )) ; => t (map '( (a . b) (b . c) (c . d) )) ; => (a b c) (map '( (a . b) (b . c) (c . d) )) ; => (b c d) (vertices '( (a . b) (b . c) (c . d) )) ; => (a b c d) ; Now we'll introduce the notion of neighbors. We first introduce two ; predicates, which allow us to tell if (from edge) = vertex or if ; (to edge) = vertex for some vertex, v. (defun from-matches (edge vertex) (declare (xargs :guard t)) (and (edgep edge) (equal (from edge) vertex))) (defun to-matches (edge vertex) (declare (xargs :guard t)) (and (edgep edge) (equal (to edge) vertex))) ; We now quantify over these predicates. This allows us to consider ; the set of all edges which originate from a vertex, or which conclude ; at a vertex. (SETS::quantify-predicate (from-matches edge vertex) :in-package-of edgep) (SETS::quantify-predicate (to-matches edge vertex) :in-package-of edgep) ; Finally, we're ready to say what the neighbors of a vertex are. I'll ; say that the "forward neighbors" are the vertices that can be directly ; reached from this node. Similarly, the "backwards neighbors" are the ; vertices that can directly reach this node. (defun neighbors-forward (g vertex) (declare (xargs :guard (graphp g))) (map (filter g vertex))) (defun neighbors-backward (g vertex) (declare (xargs :guard (graphp g))) (map (filter g vertex))) (defun neighbors (g vertex) (declare (xargs :guard (graphp g))) (SETS::union (neighbors-forward g vertex) (neighbors-backward g vertex))) ; Here are a couple of examples. (neighbors '((a . b) (b . c) (c . d)) 'a) ; => (b) (neighbors '((a . b) (b . c) (c . d)) 'b) ; => (a c) ; Here's a neat theorem, we want to show that the neighbors are always ; a subset of the vertex set. This doesn't require any human thought, ; and is an excellent, deep proof done automatically for us! The theorem ; prover uses a pick-a-point argument to prove the subset, then uses ; reasoning about the inverses of map-from and map-to finish the proof. (defthm neighbors-are-vertices (SETS::subset (neighbors g vertex) (vertices g))) (defthm neighbors-forward-are-vertices ; this is just fluff (SETS::subset (neighbors-forward g vertex) (vertices g))) (defthm neighbors-backward-are-vertices ; this is just fluff (SETS::subset (neighbors-backward g vertex) (vertices g)))