Algebra.Lattice

In mathematics, a lattice is a partially ordered set in which every two elements have a unique supremum (also called a least upper bound or join) and a unique infimum (also called a greatest lower bound or meet).

In this module lattices are defined using meet and join operators, as it's constructive one.

Unbounded lattices

class JoinSemiLattice a where

A algebraic structure with element joins: http://en.wikipedia.org/wiki/Semilattice

Associativity: x \/ (y \/ z) == (x \/ y) \/ z
Commutativity: x \/ y == y \/ x
Idempotency:   x \/ x == x

Minimal complete definition

Nothing

Methods

(\/) :: a -> a -> a infixr 5

join :: a -> a -> a

Instances

JoinSemiLattice Bool

JoinSemiLattice ()

JoinSemiLattice All

JoinSemiLattice Any

JoinSemiLattice IntSet

JoinSemiLattice Void

JoinSemiLattice a => JoinSemiLattice (Endo a)

JoinSemiLattice v => JoinSemiLattice (IntMap v)

Ord a => JoinSemiLattice (Set a)

(Eq a, Hashable a) => JoinSemiLattice (HashSet a)

JoinSemiLattice a => JoinSemiLattice (Dropped a)

JoinSemiLattice a => JoinSemiLattice (Levitated a)

JoinSemiLattice a => JoinSemiLattice (Lifted a)

JoinSemiLattice v => JoinSemiLattice (k -> v)

(JoinSemiLattice a, JoinSemiLattice b) => JoinSemiLattice (a, b)

JoinSemiLattice (Proxy * a)

(Ord k, JoinSemiLattice v) => JoinSemiLattice (Map k v)

(Eq k, Hashable k) => JoinSemiLattice (HashMap k v)

JoinSemiLattice a => JoinSemiLattice (Tagged * t a)

class MeetSemiLattice a where

A algebraic structure with element meets: http://en.wikipedia.org/wiki/Semilattice

Associativity: x /\ (y /\ z) == (x /\ y) /\ z
Commutativity: x /\ y == y /\ x
Idempotency:   x /\ x == x

Minimal complete definition

Nothing

Methods

(/\) :: a -> a -> a infixr 6

meet :: a -> a -> a

Instances

MeetSemiLattice Bool

MeetSemiLattice ()

MeetSemiLattice All

MeetSemiLattice Any

MeetSemiLattice Void

MeetSemiLattice a => MeetSemiLattice (Endo a)

Ord a => MeetSemiLattice (Set a)

(Eq a, Hashable a) => MeetSemiLattice (HashSet a)

MeetSemiLattice a => MeetSemiLattice (Dropped a)

MeetSemiLattice a => MeetSemiLattice (Levitated a)

MeetSemiLattice a => MeetSemiLattice (Lifted a)

MeetSemiLattice v => MeetSemiLattice (k -> v)

(MeetSemiLattice a, MeetSemiLattice b) => MeetSemiLattice (a, b)

MeetSemiLattice (Proxy * a)

(Ord k, MeetSemiLattice v) => MeetSemiLattice (Map k v)

(Eq k, Hashable k) => MeetSemiLattice (HashMap k v)

MeetSemiLattice a => MeetSemiLattice (Tagged * t a)

class (JoinSemiLattice a, MeetSemiLattice a) => Lattice a

The combination of two semi lattices makes a lattice if the absorption law holds: see http://en.wikipedia.org/wiki/Absorption_law and http://en.wikipedia.org/wiki/Lattice_(order)

Absorption: a \/ (a /\ b) == a /\ (a \/ b) == a

Instances

Lattice Bool

Lattice ()

Lattice All

Lattice Any

Lattice Void

Lattice a => Lattice (Endo a)

Ord a => Lattice (Set a)

Lattice a => Lattice (Dropped a)

Lattice a => Lattice (Levitated a)

Lattice a => Lattice (Lifted a)

Lattice v => Lattice (k -> v)

(Lattice a, Lattice b) => Lattice (a, b)

Lattice (Proxy * a)

(Ord k, Lattice v) => Lattice (Map k v)

Lattice a => Lattice (Tagged * t a)

joinLeq :: (Eq a, JoinSemiLattice a) => a -> a -> Bool

The partial ordering induced by the join-semilattice structure

joins1 :: JoinSemiLattice a => [a] -> a

The join of at a list of join-semilattice elements (of length at least one)

meetLeq :: (Eq a, MeetSemiLattice a) => a -> a -> Bool

The partial ordering induced by the meet-semilattice structure

meets1 :: MeetSemiLattice a => [a] -> a

The meet of at a list of meet-semilattice elements (of length at least one)

Bounded lattices

class JoinSemiLattice a => BoundedJoinSemiLattice a where

A join-semilattice with some element |bottom| that / approaches.

Identity: x \/ bottom == x

Methods

bottom :: a

Instances

BoundedJoinSemiLattice Bool

BoundedJoinSemiLattice ()

