heyting-algebras-0.0.2.0: Heyting and Boolean algebras

Algebra.Heyting

Contents

Synopsis

# 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

Minimal complete definition

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.

Fixity is less than fixity of both \/ and /\.

not :: a -> a Source #

Default implementation: not a = a ==> bottom

It is useful for optimisation reasons.

Instances
 Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: Bool -> Bool -> Bool Source # Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: () -> () -> () Source #not :: () -> () Source # Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: All -> All -> All Source #not :: All -> All Source # Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: Any -> Any -> Any Source #not :: Any -> Any Source # Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: Identity a -> Identity a -> Identity a Source #not :: Identity a -> Identity a Source # Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: Endo a -> Endo a -> Endo a Source #not :: Endo a -> Endo a Source # (Ord a, Finite a) => HeytingAlgebra (Set a) Source # Power set: the canonical example of a Boolean algebra Instance detailsDefined in Algebra.Heyting Methods(==>) :: Set a -> Set a -> Set a Source #not :: Set a -> Set a Source # (Eq a, HeytingAlgebra a) => HeytingAlgebra (Dropped a) Source # Subdirectly irreducible Heyting algebra. Instance detailsDefined in Algebra.Heyting Methods(==>) :: Dropped a -> Dropped a -> Dropped a Source #not :: Dropped a -> Dropped a Source # (Eq a, HeytingAlgebra a) => HeytingAlgebra (Levitated a) Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: Levitated a -> Levitated a -> Levitated a Source #not :: Levitated a -> Levitated a Source # Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: Lifted a -> Lifted a -> Lifted a Source #not :: Lifted a -> Lifted a Source # Source # Whenever a is a Boolean Algebra, Op a is a Boolean algebra as well, which in particular means that it is a Heyting algebra in the first place. Instance detailsDefined in Algebra.Heyting Methods(==>) :: Op a -> Op a -> Op a Source #not :: Op a -> Op a Source # (Ord a, Bounded a) => HeytingAlgebra (Ordered a) Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: Ordered a -> Ordered a -> Ordered a Source #not :: Ordered a -> Ordered a Source # (Eq a, Finite a, Hashable a) => HeytingAlgebra (HashSet a) Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: HashSet a -> HashSet a -> HashSet a Source #not :: HashSet a -> HashSet a Source # Source # Instance detailsDefined in Algebra.Boolean Methods(==>) :: Boolean a -> Boolean a -> Boolean a Source #not :: Boolean a -> Boolean a Source # Source # Instance detailsDefined in Algebra.Boolean.Free Methods Source # Instance detailsDefined in Algebra.Heyting.Free Methods HeytingAlgebra b => HeytingAlgebra (a -> b) Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: (a -> b) -> (a -> b) -> a -> b Source #not :: (a -> b) -> a -> b Source # (HeytingAlgebra a, HeytingAlgebra b) => HeytingAlgebra (a, b) Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: (a, b) -> (a, b) -> (a, b) Source #not :: (a, b) -> (a, b) Source # Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: Proxy a -> Proxy a -> Proxy a Source #not :: Proxy a -> Proxy a Source # (Ord k, Finite k, HeytingAlgebra v) => HeytingAlgebra (Map k v) Source # It is not a boolean algebra (even if values are). Instance detailsDefined in Algebra.Heyting Methods(==>) :: Map k v -> Map k v -> Map k v Source #not :: Map k v -> Map k v Source # (Eq k, Finite k, Hashable k, HeytingAlgebra v) => HeytingAlgebra (HashMap k v) Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: HashMap k v -> HashMap k v -> HashMap k v Source #not :: HashMap k v -> HashMap k v Source # (HeytingAlgebra a, HeytingAlgebra b, Eq a) => HeytingAlgebra (Layered a b) Source # Instance detailsDefined in Algebra.Heyting.Layered Methods(==>) :: Layered a b -> Layered a b -> Layered a b Source #not :: Layered a b -> Layered a b Source # HeytingAlgebra a => HeytingAlgebra (Const a b) Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: Const a b -> Const a b -> Const a b Source #not :: Const a b -> Const a b Source # HeytingAlgebra a => HeytingAlgebra (Tagged t a) Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: Tagged t a -> Tagged t a -> Tagged t a Source #not :: Tagged t a -> Tagged t a Source #

implies :: HeytingAlgebra a => a -> a -> a Source #

implies is an alias for ==>

(<=>) :: HeytingAlgebra a => a -> a -> a Source #

iff :: HeytingAlgebra a => a -> a -> a Source #

iff is an alias for <=>

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

toBoolean :: HeytingAlgebra a => a -> a Source #

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.

# 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
Instances
 Source # Instance detailsDefined in Algebra.Heyting Source # Instance detailsDefined in Algebra.Heyting Source # Instance detailsDefined in Algebra.Heyting Source # Instance detailsDefined in Algebra.Heyting Source # Instance detailsDefined in Algebra.Heyting Source # Instance detailsDefined in Algebra.Heyting (Ord a, Finite a) => BooleanAlgebra (Set a) Source # Instance detailsDefined in Algebra.Heyting Source # Every boolean algebra is isomorphic to power set P(X) of some set X; then not :: Op (P(X)) -> P(X) is a lattice isomorphism, thus Op (P(X)) is a boolean algebra, since P(X) is. Instance detailsDefined in Algebra.Heyting Source # Instance detailsDefined in Algebra.Boolean Source # Instance detailsDefined in Algebra.Boolean.Free BooleanAlgebra b => BooleanAlgebra (a -> b) Source # Instance detailsDefined in Algebra.Heyting (BooleanAlgebra a, BooleanAlgebra b) => BooleanAlgebra (a, b) Source # Instance detailsDefined in Algebra.Heyting Source # Instance detailsDefined in Algebra.Heyting BooleanAlgebra a => BooleanAlgebra (Const a b) Source # Instance detailsDefined in Algebra.Heyting BooleanAlgebra a => BooleanAlgebra (Tagged t a) Source # Instance detailsDefined in Algebra.Heyting