Safe Haskell	Safe
Language	Haskell2010

Algebra.Heyting.Properties

Description

Properties of Heyting algebras; useful for testing lawfulness of instances.

Synopsis

data BoundedMeetSemiLatticeLawViolation a
- = BMSLVNonAssociative a a a
- | BMSLVNonCommutative a a
- | BMSLVNonIdempotent a
- | BMSLVNonUnital a
- | BMSLVMeetOrderViolation a a
withArgs :: Show a => String -> [a] -> String
prop_BoundedMeetSemiLattice :: (BoundedMeetSemiLattice a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (BoundedMeetSemiLatticeLawViolation a)
data BoundedJoinSemiLatticeLawViolation a
- = BJSLVNonAssociative a a a
- | BJSLVNonCommutative a a
- | BJSLVNonIdempotent a
- | BJSLVNonUnital a
- | BJSLVJoinOrderViolation a a
prop_BoundedJoinSemiLattice :: (BoundedJoinSemiLattice a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (BoundedJoinSemiLatticeLawViolation a)
data DistributiveLatticeLawViolation a
- = DLLVJoinOverMeetViolation a a a
- | DLLVMeetOverJoinViolation a a a
prop_DistributiveLattice :: (Lattice a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (DistributiveLatticeLawViolation a)
data HeytingAlgebraLawViolation a
- = HAVImplication1 a a a
- | HAVImplication2 a a a
- | HAVNot a a
- | HAVNotAndMeet a a
- | HAVNotAndJoin a a
- | HAVImplicationAndOrd a a
- | HAVDistributiveLatticeLawViolation (DistributiveLatticeLawViolation a)
- | HAVBoundedJoinSemilatticeLawViolation (BoundedJoinSemiLatticeLawViolation a)
- | HAVBoundedMeetSemilatticeLawViolation (BoundedMeetSemiLatticeLawViolation a)
prop_implies :: (HeytingAlgebra a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a)
prop_HeytingAlgebra :: (HeytingAlgebra a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a)

Documentation

data BoundedMeetSemiLatticeLawViolation a Source #

Constructors

BMSLVNonAssociative a a a
BMSLVNonCommutative a a
BMSLVNonIdempotent a
BMSLVNonUnital a
BMSLVMeetOrderViolation a a

Instances

Eq a => Eq (BoundedMeetSemiLatticeLawViolation a) Source #
Instance details Defined in Algebra.Heyting.Properties Methods (==) :: BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a -> Bool # (/=) :: BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a -> Bool #
Ord a => Ord (BoundedMeetSemiLatticeLawViolation a) Source #
Instance details Defined in Algebra.Heyting.Properties Methods compare :: BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a -> Ordering # (<) :: BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a -> Bool # (<=) :: BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a -> Bool # (>) :: BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a -> Bool # (>=) :: BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a -> Bool # max :: BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a # min :: BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a #
Show a => Show (BoundedMeetSemiLatticeLawViolation a) Source #
Instance details Defined in Algebra.Heyting.Properties Methods showsPrec :: Int -> BoundedMeetSemiLatticeLawViolation a -> ShowS # show :: BoundedMeetSemiLatticeLawViolation a -> String # showList :: [BoundedMeetSemiLatticeLawViolation a] -> ShowS #

withArgs :: Show a => String -> [a] -> String Source #

prop_BoundedMeetSemiLattice :: (BoundedMeetSemiLattice a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (BoundedMeetSemiLatticeLawViolation a) Source #

Verifies bounded meet semilattice laws.

data BoundedJoinSemiLatticeLawViolation a Source #

Constructors

BJSLVNonAssociative a a a
BJSLVNonCommutative a a
BJSLVNonIdempotent a
BJSLVNonUnital a
BJSLVJoinOrderViolation a a

Instances

Eq a => Eq (BoundedJoinSemiLatticeLawViolation a) Source #
Instance details Defined in Algebra.Heyting.Properties Methods (==) :: BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a -> Bool # (/=) :: BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a -> Bool #
Ord a => Ord (BoundedJoinSemiLatticeLawViolation a) Source #
Instance details Defined in Algebra.Heyting.Properties Methods compare :: BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a -> Ordering # (<) :: BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a -> Bool # (<=) :: BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a -> Bool # (>) :: BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a -> Bool # (>=) :: BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a -> Bool # max :: BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a # min :: BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a #
Show a => Show (BoundedJoinSemiLatticeLawViolation a) Source #
Instance details Defined in Algebra.Heyting.Properties Methods showsPrec :: Int -> BoundedJoinSemiLatticeLawViolation a -> ShowS # show :: BoundedJoinSemiLatticeLawViolation a -> String # showList :: [BoundedJoinSemiLatticeLawViolation a] -> ShowS #

prop_BoundedJoinSemiLattice :: (BoundedJoinSemiLattice a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (BoundedJoinSemiLatticeLawViolation a) Source #

Verifies bounded join semilattice laws.

data DistributiveLatticeLawViolation a Source #

Constructors

DLLVJoinOverMeetViolation a a a
DLLVMeetOverJoinViolation a a a

Instances

Eq a => Eq (DistributiveLatticeLawViolation a) Source #
Instance details Defined in Algebra.Heyting.Properties Methods (==) :: DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a -> Bool # (/=) :: DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a -> Bool #
Ord a => Ord (DistributiveLatticeLawViolation a) Source #
Instance details Defined in Algebra.Heyting.Properties Methods compare :: DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a -> Ordering # (<) :: DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a -> Bool # (<=) :: DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a -> Bool # (>) :: DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a -> Bool # (>=) :: DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a -> Bool # max :: DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a # min :: DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a #
Show a => Show (DistributiveLatticeLawViolation a) Source #
Instance details Defined in Algebra.Heyting.Properties Methods showsPrec :: Int -> DistributiveLatticeLawViolation a -> ShowS # show :: DistributiveLatticeLawViolation a -> String # showList :: [DistributiveLatticeLawViolation a] -> ShowS #

prop_DistributiveLattice :: (Lattice a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (DistributiveLatticeLawViolation a) Source #

Distributivity laws for a lattice.

data HeytingAlgebraLawViolation a Source #

Constructors

HAVImplication1 a a a
HAVImplication2 a a a
HAVNot a a
HAVNotAndMeet a a
HAVNotAndJoin a a
HAVImplicationAndOrd a a
HAVDistributiveLatticeLawViolation (DistributiveLatticeLawViolation a)
HAVBoundedJoinSemilatticeLawViolation (BoundedJoinSemiLatticeLawViolation a)
HAVBoundedMeetSemilatticeLawViolation (BoundedMeetSemiLatticeLawViolation a)

Instances

Eq a => Eq (HeytingAlgebraLawViolation a) Source #
Instance details Defined in Algebra.Heyting.Properties Methods (==) :: HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a -> Bool # (/=) :: HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a -> Bool #
Ord a => Ord (HeytingAlgebraLawViolation a) Source #
Instance details Defined in Algebra.Heyting.Properties Methods compare :: HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a -> Ordering # (<) :: HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a -> Bool # (<=) :: HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a -> Bool # (>) :: HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a -> Bool # (>=) :: HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a -> Bool # max :: HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a # min :: HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a #
Show a => Show (HeytingAlgebraLawViolation a) Source #
Instance details Defined in Algebra.Heyting.Properties Methods showsPrec :: Int -> HeytingAlgebraLawViolation a -> ShowS # show :: HeytingAlgebraLawViolation a -> String # showList :: [HeytingAlgebraLawViolation a] -> ShowS #

prop_implies :: (HeytingAlgebra a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a) Source #

Verifies the Heyting algebra law for ==>: for all a: _ / a is left adjoint to a ==> and some other properties that are a consequence of that.

prop_HeytingAlgebra :: (HeytingAlgebra a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a) Source #

Useful for testing valid instances of HeytingAlgebra type class. It validates:

bounded lattice laws
```
prop_implies
```