Copyright | (C) 2010-2015 Maximilian Bolingbroke 2015-2019 Oleg Grenrus |
---|---|

License | BSD-3-Clause (see the file LICENSE) |

Maintainer | Oleg Grenrus <oleg.grenrus@iki.fi> |

Safe Haskell | Safe |

Language | Haskell2010 |

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.

## Synopsis

- class Lattice a where
- joinLeq :: (Eq a, Lattice a) => a -> a -> Bool
- joins1 :: (Lattice a, Foldable1 f) => f a -> a
- meetLeq :: (Eq a, Lattice a) => a -> a -> Bool
- meets1 :: (Lattice a, Foldable1 f) => f a -> a
- class Lattice a => BoundedJoinSemiLattice a where
- bottom :: a

- class Lattice a => BoundedMeetSemiLattice a where
- top :: a

- joins :: (BoundedJoinSemiLattice a, Foldable f) => f a -> a
- meets :: (BoundedMeetSemiLattice a, Foldable f) => f a -> a
- fromBool :: BoundedLattice a => Bool -> a
- type BoundedLattice a = (BoundedMeetSemiLattice a, BoundedJoinSemiLattice a)
- newtype Meet a = Meet {
- getMeet :: a

- newtype Join a = Join {
- getJoin :: a

- lfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a
- lfpFrom :: (Eq a, BoundedJoinSemiLattice a) => a -> (a -> a) -> a
- unsafeLfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a
- gfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a
- gfpFrom :: (Eq a, BoundedMeetSemiLattice a) => a -> (a -> a) -> a
- unsafeGfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a

# Unbounded lattices

class Lattice a where Source #

An algebraic structure with joins and meets.

See http://en.wikipedia.org/wiki/Lattice_(order) and http://en.wikipedia.org/wiki/Absorption_law.

`Lattice`

is very symmetric, which is seen from the laws:

*Associativity*

x`\/`

(y`\/`

z) ≡ (x`\/`

y)`\/`

z x`/\`

(y`/\`

z) ≡ (x`/\`

y)`/\`

z

*Commputativity*

x`\/`

y ≡ y`\/`

x x`/\`

y ≡ y`/\`

x

*Idempotency*

x`\/`

x ≡ x x`/\`

x ≡ x

*Absorption*

a`\/`

(a`/\`

b) ≡ a a`/\`

(a`\/`

b) ≡ a

## Instances

joinLeq :: (Eq a, Lattice a) => a -> a -> Bool Source #

The partial ordering induced by the join-semilattice structure

joins1 :: (Lattice a, Foldable1 f) => f a -> a Source #

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

meets1 :: (Lattice a, Foldable1 f) => f a -> a Source #

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

# Bounded lattices

class Lattice a => BoundedJoinSemiLattice a where Source #

A join-semilattice with an identity element `bottom`

for `\/`

.

*Laws*

x`\/`

`bottom`

≡ x

*Corollary*

x`/\`

`bottom`

≡⟨ identity ⟩ (x`/\`

`bottom`

)`\/`

`bottom`

≡⟨ absorption ⟩`bottom`

## Instances

class Lattice a => BoundedMeetSemiLattice a where Source #

A meet-semilattice with an identity element `top`

for `/\`

.

*Laws*

x`/\`

`top`

≡ x

*Corollary*

x`\/`

`top`

≡⟨ identity ⟩ (x`\/`

`top`

)`/\`

`top`

≡⟨ absorption ⟩`top`

## Instances

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

The join of a list of join-semilattice elements

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

The meet of a list of meet-semilattice elements

type BoundedLattice a = (BoundedMeetSemiLattice a, BoundedJoinSemiLattice a) Source #

# Monoid wrappers

Monoid wrapper for meet-`Lattice`

## Instances

Monad Meet Source # | |

Functor Meet Source # | |

Applicative Meet Source # | |

MonadZip Meet Source # | |

Bounded a => Bounded (Meet a) Source # | |

Eq a => Eq (Meet a) Source # | |

Data a => Data (Meet a) Source # | |

Defined in Algebra.Lattice gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Meet a -> c (Meet a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Meet a) # toConstr :: Meet a -> Constr # dataTypeOf :: Meet a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Meet a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Meet a)) # gmapT :: (forall b. Data b => b -> b) -> Meet a -> Meet a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Meet a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Meet a -> r # gmapQ :: (forall d. Data d => d -> u) -> Meet a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Meet a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Meet a -> m (Meet a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Meet a -> m (Meet a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Meet a -> m (Meet a) # | |

Ord a => Ord (Meet a) Source # | |

Read a => Read (Meet a) Source # | |

Show a => Show (Meet a) Source # | |

Generic (Meet a) Source # | |

Lattice a => Semigroup (Meet a) Source # | |

BoundedMeetSemiLattice a => Monoid (Meet a) Source # | |

Universe a => Universe (Meet a) Source # | |

Defined in Algebra.Lattice | |

Finite a => Finite (Meet a) Source # | |

Defined in Algebra.Lattice | |

(Eq a, Lattice a) => PartialOrd (Meet a) Source # | |

type Rep (Meet a) Source # | |

Defined in Algebra.Lattice |

Monoid wrapper for join-`Lattice`

## Instances

Monad Join Source # | |

Functor Join Source # | |

Applicative Join Source # | |

MonadZip Join Source # | |

Bounded a => Bounded (Join a) Source # | |

Eq a => Eq (Join a) Source # | |

Data a => Data (Join a) Source # | |

Defined in Algebra.Lattice gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Join a -> c (Join a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Join a) # toConstr :: Join a -> Constr # dataTypeOf :: Join a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Join a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Join a)) # gmapT :: (forall b. Data b => b -> b) -> Join a -> Join a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Join a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Join a -> r # gmapQ :: (forall d. Data d => d -> u) -> Join a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Join a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Join a -> m (Join a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Join a -> m (Join a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Join a -> m (Join a) # | |

Ord a => Ord (Join a) Source # | |

Read a => Read (Join a) Source # | |

Show a => Show (Join a) Source # | |

Generic (Join a) Source # | |

Lattice a => Semigroup (Join a) Source # | |

BoundedJoinSemiLattice a => Monoid (Join a) Source # | |

Universe a => Universe (Join a) Source # | |

Defined in Algebra.Lattice | |

Finite a => Finite (Join a) Source # | |

Defined in Algebra.Lattice | |

(Eq a, Lattice a) => PartialOrd (Join a) Source # | |

type Rep (Join a) Source # | |

Defined in Algebra.Lattice |

# Fixed points of chains in lattices

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

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

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

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

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

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

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.