heyting-algebras-0.0.2.0: Heyting and Boolean algebras

Algebra.Boolean

Synopsis

# 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
 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

(==>) :: 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.

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

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

Default implementation: not a = a ==> bottom

It is useful for optimisation reasons.

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

iff is an alias for <=>

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

# Adjunction between Boolean and Heyting algebras

data Boolean a Source #

Boolean is the left adjoint functor from the category of Heyting algebras to the category of Boolean algebras; its right adjoint is the inclusion.

Instances
 Bounded a => Bounded (Boolean a) Source # Instance detailsDefined in Algebra.Boolean Methods Eq a => Eq (Boolean a) Source # Instance detailsDefined in Algebra.Boolean Methods(==) :: Boolean a -> Boolean a -> Bool #(/=) :: Boolean a -> Boolean a -> Bool # Data a => Data (Boolean a) Source # Instance detailsDefined in Algebra.Boolean Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Boolean a -> c (Boolean a) #gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Boolean a) #toConstr :: Boolean a -> Constr #dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Boolean a)) #dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Boolean a)) #gmapT :: (forall b. Data b => b -> b) -> Boolean a -> Boolean a #gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Boolean a -> r #gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Boolean a -> r #gmapQ :: (forall d. Data d => d -> u) -> Boolean a -> [u] #gmapQi :: Int -> (forall d. Data d => d -> u) -> Boolean a -> u #gmapM :: Monad m => (forall d. Data d => d -> m d) -> Boolean a -> m (Boolean a) #gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Boolean a -> m (Boolean a) #gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Boolean a -> m (Boolean a) # Ord a => Ord (Boolean a) Source # Instance detailsDefined in Algebra.Boolean Methodscompare :: Boolean a -> Boolean a -> Ordering #(<) :: Boolean a -> Boolean a -> Bool #(<=) :: Boolean a -> Boolean a -> Bool #(>) :: Boolean a -> Boolean a -> Bool #(>=) :: Boolean a -> Boolean a -> Bool #max :: Boolean a -> Boolean a -> Boolean a #min :: Boolean a -> Boolean a -> Boolean a # Read a => Read (Boolean a) Source # Instance detailsDefined in Algebra.Boolean MethodsreadsPrec :: Int -> ReadS (Boolean a) # Show a => Show (Boolean a) Source # Instance detailsDefined in Algebra.Boolean MethodsshowsPrec :: Int -> Boolean a -> ShowS #show :: Boolean a -> String #showList :: [Boolean a] -> ShowS # Source # Instance detailsDefined in Algebra.Boolean Associated Typestype Rep (Boolean a) :: Type -> Type # Methodsfrom :: Boolean a -> Rep (Boolean a) x #to :: Rep (Boolean a) x -> Boolean a # Source # Instance detailsDefined in Algebra.Boolean Methods(\/) :: Boolean a -> Boolean a -> Boolean a #join :: Boolean a -> Boolean a -> Boolean a # Source # Instance detailsDefined in Algebra.Boolean Methods(/\) :: Boolean a -> Boolean a -> Boolean a #meet :: Boolean a -> Boolean a -> Boolean a # (JoinSemiLattice a, MeetSemiLattice a) => Lattice (Boolean a) Source # Instance detailsDefined in Algebra.Boolean Source # Instance detailsDefined in Algebra.Boolean Methods Source # Instance detailsDefined in Algebra.Boolean Methodstop :: Boolean a # Source # Instance detailsDefined in Algebra.Boolean Source # Instance detailsDefined in Algebra.Boolean Source # Instance detailsDefined in Algebra.Boolean Methods(==>) :: Boolean a -> Boolean a -> Boolean a Source #not :: Boolean a -> Boolean a Source # type Rep (Boolean a) Source # Instance detailsDefined in Algebra.Boolean type Rep (Boolean a) = D1 (MetaData "Boolean" "Algebra.Boolean" "heyting-algebras-0.0.2.0-9Jkaj3PWjyP6m0hdRJKaLi" True) (C1 (MetaCons "Boolean" PrefixI True) (S1 (MetaSel (Just "runBoolean") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)))

runBoolean :: Boolean a -> a Source #

extract value from Boolean

boolean :: HeytingAlgebra a => a -> Boolean a Source #

Smart constructro of the Boolean type.