Safe Haskell	Safe
Language	Haskell2010

Data.Semilattice.Property

Contents

Properties of join lattices
Properties of meet semilattices
Properties of lattices
Properties of semilattice & lattice morphisms

Synopsis

monotone_join :: JoinSemilattice r => r -> r -> r -> Bool
idempotent_join :: JoinSemilattice r => r -> Bool
idempotent_join_on :: (Join - Semigroup) r => Rel r b -> r -> b
associative_join :: JoinSemilattice r => r -> r -> r -> Bool
associative_join_on :: (Join - Semigroup) r => Rel r b -> r -> r -> r -> b
commutative_join :: JoinSemilattice r => r -> r -> Bool
commutative_join_on :: (Join - Semigroup) r => Rel r b -> r -> r -> b
neutral_join :: BoundedJoinSemilattice r => r -> Bool
neutral_join_on :: (Join - Monoid) r => Rel r b -> r -> b
distributive_join :: JoinSemilattice r => r -> r -> r -> r -> r -> Bool
monotone_meet :: MeetSemilattice r => r -> r -> r -> Bool
idempotent_meet :: MeetSemilattice r => r -> Bool
idempotent_meet_on :: (Meet - Semigroup) r => Rel r b -> r -> b
associative_meet :: MeetSemilattice r => r -> r -> r -> Bool
associative_meet_on :: (Meet - Semigroup) r => Rel r b -> r -> r -> r -> b
commutative_meet :: MeetSemilattice r => r -> r -> Bool
commutative_meet_on :: (Meet - Semigroup) r => Rel r b -> r -> r -> b
neutral_meet :: BoundedMeetSemilattice r => r -> Bool
neutral_meet_on :: (Meet - Monoid) r => Rel r b -> r -> b
distributive_meet :: MeetSemilattice r => r -> r -> r -> r -> r -> Bool
absorbative :: Lattice r => r -> r -> Bool
absorbative' :: Lattice r => r -> r -> Bool
annihilative_join :: UpperBoundedLattice r => r -> Bool
annihilative_meet :: LowerBoundedLattice r => r -> Bool
distributive :: Lattice r => r -> r -> r -> Bool
codistributive :: Lattice r => r -> r -> r -> Bool
majority_glb :: Lattice r => r -> r -> Bool
commutative_glb :: Lattice r => r -> r -> r -> Bool
commutative_glb' :: Lattice r => r -> r -> r -> Bool
associative_glb :: Lattice r => r -> r -> r -> r -> Bool
morphism_join :: JoinSemilattice r => JoinSemilattice s => (r -> s) -> r -> r -> Bool
morphism_join_on :: (Join - Semigroup) r => (Join - Semigroup) s => Rel s b -> (r -> s) -> r -> r -> b
morphism_join' :: BoundedJoinSemilattice r => BoundedJoinSemilattice s => (r -> s) -> Bool
morphism_join_on' :: (Join - Monoid) r => (Join - Monoid) s => Rel s b -> (r -> s) -> b
morphism_meet :: MeetSemilattice r => MeetSemilattice s => (r -> s) -> r -> r -> Bool
morphism_meet_on :: (Meet - Semigroup) r => (Meet - Semigroup) s => Rel s b -> (r -> s) -> r -> r -> b
morphism_meet' :: BoundedMeetSemilattice r => BoundedMeetSemilattice s => (r -> s) -> Bool
morphism_meet_on' :: (Meet - Monoid) r => (Meet - Monoid) s => Rel s b -> (r -> s) -> b
morphism_distributive :: Prd r => Prd s => Lattice r => Lattice s => (r -> s) -> r -> r -> r -> Bool

Properties of join lattices

monotone_join :: JoinSemilattice r => r -> r -> r -> Bool Source #

\( \forall a, b, c: b \leq c \Rightarrow b ∨ a \leq c ∨ a \)

This is a required property.

idempotent_join :: JoinSemilattice r => r -> Bool Source #

\( \forall a \in R: a ∨ a = a \)

 idempotent_join = absorbative top

See https://en.wikipedia.org/wiki/Band_(mathematics).

This is a required property.

idempotent_join_on :: (Join - Semigroup) r => Rel r b -> r -> b Source #

associative_join :: JoinSemilattice r => r -> r -> r -> Bool Source #

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

This is a required property.

associative_join_on :: (Join - Semigroup) r => Rel r b -> r -> r -> r -> b Source #

commutative_join :: JoinSemilattice r => r -> r -> Bool Source #

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

This is a required property.

commutative_join_on :: (Join - Semigroup) r => Rel r b -> r -> r -> b Source #

neutral_join :: BoundedJoinSemilattice r => r -> Bool Source #

\( \forall a \in R: (bottom ∨ a) = a \)

This is a required property for bounded join semilattices.

neutral_join_on :: (Join - Monoid) r => Rel r b -> r -> b Source #

distributive_join :: JoinSemilattice r => r -> r -> r -> r -> r -> Bool Source #

\( \forall a, b, c: c \leq a ∨ b \Rightarrow \exists a',b': c = a' ∨ b' \)

See https://en.wikipedia.org/wiki/Distributivity_(order_theory)#Distributivity_for_semilattices

This is a required property for distributive join semilattices.

Properties of meet semilattices

monotone_meet :: MeetSemilattice r => r -> r -> r -> Bool Source #

\( \forall a, b, c: b \leq c \Rightarrow b ∧ a \leq c ∧ a \)

