Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

## Synopsis

- neutral_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> Bool
- neutral_addition' :: (Eq r, Prd r, Monoid r, Semigroup r) => r -> Bool
- neutral_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> Bool
- neutral_multiplication' :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool
- associative_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> r -> Bool
- associative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool
- distributive :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool
- nonunital :: forall r. (Eq r, Prd r, Monoid r, Semiring r) => r -> r -> Bool
- annihilative_multiplication :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool
- homomorphism_boolean :: (Eq r, Monoid r, Semiring r) => Bool -> Bool -> Bool
- cancellative_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> r -> Bool
- cancellative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool
- commutative_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> Bool
- commutative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> Bool
- absorbative_addition :: (Eq r, Prd r, Semiring r) => r -> r -> Bool
- absorbative_addition' :: (Eq r, Prd r, Semiring r) => r -> r -> Bool
- idempotent_addition :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool
- absorbative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> Bool
- absorbative_multiplication' :: (Eq r, Prd r, Semiring r) => r -> r -> Bool
- annihilative_addition :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool
- annihilative_addition' :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool
- codistributive :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool
- ordered_preordered :: (Prd r, Semiring r) => r -> r -> Bool
- ordered_monotone_zero :: (Prd r, Monoid r) => r -> Bool
- ordered_monotone_addition :: (Prd r, Semiring r) => r -> r -> r -> Bool
- ordered_positive_addition :: (Prd r, Monoid r) => r -> r -> Bool
- ordered_monotone_multiplication :: (Prd r, Semiring r) => r -> r -> r -> Bool
- ordered_annihilative_unit :: (Prd r, Monoid r, Semiring r) => r -> Bool
- ordered_idempotent_addition :: (Prd r, Monoid r) => r -> r -> Bool
- ordered_positive_multiplication :: (Prd r, Monoid r, Semiring r) => r -> r -> Bool

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

*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 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)

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

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

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_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`

==)