Algebra.SemiBoundedLattice

Haskell typeclasses and instances of semibounded lattices, Heyting algebra, co-Heyting algebra, and Boolean algebra

Documentation

data Complemented a

Constructors

Include a

Exclude a

Instances

Show a => Show (Complemented a)

Methods

showsPrec :: Int -> Complemented a -> ShowS

show :: Complemented a -> String

showList :: [Complemented a] -> ShowS

SemiCoHeytingAlgebra a => JoinSemiLattice (Complemented a)

Methods

(\/) :: Complemented a -> Complemented a -> Complemented a

join :: Complemented a -> Complemented a -> Complemented a

SemiCoHeytingAlgebra a => MeetSemiLattice (Complemented a)

Methods

(/\) :: Complemented a -> Complemented a -> Complemented a

meet :: Complemented a -> Complemented a -> Complemented a

SemiCoHeytingAlgebra a => Lattice (Complemented a)

SemiCoHeytingAlgebra a => BoundedJoinSemiLattice (Complemented a)

Methods

bottom :: Complemented a

SemiCoHeytingAlgebra a => BoundedMeetSemiLattice (Complemented a)

Methods

top :: Complemented a

SemiCoHeytingAlgebra a => BoundedLattice (Complemented a)

SemiCoHeytingAlgebra a => BooleanAlgebra (Complemented a)

Methods

complement :: Complemented a -> Complemented a

SemiCoHeytingAlgebra a => BiHeytingAlgebra (Complemented a)

SemiCoHeytingAlgebra a => HeytingAlgebra (Complemented a)

Methods

negation :: Complemented a -> Complemented a

SemiCoHeytingAlgebra a => SemiHeytingAlgebra (Complemented a)

Methods

implication :: Complemented a -> Complemented a -> Complemented a

(-->) :: Complemented a -> Complemented a -> Complemented a

SemiCoHeytingAlgebra a => CoHeytingAlgebra (Complemented a)

Methods

supplement :: Complemented a -> Complemented a

SemiCoHeytingAlgebra a => SemiCoHeytingAlgebra (Complemented a)

Methods

subtraction :: Complemented a -> Complemented a -> Complemented a

(\\\) :: Complemented a -> Complemented a -> Complemented a

SemiCoHeytingAlgebra a => UpperBoundedDistributiveLattice (Complemented a)

SemiCoHeytingAlgebra a => LowerBoundedDistributiveLattice (Complemented a)

SemiCoHeytingAlgebra a => DistributiveLattice (Complemented a)

SemiCoHeytingAlgebra a => LowerBoundedLattice (Complemented a)

SemiCoHeytingAlgebra a => UpperBoundedLattice (Complemented a)

(/\\) :: SemiCoHeytingAlgebra a => a -> Complemented a -> a

(//\) :: SemiCoHeytingAlgebra a => Complemented a -> a -> a

class Lattice a => DistributiveLattice a

A lattice is distributive if the distributivity law holds:

Distributivity: a /\ (b \/ c) == (a /\ b) \/ (a /\ c)

see https://en.wikipedia.org/wiki/Distributive_lattice

Instances

SemiCoHeytingAlgebra a => DistributiveLattice (Complemented a)

class (BoundedJoinSemiLattice a, MeetSemiLattice a) => LowerBoundedLattice a

The combination of a BoundedJoinSemiLattice and a MeetSemiLattice makes an LowerBoundedLattice if the absorption law holds:

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

Instances

Ord a => LowerBoundedLattice (Set a)

SemiCoHeytingAlgebra a => LowerBoundedLattice (Complemented a)

class (JoinSemiLattice a, BoundedMeetSemiLattice a) => UpperBoundedLattice a

The combination of a JoinSemiLattice and a BoundedMeetSemiLattice makes an UpperBoundedLattice if the absorption law holds:

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

Instances

SemiCoHeytingAlgebra a => UpperBoundedLattice (Complemented a)

class LowerBoundedLattice a => LowerBoundedDistributiveLattice a

A lattice is distributive if the distributivity law holds:

Distributivity: a /\ (b \/ c) == (a /\ b) \/ (a /\ c)

see https://en.wikipedia.org/wiki/Distributive_lattice

Instances

Ord a => LowerBoundedDistributiveLattice (Set a)

SemiCoHeytingAlgebra a => LowerBoundedDistributiveLattice (Complemented a)

class UpperBoundedLattice a => UpperBoundedDistributiveLattice a

A lattice is distributive if the distributivity law holds:

Distributivity: a /\ (b \/ c) == (a /\ b) \/ (a /\ c)

see https://en.wikipedia.org/wiki/Distributive_lattice

Instances

SemiCoHeytingAlgebra a => UpperBoundedDistributiveLattice (Complemented a)

class BiHeytingAlgebra a => BooleanAlgebra a where

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

Methods

complement :: a -> a

Instances

SemiCoHeytingAlgebra a => BooleanAlgebra (Complemented a)

Methods

complement :: Complemented a -> Complemented a

class (BoundedLattice a, SemiHeytingAlgebra a) => HeytingAlgebra a

negation see https://ncatlab.org/nlab/show/Heyting+algebra

Instances

SemiCoHeytingAlgebra a => HeytingAlgebra (Complemented a)

Methods

negation :: Complemented a -> Complemented a

class (BoundedLattice a, SemiCoHeytingAlgebra a) => CoHeytingAlgebra a

supplement see https://ncatlab.org/nlab/show/co-Heyting+negation

Instances

SemiCoHeytingAlgebra a => CoHeytingAlgebra (Complemented a)

Methods

supplement :: Complemented a -> Complemented a

class UpperBoundedDistributiveLattice a => SemiHeytingAlgebra a where

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

Methods

implication :: a -> a -> a

(-->) :: a -> a -> a

Instances

SemiCoHeytingAlgebra a => SemiHeytingAlgebra (Complemented a)

Methods

implication :: Complemented a -> Complemented a -> Complemented a

(-->) :: Complemented a -> Complemented a -> Complemented a

class LowerBoundedDistributiveLattice a => SemiCoHeytingAlgebra a where

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

see https://ncatlab.org/nlab/show/co-Heyting+algebra

Methods

subtraction :: a -> a -> a

(\\\) :: a -> a -> a

Instances

Ord a => SemiCoHeytingAlgebra (Set a)

Methods

subtraction :: Set a -> Set a -> Set a

(\\\) :: Set a -> Set a -> Set a

SemiCoHeytingAlgebra a => SemiCoHeytingAlgebra (Complemented a)

Methods

subtraction :: Complemented a -> Complemented a -> Complemented a

(\\\) :: Complemented a -> Complemented a -> Complemented a

class (HeytingAlgebra a, CoHeytingAlgebra a) => BiHeytingAlgebra a

A lattice that is both a Heyting algebra and a co-Heyting algebra is a bi-Heyting algebra

Instances

SemiCoHeytingAlgebra a => BiHeytingAlgebra (Complemented a)