module Lattices.ResiduatedLattice(
    ResiduatedLattice(..),
    BoundedLattice(..),
    Nat
) where


type Nat = Int

-- | Lattice is an algebraic structure with join and meet operations.

-- BoundedLattice has Top and Bottom elements

-- Lattice satisfies following laws:

--

-- /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/

--

-- @

-- a '\/' (a '/\' b) ≡ a

-- a '/\' (a '\/' b) ≡ a

-- @

class RealFrac l => BoundedLattice l where
    -- | meet

    (/\) :: l -> l -> l
    -- | join

    (\/) :: l -> l -> l
    -- | also called upper bound

    top :: l 
    -- | also called lower bound

    bot :: l
    -- | constructor for lattice

    mkLattice :: Double -> l

-- | A bounded lattice with additional laws and operations namely --> and tnorm

--

-- /Commutativity/

--

-- @

-- x 'tnorm' y ≡ y 'tnorm' x

-- @

--

-- /Asociativity of 'tnorm'/

--

-- @

-- x 'tnorm' (y 'tnorm' z) ≡ (x 'tnorm' y) 'tnorm' z

-- @

--

-- /Identity Element/

-- @

--  x 'tnorm' 1 ≡ x

-- @

--

-- /Adjointness/

-- @

-- x ≤ y '-->' z iff x 'tnorm' y ≤ z 

-- @

class BoundedLattice l => ResiduatedLattice l where
    -- | residuum

    (-->), (<--) :: l -> l -> l 
    l
a <-- l
b = l
b l -> l -> l
forall l. ResiduatedLattice l => l -> l -> l
--> l
a
    -- | biresiduum 

    (<-->) :: l -> l -> l
    l
a <--> l
b = (l
a l -> l -> l
forall l. ResiduatedLattice l => l -> l -> l
--> l
b) l -> l -> l
forall l. BoundedLattice l => l -> l -> l
/\ (l
b l -> l -> l
forall l. ResiduatedLattice l => l -> l -> l
--> l
a)
    tnorm :: l -> l -> l 
    negation :: l -> l
    negation l
a = l
a l -> l -> l
forall l. ResiduatedLattice l => l -> l -> l
--> l
forall l. BoundedLattice l => l
bot
    
    power :: l -> Nat -> l
    power l
a Nat
0 = l
forall l. BoundedLattice l => l
top
    power l
a Nat
n = l
a l -> l -> l
forall l. ResiduatedLattice l => l -> l -> l
`tnorm` l -> Nat -> l
forall l. ResiduatedLattice l => l -> Nat -> l
power l
a (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1)