Data.Dioid.Property

Properties of pre-semirings & semirings

neutral_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> Bool

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

A (pre-)semiring with a right-neutral additive unit must satisfy:

neutral_addition mempty ~~ const True

Or, equivalently:

mempty <> r ~~ r

This is a required property.

neutral_addition' :: (Eq r, Prd r, Monoid r, Semigroup r) => r -> Bool

neutral_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> Bool

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

A (pre-)semiring with a right-neutral multiplicative unit must satisfy:

neutral_multiplication unit ~~ const True

Or, equivalently:

unit >< r ~~ r

This is a required property.

neutral_multiplication' :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool

associative_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> r -> Bool

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

R must right-associate addition.

This should be verified by the underlying Semigroup instance, but is included here for completeness.

This is a required property.

associative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool

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

R must right-associate multiplication.

This is a required property.

distributive :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool

\( \forall a, b, c \in R: (a + b) * c = (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.

Properties of non-unital (near-)semirings

nonunital :: forall r. (Eq r, Prd r, Monoid r, Semiring r) => r -> r -> Bool

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

If R is non-unital (i.e. unit equals mempty) 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.

Properties of unital semirings

annihilative_multiplication :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool

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

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

mempty >< a ~~ mempty

For Alternative instances this property translates to:

empty *> a ~~ empty

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

mempty >< NaN ~~ NaN

This is a required property.

homomorphism_boolean :: (Eq r, Monoid r, Semiring r) => Bool -> Bool -> Bool

fromBoolean must be a semiring homomorphism into R.

This is a required property.

Properties of cancellative semirings

cancellative_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> r -> Bool

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

If R is right-cancellative wrt addition then for all a the section (a <>) is injective.

cancellative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool

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

If R is right-cancellative wrt multiplication then for all a the section (a ><) is injective.

Properties of commutative semirings

commutative_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> Bool

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

commutative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> Bool

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

Properties of absorbative semirings

absorbative_addition :: (Eq r, Prd r, Semiring r) => r -> r -> Bool

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

Right-additive absorbativity is a generalized form of idempotency:

absorbative_addition unit a ~~ a <> a ~~ a

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

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

Left-additive absorbativity is a generalized form of idempotency:

absorbative_addition unit a ~~ a <> a ~~ a

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

absorbative_multiplication :: (Eq r, Prd r, Semiring 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, Prd r, Semiring 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 semirings

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

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

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

unit <> a ~~ unit

For a dioid this is equivalent to:

(unit <~) ~~ (unit ~~)

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

pure a <|> _ ~~ pure a

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

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

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

a <> unit ~~ unit

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

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

codistributive :: (Eq r, Prd r, Semiring 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 unit:

 codistributive unit a mempty ~~ unit ~~ unit <> 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 ordered semirings

ordered_preordered :: (Prd r, Semiring r) => r -> r -> Bool

<~ is a preordered relation relative to <>.

This is a required property.

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

mempty is a minimal or least element of r.

This is a required property.

ordered_monotone_addition :: (Prd r, Semiring 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 :: (Prd r, Semiring 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_unit :: (Prd r, Monoid r, Semiring r) => r -> Bool

<~ is consistent with annihilativity.

This means that a dioid with an annihilative multiplicative unit 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 :: (Prd r, Monoid r, Semiring r) => r -> r -> Bool

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