Algebra.Heyting

Documentation

class BoundedLattice a => HeytingAlgebra a where

Heyting algebra is a bounded semi-lattice with implication which should satisfy the following law:

x ∧ a ≤ b ⇔ x ≤ (a ⇒ b)

This means a ⇒ b is an exponential object, which makes any Heyting algebra a cartesian closed category.

Some 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

Minimal complete definition

(==>) | not

Methods

(==>) :: a -> a -> a infixr 4

Default implementation: a ==> b = not a / b, it requires not to satisfy Boolean axioms, which will make it into a Boolean algebra.

not :: a -> a

Default implementation: not a = a ==> bottom

It is useful for optimisation reasons.

Instances

HeytingAlgebra Bool

Defined in Algebra.Heyting

Methods

(==>) :: Bool -> Bool -> Bool

not :: Bool -> Bool

HeytingAlgebra ()

Defined in Algebra.Heyting

Methods

(==>) :: () -> () -> ()

not :: () -> ()

HeytingAlgebra All

Defined in Algebra.Heyting

Methods

(==>) :: All -> All -> All

not :: All -> All

HeytingAlgebra Any

Defined in Algebra.Heyting

Methods

(==>) :: Any -> Any -> Any

not :: Any -> Any

HeytingAlgebra a => HeytingAlgebra (Identity a)

Defined in Algebra.Heyting

Methods

(==>) :: Identity a -> Identity a -> Identity a

not :: Identity a -> Identity a

HeytingAlgebra a => HeytingAlgebra (Endo a)

Defined in Algebra.Heyting

Methods

(==>) :: Endo a -> Endo a -> Endo a

not :: Endo a -> Endo a

(Ord a, Finite a) => HeytingAlgebra (Set a)

Power set: the cannoical example of a Boolean algebra

Defined in Algebra.Heyting

Methods

(==>) :: Set a -> Set a -> Set a

not :: Set a -> Set a

(Eq a, HeytingAlgebra a) => HeytingAlgebra (Dropped a)

Defined in Algebra.Heyting

Methods

(==>) :: Dropped a -> Dropped a -> Dropped a

not :: Dropped a -> Dropped a

(Eq a, HeytingAlgebra a) => HeytingAlgebra (Levitated a)

Defined in Algebra.Heyting

Methods

(==>) :: Levitated a -> Levitated a -> Levitated a

not :: Levitated a -> Levitated a

HeytingAlgebra a => HeytingAlgebra (Lifted a)

Defined in Algebra.Heyting

Methods

(==>) :: Lifted a -> Lifted a -> Lifted a

not :: Lifted a -> Lifted a

(Ord a, Bounded a) => HeytingAlgebra (Ordered a)

Defined in Algebra.Heyting

Methods

(==>) :: Ordered a -> Ordered a -> Ordered a

not :: Ordered a -> Ordered a

(Eq a, Finite a, Hashable a) => HeytingAlgebra (HashSet a)

Defined in Algebra.Heyting

Methods

(==>) :: HashSet a -> HashSet a -> HashSet a

not :: HashSet a -> HashSet a

HeytingAlgebra a => HeytingAlgebra (Boolean a)

Defined in Algebra.Boolean

Methods

(==>) :: Boolean a -> Boolean a -> Boolean a

not :: Boolean a -> Boolean a

HeytingAlgebra (FreeBoolean a)

Defined in Algebra.Boolean.Free

Methods

(==>) :: FreeBoolean a -> FreeBoolean a -> FreeBoolean a

not :: FreeBoolean a -> FreeBoolean a

HeytingAlgebra (FreeHeyting a)

Defined in Algebra.Heyting.Free

Methods

(==>) :: FreeHeyting a -> FreeHeyting a -> FreeHeyting a

not :: FreeHeyting a -> FreeHeyting a

HeytingAlgebra b => HeytingAlgebra (a -> b)

Defined in Algebra.Heyting

Methods

(==>) :: (a -> b) -> (a -> b) -> a -> b

not :: (a -> b) -> a -> b

(HeytingAlgebra a, HeytingAlgebra b) => HeytingAlgebra (a, b)

Defined in Algebra.Heyting

Methods

(==>) :: (a, b) -> (a, b) -> (a, b)

not :: (a, b) -> (a, b)

HeytingAlgebra (Proxy a)

Defined in Algebra.Heyting

Methods

(==>) :: Proxy a -> Proxy a -> Proxy a

not :: Proxy a -> Proxy a

(Ord k, Finite k, HeytingAlgebra v) => HeytingAlgebra (Map k v)

It is not a boolean algebra (even if values are).

Defined in Algebra.Heyting

Methods

(==>) :: Map k v -> Map k v -> Map k v

not :: Map k v -> Map k v

(Eq k, Finite k, Hashable k, HeytingAlgebra v) => HeytingAlgebra (HashMap k v)

Defined in Algebra.Heyting

Methods

(==>) :: HashMap k v -> HashMap k v -> HashMap k v

not :: HashMap k v -> HashMap k v

(HeytingAlgebra a, HeytingAlgebra b, Eq a) => HeytingAlgebra (Layered a b)

Defined in Algebra.Heyting.Layered

Methods

(==>) :: Layered a b -> Layered a b -> Layered a b

not :: Layered a b -> Layered a b

HeytingAlgebra a => HeytingAlgebra (Const a b)

Defined in Algebra.Heyting

Methods

(==>) :: Const a b -> Const a b -> Const a b

not :: Const a b -> Const a b

HeytingAlgebra a => HeytingAlgebra (Tagged t a)

Defined in Algebra.Heyting

Methods

(==>) :: Tagged t a -> Tagged t a -> Tagged t a

not :: Tagged t a -> Tagged t a

iff :: HeytingAlgebra a => a -> a -> a

Less than fixity of both \/ and /\.

iff' :: (Eq a, HeytingAlgebra a) => a -> a -> Bool

toBoolean :: HeytingAlgebra a => a -> a

Every Heyting algebra contains a Boolean algebra. toBoolean maps onto it; moreover it is a monad (Heyting algebra is a category as every poset is) which preserves finite infima.

Properties

Properties are exported only if export-properties cabal flag is defined.

prop_BoundedMeetSemiLattice :: (BoundedMeetSemiLattice a, Eq a, Show a) => a -> a -> a -> Property

Verfifies bounded meet semilattice laws.

prop_BoundedJoinSemiLattice :: (BoundedJoinSemiLattice a, Eq a, Show a) => a -> a -> a -> Property

Verfifies bounded join semilattice laws.

prop_HeytingAlgebra :: (HeytingAlgebra a, Eq a, Show a) => a -> a -> a -> Property

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

• bounded lattice laws

• prop_implies

prop_implies :: (HeytingAlgebra a, Eq a, Show a) => a -> a -> a -> Property

Verifies the Heyting algebra law for ==>: for all a: _ / a is left adjoint to a ==>