Copyright	(C) 2019 Oleg Grenrus
License	BSD-3-Clause (see the file LICENSE)
Maintainer	Oleg Grenrus <oleg.grenrus@iki.fi>
Safe Haskell	Safe
Language	Haskell2010

Algebra.Heyting

Description

Synopsis

class BoundedLattice a => Heyting a where
- (==>) :: a -> a -> a
- neg :: a -> a
- (<=>) :: a -> a -> a

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 Methods (==>) :: ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne Source # neg :: ZeroHalfOne -> ZeroHalfOne Source # (<=>) :: ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne Source #
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 Methods (==>) :: Identity a -> Identity a -> Identity a Source # neg :: Identity a -> Identity a Source # (<=>) :: Identity a -> Identity a -> Identity a Source #
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 #