! MinSpanForest.ax - specification axioms for minimum spanning forest function ! - result will be a minimum spanning tree if the input graph is connected ! - will be compared to Kruskal's and Prim's algorithms in C and other langs !---+----x----+----x----+----x----+----x----+----x----+----x----+----x----+----8 !/ top-level predicate: (MSF ) - input weighted undirected graph = (.. ..) -- sequence (set) of >=0 weighted undirected edges - weighted undirected edge = ( ) -- edge between vertices A and B with weight wt -- order of vertices for undirected edge doesn't matter - symbol for a vertex X (just equality and inequality between vertex symbols is needed) - natural number weight given as an unsigned decimal number symbol -- Note that the set of vertices is implied by the set of edges. (Thus, we can't represent isolated vertices without edges.) -- We allow a multigraph where there can be >1 edges (with or without different weights) between two vertices. The edges may have the vertices in different orders. (The minimum spanning forest, of course, would only contain the/an edge of minimum weight.) We also allow loops where an edge goes to and from the same vertex. (The minimum spanning forest, of course, would exclude these edges.) - output weighted undirected graph representing minimum spanning forest -- same format as the input weighted undirected graph -- The output graph is just a subset of the input edges and we keep the same edge order and the same vertex order for each edge. -- If there is more than one minimum spanning forest (with the same minimum weight), our output graph can nondeterministically be any one of those solutions. example wug: ((B F 7) (G C 8) (D H 7) (A E 4) (A F 2) (E B 9) (F C 5) (A B 8) (E F 6) (G F 9)) (A)--8---(B) (C) (D) | \ / | / | | | 2 9 | 5 | | 4 \/ 7 / 8 7 | /\ | / | | | / \ | / | | | / \ | / | | (E)--6---(F)--9---(G) (H) minimum spanning forest: ((B F 7) (G C 8) (D H 7) (A E 4) (A F 2) (F C 5)) (A) (B) (C) (D) | \ | / | | | 2 | 5 | | 4 \ 7 / 8 7 | \ | / | | | \ | / | | | \ | / | | (E) (F) (G) (H) See utilities directory for utility function definitions. !\ ! MSF - Minimum Spanning Forest (MSF %wug %wugMSF)< ((filter edge-verts-differ?) %wug %wugll), ! get loop-less version of graph ! -- we need this to eliminate isolated vertices with loop edges (all_subsets %wugll %wugsubs), ! get all (loop-less) subgraphs ! -- we get all edge subsets ((filter (same-components? %wugll)) %wugsubs %wugspan), ! -- get spanning subgraphs (same connected components as original) ((min graph-weight+) %wugspan %wugMSF). ! get spanning subgr w min weight ! non-deterministic if more than one minimum! ! components - connected components of an undirected graph ! (returns partition of the set of vertices obtained from sequence of edges) (components %wug %components)< ((map pre2) %wug %edge_verts), ! -- init "components" to separate 2-vertex subsets for each edge ! (we remove the weights) ! (since tbere are no loop edges, the end vertices are distinct) ((repeat merge_sets) %edge_verts %components), ! -- repeatedly merge vertex subsets that have a vertex in common ! (gives larger vertex subsets that are connected) (partition %components). ! the vertex subsets form a partition ! -- at this point no two vertex subsets have a vertex in common ! -- thus the vertex subsets are all the connected components ! some supporting graph function definitions (define_func edge-verts-differ? (comp not (1 ==?) pre2)). ! returns `t if edge end-vertices differ (define_func (same-components? %wug) (comp =ssets? (constr (comp components (`' %wug)) components))). ! tests if input graph has same components as graph in function (define_func edge-weight (comp dec_sym sel2)). ! edge wt as natural number (define_func edge-weight+ (comp (partial plus (s 0)) edge-weight)). ! get incremented edge weight ! -- This makes sure that 0-weight edges have a positive weight; ! otherwise, they might be left in the minimum weight graph. (define_func graph-weight+ (comp sum (map edge-weight+))). ! sum of incremented weights !/ alternative (with same number of lines): (define_func graph-weight+ (comp plus (constr (comp plus (map edge-weight)) length))). ! -- uses graph length to add 1 to each edge weight ! -- Note that plus has been generalized to add a sequence of numbers. !\