Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Data.Dioid.Property
Contents
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
amempty
~~unit
~~unit
<>
a
idempotent mulitiplication:
codistributive
mempty
mempty
a ~~ a ~~ a><
a
and idempotent addition:
codistributive
amempty
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
==)