Copyright | (c) Hao Xu 2016 |
---|---|
License | BSD-3 |
Maintainer | xuh@email.unc.edu |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell2010 |
Haskell typeclasses and instances of semibounded lattices, Heyting algebra, co-Heyting algebra, and Boolean algebra
- data Complemented a
- (/\\) :: SemiCoHeytingAlgebra a => a -> Complemented a -> a
- (//\) :: SemiCoHeytingAlgebra a => Complemented a -> a -> a
- class Lattice a => DistributiveLattice a
- class (BoundedJoinSemiLattice a, MeetSemiLattice a) => LowerBoundedLattice a
- class (JoinSemiLattice a, BoundedMeetSemiLattice a) => UpperBoundedLattice a
- class LowerBoundedLattice a => LowerBoundedDistributiveLattice a
- class UpperBoundedLattice a => UpperBoundedDistributiveLattice a
- class BiHeytingAlgebra a => BooleanAlgebra a where
- class (BoundedLattice a, SemiHeytingAlgebra a) => HeytingAlgebra a
- class (BoundedLattice a, SemiCoHeytingAlgebra a) => CoHeytingAlgebra a
- class UpperBoundedDistributiveLattice a => SemiHeytingAlgebra a where
- class LowerBoundedDistributiveLattice a => SemiCoHeytingAlgebra a where
- class (HeytingAlgebra a, CoHeytingAlgebra a) => BiHeytingAlgebra a
Documentation
data Complemented a Source #
(/\\) :: SemiCoHeytingAlgebra a => a -> Complemented a -> a Source #
(//\) :: SemiCoHeytingAlgebra a => Complemented a -> a -> a Source #
class Lattice a => DistributiveLattice a Source #
A lattice is distributive if the distributivity law holds:
Distributivity: a /\ (b \/ c) == (a /\ b) \/ (a /\ c)
class (BoundedJoinSemiLattice a, MeetSemiLattice a) => LowerBoundedLattice a Source #
The combination of a BoundedJoinSemiLattice and a MeetSemiLattice makes an LowerBoundedLattice if the absorption law holds:
Absorption: a \/ (a /\ b) == a /\ (a \/ b) == a
LowerBoundedLattice Integer Source # | |
Ord a => LowerBoundedLattice (Set a) Source # | |
SemiCoHeytingAlgebra a => LowerBoundedLattice (Complemented a) Source # | |
class (JoinSemiLattice a, BoundedMeetSemiLattice a) => UpperBoundedLattice a Source #
The combination of a JoinSemiLattice and a BoundedMeetSemiLattice makes an UpperBoundedLattice if the absorption law holds:
Absorption: a \/ (a /\ b) == a /\ (a \/ b) == a
class LowerBoundedLattice a => LowerBoundedDistributiveLattice a Source #
A lattice is distributive if the distributivity law holds:
Distributivity: a /\ (b \/ c) == (a /\ b) \/ (a /\ c)
class UpperBoundedLattice a => UpperBoundedDistributiveLattice a Source #
A lattice is distributive if the distributivity law holds:
Distributivity: a /\ (b \/ c) == (a /\ b) \/ (a /\ c)
class BiHeytingAlgebra a => BooleanAlgebra a where Source #
A Boolean Algebra is a complemented distributive lattice, see https://en.wikipedia.org/wiki/Boolean_algebra_(structure) or equivalently a Heyting algebra where
negation (negation a) == a
in a Boolean algebra
supplement == negation
complement :: a -> a Source #
class (BoundedLattice a, SemiHeytingAlgebra a) => HeytingAlgebra a Source #
negation see https://ncatlab.org/nlab/show/Heyting+algebra
class (BoundedLattice a, SemiCoHeytingAlgebra a) => CoHeytingAlgebra a Source #
supplement see https://ncatlab.org/nlab/show/co-Heyting+negation
class UpperBoundedDistributiveLattice a => SemiHeytingAlgebra a where Source #
In most literature, a Heyting algebra requires a bounded lattice. We only require a UpperBoundedDistributiveLattice here for semi-Heyting algebra. (here the lattice must be upper bounded) The following law holds:
x /\ a <= b if and only if x <= (a --> b)
see https://ncatlab.org/nlab/show/Heyting+algebra Heyting algebras are always distributive. see https://en.wikipedia.org/wiki/Heyting_algebra#Distributivity
class LowerBoundedDistributiveLattice a => SemiCoHeytingAlgebra a where Source #
A semi-co-Heyting Algebra is dual of a semi-Heyting algebra where the following law holds:
x \\\ y <= z if and only if x <= y \/ z
class (HeytingAlgebra a, CoHeytingAlgebra a) => BiHeytingAlgebra a Source #
A lattice that is both a Heyting algebra and a co-Heyting algebra is a bi-Heyting algebra