<~ is a preordered relation relative to <>.

This is a required property.

mempty is a minimal or least element of r.

This is a required property.

( 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.

$\forall a, b: a + b = 0 \Rightarrow a = 0 \wedge b = 0$

This is a required property.

( 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.

<~ is consistent with annihilativity.

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

(one <~) ≡ (one ==)

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

$\forall a, b: a * b = 0 \Rightarrow a = 0 \vee b = 0$

$\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

$\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

$\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.

$\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.

$\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

$\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.

$\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.

$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

$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:

$\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$