{-# LANGUAGE FlexibleInstances #-}
{-|
Module      : Algebra.SemiBoundedLattice
Description : Haskell typeclasses and instances of semibounded lattices, Heyting algebra, co-Heyting algebra, and Boolean algebra
Copyright   : (c) Hao Xu, 2016
License     : BSD-3
Maintainer  : xuh@email.unc.edu
Stability   : experimental
Portability : portable

Haskell typeclasses and instances of semibounded lattices, Heyting algebra, co-Heyting algebra, and Boolean algebra
-}
module Algebra.SemiBoundedLattice (
  Complemented (..), (/\\), (//\),
  DistributiveLattice, LowerBoundedLattice, UpperBoundedLattice, LowerBoundedDistributiveLattice, UpperBoundedDistributiveLattice, BooleanAlgebra (..),
  HeytingAlgebra (..), CoHeytingAlgebra (..), SemiHeytingAlgebra (..), SemiCoHeytingAlgebra (..), BiHeytingAlgebra) where

-- import Data.List (union, intersect, (\\))
import Data.Set (union, intersection, (\\), Set)

import Algebra.Lattice (JoinSemiLattice(..), MeetSemiLattice(..), BoundedJoinSemiLattice(..), BoundedMeetSemiLattice(..), Lattice (..), BoundedLattice(..))

-- | 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 (JoinSemiLattice a, BoundedMeetSemiLattice a) => UpperBoundedLattice a where

-- | The combination of a BoundedJoinSemiLattice and a MeetSemiLattice makes an LowerBoundedLattice if the absorption law holds:
--
-- > Absorption: a \/ (a /\ b) == a /\ (a \/ b) == a
class (BoundedJoinSemiLattice a, MeetSemiLattice a) => LowerBoundedLattice a where

-- | 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>
class Lattice a => DistributiveLattice a where

-- | 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>
class LowerBoundedLattice a => LowerBoundedDistributiveLattice a where

-- | 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>
class UpperBoundedLattice a => UpperBoundedDistributiveLattice 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>
class LowerBoundedDistributiveLattice a => SemiCoHeytingAlgebra a where
  subtraction :: a -> a -> a
  (\\\) :: a -> a -> a
  (\\\) = a -> a -> a
forall a. SemiCoHeytingAlgebra a => a -> a -> a
subtraction
  subtraction = a -> a -> a
forall a. SemiCoHeytingAlgebra a => a -> a -> a
(\\\)

-- | supplement
-- see <https://ncatlab.org/nlab/show/co-Heyting+negation>
class (BoundedLattice a, SemiCoHeytingAlgebra a) => CoHeytingAlgebra a where
  supplement :: a -> a
  supplement a
a = a
forall a. BoundedMeetSemiLattice a => a
top a -> a -> a
forall a. SemiCoHeytingAlgebra a => a -> a -> a
\\\ a
a

-- | 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 UpperBoundedDistributiveLattice a => SemiHeytingAlgebra a where
  implication :: a -> a -> a
  (-->) :: a -> a -> a
  (-->) = a -> a -> a
forall a. SemiHeytingAlgebra a => a -> a -> a
implication
  implication = a -> a -> a
forall a. SemiHeytingAlgebra a => a -> a -> a
(-->)

-- | negation
-- see <https://ncatlab.org/nlab/show/Heyting+algebra>
class (BoundedLattice a, SemiHeytingAlgebra a) => HeytingAlgebra a where
  negation :: a -> a
  negation a
a = a
a a -> a -> a
forall a. SemiHeytingAlgebra a => a -> a -> a
--> a
forall a. BoundedJoinSemiLattice a => a
bottom

-- | A lattice that is both a Heyting algebra and a co-Heyting algebra is a bi-Heyting algebra
class (HeytingAlgebra a, CoHeytingAlgebra a) => BiHeytingAlgebra 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
class BiHeytingAlgebra a => BooleanAlgebra a where
  complement :: a -> a
  complement = a -> a
forall a. CoHeytingAlgebra a => a -> a
supplement

data Complemented a = Include a | Exclude a deriving Int -> Complemented a -> ShowS
[Complemented a] -> ShowS
Complemented a -> String
(Int -> Complemented a -> ShowS)
-> (Complemented a -> String)
-> ([Complemented a] -> ShowS)
-> Show (Complemented a)
forall a. Show a => Int -> Complemented a -> ShowS
forall a. Show a => [Complemented a] -> ShowS
forall a. Show a => Complemented a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Complemented a] -> ShowS
$cshowList :: forall a. Show a => [Complemented a] -> ShowS
show :: Complemented a -> String
$cshow :: forall a. Show a => Complemented a -> String
showsPrec :: Int -> Complemented a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Complemented a -> ShowS
Show

instance SemiCoHeytingAlgebra a => JoinSemiLattice (Complemented a) where
    (Include a
vars) \/ :: Complemented a -> Complemented a -> Complemented a
\/ (Include a
vars2) = a -> Complemented a
forall a. a -> Complemented a
Include (a
vars a -> a -> a
forall a. JoinSemiLattice a => a -> a -> a
\/ a
vars2)
    (Include a
vars) \/ (Exclude a
vars2) = a -> Complemented a
forall a. a -> Complemented a
Exclude (a
vars2 a -> a -> a
forall a. SemiCoHeytingAlgebra a => a -> a -> a
\\\ a
vars)
    (Exclude a
vars) \/ (Include a
vars2) = a -> Complemented a
forall a. a -> Complemented a
Exclude (a
vars a -> a -> a
forall a. SemiCoHeytingAlgebra a => a -> a -> a
\\\ a
vars2)
    (Exclude a
vars) \/ (Exclude a
vars2) = a -> Complemented a
forall a. a -> Complemented a
Exclude (a
vars2 a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ a
vars)

instance SemiCoHeytingAlgebra a => MeetSemiLattice (Complemented a) where
    (Include a
vars) /\ :: Complemented a -> Complemented a -> Complemented a
/\ (Include a
vars2) = a -> Complemented a
forall a. a -> Complemented a
Include (a
vars a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ a
vars2)
    (Exclude a
vars) /\ (Include a
vars2) = a -> Complemented a
forall a. a -> Complemented a
Include (a
vars2 a -> a -> a
forall a. SemiCoHeytingAlgebra a => a -> a -> a
\\\ a
vars)
    (Include a
vars) /\ (Exclude a
vars2) = a -> Complemented a
forall a. a -> Complemented a
Include (a
vars a -> a -> a
forall a. SemiCoHeytingAlgebra a => a -> a -> a
\\\ a
vars2)
    (Exclude a
vars) /\ (Exclude a
vars2) = a -> Complemented a
forall a. a -> Complemented a
Exclude (a
vars a -> a -> a
forall a. JoinSemiLattice a => a -> a -> a
\/ a
vars2)

instance SemiCoHeytingAlgebra a => BoundedJoinSemiLattice (Complemented a) where
    bottom :: Complemented a
bottom = Complemented a
forall a. BoundedJoinSemiLattice a => a
bottom

instance SemiCoHeytingAlgebra a => BoundedMeetSemiLattice (Complemented a) where
    top :: Complemented a
top = a -> Complemented a
forall a. a -> Complemented a
Exclude a
forall a. BoundedJoinSemiLattice a => a
bottom

instance SemiCoHeytingAlgebra a => Lattice (Complemented a) where
instance SemiCoHeytingAlgebra a => LowerBoundedLattice (Complemented a) where
instance SemiCoHeytingAlgebra a => UpperBoundedLattice (Complemented a) where
instance SemiCoHeytingAlgebra a => BoundedLattice (Complemented a) where
instance SemiCoHeytingAlgebra a => DistributiveLattice (Complemented a) where
instance SemiCoHeytingAlgebra a => LowerBoundedDistributiveLattice (Complemented a) where
instance SemiCoHeytingAlgebra a => UpperBoundedDistributiveLattice (Complemented a) where
instance SemiCoHeytingAlgebra a => SemiCoHeytingAlgebra (Complemented a) where
  Include a
a \\\ :: Complemented a -> Complemented a -> Complemented a
\\\ Include a
b = a -> Complemented a
forall a. a -> Complemented a
Include (a
a a -> a -> a
forall a. SemiCoHeytingAlgebra a => a -> a -> a
\\\ a
b)
  Include a
a \\\ Exclude a
b = a -> Complemented a
forall a. a -> Complemented a
Include (a
a a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ a
b)
  Exclude a
a \\\ Include a
b = a -> Complemented a
forall a. a -> Complemented a
Exclude (a
a a -> a -> a
forall a. JoinSemiLattice a => a -> a -> a
\/ a
b)
  Exclude a
a \\\ Exclude a
b = a -> Complemented a
forall a. a -> Complemented a
Include (a
b a -> a -> a
forall a. SemiCoHeytingAlgebra a => a -> a -> a
\\\ a
a)

instance SemiCoHeytingAlgebra a => SemiHeytingAlgebra (Complemented a) where
  Complemented a
a --> :: Complemented a -> Complemented a -> Complemented a
--> Complemented a
b = (Complemented a
forall a. BoundedMeetSemiLattice a => a
top Complemented a -> Complemented a -> Complemented a
forall a. SemiCoHeytingAlgebra a => a -> a -> a
\\\ Complemented a
a) Complemented a -> Complemented a -> Complemented a
forall a. JoinSemiLattice a => a -> a -> a
\/ Complemented a
b

instance SemiCoHeytingAlgebra a => CoHeytingAlgebra (Complemented a) where
instance SemiCoHeytingAlgebra a => HeytingAlgebra (Complemented a) where
instance SemiCoHeytingAlgebra a => BiHeytingAlgebra (Complemented a) where
instance SemiCoHeytingAlgebra a => BooleanAlgebra (Complemented a) where

instance Ord a => LowerBoundedLattice (Set a)
instance Ord a => LowerBoundedDistributiveLattice (Set a)
instance Ord a => SemiCoHeytingAlgebra (Set a) where
  subtraction :: Set a -> Set a -> Set a
subtraction = Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
(\\)

instance MeetSemiLattice Integer where
  /\ :: Integer -> Integer -> Integer
(/\) = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min
instance JoinSemiLattice Integer where
  \/ :: Integer -> Integer -> Integer
(\/) = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max
instance BoundedJoinSemiLattice Integer where
  bottom :: Integer
bottom = Integer
0
instance LowerBoundedLattice Integer
instance LowerBoundedDistributiveLattice Integer
instance SemiCoHeytingAlgebra Integer where
  subtraction :: Integer -> Integer -> Integer
subtraction Integer
a Integer
b = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
0 (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b)

(/\\), rmeetproj :: SemiCoHeytingAlgebra a => a -> Complemented a -> a
rmeetproj :: a -> Complemented a -> a
rmeetproj a
vars (Include a
vars2) = a
vars a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ a
vars2
rmeetproj a
vars (Exclude a
vars2) = a
vars a -> a -> a
forall a. SemiCoHeytingAlgebra a => a -> a -> a
\\\ a
vars2
/\\ :: a -> Complemented a -> a
(/\\) = a -> Complemented a -> a
forall a. SemiCoHeytingAlgebra a => a -> Complemented a -> a
rmeetproj

(//\), lmeetproj :: SemiCoHeytingAlgebra a => Complemented a -> a -> a
lmeetproj :: Complemented a -> a -> a
lmeetproj (Include a
vars2) a
vars = a
vars a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ a
vars2
lmeetproj (Exclude a
vars2) a
vars = a
vars a -> a -> a
forall a. SemiCoHeytingAlgebra a => a -> a -> a
\\\ a
vars2
//\ :: Complemented a -> a -> a
(//\) = Complemented a -> a -> a
forall a. SemiCoHeytingAlgebra a => Complemented a -> a -> a
lmeetproj