| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Algebra.Heyting
Contents
Synopsis
- class BoundedLattice a => HeytingAlgebra a where
- implies :: HeytingAlgebra a => a -> a -> a
- (<=>) :: HeytingAlgebra a => a -> a -> a
- iff :: HeytingAlgebra a => a -> a -> a
- iff' :: (Eq a, HeytingAlgebra a) => a -> a -> Bool
- toBoolean :: HeytingAlgebra a => a -> a
- class HeytingAlgebra a => BooleanAlgebra a
Heyting algebras
class BoundedLattice a => HeytingAlgebra a where Source #
Heyting algebra is a bounded semi-lattice with implication which should satisfy the following law:
x ∧ a ≤ b ⇔ x ≤ (a ⇒ b)
We also require that a Heyting algebra is a distributive lattice, which means any of the two equivalent conditions holds:
a ∧ (b ∨ c) = a ∧ b ∨ a ∧ c
a ∨ (b ∧ c) = (a ∨ b) ∧ (a ∨ c)
This means a ⇒ b is an
exponential object,
which makes any Heyting algebra
a cartesian
closed category.
This means that Curry isomorphism holds (which takes a form of an actual
equality):
a ⇒ (b ⇒ c) = (a ∧ b) ⇒ c
Some other useful properties of Heyting algebras:
(a ⇒ b) ∧ a ≤ b
b ≤ a ⇒ a ∧ b
a ≤ b iff a ⇒ b = ⊤
b ≤ b' then a ⇒ b ≤ a ⇒ b'
a'≤ a then a' ⇒ b ≤ a ⇒ b
not (a ∧ b) = not (a ∨ b)
not (a ∨ b) = not a ∧ not b
Methods
(==>) :: 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.
Instances
(<=>) :: HeytingAlgebra a => a -> a -> a Source #
toBoolean :: HeytingAlgebra a => a -> a Source #
Every Heyting algebra contains a Boolean algebra. toBoolean
Boolean algebras
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