| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Algebra.Boolean
Synopsis
- class HeytingAlgebra a => BooleanAlgebra a
- (==>) :: HeytingAlgebra a => a -> a -> a
- not :: HeytingAlgebra a => a -> a
- iff :: HeytingAlgebra a => a -> a -> a
- iff' :: (Eq a, HeytingAlgebra a) => a -> a -> Bool
- data Boolean a
- runBoolean :: Boolean a -> a
- boolean :: HeytingAlgebra a => a -> Boolean a
- prop_not :: (HeytingAlgebra a, Eq a, Show a) => a -> Property
- prop_BooleanAlgebra :: (BooleanAlgebra a, Eq a, Show a) => a -> a -> a -> Property
Documentation
class HeytingAlgebra a => BooleanAlgebra a Source #
Boolean algebra is a Heyting algebra which negation satisfies the law of excluded middle, i.e. either of the following:
not . not == not
or
x ∨ not x == top
Another characterisation of Boolean algebras is as complemented distributive lattices where the complement satisfies the following three properties:
(not a) ∧ a == bottom and (not a) ∨ a == top -- excluded middle law
not (not a) == a -- involution law
a ≤ b ⇒ not b ≤ not a -- order-reversing
Instances
(==>) :: HeytingAlgebra a => a -> a -> a infixr 4 Source #
Default implementation: a ==> b = not a / b, it requires not to
satisfy Boolean axioms, which will make it into a Boolean algebra.
not :: HeytingAlgebra a => a -> a Source #
Adjunction between Boolean and Heyting algebras
Boolean
Instances
runBoolean :: Boolean a -> a Source #
extract value from Boolean
Properties
Properties are exported only if export-properties cabal flag is defined.
prop_not :: (HeytingAlgebra a, Eq a, Show a) => a -> Property Source #
Test that not
prop_BooleanAlgebra :: (BooleanAlgebra a, Eq a, Show a) => a -> a -> a -> Property Source #
Test that a is satisfy both prop_HeytingAlgebraprop_not