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