Data.Dioid.Property

Required properties of pre-dioids

nonunital_on :: Presemiring r => Rel r b -> r -> r -> b

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

If R is non-unital (i.e. one is not distinct from zero) then it will instead satisfy a right-absorbtion property.

This follows from right-neutrality and right-distributivity.

Compare codistributive and closed_stable.

When R is also left-distributive we get: \( \forall a, b \in R: a * b = a + a * b + b \)

See also Warning and https://blogs.ncl.ac.uk/andreymokhov/united-monoids/#whatif.

associative_addition_on :: (Additive - Semigroup) r => Rel r b -> r -> r -> r -> b

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

All semigroups must right-associate addition.

This is a required property.

associative_multiplication_on :: (Multiplicative - Semigroup) r => Rel r b -> r -> r -> r -> b

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

All semigroups must right-associate multiplication.

This is a required property.

distributive_on :: Presemiring r => Rel r b -> r -> r -> r -> b

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

R must right-distribute multiplication.

When R is a functor and the semiring structure is derived from Alternative, this translates to:

(a <|> b) *> c = (a *> c) <|> (b *> c)

See https://en.wikibooks.org/wiki/Haskell/Alternative_and_MonadPlus.

This is a required property.

distributive_finite1_on :: (Presemiring r, Foldable1 f) => Rel r b -> f r -> r -> b

\( \forall M \geq 1; a_1 \dots a_M, b \in R: (\sum_{i=1}^M a_i) * b \sim \sum_{i=1}^M a_i * b \)

R must right-distribute multiplication over finite (non-empty) sums.

For types with exact arithmetic this follows from distributive and the universality of fold1.

commutative_addition_on :: (Additive - Semigroup) r => Rel r b -> r -> r -> b

\( \forall a, b \in R: a + b \sim b + a \)

This is a an optional property for semigroups, and a required property for semirings.

preordered :: Prd r => (Additive - Semigroup) r => r -> r -> Bool

<= is a preordered relation relative to +.

This is a required property.

morphism_predioid :: Prd r => Prd s => Predioid r => Predioid s => (r -> s) -> r -> r -> r -> Bool

Predioid morphisms are monotone, distributive semigroup morphisms.

This is a required property for predioid morphisms.

monotone_addition :: Prd r => (Additive - Semigroup) 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_on.

monotone_addition x y z <==> morphism_predioid (add x) y z 

This is a required property.

monotone_multiplication :: Prd r => (Multiplicative - Semigroup) 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_on.

monotone_multiplication x y z <==> morphism_predioid (mul x) y z

This is a required property.

Required properties of dioids

neutral_addition_on :: (Additive - Monoid) r => Rel r b -> r -> b

\( \forall a \in R: (z + a) \sim a \)

A semigroup with a right-neutral additive identity must satisfy:

neutral_addition zero ~~ const True

Or, equivalently:

zero + r ~~ r

This is a required property for additive monoids.

neutral_multiplication_on :: (Multiplicative - Monoid) r => Rel r b -> r -> b

\( \forall a \in R: (o * a) \sim a \)

A semigroup with a right-neutral multiplicative identity must satisfy:

neutral_multiplication one ~~ const True

Or, equivalently:

one * r ~~ r

This is a required propert for multiplicative monoids.

annihilative_multiplication_on :: Semiring r => Rel r b -> r -> b

\( \forall a \in R: (z * a) \sim u \)

A R is semiring then its addititive one must be right-annihilative, i.e.:

zero * a ~~ zero

For Alternative instances this property translates to:

empty *> a ~~ empty

All right semirings must have a right-absorbative addititive one, however note that depending on the Prd instance this does not preclude IEEE754-mandated behavior such as:

zero * NaN ~~ NaN

This is a required property.

distributive_finite_on :: (Semiring r, Foldable f) => Rel r b -> f r -> r -> b

\( \forall M \geq 0; a_1 \dots a_M, b \in R: (\sum_{i=1}^M a_i) * b \sim \sum_{i=1}^M a_i * b \)

R must right-distribute multiplication between finite sums.

For types with exact arithmetic this follows from distributive & neutral_multiplication.

monotone_zero :: Prd r => (Additive - Monoid) r => r -> Bool

