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

Copyright(C) 2019 Oleg Grenrus
LicenseBSD-3-Clause (see the file LICENSE)
MaintainerOleg Grenrus <oleg.grenrus@iki.fi>
Safe HaskellSafe
LanguageHaskell2010

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

Defined in Algebra.Heyting

Methods

(==>) :: Bool -> Bool -> Bool Source #

neg :: Bool -> Bool Source #

(<=>) :: Bool -> Bool -> Bool Source #

Heyting () Source # 
Instance details

Defined in Algebra.Heyting

Methods

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

neg :: () -> () Source #

(<=>) :: () -> () -> () Source #

Heyting All Source # 
Instance details

Defined in Algebra.Heyting

Methods

(==>) :: All -> All -> All Source #

neg :: All -> All Source #

(<=>) :: All -> All -> All Source #

Heyting Any Source # 
Instance details

Defined in Algebra.Heyting

Methods

(==>) :: Any -> Any -> Any Source #

neg :: Any -> Any Source #

(<=>) :: Any -> Any -> Any Source #

Heyting ZeroHalfOne Source #

Not boolean: neg Half \/ Half = Half /= One

Instance details

Defined in Algebra.Lattice.ZeroHalfOne

Heyting M2 Source # 
Instance details

Defined in Algebra.Lattice.M2

Methods

(==>) :: M2 -> M2 -> M2 Source #

neg :: M2 -> M2 Source #

(<=>) :: M2 -> M2 -> M2 Source #

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

Defined in Algebra.Heyting

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

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

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

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

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

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

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

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

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

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