-- | Gödel–Dummett fuzzy logic on an ordered unit interval.
--
-- Meet/join are min/max; implication is the standard Gödel rule.
-- Heyting but not Boolean: excluded middle fails for intermediate degrees.
module Circuit.Logics.Goedel
  ( Goedel (..),
    mkGoedel,
    unGoedel,
    godei,
  )
where

import Circuit.Logics.Boolean (Complemented (..))
import Circuit.Logics.Heyting (Heyting (..))
import Circuit.Logics.Lattice
  ( JoinSemiLattice (..),
    LowerBounded (..),
    MeetSemiLattice (..),
    UpperBounded (..),
  )
import Data.Ratio (Rational)

-- | Gödel truth degree, intended in @[0,1]@.
--
-- The constructor is strict about bounds via 'mkGoedel'; the newtype is
-- still exposed for zero-cost unwrapping when the invariant is trusted.
newtype Goedel r = Goedel r
  deriving (Goedel r -> Goedel r -> Bool
(Goedel r -> Goedel r -> Bool)
-> (Goedel r -> Goedel r -> Bool) -> Eq (Goedel r)
forall r. Eq r => Goedel r -> Goedel r -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall r. Eq r => Goedel r -> Goedel r -> Bool
== :: Goedel r -> Goedel r -> Bool
$c/= :: forall r. Eq r => Goedel r -> Goedel r -> Bool
/= :: Goedel r -> Goedel r -> Bool
Eq, Eq (Goedel r)
Eq (Goedel r) =>
(Goedel r -> Goedel r -> Ordering)
-> (Goedel r -> Goedel r -> Bool)
-> (Goedel r -> Goedel r -> Bool)
-> (Goedel r -> Goedel r -> Bool)
-> (Goedel r -> Goedel r -> Bool)
-> (Goedel r -> Goedel r -> Goedel r)
-> (Goedel r -> Goedel r -> Goedel r)
-> Ord (Goedel r)
Goedel r -> Goedel r -> Bool
Goedel r -> Goedel r -> Ordering
Goedel r -> Goedel r -> Goedel r
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall r. Ord r => Eq (Goedel r)
forall r. Ord r => Goedel r -> Goedel r -> Bool
forall r. Ord r => Goedel r -> Goedel r -> Ordering
forall r. Ord r => Goedel r -> Goedel r -> Goedel r
$ccompare :: forall r. Ord r => Goedel r -> Goedel r -> Ordering
compare :: Goedel r -> Goedel r -> Ordering
$c< :: forall r. Ord r => Goedel r -> Goedel r -> Bool
< :: Goedel r -> Goedel r -> Bool
$c<= :: forall r. Ord r => Goedel r -> Goedel r -> Bool
<= :: Goedel r -> Goedel r -> Bool
$c> :: forall r. Ord r => Goedel r -> Goedel r -> Bool
> :: Goedel r -> Goedel r -> Bool
$c>= :: forall r. Ord r => Goedel r -> Goedel r -> Bool
>= :: Goedel r -> Goedel r -> Bool
$cmax :: forall r. Ord r => Goedel r -> Goedel r -> Goedel r
max :: Goedel r -> Goedel r -> Goedel r
$cmin :: forall r. Ord r => Goedel r -> Goedel r -> Goedel r
min :: Goedel r -> Goedel r -> Goedel r
Ord, Int -> Goedel r -> ShowS
[Goedel r] -> ShowS
Goedel r -> String
(Int -> Goedel r -> ShowS)
-> (Goedel r -> String) -> ([Goedel r] -> ShowS) -> Show (Goedel r)
forall r. Show r => Int -> Goedel r -> ShowS
forall r. Show r => [Goedel r] -> ShowS
forall r. Show r => Goedel r -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall r. Show r => Int -> Goedel r -> ShowS
showsPrec :: Int -> Goedel r -> ShowS
$cshow :: forall r. Show r => Goedel r -> String
show :: Goedel r -> String
$cshowList :: forall r. Show r => [Goedel r] -> ShowS
showList :: [Goedel r] -> ShowS
Show, ReadPrec [Goedel r]
ReadPrec (Goedel r)
Int -> ReadS (Goedel r)
ReadS [Goedel r]
(Int -> ReadS (Goedel r))
-> ReadS [Goedel r]
-> ReadPrec (Goedel r)
-> ReadPrec [Goedel r]
-> Read (Goedel r)
forall r. Read r => ReadPrec [Goedel r]
forall r. Read r => ReadPrec (Goedel r)
forall r. Read r => Int -> ReadS (Goedel r)
forall r. Read r => ReadS [Goedel r]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: forall r. Read r => Int -> ReadS (Goedel r)
readsPrec :: Int -> ReadS (Goedel r)
$creadList :: forall r. Read r => ReadS [Goedel r]
readList :: ReadS [Goedel r]
$creadPrec :: forall r. Read r => ReadPrec (Goedel r)
readPrec :: ReadPrec (Goedel r)
$creadListPrec :: forall r. Read r => ReadPrec [Goedel r]
readListPrec :: ReadPrec [Goedel r]
Read)

