heyting-algebras-0.0.2.0: Heyting and Boolean algebras

Safe HaskellNone
LanguageHaskell2010

Algebra.Boolean

Contents

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
BooleanAlgebra Bool Source # 
Instance details

Defined in Algebra.Heyting

BooleanAlgebra () Source # 
Instance details

Defined in Algebra.Heyting

BooleanAlgebra All Source # 
Instance details

Defined in Algebra.Heyting

BooleanAlgebra Any Source # 
Instance details

Defined in Algebra.Heyting

BooleanAlgebra a => BooleanAlgebra (Identity a) Source # 
Instance details

Defined in Algebra.Heyting

BooleanAlgebra a => BooleanAlgebra (Endo a) Source # 
Instance details

Defined in Algebra.Heyting

(Ord a, Finite a) => BooleanAlgebra (Set a) Source # 
Instance details

Defined in Algebra.Heyting

BooleanAlgebra a => BooleanAlgebra (Op a) 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 details

Defined in Algebra.Heyting

HeytingAlgebra a => BooleanAlgebra (Boolean a) Source # 
Instance details

Defined in Algebra.Boolean

BooleanAlgebra (FreeBoolean a) Source # 
Instance details

Defined in Algebra.Boolean.Free

BooleanAlgebra b => BooleanAlgebra (a -> b) Source # 
Instance details

Defined in Algebra.Heyting

(BooleanAlgebra a, BooleanAlgebra b) => BooleanAlgebra (a, b) Source # 
Instance details

Defined in Algebra.Heyting

BooleanAlgebra (Proxy a) Source # 
Instance details

Defined in Algebra.Heyting

BooleanAlgebra a => BooleanAlgebra (Const a b) Source # 
Instance details

Defined in Algebra.Heyting

BooleanAlgebra a => BooleanAlgebra (Tagged t a) Source # 
Instance details

Defined 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 details

Defined in Algebra.Boolean

Methods

minBound :: Boolean a #

maxBound :: Boolean a #

Eq a => Eq (Boolean a) Source # 
Instance details

Defined in Algebra.Boolean

Methods

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

(/=) :: Boolean a -> Boolean a -> Bool #

Data a => Data (Boolean a) Source # 
Instance details

Defined in Algebra.Boolean

Methods

gfoldl :: (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 #

dataTypeOf :: Boolean a -> DataType #

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 details

Defined in Algebra.Boolean

Methods

compare :: 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 details

Defined in Algebra.Boolean

Methods

readsPrec :: Int -> ReadS (Boolean a) #

readList :: ReadS [Boolean a] #

readPrec :: ReadPrec (Boolean a) #

readListPrec :: ReadPrec [Boolean a] #

Show a => Show (Boolean a) Source # 
Instance details

Defined in Algebra.Boolean

Methods

showsPrec :: Int -> Boolean a -> ShowS #

show :: Boolean a -> String #

showList :: [Boolean a] -> ShowS #

Generic (Boolean a) Source # 
Instance details

Defined in Algebra.Boolean

Associated Types

type Rep (Boolean a) :: Type -> Type #

Methods

from :: Boolean a -> Rep (Boolean a) x #

to :: Rep (Boolean a) x -> Boolean a #

JoinSemiLattice a => JoinSemiLattice (Boolean a) Source # 
Instance details

Defined in Algebra.Boolean

Methods

(\/) :: Boolean a -> Boolean a -> Boolean a #

join :: Boolean a -> Boolean a -> Boolean a #

MeetSemiLattice a => MeetSemiLattice (Boolean a) Source # 
Instance details

Defined 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 details

Defined in Algebra.Boolean

BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Boolean a) Source # 
Instance details

Defined in Algebra.Boolean

Methods

bottom :: Boolean a #

BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Boolean a) Source # 
Instance details

Defined in Algebra.Boolean

Methods

top :: Boolean a #

(BoundedJoinSemiLattice a, BoundedMeetSemiLattice a) => BoundedLattice (Boolean a) Source # 
Instance details

Defined in Algebra.Boolean

HeytingAlgebra a => BooleanAlgebra (Boolean a) Source # 
Instance details

Defined in Algebra.Boolean

HeytingAlgebra a => HeytingAlgebra (Boolean a) Source # 
Instance details

Defined in Algebra.Boolean

Methods

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

not :: Boolean a -> Boolean a Source #

type Rep (Boolean a) Source # 
Instance details

Defined 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.