Copyright | (c) Hao Xu 2016 |
---|---|

License | BSD-3 |

Maintainer | xuh@email.unc.edu |

Stability | experimental |

Portability | portable |

Safe Haskell | Safe-Inferred |

Language | Haskell2010 |

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

## Synopsis

- 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
- 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 #

#### Instances

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

#### Instances

SemiCoHeytingAlgebra a => DistributiveLattice (Complemented a) Source # | |

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

LowerBoundedLattice Integer Source # | |

Defined in Algebra.SemiBoundedLattice | |

Ord a => LowerBoundedLattice (Set a) Source # | |

Defined in Algebra.SemiBoundedLattice | |

SemiCoHeytingAlgebra a => LowerBoundedLattice (Complemented a) Source # | |

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

SemiCoHeytingAlgebra a => UpperBoundedLattice (Complemented a) Source # | |

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)

#### Instances

LowerBoundedDistributiveLattice Integer Source # | |

Defined in Algebra.SemiBoundedLattice | |

Ord a => LowerBoundedDistributiveLattice (Set a) Source # | |

Defined in Algebra.SemiBoundedLattice | |

SemiCoHeytingAlgebra a => LowerBoundedDistributiveLattice (Complemented a) Source # | |

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)

#### Instances

SemiCoHeytingAlgebra a => UpperBoundedDistributiveLattice (Complemented a) Source # | |

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

Nothing

complement :: a -> a Source #

#### Instances

SemiCoHeytingAlgebra a => BooleanAlgebra (Complemented a) Source # | |

Defined in Algebra.SemiBoundedLattice complement :: Complemented a -> Complemented a Source # |

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

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

Nothing

#### Instances

SemiCoHeytingAlgebra a => HeytingAlgebra (Complemented a) Source # | |

Defined in Algebra.SemiBoundedLattice 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

Nothing

supplement :: a -> a Source #

#### Instances

SemiCoHeytingAlgebra a => CoHeytingAlgebra (Complemented a) Source # | |

Defined in Algebra.SemiBoundedLattice 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

Nothing

#### Instances

SemiCoHeytingAlgebra a => SemiHeytingAlgebra (Complemented a) Source # | |

Defined in Algebra.SemiBoundedLattice 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

Nothing

#### Instances

SemiCoHeytingAlgebra Integer Source # | |

Ord a => SemiCoHeytingAlgebra (Set a) Source # | |

SemiCoHeytingAlgebra a => SemiCoHeytingAlgebra (Complemented a) Source # | |

Defined in Algebra.SemiBoundedLattice 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

SemiCoHeytingAlgebra a => BiHeytingAlgebra (Complemented a) Source # | |

Defined in Algebra.SemiBoundedLattice |