Data.Lattice

Lattices & algebras

Types

type Lattice a = (Eq a, Semilattice L a, Extremal L a, Semilattice R a, Extremal R a)

Bounded lattices.

Neutrality:

The least and greatest elements of a complete a are given by the unique upper and lower adjoints to the function a -> ().

x \/ false = x
x /\ true = x
glb false x true = x
lub false x true = x

type Semilattice k a = Connection k (a, a) a

Semilattices.

A complete is a partially ordered set in which every two elements have a unique join (least upper bound or supremum) and a unique meet (greatest lower bound or infimum).

These operations may in turn be defined by the lower and upper adjoints to the unique function a -> (a, a).

Associativity

x \/ (y \/ z) = (x \/ y) \/ z
x /\ (y /\ z) = (x /\ y) /\ z

Commutativity

x \/ y = y \/ x
x /\ y = y /\ x

Idempotency

x \/ x = x
x /\ x = x

Absorption

(x \/ y) /\ y = y
(x /\ y) \/ y = y

See Absorption.

Note that distributivity is _not_ a requirement for a complete. However when a is distributive we have;

glb x y z = lub x y z

See https://en.wikipedia.org/wiki/Lattice_(order).

HeytingL

type HeytingL = Heyting L

A convenience alias for a co-Heyting algebra.

(\\) :: Heyting L a => a -> a -> a infixl 8

Logical co-implication:

\( a \Rightarrow b = \wedge \{x \mid a \leq b \vee x \} \)

Laws:

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

>>> False \\ False
False
>>> False \\ True
False
>>> True \\ False
True
>>> True \\ True
False

For many collections (e.g. Set) \\ coincides with the native \\ operator.

>>> :set -XOverloadedLists
>>> [GT,EQ] Set.\\ [LT]
fromList [EQ,GT]
>>> [GT,EQ] \\ [LT]
fromList [EQ,GT]

non :: Heyting L a => a -> a

Logical co-negation.

 non x = true \\ x

Laws:

non false = true
non true = false
x >= non (non x)
non (x /\ y) >= non x
non (y \\ x) = non (non x) \/ non y
non (x /\ y) = non x \/ non y
x \/ non x = true
non (non (non x)) = non x
non (non (x /\ non x)) = false

equiv :: Heyting L a => a -> a -> a

Intuitionistic co-equivalence.

boundary :: Heyting L a => a -> a

The co-Heyting boundary operator.

x = boundary x \/ (non . non) x
boundary (x /\ y) = (boundary x /\ y) \/ (x /\ boundary y)  -- (Leibniz rule)
boundary (x \/ y) \/ boundary (x /\ y) = boundary x \/ boundary y

booleanL :: Heyting L a => Conn L a a

An adjunction between a co-Heyting algebra and its Boolean sub-algebra.

Double negation is a join-preserving comonad.

heytingL :: Lattice a => (a -> a -> a) -> a -> Conn L a a

Default constructor for a co-Heyting algebra.

HeytingR

type HeytingR = Heyting R

A convenience alias for a Heyting algebra.

