module Data.Semigroup.Quantale where import Data.Connection hiding (floor', ceiling') import Data.Float import Data.Group import Data.Prd import Data.Prd.Lattice import Data.Word import Data.Semigroup.Orphan () import Prelude hiding (negate, until) import Test.Property.Util ((<==>),(==>)) import qualified Prelude as Pr residuated :: Quantale a => a -> a -> a -> Bool residuated x y z = x <> y <~ z <==> y <~ x \\ z <==> x <~ z // y {- In the interest of usability we abuse terminology slightly and use 'quantale' to describe any residuated, partially ordered semigroup. This admits instances of hoops and triangular (co)-norms. There are several additional properties that apply when the poset structure is lattice-ordered (i.e. a residuated lattice) or when the semigroup is a monoid or semiring. See the associated 'Properties' module. distributive_cross as bs = maybe True (~~ cross as bs) $ pjoin as <> pjoin bs where cross = join (liftA2 (<>) a b) --lattice version distributive_cross' as bs = cross as bs ~~ join as <> join bs where cross = join (liftA2 (<>) a b) join as \\ b ~~ meet (fmap (\\b) as) a \\ meet bs ~~ meet (fmap (a\\) bs) ideal_residuated :: (Quantale a, Ideal a, Functor (Rep a)) => a -> a -> Bool ideal_residuated x y = x \\ y =~ join (fmap (x<>) (connl ideal $ y)) ideal_residuated' :: (Quantale a, Ideal a, Functor (Rep a)) => a -> a -> Bool ideal_residuated' x y = x // y =~ join (fmap (<>x) (connl ideal $ y)) x \/ y = (x // y) <> y -- unit (minus_plus x) y -- (y // x) + x x /\ y = x <> (x \\ y) -- (y + x) // x -- x \\ (x + y) minimal \\ x =~ maximal =~ x \\ maximal mempty \\ x ~~ unit -} class (Semigroup a, Prd a) => Quantale a where residr :: a -> Conn a a residr x = Conn (x<>) (x\\) residl :: a -> Conn a a residl x = Conn (<>x) (//x) (\\) :: a -> a -> a x \\ y = connr (residr x) y (//) :: a -> a -> a x // y = connl (residl x) y instance Quantale Float where x \\ y = y // x --x <> y <~ z iff y <~ x \\ z iff x <~ z // y. y // x | y =~ x = 0 | otherwise = let z = y - x in if z + x <~ y then upper z (x<>) y else lower' z (x<>) y -- @'lower'' x@ is the least element /y/ in the descending -- chain such that @not $ f y '<~' x@. -- lower' z f x = until (\y -> f y <~ x) ge (shift $ -1) z -- @'upper' y@ is the greatest element /x/ in the ascending -- chain such that @g x '<~' y@. -- upper z g y = while (\x -> g x <~ y) le (shift 1) z