Algebra.Boolean

Documentation

class HeytingAlgebra a => BooleanAlgebra a

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

Defined in Algebra.Heyting

BooleanAlgebra ()

Defined in Algebra.Heyting

BooleanAlgebra All

Defined in Algebra.Heyting

BooleanAlgebra Any

Defined in Algebra.Heyting

BooleanAlgebra a => BooleanAlgebra (Identity a)

Defined in Algebra.Heyting

BooleanAlgebra a => BooleanAlgebra (Endo a)

Defined in Algebra.Heyting

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

Defined in Algebra.Heyting

BooleanAlgebra a => BooleanAlgebra (Op a)

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.

Defined in Algebra.Heyting

HeytingAlgebra a => BooleanAlgebra (Boolean a)

Defined in Algebra.Boolean

BooleanAlgebra (FreeBoolean a)

Defined in Algebra.Boolean.Free

BooleanAlgebra b => BooleanAlgebra (a -> b)

Defined in Algebra.Heyting

(BooleanAlgebra a, BooleanAlgebra b) => BooleanAlgebra (a, b)

Defined in Algebra.Heyting

BooleanAlgebra (Proxy a)

Defined in Algebra.Heyting

BooleanAlgebra a => BooleanAlgebra (Const a b)

Defined in Algebra.Heyting

BooleanAlgebra a => BooleanAlgebra (Tagged t a)

Defined in Algebra.Heyting

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

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

not :: HeytingAlgebra a => a -> a

Default implementation: not a = a ==> bottom

It is useful for optimisation reasons.

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

iff is an alias for <=>

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

Adjunction between Boolean and Heyting algebras

data Boolean a

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)

Defined in Algebra.Boolean

Methods

minBound :: Boolean a

maxBound :: Boolean a

Eq a => Eq (Boolean a)

Defined in Algebra.Boolean

Methods

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

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

Data a => Data (Boolean a)

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)

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)

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)

Defined in Algebra.Boolean

Methods

showsPrec :: Int -> Boolean a -> ShowS

show :: Boolean a -> String

showList :: [Boolean a] -> ShowS

Generic (Boolean a)

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)

Defined in Algebra.Boolean

Methods

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

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

MeetSemiLattice a => MeetSemiLattice (Boolean a)

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)

Defined in Algebra.Boolean

BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Boolean a)

Defined in Algebra.Boolean

Methods

bottom :: Boolean a

BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Boolean a)

Defined in Algebra.Boolean

Methods

top :: Boolean a

(BoundedJoinSemiLattice a, BoundedMeetSemiLattice a) => BoundedLattice (Boolean a)

Defined in Algebra.Boolean

HeytingAlgebra a => BooleanAlgebra (Boolean a)

Defined in Algebra.Boolean

HeytingAlgebra a => HeytingAlgebra (Boolean a)

Defined in Algebra.Boolean

Methods

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

not :: Boolean a -> Boolean a

type Rep (Boolean a)

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

extract value from Boolean

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

Smart constructro of the Boolean type.