Add proof (from email)

diff --git a/yarrg/yppedia-chart-parser b/yarrg/yppedia-chart-parser
index f834362873ee53fe271abaafd92a1e70a6e32315..92b609cf3268a97a72a0c921e5e98128a09ed4f2 100755 (executable)
--- a/yarrg/yppedia-chart-parser
+++ b/yarrg/yppedia-chart-parser
@@ -374,6 +374,73 @@ sub compare_island_lists () {
 
 sub shortest_path_reduction ($$) {
     my ($what,$base) = @_;
+    #
+    # Takes a graph $base (and a string for messages $what) and returns
+    # a new graph which is the miminal shortest path transient reduction
+    # of $base.
+    #
+    # We also check that the shortest path closure of the intended result
+    # is the same graph as the input.  Thus the input must itself be
+    # a shortest path closure; if it isn't, we die.
+
+    my $proof=<<'END'; # way to make a big comment
+
+    Premises and definitions:
+
+    1. F is a connected undirected weighted graph with positive edge
+       weights.
+
+    2. All graphs we will consider have the same vertices as F.
+
+    3. G = Closure(F) is the complete graph whose edge weights
+       are the shortest paths in F.  (G is the input graph $base.)
+
+    3a. |XY| for vertices X, Y is the weight of the edge XY in G.
+
+    4. A `reduction' of G is a subgraph K of G such that Closure(K) = G.
+       The reduction is `minimal' if there is no strict subgraph K'
+       of K such that Closure(K') = G.
+
+    5. Now each edge of G may be:
+       - `unnecessary': included in no minimal reductions of G.
+       - `essential': included in all minimal reductions of G.
+       - `contingent': included in some but not all.
+
+    6. Consider for any edge AC between the vertices A and C,
+       whether there is any B such that |AB|+|BC| = |AC| ?
+       (There can be no B such that the sum < |AC| since that would
+       mean that |AC| wasn't equal to the shortest path length.)
+
+    6a. No such B:  AC is therefore the only shortest path from A to C
+       (since G is not a multigraph).  AC is thus an essential edge.
+
+    6b. Some such B: Call all such edges AC `questionable'.
+
+    6c. Thus all edges are essential or questionable.
+
+    7. Suppose AC is a shortest contingent edge.  AC must be
+       questionable since it is not essential.  Suppose it is
+       made questionable by the existence of B such that |AB|+|BC| =
+       |AC|.  Consider AB and BC.  Since |AB| and |BC| are positive,
+       |BC| and |AB| must be < |AC| ie AB and BC are shorter than AC.
+       Since AC is a shortest contingent edge, there must be shortest
+       paths in G for AB and BC consisting entirely of essential edges.
+
+    8. Therefore it is always safe to remove AC since the paths
+       A..B and B..C will definitely still remain and provide a path
+       A..B..C with length |AB|+|BC| = |AC|.
+
+    9. Thus AC is unnecessary, contradicting the assumption in 7.
+       There are therefore no shortest contingent edges, and
+       thus no contingent edges.
+
+    10. We can construct a minimal reduction directly: for each edge
+        AC in G, search for a vertex B such that |AB|+|BC| = |AC|.
+        If we find none, AC is essential.  If we find one then AC is
+        not essential and is therefore unnecessary.
+
+END
+    
     printf DEBUG "spr %s before %d\n", $what, scalar($base->edges());
 
     my $result= Graph::Undirected->new();
@@ -416,7 +483,7 @@ sub shortest_path_reduction ($$) {
     }
     return $result;
 }
-           
+
 sub yppedia_graph_spr () {
     my $base= Graph::Undirected->new();
     foreach my $na (sort keys %winode2island) {