{-# LANGUAGE FlexibleInstances #-}
module Algebra.SemiBoundedLattice (
Complemented (..), (/\\), (//\),
DistributiveLattice, LowerBoundedLattice, UpperBoundedLattice, LowerBoundedDistributiveLattice, UpperBoundedDistributiveLattice, BooleanAlgebra (..),
HeytingAlgebra (..), CoHeytingAlgebra (..), SemiHeytingAlgebra (..), SemiCoHeytingAlgebra (..), BiHeytingAlgebra) where
import Data.Set (union, intersection, (\\), Set)
import Algebra.Lattice (JoinSemiLattice(..), MeetSemiLattice(..), BoundedJoinSemiLattice(..), BoundedMeetSemiLattice(..), Lattice (..), BoundedLattice(..))
class (JoinSemiLattice a, BoundedMeetSemiLattice a) => UpperBoundedLattice a where
class (BoundedJoinSemiLattice a, MeetSemiLattice a) => LowerBoundedLattice a where
class Lattice a => DistributiveLattice a where
class LowerBoundedLattice a => LowerBoundedDistributiveLattice a where
class UpperBoundedLattice a => UpperBoundedDistributiveLattice a where
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
(\\\)
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
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
(-->)
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
class (HeytingAlgebra a, CoHeytingAlgebra a) => BiHeytingAlgebra a where
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