Theory Aggregation_Algebras
section ‹Algebras for Aggregation and Minimisation›
text ‹
This theory gives algebras with operations for aggregation and minimisation.
In the weighted-graph model of matrices over (extended) numbers, the operations have the following meaning.
The binary operation $+$ adds the weights of corresponding edges of two graphs.
Addition does not have to be the standard addition on numbers, but can be any aggregation satisfying certain basic properties as demonstrated by various models of the algebras in another theory.
The unary operation ‹sum› adds the weights of all edges of a graph.
The result is a single aggregated weight using the same aggregation as $+$ but applied internally to the edges of a single graph.
The unary operation ‹minarc› finds an edge with a minimal weight in a graph.
It yields the position of such an edge as a regular element of a Stone relation algebra.
We give axioms for these operations which are sufficient to prove the correctness of Prim's and Kruskal's minimum spanning tree algorithms.
The operations have been proposed and axiomatised first in \<^cite>‹"Guttmann2016c"› with simplified axioms given in \<^cite>‹"Guttmann2018a"›.
The present version adds two axioms to prove total correctness of the spanning tree algorithms as discussed in \<^cite>‹"Guttmann2018b"›.
›
theory Aggregation_Algebras
imports Stone_Kleene_Relation_Algebras.Kleene_Relation_Algebras
begin
context sup
begin
no_notation
sup (infixl "+" 65)
end
context plus
begin
notation
plus (infixl "+" 65)
end
text ‹
We first introduce s-algebras as a class with the operations $+$ and ‹sum›.
Axiom ‹sum_plus_right_isotone› states that for non-empty graphs, the operation $+$ is $\leq$-isotone in its second argument on the image of the aggregation operation ‹sum›.
Axiom ‹sum_bot› expresses that the empty graph contributes no weight.
Axiom ‹sum_plus› generalises the inclusion-exclusion principle to sets of weights.
Axiom ‹sum_conv› specifies that reversing edge directions does not change the aggregated weight.
In instances of ‹s_algebra›, aggregated weights can be partially ordered.
›
class sum =
fixes sum :: "'a ⇒ 'a"
class s_algebra = stone_relation_algebra + plus + sum +
assumes sum_plus_right_isotone: "x ≠ bot ∧ sum x ≤ sum y ⟶ sum z + sum x ≤ sum z + sum y"
assumes sum_bot: "sum x + sum bot = sum x"
assumes sum_plus: "sum x + sum y = sum (x ⊔ y) + sum (x ⊓ y)"
assumes sum_conv: "sum (x⇧T) = sum x"
begin
lemma sum_disjoint:
assumes "x ⊓ y = bot"
shows "sum ((x ⊔ y) ⊓ z) = sum (x ⊓ z) + sum (y ⊓ z)"
by (subst sum_plus) (metis assms inf.sup_monoid.add_assoc inf.sup_monoid.add_commute inf_bot_left inf_sup_distrib2 sum_bot)
lemma sum_disjoint_3:
assumes "w ⊓ x = bot"
and "w ⊓ y = bot"
and "x ⊓ y = bot"
shows "sum ((w ⊔ x ⊔ y) ⊓ z) = sum (w ⊓ z) + sum (x ⊓ z) + sum (y ⊓ z)"
by (metis assms inf_sup_distrib2 sup_idem sum_disjoint)
lemma sum_symmetric:
assumes "y = y⇧T"
shows "sum (x⇧T ⊓ y) = sum (x ⊓ y)"
by (metis assms sum_conv conv_dist_inf)
lemma sum_commute:
"sum x + sum y = sum y + sum x"
by (metis inf_commute sum_plus sup_commute)
end
text ‹
We next introduce the operation ‹minarc›.
Axiom ‹minarc_below› expresses that the result of ‹minarc› is contained in the graph ignoring the weights.
Axiom ‹minarc_arc› states that the result of ‹minarc› is a single unweighted edge if the graph is not empty.
Axiom ‹minarc_min› specifies that any edge in the graph weighs at least as much as the edge at the position indicated by the result of ‹minarc›, where weights of edges between different nodes are compared by applying the operation ‹sum› to single-edge graphs.
Axiom ‹sum_linear› requires that aggregated weights are linearly ordered, which is necessary for both Prim's and Kruskal's minimum spanning tree algorithms.
Axiom ‹finite_regular› ensures that there are only finitely many unweighted graphs, and therefore only finitely many edges and nodes in a graph; again this is necessary for the minimum spanning tree algorithms we consider.
›
class minarc =
fixes minarc :: "'a ⇒ 'a"
class m_algebra = s_algebra + minarc +
assumes minarc_below: "minarc x ≤ --x"
assumes minarc_arc: "x ≠ bot ⟶ arc (minarc x)"
assumes minarc_min: "arc y ∧ y ⊓ x ≠ bot ⟶ sum (minarc x ⊓ x) ≤ sum (y ⊓ x)"
assumes sum_linear: "sum x ≤ sum y ∨ sum y ≤ sum x"
assumes finite_regular: "finite { x . regular x }"
begin
text ‹
Axioms ‹minarc_below› and ‹minarc_arc› suffice to derive the Tarski rule in Stone relation algebras.
›
subclass stone_relation_algebra_tarski
proof unfold_locales
fix x
let ?a = "minarc x"
assume 1: "regular x"
assume "x ≠ bot"
hence "arc ?a"
by (simp add: minarc_arc)
hence "top = top * ?a * top"
by (simp add: comp_associative)
also have "... ≤ top * --x * top"
by (simp add: minarc_below mult_isotone)
finally show "top * x * top = top"
using 1 order.antisym by simp
qed
lemma minarc_bot:
"minarc bot = bot"
by (metis bot_unique minarc_below regular_closed_bot)
lemma minarc_bot_iff:
"minarc x = bot ⟷ x = bot"
using covector_bot_closed inf_bot_right minarc_arc vector_bot_closed minarc_bot by fastforce
lemma minarc_meet_bot:
assumes "minarc x ⊓ x = bot"
shows "minarc x = bot"
proof -
have "minarc x ≤ -x"
using assms pseudo_complement by auto
thus ?thesis
by (metis minarc_below inf_absorb1 inf_import_p inf_p)
qed
lemma minarc_meet_bot_minarc_iff:
"minarc x ⊓ x = bot ⟷ minarc x = bot"
using comp_inf.semiring.mult_not_zero minarc_meet_bot by blast
lemma minarc_meet_bot_iff:
"minarc x ⊓ x = bot ⟷ x = bot"
using inf_bot_right minarc_bot_iff minarc_meet_bot by blast
lemma minarc_regular:
"regular (minarc x)"
proof (cases "x = bot")
assume "x = bot"
thus ?thesis
by (simp add: minarc_bot)
next
assume "x ≠ bot"
thus ?thesis
by (simp add: arc_regular minarc_arc)
qed
lemma minarc_selection:
"selection (minarc x ⊓ y) y"
using inf_assoc minarc_regular selection_closed_id by auto
lemma minarc_below_regular:
"regular x ⟹ minarc x ≤ x"
by (metis minarc_below)
end
class m_kleene_algebra = m_algebra + stone_kleene_relation_algebra
end