(//) :: Heyting R a => a -> a -> a infixr 8

Logical implication:

\( a \Rightarrow b = \vee \{x \mid x \wedge a \leq b \} \)

Laws:

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

>>> False // False
True
>>> False // True
True
>>> True // False
False
>>> True // True
True

neg :: Heyting R a => a -> a

Logical negation.

 neg x = x // false

Laws:

neg false = true
neg true = false
x <= neg (neg x)
neg (x \/ y) <= neg x
neg (x // y) = neg (neg x) /\ neg y
neg (x \/ y) = neg x /\ neg y
x /\ neg x = false
neg (neg (neg x)) = neg x
neg (neg (x \/ neg x)) = true

Some logics may in addition obey De Morgan conditions.

iff :: Heyting R a => a -> a -> a

Intuitionistic equivalence.

When a=Bool this is 'if-and-only-if'.

middle :: Heyting R a => a -> a

The Heyting (not necessarily excluded) middle operator.

booleanR :: Heyting R a => Conn R a a

An adjunction between a Heyting algebra and its Boolean sub-algebra.

Double negation is a meet-preserving monad.

heytingR :: Lattice a => (a -> a -> a) -> a -> Conn R a a

Default constructor for a Heyting algebra.

Heyting

(\/) :: Semilattice L a => a -> a -> a infixr 5

Semigroup operation on a join-semilattice.

(\/) = curry $ lowerL forked

(/\) :: Semilattice R a => a -> a -> a infixr 6

Semigroup operation on a meet-semilattice.

(/\) = curry $ upperR forked

glb :: Triple (a, a) a => a -> a -> a -> a

Greatest lower bound operator.

glb x x y = x
glb x y z = glb z x y
glb x x y = x
glb x y z = glb x z y
glb (glb x w y) w z = glb x w (glb y w z)

>>> glb 1.0 9.0 7.0
7.0
>>> glb 1.0 9.0 (0.0 / 0.0)
9.0
>>> glb (fromList [1..3]) (fromList [3..5]) (fromList [5..7]) :: Set Int
fromList [3,5]

lub :: Triple (a, a) a => a -> a -> a -> a

Least upper bound operator.

The order dual of glb.

>>> lub 1.0 9.0 7.0
7.0
>>> lub 1.0 9.0 (0.0 / 0.0)
1.0

true :: Lattice a => a

The unique top element of a bounded lattice

x /\ true = x
x \/ true = true

false :: Lattice a => a

The unique bottom element of a bounded lattice

x /\ false = false
x \/ false = x

class Lattice a => Heyting k a where

Heyting algebras

A Heyting algebra is a bounded, distributive complete equipped with an implication operation.

• The complete of closed subsets of a trueological space is the primordial example of a HeytingL (co-Heyting) algebra.
• The dual complete of open subsets of a trueological space is likewise the primordial example of a HeytingR algebra.

Heyting 'L:

Co-implication to a is the lower adjoint of disjunction with a:

x \\ a <= y <=> x <= y \/ a

Note that co-Heyting algebras needn't obey the law of non-contradiction:

EQ /\ non EQ = EQ /\ GT \\ EQ = EQ /\ GT = EQ /= LT

See https://ncatlab.org/nlab/show/co-Heyting+algebra

Heyting 'R:

Implication from a is the upper adjoint of conjunction with a:

x <= a // y <=> a /\ x <= y

Similarly, Heyting algebras needn't obey the law of the excluded middle:

EQ \/ neg EQ = EQ \/ EQ // LT = EQ \/ LT = EQ /= GT

See https://ncatlab.org/nlab/show/Heyting+algebra

Methods

heyting :: a -> Conn k a a

The defining connection of a (co-)Heyting algebra.

heyting @'L x = ConnL (\\ x) (\/ x) 
heyting @'R x = ConnR (x /\) (x //)

Instances

Heyting L Bool

Defined in Data.Lattice

Methods

heyting :: Bool -> Conn L Bool Bool

Heyting L Int

Defined in Data.Lattice

Methods

heyting :: Int -> Conn L Int Int

Heyting L Int8

Defined in Data.Lattice

Methods

heyting :: Int8 -> Conn L Int8 Int8

Heyting L Int16

Defined in Data.Lattice

Methods

heyting :: Int16 -> Conn L Int16 Int16

Heyting L Int32

Defined in Data.Lattice

Methods

heyting :: Int32 -> Conn L Int32 Int32

Heyting L Int64

Defined in Data.Lattice

Methods

heyting :: Int64 -> Conn L Int64 Int64

Heyting L Ordering

Defined in Data.Lattice

Methods

heyting :: Ordering -> Conn L Ordering Ordering

Heyting L Word

Defined in Data.Lattice

Methods

heyting :: Word -> Conn L Word Word

Heyting L Word8

Defined in Data.Lattice

Methods

heyting :: Word8 -> Conn L Word8 Word8

Heyting L Word16

Defined in Data.Lattice

Methods

heyting :: Word16 -> Conn L Word16 Word16

Heyting L Word32

Defined in Data.Lattice

Methods

heyting :: Word32 -> Conn L Word32 Word32

Heyting L Word64

Defined in Data.Lattice

Methods

heyting :: Word64 -> Conn L Word64 Word64

Heyting L ()

Defined in Data.Lattice

Methods

heyting :: () -> Conn L () ()

Heyting L IntSet

Defined in Data.Lattice

Methods

heyting :: IntSet -> Conn L IntSet IntSet

Heyting R Bool

Defined in Data.Lattice

Methods

heyting :: Bool -> Conn R Bool Bool

Heyting R Int

Defined in Data.Lattice

Methods

heyting :: Int -> Conn R Int Int

Heyting R Int8

Defined in Data.Lattice

Methods

heyting :: Int8 -> Conn R Int8 Int8

Heyting R Int16

Defined in Data.Lattice

Methods

heyting :: Int16 -> Conn R Int16 Int16

Heyting R Int32

Defined in Data.Lattice

Methods

heyting :: Int32 -> Conn R Int32 Int32

Heyting R Int64

Defined in Data.Lattice

Methods

heyting :: Int64 -> Conn R Int64 Int64

Heyting R Ordering

Defined in Data.Lattice

Methods

heyting :: Ordering -> Conn R Ordering Ordering

Heyting R Word

Defined in Data.Lattice

Methods

heyting :: Word -> Conn R Word Word

Heyting R Word8

Defined in Data.Lattice

Methods

heyting :: Word8 -> Conn R Word8 Word8

Heyting R Word16

Defined in Data.Lattice

Methods

heyting :: Word16 -> Conn R Word16 Word16

Heyting R Word32

Defined in Data.Lattice

Methods

heyting :: Word32 -> Conn R Word32 Word32

Heyting R Word64

Defined in Data.Lattice

Methods

heyting :: Word64 -> Conn R Word64 Word64

Heyting R ()

Defined in Data.Lattice

Methods

heyting :: () -> Conn R () ()

Heyting R IntSet

Defined in Data.Lattice

Methods

heyting :: IntSet -> Conn R IntSet IntSet

Finite a => Heyting L (Predicate a)

Defined in Data.Lattice

Methods

heyting :: Predicate a -> Conn L (Predicate a) (Predicate a)

(Finite a, Biheyting a) => Heyting L (Endo a)

Defined in Data.Lattice

Methods

heyting :: Endo a -> Conn L (Endo a) (Endo a)

(Total a, Finite a) => Heyting L (Set a)

Defined in Data.Lattice

Methods

heyting :: Set a -> Conn L (Set a) (Set a)

KnownNat n => Heyting L (Finite n)

Defined in Data.Lattice

Methods

heyting :: Finite n -> Conn L (Finite n) (Finite n)

Heyting R a => Heyting R (Maybe a)

Defined in Data.Lattice

Methods

heyting :: Maybe a -> Conn R (Maybe a) (Maybe a)

Finite a => Heyting R (Predicate a)

Defined in Data.Lattice

Methods

heyting :: Predicate a -> Conn R (Predicate a) (Predicate a)

(Finite a, Biheyting a) => Heyting R (Endo a)

Defined in Data.Lattice

Methods

heyting :: Endo a -> Conn R (Endo a) (Endo a)

(Total a, Finite a) => Heyting R (Set a)

Defined in Data.Lattice

Methods

heyting :: Set a -> Conn R (Set a) (Set a)

KnownNat n => Heyting R (Finite n)

Defined in Data.Lattice

Methods

heyting :: Finite n -> Conn R (Finite n) (Finite n)

Heyting R a => Heyting R (Extended a)

Defined in Data.Lattice

Methods

heyting :: Extended a -> Conn R (Extended a) (Extended a)

Heyting R a => Heyting R (Lowered a)

Subdirectly irreducible Heyting algebra.

Defined in Data.Lattice

Methods

heyting :: Lowered a -> Conn R (Lowered a) (Lowered a)

Heyting R a => Heyting R (Lifted a)

Defined in Data.Lattice

Methods

heyting :: Lifted a -> Conn R (Lifted a) (Lifted a)

(Heyting k a, Heyting k b) => Heyting k (a, b)

Defined in Data.Lattice

Methods

heyting :: (a, b) -> Conn k (a, b) (a, b)

(Finite a, Biheyting b) => Heyting L (a -> b)

Defined in Data.Lattice

Methods

heyting :: (a -> b) -> Conn L (a -> b) (a -> b)

(Finite a, Biheyting b) => Heyting L (Op b a)

Defined in Data.Lattice

Methods

heyting :: Op b a -> Conn L (Op b a) (Op b a)

(Finite a, Biheyting b) => Heyting R (a -> b)

Defined in Data.Lattice

Methods

heyting :: (a -> b) -> Conn R (a -> b) (a -> b)

(Finite a, Biheyting b) => Heyting R (Op b a)

Defined in Data.Lattice

Methods

heyting :: Op b a -> Conn R (Op b a) (Op b a)

Symmetric

type Biheyting a = (HeytingL a, HeytingR a)

A bi-Heyting algebra.

Laws:

neg x <= non x

with equality occurring iff a is a Boolean algebra.

class Biheyting a => Symmetric a where

Symmetric Heyting algebras

A symmetric Heyting algebra is a De Morgan bi-Heyting algebra with an idempotent, antitone negation operator.

Laws:

x <= y => not y <= not x -- antitone
not . not = id           -- idempotence
x \\ y = not (not y // not x)
x // y = not (not y \\ not x)

and:

converseR x <= converseL x

with equality occurring iff a is a Boolean algebra.

Minimal complete definition

not

Methods

not :: a -> a

Symmetric negation.

not . not = id
neg . neg = converseR . converseL
non . non = converseL . converseR
neg . non = converseR . converseR
non . neg = converseL . converseL

neg = converseR . not = not . converseL
non = not . converseR = converseL . not
x \\ y = not (not y // not x)
x // y = not (not y \\ not x)

xor :: a -> a -> a infixl 4

Exclusive or.

xor x y = (x \/ y) /\ (not x \/ not y)

converseL :: a -> a

Left converse operator.

converseR :: a -> a

Right converse operator.

Instances

Symmetric Bool

Defined in Data.Lattice

Methods

not :: Bool -> Bool

xor :: Bool -> Bool -> Bool

converseL :: Bool -> Bool

converseR :: Bool -> Bool

Symmetric Ordering

Defined in Data.Lattice

Methods

not :: Ordering -> Ordering

xor :: Ordering -> Ordering -> Ordering

converseL :: Ordering -> Ordering

converseR :: Ordering -> Ordering

Symmetric ()

Defined in Data.Lattice

Methods

not :: () -> ()

xor :: () -> () -> ()

converseL :: () -> ()

converseR :: () -> ()

Symmetric IntSet

Defined in Data.Lattice

Methods

not :: IntSet -> IntSet

xor :: IntSet -> IntSet -> IntSet

converseL :: IntSet -> IntSet

converseR :: IntSet -> IntSet

Finite a => Symmetric (Predicate a)

Defined in Data.Lattice

Methods

not :: Predicate a -> Predicate a

xor :: Predicate a -> Predicate a -> Predicate a

converseL :: Predicate a -> Predicate a

converseR :: Predicate a -> Predicate a

(Finite a, Symmetric a) => Symmetric (Endo a)

Defined in Data.Lattice

Methods

not :: Endo a -> Endo a

xor :: Endo a -> Endo a -> Endo a

converseL :: Endo a -> Endo a

converseR :: Endo a -> Endo a

(Total a, Finite a) => Symmetric (Set a)

Defined in Data.Lattice

Methods

not :: Set a -> Set a

xor :: Set a -> Set a -> Set a

converseL :: Set a -> Set a

converseR :: Set a -> Set a

(Finite a, Symmetric b) => Symmetric (a -> b)

Defined in Data.Lattice

Methods

not :: (a -> b) -> a -> b

xor :: (a -> b) -> (a -> b) -> a -> b

converseL :: (a -> b) -> a -> b

converseR :: (a -> b) -> a -> b

(Symmetric a, Symmetric b) => Symmetric (a, b)

Defined in Data.Lattice

Methods

not :: (a, b) -> (a, b)

xor :: (a, b) -> (a, b) -> (a, b)

converseL :: (a, b) -> (a, b)

converseR :: (a, b) -> (a, b)

(Finite a, Symmetric b) => Symmetric (Op b a)

Defined in Data.Lattice

Methods

not :: Op b a -> Op b a

xor :: Op b a -> Op b a -> Op b a

converseL :: Op b a -> Op b a

converseR :: Op b a -> Op b a

symmetricL :: Symmetric a => a -> ConnL a a

Default constructor for a co-Heyting algebra.

symmetricR :: Symmetric a => a -> ConnR a a

Default constructor for a Heyting algebra.

Boolean

class Symmetric a => Boolean a where

Boolean algebras.

Boolean algebras are symmetric Heyting algebras that satisfy both the law of excluded middle and the law of law of non-contradiction:

x \/ neg x = true
x /\ non x = false

If a is Boolean we also have:

non = not = neg

Minimal complete definition

Nothing

Methods

boolean :: Trip a a

A witness to the lawfulness of a boolean algebra.

Instances

Boolean Bool

Defined in Data.Lattice

Methods

boolean :: Trip Bool Bool

Boolean ()

Defined in Data.Lattice

Methods

boolean :: Trip () ()

Boolean IntSet

Defined in Data.Lattice

Methods

boolean :: Trip IntSet IntSet

Finite a => Boolean (Predicate a)

Defined in Data.Lattice

Methods

boolean :: Trip (Predicate a) (Predicate a)

(Finite a, Boolean a) => Boolean (Endo a)

Defined in Data.Lattice

Methods

boolean :: Trip (Endo a) (Endo a)

(Total a, Finite a) => Boolean (Set a)

Defined in Data.Lattice

Methods

boolean :: Trip (Set a) (Set a)

(Finite a, Boolean b) => Boolean (a -> b)

Defined in Data.Lattice

Methods

boolean :: Trip (a -> b) (a -> b)

(Boolean a, Boolean b) => Boolean (a, b)

Defined in Data.Lattice

Methods

boolean :: Trip (a, b) (a, b)

(Finite a, Boolean b) => Boolean (Op b a)

Defined in Data.Lattice

Methods

boolean :: Trip (Op b a) (Op b a)