connections-0.0.1: Partial orders, Galois connections, ordered semirings, & residuated lattices.

Data.Dioid.Property

Synopsis

# Properties of pre-semirings & semirings

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

$$\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_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> Bool Source #

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

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

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

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 Source #

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

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


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 Source #

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

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

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

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

$$\forall a, b \in R: a + b = b + a$$

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

$$\forall a, b \in R: a * b = b * a$$

# Properties of absorbative semirings

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

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

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


absorbative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> Bool Source #

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


absorbative_multiplication' :: (Eq r, Prd r, Semiring r) => r -> r -> Bool Source #

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


# Properties of annihilative semirings

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

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

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

codistributive :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool Source #

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

 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 Source #

<~ is a preordered relation relative to <>.

This is a required property.

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

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 Source #

( 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 Source #

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

( 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 Source #

<~ 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 Source #

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

ordered_positive_multiplication :: (Prd r, Monoid r, Semiring r) => r -> r -> Bool Source #

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