Data.Dioid.Property

Properties of dioids (aka ordered semirings)

ordered_preordered :: Dioid r => r -> r -> Bool

<~ is a preordered relation relative to <>.

This is a required property.

ordered_monotone_zero :: (Monoid r, Dioid r) => r -> Bool

mempty is a minimal or least element of r.

This is a required property.

ordered_monotone_addition :: Dioid r => r -> r -> r -> Bool

( forall a, b, c: b leq c Rightarrow b + a leq c + a

In an ordered semiring this follows directly from the definition of <~.

Compare cancellative_addition.

This is a required property.

ordered_positive_addition :: (Prd r, Monoid r) => r -> r -> Bool

\( \forall a, b: a + b = 0 \Rightarrow a = 0 \wedge b = 0 \)

This is a required property.

ordered_monotone_multiplication :: Dioid r => r -> r -> r -> Bool

( forall a, b, c: b leq c Rightarrow b * a leq c * a

In an ordered semiring this follows directly from distributive and the definition of <~.

Compare cancellative_multiplication.

This is a required property.

ordered_annihilative_sunit :: (Monoid r, Dioid r) => r -> Bool

<~ is consistent with annihilativity.

This means that a dioid with an annihilative multiplicative sunit must satisfy:

(one <~) ≡ (one ==)

ordered_idempotent_addition :: (Prd r, Monoid r) => r -> r -> Bool

( forall a, b: a leq b Rightarrow a + b = b

ordered_positive_multiplication :: (Monoid r, Dioid r) => r -> r -> Bool

\( \forall a, b: a * b = 0 \Rightarrow a = 0 \vee b = 0 \)

Properties of absorbative dioids

absorbative_addition :: (Eq r, Dioid r) => r -> r -> Bool

\( \forall a, b \in R: a * b + b = b \)

Right-additive absorbativity is a generalized form of idempotency:

absorbative_addition sunit a ~~ a <> a ~~ a

absorbative_addition' :: (Eq r, Dioid r) => r -> r -> Bool

\( \forall a, b \in R: b + b * a = b \)

Left-additive absorbativity is a generalized form of idempotency:

absorbative_addition sunit a ~~ a <> a ~~ a

idempotent_addition :: (Eq r, Monoid r, Dioid r) => r -> Bool

absorbative_multiplication :: (Eq r, Dioid r) => r -> r -> Bool

\( \forall a, b \in R: (a + b) * b = b \)

Right-mulitplicative absorbativity is a generalized form of idempotency:

absorbative_multiplication mempty a ~~ a >< a ~~ a

See https://en.wikipedia.org/wiki/Absorption_law.

absorbative_multiplication' :: (Eq r, Dioid r) => r -> r -> Bool

\( \forall a, b \in R: b * (b + a) = b \)

Left-mulitplicative absorbativity is a generalized form of idempotency:

absorbative_multiplication' mempty a ~~ a >< a ~~ a

See https://en.wikipedia.org/wiki/Absorption_law.

Properties of annihilative dioids

annihilative_addition :: (Eq r, Monoid r, Dioid r) => r -> Bool

\( \forall a \in R: o + a = o \)

A unital semiring with a right-annihilative muliplicative sunit must satisfy:

sunit <> a ~~ sunit

For a dioid this is equivalent to:

(sunit <~) ~~ (sunit ~~)

For Alternative instances this is known as the left-catch law:

pure a <|> _ ~~ pure a

annihilative_addition' :: (Eq r, Monoid r, Dioid r) => r -> Bool

\( \forall a \in R: a + o = o \)

A unital semiring with a left-annihilative muliplicative sunit must satisfy:

a <> sunit ~~ sunit

Note that the left-annihilative property is too strong for many instances. This is because it requires that any effects that r generates be undsunit.

See https://winterkoninkje.dreamwidth.org/90905.html.

codistributive :: (Eq r, Dioid r) => r -> r -> r -> Bool

\( \forall a, b, c \in R: c + (a * b) \equiv (c + a) * (c + b) \)

A right-codistributive semiring has a right-annihilative muliplicative sunit:

 codistributive sunit a mempty ~~ sunit ~~ sunit <> a

idempotent mulitiplication:

 codistributive mempty mempty a ~~ a ~~ a >< a

and idempotent addition:

 codistributive a mempty a ~~ a ~~ a <> a

Furthermore if R is commutative then it is a right-distributive lattice.

Properties of kleene dioids

kleene_pstable :: (Eq r, Prd r, Monoid r, Dioid r) => Natural -> r -> Bool

\( 1 + \sum_{i=1}^{P+1} a^i = 1 + \sum_{i=1}^{P} a^i \)

If a is p-stable for some p, then we have:

powers p a ~~ a >< powers p a <> sunit  ~~ powers p a >< a <> sunit 

If <> and >< are idempotent then every element is 1-stable:

 a >< a <> a <> sunit = a <> a <> sunit = a <> sunit

kleene_paffine :: (Eq r, Monoid r, Dioid r) => Natural -> r -> r -> Bool

\( x = a * x + b \Rightarrow x = (1 + \sum_{i=1}^{P} a^i) * b \)

If a is p-stable for some p, then we have:

kleene_stable :: (Eq r, Monoid r, Dioid r, Kleene r) => r -> Bool

\( \forall a \in R : a^* = a^* * a + 1 \)

Closure is p-stability for all a in the limit as \( p \to \infinity \).

One way to think of this property is that all geometric series "converge":

\( \forall a \in R : 1 + \sum_{i \geq 1} a^i \in R \)

kleene_affine :: (Eq r, Monoid r, Dioid r, Kleene r) => r -> r -> Bool

idempotent_star :: (Eq r, Monoid r, Dioid r, Kleene r) => r -> Bool