zero is a minimal or least element of r.

This is a required property.

morphism_dioid :: Prd r => Prd s => Dioid r => Dioid s => (r -> s) -> r -> r -> r -> Bool

Dioid morphisms are monoidal predioid morphisms.

This is a required property for dioid morphisms.

annihilative_unit :: Prd r => (Multiplicative - Monoid) r => r -> Bool

<= is consistent with annihilativity.

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

(one <=) = (one ==)

This is a required property.

pos_addition :: Prd r => (Additive - Monoid) r => r -> r -> Bool

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

This is a required property.

pos_multiplication :: Dioid r => r -> r -> Bool

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

Dioids which are groups wrt multiplication are often referred to as pos dioids or semi-fields

Left distributive pre-dioids & dioids

distributive_cross_on :: (Semiring r, Applicative f, Foldable f) => Rel r b -> f r -> f r -> b

\( \forall M,N \geq 0; a_1 \dots a_M, b_1 \dots b_N \in R: (\sum_{i=1}^M a_i) * (\sum_{j=1}^N b_j) \sim \sum_{i=1 j=1}^{i=M j=N} a_i * b_j \)

If R is also left-distributive then it supports cross-multiplication.

distributive_cross1_on :: (Presemiring r, Apply f, Foldable1 f) => Rel r b -> f r -> f r -> b

\( \forall M,N \geq 1; a_1 \dots a_M, b_1 \dots b_N \in R: (\sum_{i=1}^M a_i) * (\sum_{j=1}^N b_j) = \sum_{i=1 j=1}^{i=M j=N} a_i * b_j \)

If R is also left-distributive then it supports (non-empty) cross-multiplication.

Commutative pre-dioids & dioids

commutative_multiplication_on :: (Multiplicative - Semigroup) r => Rel r b -> r -> r -> b

\( \forall a, b \in R: a * b \sim b * a \)

This is a an optional property for semigroups, and a optional property for semirings. It is a required property for rings.

Absorbative pre-dioids & dioids

absorbative_addition_on :: Presemiring r => Rel r b -> r -> r -> b

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

Right-additive absorbativity is a generalized form of idempotency:

absorbative_addition one a ~~ a + a ~~ a

This is a required property for semilattices and lattices.

absorbative_addition_on' :: Presemiring r => Rel r b -> r -> r -> b

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

Left-additive absorbativity is a generalized form of idempotency:

absorbative_addition one a ~~ a + a ~~ a

absorbative_multiplication_on :: Presemiring r => Rel r b -> r -> r -> b

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

Right-mulitplicative absorbativity is a generalized form of idempotency:

absorbative_multiplication zero a ~~ a * a ~~ a

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

This is a required property for semilattices and lattices.

absorbative_multiplication_on' :: Presemiring r => Rel r b -> r -> r -> b

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

Left-mulitplicative absorbativity is a generalized form of idempotency:

absorbative_multiplication' zero a ~~ a * a ~~ a

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

Annihilative pre-dioids & dioids

annihilative_addition :: Eq r => Dioid r => r -> Bool

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

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

one + a ~~ one

For a dioid this is equivalent to:

(one <=) = (one ~~)

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

pure a <|> _ ~~ pure a

This is a required property for bounded lattices.

annihilative_addition' :: Eq r => Dioid r => r -> Bool

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

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

a + one ~~ one

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

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

This is a required property for bounded lattices.

codistributive :: Eq r => Predioid 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 one:

 codistributive one a zero = one ~~ one + a

idempotent mulitiplication:

 codistributive zero zero a = a ~~ a * a

and idempotent addition:

 codistributive a zero a = a ~~ a + a

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

Idempotent pre-dioids & dioids

monotone_addition' :: Prd r => (Additive - Semigroup) r => r -> r -> Bool

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

This is a required property for semilattices and lattices.

idempotent_addition :: Eq r => Dioid r => r -> Bool

\( \forall a : a + a = a \)

See https://en.wikipedia.org/wiki/Band_(mathematics).

This is a required property for semilattices and lattices.

idempotent_multiplication :: Eq r => Dioid r => r -> Bool

\( \forall a : a * a = a \)

This is a required property for semilattices and lattices.