Theory Semirings
section ‹Semirings›
text ‹
This theory develops a hierarchy of idempotent semirings.
All kinds of semiring considered here are bounded semilattices, but many lack additional properties typically assumed for semirings.
In particular, we consider the variants of semirings, in which
\begin{itemize}
\item multiplication is not required to be associative;
\item a right zero and unit of multiplication need not exist;
\item multiplication has a left residual;
\item multiplication from the left is not required to distribute over addition;
\item the semilattice order has a greatest element.
\end{itemize}
We have applied results from this theory a number of papers for unifying computation models.
For example, see \<^cite>‹"Guttmann2012c"› for various relational and matrix-based computation models and \<^cite>‹"BerghammerGuttmann2015b"› for multirelational models.
The main results in this theory relate different ways of defining reflexive-transitive closures as discussed in \<^cite>‹"BerghammerGuttmann2015b"›.
›
theory Semirings
imports Fixpoints
begin
subsection ‹Idempotent Semirings›
text ‹
The following definitions are standard for relations.
Putting them into a general class that depends only on the signature facilitates reuse.
Coreflexives are sometimes called partial identities, subidentities, monotypes or tests.
›
class times_one_ord = times + one + ord
begin
abbreviation reflexive :: "'a ⇒ bool" where "reflexive x ≡ 1 ≤ x"
abbreviation coreflexive :: "'a ⇒ bool" where "coreflexive x ≡ x ≤ 1"
abbreviation transitive :: "'a ⇒ bool" where "transitive x ≡ x * x ≤ x"
abbreviation dense_rel :: "'a ⇒ bool" where "dense_rel x ≡ x ≤ x * x"
abbreviation idempotent :: "'a ⇒ bool" where "idempotent x ≡ x * x = x"
abbreviation preorder :: "'a ⇒ bool" where "preorder x ≡ reflexive x ∧ transitive x"
abbreviation "coreflexives ≡ { x . coreflexive x }"
end
text ‹
The first algebra is a very weak idempotent semiring, in which multiplication is not necessarily associative.
›
class non_associative_left_semiring = bounded_semilattice_sup_bot + times + one +
assumes mult_left_sub_dist_sup: "x * y ⊔ x * z ≤ x * (y ⊔ z)"
assumes mult_right_dist_sup: "(x ⊔ y) * z = x * z ⊔ y * z"
assumes mult_left_zero [simp]: "bot * x = bot"
assumes mult_left_one [simp]: "1 * x = x"
assumes mult_sub_right_one: "x ≤ x * 1"
begin
subclass times_one_ord .
text ‹
We first show basic isotonicity and subdistributivity properties of multiplication.
›
lemma mult_left_isotone:
"x ≤ y ⟹ x * z ≤ y * z"
using mult_right_dist_sup sup_right_divisibility by auto
lemma mult_right_isotone:
"x ≤ y ⟹ z * x ≤ z * y"
using mult_left_sub_dist_sup sup.bounded_iff sup_right_divisibility by auto
lemma mult_isotone:
"w ≤ y ⟹ x ≤ z ⟹ w * x ≤ y * z"
using order_trans mult_left_isotone mult_right_isotone by blast
lemma affine_isotone:
"isotone (λx . y * x ⊔ z)"
using isotone_def mult_right_isotone sup_left_isotone by auto
lemma mult_left_sub_dist_sup_left:
"x * y ≤ x * (y ⊔ z)"
by (simp add: mult_right_isotone)
lemma mult_left_sub_dist_sup_right:
"x * z ≤ x * (y ⊔ z)"
by (simp add: mult_right_isotone)
lemma mult_right_sub_dist_sup_left:
"x * z ≤ (x ⊔ y) * z"
by (simp add: mult_left_isotone)
lemma mult_right_sub_dist_sup_right:
"y * z ≤ (x ⊔ y) * z"
by (simp add: mult_left_isotone)
lemma case_split_left:
assumes "1 ≤ w ⊔ z"
and "w * x ≤ y"
and "z * x ≤ y"
shows "x ≤ y"
proof -
have "(w ⊔ z) * x ≤ y"
by (simp add: assms(2-3) mult_right_dist_sup)
thus ?thesis
by (metis assms(1) dual_order.trans mult_left_one mult_left_isotone)
qed
lemma case_split_left_equal:
"w ⊔ z = 1 ⟹ w * x = w * y ⟹ z * x = z * y ⟹ x = y"
by (metis mult_left_one mult_right_dist_sup)
text ‹
Next we consider under which semiring operations the above properties are closed.
›
lemma reflexive_one_closed:
"reflexive 1"
by simp
lemma reflexive_sup_closed:
"reflexive x ⟹ reflexive (x ⊔ y)"
by (simp add: le_supI1)
lemma reflexive_mult_closed:
"reflexive x ⟹ reflexive y ⟹ reflexive (x * y)"
using mult_isotone by fastforce
lemma coreflexive_bot_closed:
"coreflexive bot"
by simp
lemma coreflexive_one_closed:
"coreflexive 1"
by simp
lemma coreflexive_sup_closed:
"coreflexive x ⟹ coreflexive y ⟹ coreflexive (x ⊔ y)"
by simp
lemma coreflexive_mult_closed:
"coreflexive x ⟹ coreflexive y ⟹ coreflexive (x * y)"
using mult_isotone by fastforce
lemma transitive_bot_closed:
"transitive bot"
by simp
lemma transitive_one_closed:
"transitive 1"
by simp
lemma dense_bot_closed:
"dense_rel bot"
by simp
lemma dense_one_closed:
"dense_rel 1"
by simp
lemma dense_sup_closed:
"dense_rel x ⟹ dense_rel y ⟹ dense_rel (x ⊔ y)"
by (metis mult_right_dist_sup order_lesseq_imp sup.mono mult_left_sub_dist_sup_left mult_left_sub_dist_sup_right)
lemma idempotent_bot_closed:
"idempotent bot"
by simp
lemma idempotent_one_closed:
"idempotent 1"
by simp
lemma preorder_one_closed:
"preorder 1"
by simp
lemma coreflexive_transitive:
"coreflexive x ⟹ transitive x"
using mult_left_isotone by fastforce
lemma preorder_idempotent:
"preorder x ⟹ idempotent x"
using order.antisym mult_isotone by fastforce
text ‹
We study the following three ways of defining reflexive-transitive closures.
Each of them is given as a least prefixpoint, but the underlying functions are different.
They implement left recursion, right recursion and symmetric recursion, respectively.
›
abbreviation Lf :: "'a ⇒ ('a ⇒ 'a)" where "Lf y ≡ (λx . 1 ⊔ x * y)"
abbreviation Rf :: "'a ⇒ ('a ⇒ 'a)" where "Rf y ≡ (λx . 1 ⊔ y * x)"
abbreviation Sf :: "'a ⇒ ('a ⇒ 'a)" where "Sf y ≡ (λx . 1 ⊔ y ⊔ x * x)"
abbreviation lstar :: "'a ⇒ 'a" where "lstar y ≡ pμ (Lf y)"
abbreviation rstar :: "'a ⇒ 'a" where "rstar y ≡ pμ (Rf y)"
abbreviation sstar :: "'a ⇒ 'a" where "sstar y ≡ pμ (Sf y)"
text ‹
All functions are isotone and, therefore, if the prefixpoints exist they are also fixpoints.
›
lemma lstar_rec_isotone:
"isotone (Lf y)"
using isotone_def sup_right_divisibility sup_right_isotone mult_right_sub_dist_sup_right by auto
lemma rstar_rec_isotone:
"isotone (Rf y)"
using isotone_def sup_right_divisibility sup_right_isotone mult_left_sub_dist_sup_right by auto
lemma sstar_rec_isotone:
"isotone (Sf y)"
using isotone_def sup_right_isotone mult_isotone by auto
lemma lstar_fixpoint:
"has_least_prefixpoint (Lf y) ⟹ lstar y = μ (Lf y)"
by (simp add: pmu_mu lstar_rec_isotone)
lemma rstar_fixpoint:
"has_least_prefixpoint (Rf y) ⟹ rstar y = μ (Rf y)"
by (simp add: pmu_mu rstar_rec_isotone)
lemma sstar_fixpoint:
"has_least_prefixpoint (Sf y) ⟹ sstar y = μ (Sf y)"
by (simp add: pmu_mu sstar_rec_isotone)
lemma sstar_increasing:
"has_least_prefixpoint (Sf y) ⟹ y ≤ sstar y"
using order_trans pmu_unfold sup_ge1 sup_ge2 by blast
text ‹
The fixpoint given by right recursion is always below the one given by symmetric recursion.
›
lemma rstar_below_sstar:
assumes "has_least_prefixpoint (Rf y)"
and "has_least_prefixpoint (Sf y)"
shows "rstar y ≤ sstar y"
proof -
have "y ≤ sstar y"
using assms(2) pmu_unfold by force
hence "Rf y (sstar y) ≤ Sf y (sstar y)"
by (meson sup.cobounded1 sup.mono mult_left_isotone)
also have "... ≤ sstar y"
using assms(2) pmu_unfold by blast
finally show ?thesis
using assms(1) is_least_prefixpoint_def least_prefixpoint by auto
qed
end
text ‹
Our next structure adds one half of the associativity property.
This inequality holds, for example, for multirelations under the compositions defined by Parikh and Peleg \<^cite>‹"Parikh1983" and "Peleg1987"›.
The converse inequality requires up-closed multirelations for Parikh's composition.
›
class pre_left_semiring = non_associative_left_semiring +
assumes mult_semi_associative: "(x * y) * z ≤ x * (y * z)"
begin
lemma mult_one_associative [simp]:
"x * 1 * y = x * y"
by (metis dual_order.antisym mult_left_isotone mult_left_one mult_semi_associative mult_sub_right_one)
lemma mult_sup_associative_one:
"(x * (y * 1)) * z ≤ x * (y * z)"
by (metis mult_semi_associative mult_one_associative)
lemma rstar_increasing:
assumes "has_least_prefixpoint (Rf y)"
shows "y ≤ rstar y"
proof -
have "Rf y (rstar y) ≤ rstar y"
using assms pmu_unfold by blast
thus ?thesis
by (metis le_supE mult_right_isotone mult_sub_right_one sup.absorb_iff2)
qed
end
text ‹
For the next structure we add a left residual operation.
Such a residual is available, for example, for multirelations.
The operator notation for binary division is introduced in a class that requires a unary inverse.
This is appropriate for fields, but too strong in the present context of semirings.
We therefore reintroduce it without requiring a unary inverse.
›
no_notation
inverse_divide (infixl "'/" 70)
notation
divide (infixl "'/" 70)
class residuated_pre_left_semiring = pre_left_semiring + divide +
assumes lres_galois: "x * y ≤ z ⟷ x ≤ z / y"
begin
text ‹
We first derive basic properties of left residuals from the Galois connection.
›
lemma lres_left_isotone:
"x ≤ y ⟹ x / z ≤ y / z"
using dual_order.trans lres_galois by blast
lemma lres_right_antitone:
"x ≤ y ⟹ z / y ≤ z / x"
using dual_order.trans lres_galois mult_right_isotone by blast
lemma lres_inverse:
"(x / y) * y ≤ x"
by (simp add: lres_galois)
lemma lres_one:
"x / 1 ≤ x"
using mult_sub_right_one order_trans lres_inverse by blast
lemma lres_mult_sub_lres_lres:
"x / (z * y) ≤ (x / y) / z"
using lres_galois mult_semi_associative order.trans by blast
lemma mult_lres_sub_assoc:
"x * (y / z) ≤ (x * y) / z"
by (meson dual_order.trans lres_galois mult_right_isotone lres_inverse lres_mult_sub_lres_lres)
text ‹
With the help of a left residual, it follows that left recursion is below right recursion.
›
lemma lstar_below_rstar:
assumes "has_least_prefixpoint (Lf y)"
and "has_least_prefixpoint (Rf y)"
shows "lstar y ≤ rstar y"
proof -
have "y * (rstar y / y) * y ≤ y * rstar y"
using lres_galois mult_lres_sub_assoc by auto
also have "... ≤ rstar y"
using assms(2) le_supE pmu_unfold by blast
finally have "y * (rstar y / y) ≤ rstar y / y"
by (simp add: lres_galois)
hence "Rf y (rstar y / y) ≤ rstar y / y"
using assms(2) lres_galois rstar_increasing by fastforce
hence "rstar y ≤ rstar y / y"
using assms(2) is_least_prefixpoint_def least_prefixpoint by auto
hence "Lf y (rstar y) ≤ rstar y"
using assms(2) lres_galois pmu_unfold by fastforce
thus ?thesis
using assms(1) is_least_prefixpoint_def least_prefixpoint by auto
qed
text ‹
Moreover, right recursion gives the same result as symmetric recursion.
The next proof follows an argument of \<^cite>‹‹Satz 10.1.5› in "Berghammer2012"›.
›
lemma rstar_sstar:
assumes "has_least_prefixpoint (Rf y)"
and "has_least_prefixpoint (Sf y)"
shows "rstar y = sstar y"
proof -
have "Rf y (rstar y / rstar y) * rstar y ≤ rstar y ⊔ y * ((rstar y / rstar y) * rstar y)"
using mult_right_dist_sup mult_semi_associative sup_right_isotone by auto
also have "... ≤ rstar y ⊔ y * rstar y"
using mult_right_isotone sup_right_isotone lres_inverse by blast
also have "... ≤ rstar y"
using assms(1) pmu_unfold by fastforce
finally have "Rf y (rstar y / rstar y) ≤ rstar y / rstar y"
by (simp add: lres_galois)
hence "rstar y * rstar y ≤ rstar y"
using assms(1) is_least_prefixpoint_def least_prefixpoint lres_galois by auto
hence "y ⊔ rstar y * rstar y ≤ rstar y"
by (simp add: assms(1) rstar_increasing)
hence "Sf y (rstar y) ≤ rstar y"
using assms(1) pmu_unfold by force
hence "sstar y ≤ rstar y"
using assms(2) is_least_prefixpoint_def least_prefixpoint by auto
thus ?thesis
by (simp add: assms order.antisym rstar_below_sstar)
qed
end
context monoid_mult
begin
lemma monoid_power_closed:
assumes "P 1" "P x" "⋀y z . P y ⟹ P z ⟹ P (y * z)"
shows "P (x ^ n)"
proof (induct n)
case 0
thus ?case
by (simp add: assms(1))
next
case (Suc n)
thus ?case
by (simp add: assms(2,3))
qed
end
text ‹
In the next structure we add full associativity of multiplication, as well as a right unit.
Still, multiplication does not need to have a right zero and does not need to distribute over addition from the left.
›
class idempotent_left_semiring = non_associative_left_semiring + monoid_mult
begin
subclass pre_left_semiring
by unfold_locales (simp add: mult_assoc)
lemma zero_right_mult_decreasing:
"x * bot ≤ x"
by (metis bot_least mult_1_right mult_right_isotone)
text ‹
The following result shows that for dense coreflexives there are two equivalent ways to express that a property is preserved.
In the setting of Kleene algebras, this is well known for tests, which form a Boolean subalgebra.
The point here is that only very few properties of tests are needed to show the equivalence.
›
lemma test_preserves_equation:
assumes "dense_rel p"
and "coreflexive p"
shows "p * x ≤ x * p ⟷ p * x = p * x * p"
proof
assume 1: "p * x ≤ x * p"
have "p * x ≤ p * p * x"
by (simp add: assms(1) mult_left_isotone)
also have "... ≤ p * x * p"
using 1 by (simp add: mult_right_isotone mult_assoc)
finally show "p * x = p * x * p"
using assms(2) order.antisym mult_right_isotone by fastforce
next
assume "p * x = p * x * p"
thus "p * x ≤ x * p"
by (metis assms(2) mult_left_isotone mult_left_one)
qed
end
text ‹
The next structure has both distributivity properties of multiplication.
Only a right zero is missing from full semirings.
This is important as many computation models do not have a right zero of sequential composition.
›
class idempotent_left_zero_semiring = idempotent_left_semiring +
assumes mult_left_dist_sup: "x * (y ⊔ z) = x * y ⊔ x * z"
begin
lemma case_split_right:
assumes "1 ≤ w ⊔ z"
and "x * w ≤ y"
and "x * z ≤ y"
shows "x ≤ y"
proof -
have "x * (w ⊔ z) ≤ y"
by (simp add: assms(2-3) mult_left_dist_sup)
thus ?thesis
by (metis assms(1) dual_order.trans mult_1_right mult_right_isotone)
qed
lemma case_split_right_equal:
"w ⊔ z = 1 ⟹ x * w = y * w ⟹ x * z = y * z ⟹ x = y"
by (metis mult_1_right mult_left_dist_sup)
text ‹
This is the first structure we can connect to the semirings provided by Isabelle/HOL.
›
sublocale semiring: ordered_semiring sup bot less_eq less times
apply unfold_locales
using sup_right_isotone apply blast
apply (simp add: mult_right_dist_sup)
apply (simp add: mult_left_dist_sup)
apply (simp add: mult_right_isotone)
by (simp add: mult_left_isotone)
sublocale semiring: semiring_numeral 1 times sup ..
end
text ‹
Completing this part of the hierarchy, we obtain idempotent semirings by adding a right zero of multiplication.
›
class idempotent_semiring = idempotent_left_zero_semiring +
assumes mult_right_zero [simp]: "x * bot = bot"
begin
sublocale semiring: semiring_0 sup bot times
by unfold_locales simp_all
end
subsection ‹Bounded Idempotent Semirings›
text ‹
All of the following semirings have a greatest element in the underlying semilattice order.
With this element, we can express further standard properties of relations.
We extend each class in the above hierarchy in turn.
›
class times_top = times + top
begin
abbreviation vector :: "'a ⇒ bool" where "vector x ≡ x * top = x"
abbreviation covector :: "'a ⇒ bool" where "covector x ≡ top * x = x"
abbreviation total :: "'a ⇒ bool" where "total x ≡ x * top = top"
abbreviation surjective :: "'a ⇒ bool" where "surjective x ≡ top * x = top"
abbreviation "vectors ≡ { x . vector x }"
abbreviation "covectors ≡ { x . covector x }"
end
class bounded_non_associative_left_semiring = non_associative_left_semiring + top +
assumes sup_right_top [simp]: "x ⊔ top = top"
begin
subclass times_top .
text ‹
We first give basic properties of the greatest element.
›
lemma sup_left_top [simp]:
"top ⊔ x = top"
using sup_right_top sup.commute by fastforce
lemma top_greatest [simp]:
"x ≤ top"
by (simp add: le_iff_sup)
lemma top_left_mult_increasing:
"x ≤ top * x"
by (metis mult_left_isotone mult_left_one top_greatest)
lemma top_right_mult_increasing:
"x ≤ x * top"
using mult_right_isotone mult_sub_right_one order_trans top_greatest by blast
lemma top_mult_top [simp]:
"top * top = top"
by (simp add: order.antisym top_left_mult_increasing)
text ‹
Closure of the above properties under the semiring operations is considered next.
›
lemma vector_bot_closed:
"vector bot"
by simp
lemma vector_top_closed:
"vector top"
by simp
lemma vector_sup_closed:
"vector x ⟹ vector y ⟹ vector (x ⊔ y)"
by (simp add: mult_right_dist_sup)
lemma covector_top_closed:
"covector top"
by simp
lemma total_one_closed:
"total 1"
by simp
lemma total_top_closed:
"total top"
by simp
lemma total_sup_closed:
"total x ⟹ total (x ⊔ y)"
by (simp add: mult_right_dist_sup)
lemma surjective_one_closed:
"surjective 1"
by (simp add: order.antisym mult_sub_right_one)
lemma surjective_top_closed:
"surjective top"
by simp
lemma surjective_sup_closed:
"surjective x ⟹ surjective (x ⊔ y)"
by (metis le_iff_sup mult_left_sub_dist_sup_left sup_left_top)
lemma reflexive_top_closed:
"reflexive top"
by simp
lemma transitive_top_closed:
"transitive top"
by simp
lemma dense_top_closed:
"dense_rel top"
by simp
lemma idempotent_top_closed:
"idempotent top"
by simp
lemma preorder_top_closed:
"preorder top"
by simp
end
text ‹
Some closure properties require at least half of associativity.
›
class bounded_pre_left_semiring = pre_left_semiring + bounded_non_associative_left_semiring
begin
lemma vector_mult_closed:
"vector y ⟹ vector (x * y)"
by (metis order.antisym mult_semi_associative top_right_mult_increasing)
lemma surjective_mult_closed:
"surjective x ⟹ surjective y ⟹ surjective (x * y)"
by (metis order.antisym mult_semi_associative top_greatest)
end
text ‹
We next consider residuals with the greatest element.
›
class bounded_residuated_pre_left_semiring = residuated_pre_left_semiring + bounded_pre_left_semiring
begin
lemma lres_top_decreasing:
"x / top ≤ x"
using lres_inverse order.trans top_right_mult_increasing by blast
lemma top_lres_absorb [simp]:
"top / x = top"
using order.antisym lres_galois top_greatest by blast
lemma covector_lres_closed:
"covector x ⟹ covector (x / y)"
by (metis order.antisym mult_lres_sub_assoc top_left_mult_increasing)
end
text ‹
Some closure properties require full associativity.
›
class bounded_idempotent_left_semiring = bounded_pre_left_semiring + idempotent_left_semiring
begin
lemma covector_mult_closed:
"covector x ⟹ covector (x * y)"
by (metis mult_assoc)
lemma total_mult_closed:
"total x ⟹ total y ⟹ total (x * y)"
by (simp add: mult_assoc)
lemma total_power_closed:
"total x ⟹ total (x ^ n)"
apply (rule monoid_power_closed)
using total_mult_closed by auto
lemma surjective_power_closed:
"surjective x ⟹ surjective (x ^ n)"
apply (rule monoid_power_closed)
using surjective_mult_closed by auto
end
text ‹
Some closure properties require distributivity from the left.
›
class bounded_idempotent_left_zero_semiring = bounded_idempotent_left_semiring + idempotent_left_zero_semiring
begin
lemma covector_sup_closed:
"covector x ⟹ covector y ⟹ covector (x ⊔ y)"
by (simp add: mult_left_dist_sup)
end
text ‹
Our final structure is an idempotent semiring with a greatest element.
›
class bounded_idempotent_semiring = bounded_idempotent_left_zero_semiring + idempotent_semiring
begin
lemma covector_bot_closed:
"covector bot"
by simp
end
end