| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Data.Lattice
Description
Lattices & algebras
Synopsis
- type Lattice a = (Join a, Meet a)
- class Order a => Semilattice k a where
- bound :: Cast k () a
- semilattice :: Cast k (a, a) a
- type Meet = Semilattice R
- (/\) :: Meet a => a -> a -> a
- glb :: Lattice a => a -> a -> a -> a
- top :: Meet a => a
- type Join = Semilattice L
- (\/) :: Join a => a -> a -> a
- lub :: Lattice a => a -> a -> a -> a
- bottom :: Join a => a
- type Biheyting a = (Coheyting a, Heyting a)
- class Semilattice k a => Algebra k a where
- type Heyting a = (Lattice a, Algebra R a)
- (//) :: Algebra R a => a -> a -> a
- iff :: Algebra R a => a -> a -> a
- neg :: Heyting a => a -> a
- middle :: Heyting a => a -> a
- heyting :: Meet a => (a -> a -> a) -> a -> Cast R a a
- booleanR :: Heyting a => Cast R a a
- type Coheyting a = (Lattice a, Algebra L a)
- (\\) :: Algebra L a => a -> a -> a
- equiv :: Algebra L a => a -> a -> a
- non :: Coheyting a => a -> a
- boundary :: Coheyting a => a -> a
- coheyting :: Join a => (a -> a -> a) -> a -> Cast L a a
- booleanL :: Coheyting a => Cast L a a
- class Biheyting a => Symmetric a where
- converseL :: Symmetric a => a -> a
- converseR :: Symmetric a => a -> a
- symmetricL :: Symmetric a => a -> Cast L a a
- symmetricR :: Symmetric a => a -> Cast R a a
- class Symmetric a => Boolean a where
Semilattice
class Order a => Semilattice k a where Source #
Bounded lattices.
A lattice is a partially ordered set in which every two elements have a unique join (least upper bound or supremum) and a unique meet (greatest lower bound or infimum).
A bound lattice adds unique elements top and bottom, which serve as
identities to \/ and /\, respectively.
Neutrality:
x\/bottom= x x/\top= xglbbottomxtop= xlubbottomxtop= x
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
(x\/y)/\y = y (x/\y)\/y = y
See Absorption.
Note that distributivity is _not_ a requirement for a complete. However when a is distributive we have:
glbx y z =lubx y z
Methods
The defining connection of a bound semilattice.
bottom and top are defined by the left and right adjoints to a -> ().
semilattice :: Cast k (a, a) a Source #
Instances
Meet
type Meet = Semilattice R Source #
A convenience alias for a meet semilattice
glb :: Lattice a => a -> a -> a -> a Source #
Greatest lower bound operator.
glb x x y = x glb x y z = glb z x y glb x y z = glb x z y glb (glb x w y) w z = glb x w (glb y w z)
>>>glb 1.0 9.0 7.07.0>>>glb 1.0 9.0 (0.0 / 0.0)9.0>>>glb (fromList [1..3]) (fromList [3..5]) (fromList [5..7]) :: IntSetfromList [3,5]
Join
type Join = Semilattice L Source #
A convenience alias for a join semilattice
lub :: Lattice a => a -> a -> a -> a Source #
Least upper bound operator.
The order dual of glb.
>>>lub 1.0 9.0 7.07.0>>>lub 1.0 9.0 (0.0 / 0.0)1.0
bottom :: Join a => a Source #
The unique bottom element of a bound lattice
x /\ bottom = bottom x \/ bottom = x
Algebra
class Semilattice k a => Algebra k a where Source #
Heyting and co-Heyting algebras
A Heyting algebra is a bound, distributive lattice equipped with an implication operation.
- The complete of closed subsets of a topological space is the primordial example of a Coheyting (co-Algebra) algebra.
- The dual complete of open subsets of a topological space is likewise the primordial example of a Heyting algebra.
Coheyting:
Co-implication to a is the lower adjoint of disjunction with a:
x \\ a <= y <=> x <= y \/ a
Note that co-Heyting algebras needn't obey the law of non-contradiction:
EQ /\ non EQ = EQ /\ GT \\ EQ = EQ /\ GT = EQ /= LT
See https://ncatlab.org/nlab/show/co-Heyting+algebra
Heyting:
Implication from a is the upper adjoint of conjunction with a:
x <= a // y <=> a /\ x <= y
Similarly, Heyting algebras needn't obey the law of the excluded middle:
EQ \/ neg EQ = EQ \/ EQ // LT = EQ \/ LT = EQ /= GT
Methods
algebra :: a -> Cast k a a Source #
The defining connection of a (co-)Heyting algebra.
algebra @'L x = CastL (\\ x) (\/ x) algebra @'R x = CastR (x /\) (x //)
Instances
Heyting
(//) :: Algebra R a => a -> a -> a infixr 8 Source #
Logical implication:
\( a \Rightarrow b = \vee \{x \mid x \wedge a \leq b \} \)
Laws:
x /\ y <= z <=> x <= y // z x // y <= x // (y \/ z) x <= y => z // x <= z // y y <= x // (x /\ y) x <= y <=> x // y = top (x \/ z) // y <= x // y (x /\ y) // z = x // y // z x // (y /\ z) = x // y /\ x // z x /\ x // y = x /\ y
>>>False // FalseTrue>>>False // TrueTrue>>>True // FalseFalse>>>True // TrueTrue
iff :: Algebra R a => a -> a -> a Source #
Intuitionistic equivalence.
When a is Bool this is 'if-and-only-if'.
neg :: Heyting a => a -> a Source #
Logical negation.
negx = x//bottom
Laws:
neg bottom = top neg top = bottom x <= neg (neg x) neg (x \/ y) <= neg x neg (x // y) = neg (neg x) /\ neg y neg (x \/ y) = neg x /\ neg y x /\ neg x = bottom neg (neg (neg x)) = neg x neg (neg (x \/ neg x)) = top
Some logics may in addition obey De Morgan conditions.
middle :: Heyting a => a -> a Source #
The Algebra (not necessarily excluded) middle operator.
heyting :: Meet a => (a -> a -> a) -> a -> Cast R a a Source #
Default constructor for a Algebra algebra.
booleanR :: Heyting a => Cast R a a Source #
An adjunction between a Algebra algebra and its Boolean sub-algebra.
Double negation is a meet-preserving monad.
Coheyting
(\\) :: Algebra L a => a -> a -> a infixl 8 Source #
Logical co-implication:
\( a \Rightarrow b = \wedge \{x \mid a \leq b \vee x \} \)
Laws:
x \\ y <= z <=> x <= y \/ z x \\ y >= (x /\ z) \\ y x >= y => x \\ z >= y \\ z x >= x \\ y x >= y <=> y \\ x = bottom x \\ (y /\ z) >= x \\ y z \\ (x \/ y) = z \\ x \\ y (y \/ z) \\ x = y \\ x \/ z \\ x x \/ y \\ x = x \/ y
>>>False \\ FalseFalse>>>False \\ TrueFalse>>>True \\ FalseTrue>>>True \\ TrueFalse
For many collections (e.g. Set) \\ coincides with the native \\ operator.
>>>:set -XOverloadedLists>>>[GT,EQ] Set.\\ [LT]fromList [EQ,GT]>>>[GT,EQ] \\ [LT]fromList [EQ,GT]
non :: Coheyting a => a -> a Source #
Logical co-negation.
nonx =top\\x
Laws:
non bottom = top non top = bottom x >= non (non x) non (x /\ y) >= non x non (y \\ x) = non (non x) \/ non y non (x /\ y) = non x \/ non y x \/ non x = top non (non (non x)) = non x non (non (x /\ non x)) = bottom
boundary :: Coheyting a => a -> a Source #
The co-Heyting boundary operator.
x = boundary x \/ (non . non) x boundary (x /\ y) = (boundary x /\ y) \/ (x /\ boundary y) -- (Leibniz rule) boundary (x \/ y) \/ boundary (x /\ y) = boundary x \/ boundary y
coheyting :: Join a => (a -> a -> a) -> a -> Cast L a a Source #
Default constructor for a co-Heyting algebra.
booleanL :: Coheyting a => Cast L a a Source #
An adjunction between a co-Heyting algebra and its Boolean sub-algebra.
Double negation is a join-preserving comonad.
Symmetric
class Biheyting a => Symmetric a where Source #
Symmetric Heyting algebras
A symmetric Heyting algebra is a De Morgan bi-Algebra algebra with an idempotent, antitone negation operator.
Laws:
x <= y => not y <= not x -- antitone not . not = id -- idempotence x \\ y = not (not y // not x) x // y = not (not y \\ not x)
and:
converseR x <= converseL x
with equality occurring iff a is a Boolean algebra.
Minimal complete definition
Methods
Symmetric negation.
not . not = id neg . neg = converseR . converseL non . non = converseL . converseR neg . non = converseR . converseR non . neg = converseL . converseL
neg = converseR . not = not . converseL non = not . converseR = converseL . not x \\ y = not (not y // not x) x // y = not (not y \\ not x)
xor :: a -> a -> a infixl 4 Source #
Exclusive or.
xor x y = (x \/ y) /\ (not x \/ not y)
Boolean
class Symmetric a => Boolean a where Source #
Boolean algebras.
Boolean algebras are symmetric Algebra algebras that satisfy both the law of excluded middle and the law of law of non-contradiction:
x \/ neg x = top x /\ non x = bottom
If a is Boolean we also have:
non = not = neg
Minimal complete definition
Nothing