BoundedJoinSemiLattice All

BoundedJoinSemiLattice Any

BoundedJoinSemiLattice IntSet

BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Endo a)

JoinSemiLattice v => BoundedJoinSemiLattice (IntMap v)

Ord a => BoundedJoinSemiLattice (Set a)

(Eq a, Hashable a) => BoundedJoinSemiLattice (HashSet a)

BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Dropped a)

JoinSemiLattice a => BoundedJoinSemiLattice (Levitated a)

JoinSemiLattice a => BoundedJoinSemiLattice (Lifted a)

BoundedJoinSemiLattice v => BoundedJoinSemiLattice (k -> v)

(BoundedJoinSemiLattice a, BoundedJoinSemiLattice b) => BoundedJoinSemiLattice (a, b)

BoundedJoinSemiLattice (Proxy * a)

(Ord k, JoinSemiLattice v) => BoundedJoinSemiLattice (Map k v)

(Eq k, Hashable k) => BoundedJoinSemiLattice (HashMap k v)

BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Tagged * t a)

class MeetSemiLattice a => BoundedMeetSemiLattice a where

A meet-semilattice with some element |top| that / approaches.

Identity: x /\ top == x

Methods

top :: a

Instances

BoundedMeetSemiLattice Bool

BoundedMeetSemiLattice ()

BoundedMeetSemiLattice All

BoundedMeetSemiLattice Any

BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Endo a)

(Ord a, Finite a) => BoundedMeetSemiLattice (Set a)

MeetSemiLattice a => BoundedMeetSemiLattice (Dropped a)

MeetSemiLattice a => BoundedMeetSemiLattice (Levitated a)

BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Lifted a)

BoundedMeetSemiLattice v => BoundedMeetSemiLattice (k -> v)

(BoundedMeetSemiLattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (a, b)

BoundedMeetSemiLattice (Proxy * a)

(Ord k, Finite k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (Map k v)

BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Tagged * t a)

class (Lattice a, BoundedJoinSemiLattice a, BoundedMeetSemiLattice a) => BoundedLattice a

Lattices with both bounds

Instances

BoundedLattice Bool

BoundedLattice ()

BoundedLattice All

BoundedLattice Any

BoundedLattice a => BoundedLattice (Endo a)

(Ord a, Finite a) => BoundedLattice (Set a)

BoundedLattice a => BoundedLattice (Dropped a)

Lattice a => BoundedLattice (Levitated a)

BoundedLattice a => BoundedLattice (Lifted a)

BoundedLattice v => BoundedLattice (k -> v)

(BoundedLattice a, BoundedLattice b) => BoundedLattice (a, b)

BoundedLattice (Proxy * a)

(Ord k, Finite k, BoundedLattice v) => BoundedLattice (Map k v)

BoundedLattice a => BoundedLattice (Tagged * t a)

joins :: (BoundedJoinSemiLattice a, Foldable f) => f a -> a

The join of a list of join-semilattice elements

meets :: (BoundedMeetSemiLattice a, Foldable f) => f a -> a

The meet of a list of meet-semilattice elements

Monoid wrappers

newtype Meet a

Monoid wrapper for MeetSemiLattice

Constructors

Meet

Fields

getMeet :: a

Instances

Bounded a => Bounded (Meet a)

Eq a => Eq (Meet a)

Data a => Data (Meet a)

Ord a => Ord (Meet a)

Read a => Read (Meet a)

Show a => Show (Meet a)

BoundedMeetSemiLattice a => Monoid (Meet a)

MeetSemiLattice a => Semigroup (Meet a)

Typeable (* -> *) Meet

newtype Join a

Monoid wrapper for JoinSemiLattice

Constructors

Join

Fields

getJoin :: a

Instances

Bounded a => Bounded (Join a)

Eq a => Eq (Join a)

Data a => Data (Join a)

Ord a => Ord (Join a)

Read a => Read (Join a)

Show a => Show (Join a)

BoundedJoinSemiLattice a => Monoid (Join a)

JoinSemiLattice a => Semigroup (Join a)

Typeable (* -> *) Join

Fixed points of chains in lattices

lfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a

Implementation of Kleene fixed-point theorem http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem. Forces the function to be monotone.

lfpFrom :: (Eq a, BoundedJoinSemiLattice a) => a -> (a -> a) -> a

Implementation of Kleene fixed-point theorem http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem. Forces the function to be monotone.

unsafeLfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a

Implementation of Kleene fixed-point theorem http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem. Assumes that the function is monotone and does not check if that is correct.

gfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a

Implementation of Kleene fixed-point theorem http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem. Forces the function to be antinone.

gfpFrom :: (Eq a, BoundedMeetSemiLattice a) => a -> (a -> a) -> a

Implementation of Kleene fixed-point theorem http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem. Forces the function to be antinone.

unsafeGfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a

Implementation of Kleene fixed-point theorem http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem. Assumes that the function is antinone and does not check if that is correct.