Copyright	(c) Hao Xu 2016
License	BSD-3
Maintainer	xuh@email.unc.edu
Stability	experimental
Portability	portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Algebra.SemiBoundedLattice

Contents

Orphan instances

Description

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

Synopsis

data Complemented a
- = Include a
- | Exclude 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
- complement :: a -> a
class (BoundedLattice a, SemiHeytingAlgebra a) => HeytingAlgebra a where
- negation :: a -> a
class (BoundedLattice a, SemiCoHeytingAlgebra a) => CoHeytingAlgebra a where
- supplement :: a -> a
class UpperBoundedDistributiveLattice a => SemiHeytingAlgebra a where
- implication :: a -> a -> a
- (-->) :: a -> a -> a
class LowerBoundedDistributiveLattice a => SemiCoHeytingAlgebra a where
- subtraction :: a -> a -> a
- (\\\) :: a -> a -> a
class (HeytingAlgebra a, CoHeytingAlgebra a) => BiHeytingAlgebra a

Documentation

data Complemented a Source #

Constructors

Include a
Exclude a

Instances

Instances details

Show a => Show (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice Methods showsPrec :: Int -> Complemented a -> ShowS # show :: Complemented a -> String # showList :: [Complemented a] -> ShowS #
SemiCoHeytingAlgebra a => JoinSemiLattice (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice Methods (\/) :: Complemented a -> Complemented a -> Complemented a # join :: Complemented a -> Complemented a -> Complemented a #
SemiCoHeytingAlgebra a => MeetSemiLattice (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice Methods (/\) :: Complemented a -> Complemented a -> Complemented a # meet :: Complemented a -> Complemented a -> Complemented a #
SemiCoHeytingAlgebra a => Lattice (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice
SemiCoHeytingAlgebra a => BoundedJoinSemiLattice (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice Methods bottom :: Complemented a #
SemiCoHeytingAlgebra a => BoundedMeetSemiLattice (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice Methods top :: Complemented a #
SemiCoHeytingAlgebra a => BoundedLattice (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice
SemiCoHeytingAlgebra a => BooleanAlgebra (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice Methods complement :: Complemented a -> Complemented a Source #
SemiCoHeytingAlgebra a => BiHeytingAlgebra (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice
SemiCoHeytingAlgebra a => HeytingAlgebra (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice Methods negation :: Complemented a -> Complemented a Source #
SemiCoHeytingAlgebra a => SemiHeytingAlgebra (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice Methods implication :: Complemented a -> Complemented a -> Complemented a Source # (-->) :: Complemented a -> Complemented a -> Complemented a Source #
SemiCoHeytingAlgebra a => CoHeytingAlgebra (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice Methods supplement :: Complemented a -> Complemented a Source #
SemiCoHeytingAlgebra a => SemiCoHeytingAlgebra (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice Methods subtraction :: Complemented a -> Complemented a -> Complemented a Source # (\\\) :: Complemented a -> Complemented a -> Complemented a Source #
SemiCoHeytingAlgebra a => UpperBoundedDistributiveLattice (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice
SemiCoHeytingAlgebra a => LowerBoundedDistributiveLattice (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice
SemiCoHeytingAlgebra a => DistributiveLattice (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice
SemiCoHeytingAlgebra a => LowerBoundedLattice (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice
SemiCoHeytingAlgebra a => UpperBoundedLattice (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice

(/\\) :: 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)

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

Instances

Instances details

SemiCoHeytingAlgebra a => DistributiveLattice (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice

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

Instances

Instances details

LowerBoundedLattice Integer Source #
Instance details Defined in Algebra.SemiBoundedLattice
Ord a => LowerBoundedLattice (Set a) Source #
Instance details Defined in Algebra.SemiBoundedLattice
SemiCoHeytingAlgebra a => LowerBoundedLattice (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice

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

Instances

Instances details

SemiCoHeytingAlgebra a => UpperBoundedLattice (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice

class LowerBoundedLattice a => LowerBoundedDistributiveLattice a Source #

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

Instances details

LowerBoundedDistributiveLattice Integer Source #
Instance details Defined in Algebra.SemiBoundedLattice
Ord a => LowerBoundedDistributiveLattice (Set a) Source #
Instance details Defined in Algebra.SemiBoundedLattice
SemiCoHeytingAlgebra a => LowerBoundedDistributiveLattice (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice

class UpperBoundedLattice a => UpperBoundedDistributiveLattice a Source #

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

Instances details

SemiCoHeytingAlgebra a => UpperBoundedDistributiveLattice (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice

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

Minimal complete definition

Nothing

Methods

complement :: a -> a Source #

Instances

Instances details

SemiCoHeytingAlgebra a => BooleanAlgebra (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice Methods complement :: Complemented a -> Complemented a Source #

class (BoundedLattice a, SemiHeytingAlgebra a) => HeytingAlgebra a where Source #

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

Minimal complete definition

Nothing

Methods

negation :: a -> a Source #

Instances

Instances details

SemiCoHeytingAlgebra a => HeytingAlgebra (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice Methods negation :: Complemented a -> Complemented a Source #

class (BoundedLattice a, SemiCoHeytingAlgebra a) => CoHeytingAlgebra a where Source #

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

Minimal complete definition

Nothing

Methods

supplement :: a -> a Source #

Instances

Instances details

SemiCoHeytingAlgebra a => CoHeytingAlgebra (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice Methods supplement :: Complemented a -> Complemented a Source #

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

Minimal complete definition

Nothing

Methods

implication :: a -> a -> a Source #

(-->) :: a -> a -> a Source #

Instances

Instances details

SemiCoHeytingAlgebra a => SemiHeytingAlgebra (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice Methods implication :: Complemented a -> Complemented a -> Complemented a Source # (-->) :: Complemented a -> Complemented a -> Complemented a Source #

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

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

Minimal complete definition

Nothing

Methods

subtraction :: a -> a -> a Source #

(\\\) :: a -> a -> a Source #

Instances

Instances details

SemiCoHeytingAlgebra Integer Source #
Instance details Defined in Algebra.SemiBoundedLattice Methods subtraction :: Integer -> Integer -> Integer Source # (\\\) :: Integer -> Integer -> Integer Source #
Ord a => SemiCoHeytingAlgebra (Set a) Source #
Instance details Defined in Algebra.SemiBoundedLattice Methods subtraction :: Set a -> Set a -> Set a Source # (\\\) :: Set a -> Set a -> Set a Source #
SemiCoHeytingAlgebra a => SemiCoHeytingAlgebra (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice Methods subtraction :: Complemented a -> Complemented a -> Complemented a Source # (\\\) :: Complemented a -> Complemented a -> Complemented a Source #

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

Instances

Instances details

SemiCoHeytingAlgebra a => BiHeytingAlgebra (Complemented a) Source #
Instance details Defined in Algebra.SemiBoundedLattice

Orphan instances

JoinSemiLattice Integer Source #
Instance details Methods (\/) :: Integer -> Integer -> Integer # join :: Integer -> Integer -> Integer #
MeetSemiLattice Integer Source #
Instance details Methods (/\) :: Integer -> Integer -> Integer # meet :: Integer -> Integer -> Integer #
BoundedJoinSemiLattice Integer Source #
Instance details Methods bottom :: Integer #