This is a required property.

idempotent_meet :: MeetSemilattice r => r -> Bool Source #

\( \forall a \in R: a ∧ a = a \)

 idempotent_meet = absorbative bottom

See https://en.wikipedia.org/wiki/Band_(mathematics).

This is a required property.

idempotent_meet_on :: (Meet - Semigroup) r => Rel r b -> r -> b Source #

associative_meet :: MeetSemilattice r => r -> r -> r -> Bool Source #

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

This is a required property.

associative_meet_on :: (Meet - Semigroup) r => Rel r b -> r -> r -> r -> b Source #

commutative_meet :: MeetSemilattice r => r -> r -> Bool Source #

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

This is a required property.

commutative_meet_on :: (Meet - Semigroup) r => Rel r b -> r -> r -> b Source #

neutral_meet :: BoundedMeetSemilattice r => r -> Bool Source #

\( \forall a \in R: (bottom ∧ a) = a \)

This is a required property for bounded meet semilattices.

neutral_meet_on :: (Meet - Monoid) r => Rel r b -> r -> b Source #

distributive_meet :: MeetSemilattice r => r -> r -> r -> r -> r -> Bool Source #

\( \forall a, b, c: c \leq a ∨ b \Rightarrow \exists a',b': c = a' ∧ b' \)

See https://en.wikipedia.org/wiki/Distributivity_(order_theory)#Distributivity_for_semilattices

This is a required property for distributive meet semilattices.

Properties of lattices

absorbative :: Lattice r => r -> r -> Bool Source #

\( \forall a, b \in R: a ∧ b ∨ b = b \)

Absorbativity is a generalized form of idempotency:

absorbative top a = a ∨ a = a

This is a required property.

absorbative' :: Lattice r => r -> r -> Bool Source #

\( \forall a, b \in R: a ∨ b ∧ b = b \)

Absorbativity is a generalized form of idempotency:

absorbative' bottom a = a ∨ a = a

This is a required property.

annihilative_join :: UpperBoundedLattice r => r -> Bool Source #

\( \forall a \in R: (top ∨ a) = top \)

If R is a lattice then its top element must be annihilative.

This is a required property.

annihilative_meet :: LowerBoundedLattice r => r -> Bool Source #

\( \forall a \in R: (bottom ∧ a) = bottom \)

If R is a lattice then its bottom element must be annihilative.

For Semiring instances this property translates to:

zero * a = zero

For Alternative instances this property translates to:

empty *> a = empty

This is a required property.

distributive :: Lattice r => r -> r -> r -> Bool Source #

codistributive :: Lattice 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 meet:

 codistributive top a bottom = top =~ top ∨ a

idempotent mulitiplication:

 codistributive bottom bottom a = a =~ a ∧ a

and idempotent addition:

 codistributive a bottom a = a =~ a ∨ a

Furthermore if R is commutative then it is a right-distributive lattice.

majority_glb :: Lattice r => r -> r -> Bool Source #

 glb x x y = x

commutative_glb :: Lattice r => r -> r -> r -> Bool Source #

 glb x y z = glb z x y

commutative_glb' :: Lattice r => r -> r -> r -> Bool Source #

 glb x y z = glb x z y

associative_glb :: Lattice r => r -> r -> r -> r -> Bool Source #

 glb (glb x w y) w z = glb x w (glb y w z)

Properties of semilattice & lattice morphisms

morphism_join :: JoinSemilattice r => JoinSemilattice s => (r -> s) -> r -> r -> Bool Source #

\( \forall a, b: f(a ∨ b) = f(a) ∨ f(b) \)

Given two join-semilattices (S, ∨) and (T, ∨), a homomorphism is a monotone function f: S → T such that

 f (x ∨ y) =~ f x ∨ f y

This is a required property for join semilattice morphisms.

morphism_join_on :: (Join - Semigroup) r => (Join - Semigroup) s => Rel s b -> (r -> s) -> r -> r -> b Source #

morphism_join' :: BoundedJoinSemilattice r => BoundedJoinSemilattice s => (r -> s) -> Bool Source #

\( \forall a, b: f(bottom) = bottom \)

This is a required property for bounded join semilattice morphisms.

morphism_join_on' :: (Join - Monoid) r => (Join - Monoid) s => Rel s b -> (r -> s) -> b Source #

morphism_meet :: MeetSemilattice r => MeetSemilattice s => (r -> s) -> r -> r -> Bool Source #

\( \forall a, b: f(a ∧ b) = f(a) ∧ f(b) \)

The obvious dual replacing ∧ with ∨ and bottom with top transforms this definition of a join-semilattice homomorphism into its meet-semilattice equivalent.

This is a required property for meet semilattice morphisms.

morphism_meet_on :: (Meet - Semigroup) r => (Meet - Semigroup) s => Rel s b -> (r -> s) -> r -> r -> b Source #

morphism_meet' :: BoundedMeetSemilattice r => BoundedMeetSemilattice s => (r -> s) -> Bool Source #

\( \forall a, b: f(top) = top \)

This is a required property for bounded meet semilattice morphisms.

morphism_meet_on' :: (Meet - Monoid) r => (Meet - Monoid) s => Rel s b -> (r -> s) -> b Source #

morphism_distributive :: Prd r => Prd s => Lattice r => Lattice s => (r -> s) -> r -> r -> r -> Bool Source #

Distributive lattice morphisms are compatible with glb.