Safe Haskell	None
Language	GHC2024

Circuit.Logics.Heyting

Description

Heyting algebras: bounded lattices with implication.

A Heyting algebra need not be Boolean: excluded middle may fail. Classical Bool is Heyting (via material implication); H3 and Goedel are the standard non-Boolean examples in this package.

Synopsis

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

Documentation

class BoundedLattice a => Heyting a where Source #

Bounded lattice with relative pseudo-complement (==>).

Characteristic properties (see Circuit.Logics.Laws):

a ==> a           == top
a /\ (a ==> b)    == a /\ b
b /\ (a ==> b)    == b
a ==> (b /\ c)    == (a ==> b) /\ (a ==> c)

Methods

(==>) :: a -> a -> a infixr 1 Source #

Implication (relative pseudo-complement).

Instances

Instances details

Heyting H3 Source #
Instance details Defined in Circuit.Logics.H3 Methods (==>) :: H3 -> H3 -> H3 Source #
Heyting Bool Source #
Instance details Defined in Circuit.Logics.Heyting Methods (==>) :: Bool -> Bool -> Bool Source #
(Ord r, Num r) => Heyting (Goedel r) Source #
Instance details Defined in Circuit.Logics.Goedel Methods (==>) :: Goedel r -> Goedel r -> Goedel r Source #