-- | Clamp to the unit interval and wrap.
mkGoedel :: (Ord r, Num r) => r -> Goedel r
mkGoedel :: forall r. (Ord r, Num r) => r -> Goedel r
mkGoedel r
r = r -> Goedel r
forall r. r -> Goedel r
Goedel (r -> r -> r
forall a. Ord a => a -> a -> a
max r
0 (r -> r -> r
forall a. Ord a => a -> a -> a
min r
1 r
r))

unGoedel :: Goedel r -> r
unGoedel :: forall r. Goedel r -> r
unGoedel (Goedel r
r) = r
r

-- | Alias matching common spelling in the literature.
godei :: Rational -> Goedel Rational
godei :: Rational -> Goedel Rational
godei = Rational -> Goedel Rational
forall r. (Ord r, Num r) => r -> Goedel r
mkGoedel

instance (Ord r) => JoinSemiLattice (Goedel r) where
  Goedel r
a \/ :: Goedel r -> Goedel r -> Goedel r
\/ Goedel r
b = r -> Goedel r
forall r. r -> Goedel r
Goedel (r -> r -> r
forall a. Ord a => a -> a -> a
max r
a r
b)

instance (Ord r) => MeetSemiLattice (Goedel r) where
  Goedel r
a /\ :: Goedel r -> Goedel r -> Goedel r
/\ Goedel r
b = r -> Goedel r
forall r. r -> Goedel r
Goedel (r -> r -> r
forall a. Ord a => a -> a -> a
min r
a r
b)

instance (Ord r, Num r) => LowerBounded (Goedel r) where
  bottom :: Goedel r
bottom = r -> Goedel r
forall r. r -> Goedel r
Goedel r
0

instance (Ord r, Num r) => UpperBounded (Goedel r) where
  top :: Goedel r
top = r -> Goedel r
forall r. r -> Goedel r
Goedel r
1

instance (Ord r, Num r) => Heyting (Goedel r) where
  Goedel r
a ==> :: Goedel r -> Goedel r -> Goedel r
==> Goedel r
b
    | r
a r -> r -> Bool
forall a. Ord a => a -> a -> Bool
<= r
b = r -> Goedel r
forall r. r -> Goedel r
Goedel r
1
    | Bool
otherwise = r -> Goedel r
forall r. r -> Goedel r
Goedel r
b

-- | Gödel negation as @a ==> bottom@ (sharp: only 0 maps to 1).
instance (Ord r, Num r) => Complemented (Goedel r) where
  complement :: Goedel r -> Goedel r
complement Goedel r
a = Goedel r
a Goedel r -> Goedel r -> Goedel r
forall a. Heyting a => a -> a -> a
==> Goedel r
forall a. LowerBounded a => a
bottom