Data.Semiring.Property

See the connections package for idempotent & selective semirings, and lattices.

Required properties of pre-semirings

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.

morphism_presemiring :: Eq s => Presemiring r => Presemiring s => (r -> s) -> r -> r -> r -> Bool

Presemiring morphisms are distributive semigroup morphisms.

This is a required property for presemiring morphisms.

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.

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.

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.

morphism_distribitive_on :: Presemiring r => Presemiring s => Rel s b -> (r -> s) -> r -> r -> r -> b

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

Presemiring morphisms must be compatible with right-distribution.

Required properties of semirings

morphism_semiring :: Eq s => Semiring r => Semiring s => (r -> s) -> r -> r -> r -> Bool

Semiring morphisms are monoidal presemiring morphisms.

This is a required property for semiring morphisms.

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.

Left-distributive presemirings and semirings

distributive_xmult_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 xmult-multiplication.

distributive_xmult1_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) xmult-multiplication.

Commutative presemirings & semirings

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.

Cancellative presemirings & semirings

cancellative_addition_on :: (Additive - Semigroup) r => Rel r Bool -> r -> r -> r -> Bool

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

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

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

cancellative_multiplication_on :: (Multiplicative - Semigroup) r => Rel r Bool -> r -> r -> r -> Bool

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

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