lattices-2: Fine-grained library for constructing and manipulating lattices

Algebra.Heyting

Description

Synopsis

# Documentation

class BoundedLattice a => Heyting a where Source #

A Heyting algebra is a bounded lattice equipped with a binary operation $$a \to b$$ of implication.

Laws

x ==> x        ≡ top
x /\ (x ==> y) ≡ x /\ y
y /\ (x ==> y) ≡ y
x ==> (y /\ z) ≡ (x ==> y) /\ (x ==> z)


Minimal complete definition

(==>)

Methods

(==>) :: a -> a -> a infixr 5 Source #

Implication.

neg :: a -> a Source #

Negation.

neg x = x ==> bottom


(<=>) :: a -> a -> a infixr 5 Source #

Equivalence.

x <=> y = (x ==> y) /\ (y ==> x)

Instances
 Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: Bool -> Bool -> Bool Source #(<=>) :: Bool -> Bool -> Bool Source # Heyting () Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: () -> () -> () Source #neg :: () -> () Source #(<=>) :: () -> () -> () Source # Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: All -> All -> All Source #neg :: All -> All Source #(<=>) :: All -> All -> All Source # Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: Any -> Any -> Any Source #neg :: Any -> Any Source #(<=>) :: Any -> Any -> Any Source # Source # Not boolean: neg Half \/ Half = Half /= One Instance detailsDefined in Algebra.Lattice.ZeroHalfOne Methods Source # Instance detailsDefined in Algebra.Lattice.M2 Methods(==>) :: M2 -> M2 -> M2 Source #neg :: M2 -> M2 Source #(<=>) :: M2 -> M2 -> M2 Source # Heyting a => Heyting (Identity a) Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: Identity a -> Identity a -> Identity a Source #neg :: Identity a -> Identity a Source #(<=>) :: Identity a -> Identity a -> Identity a Source # Heyting a => Heyting (Endo a) Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: Endo a -> Endo a -> Endo a Source #neg :: Endo a -> Endo a Source #(<=>) :: Endo a -> Endo a -> Endo a Source # (Ord a, Finite a) => Heyting (Set a) Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: Set a -> Set a -> Set a Source #neg :: Set a -> Set a Source #(<=>) :: Set a -> Set a -> Set a Source # (Eq a, Hashable a, Finite a) => Heyting (HashSet a) Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: HashSet a -> HashSet a -> HashSet a Source #neg :: HashSet a -> HashSet a Source #(<=>) :: HashSet a -> HashSet a -> HashSet a Source # (Ord a, Bounded a) => Heyting (Ordered a) Source # This is interesting logic, as it satisfies both de Morgan laws; but isn't Boolean: i.e. law of exluded middle doesn't hold.Negation "smashes" value into minBound or maxBound. Instance detailsDefined in Algebra.Lattice.Ordered Methods(==>) :: Ordered a -> Ordered a -> Ordered a Source #neg :: Ordered a -> Ordered a Source #(<=>) :: Ordered a -> Ordered a -> Ordered a Source # Heyting (Free a) Source # Instance detailsDefined in Algebra.Heyting.Free Methods(==>) :: Free a -> Free a -> Free a Source #neg :: Free a -> Free a Source #(<=>) :: Free a -> Free a -> Free a Source # Heyting a => Heyting (b -> a) Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: (b -> a) -> (b -> a) -> b -> a Source #neg :: (b -> a) -> b -> a Source #(<=>) :: (b -> a) -> (b -> a) -> b -> a Source # Heyting (Proxy a) Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: Proxy a -> Proxy a -> Proxy a Source #neg :: Proxy a -> Proxy a Source #(<=>) :: Proxy a -> Proxy a -> Proxy a Source # Heyting a => Heyting (Const a b) Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: Const a b -> Const a b -> Const a b Source #neg :: Const a b -> Const a b Source #(<=>) :: Const a b -> Const a b -> Const a b Source # Heyting a => Heyting (Tagged b a) Source # Instance detailsDefined in Algebra.Heyting Methods(==>) :: Tagged b a -> Tagged b a -> Tagged b a Source #neg :: Tagged b a -> Tagged b a Source #(<=>) :: Tagged b a -> Tagged b a -> Tagged b a Source #