packages feed

rings (empty) → 0.0.1

raw patch · 9 files changed

+854/−0 lines, 9 filesdep +basedep +containersdep +contravariantsetup-changed

Dependencies added: base, containers, contravariant, property, semigroupoids

Files

+ ChangeLog.md view
@@ -0,0 +1,5 @@+# Revision history for dioids++## 0.0.1  -- YYYY-mm-dd++* First version. Released on an unsuspecting world.
+ LICENSE view
@@ -0,0 +1,14 @@+BSD 3-Clause License++Copyright Christopher McKinlay (c) 2019++Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:++1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.++3. Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ rings.cabal view
@@ -0,0 +1,37 @@+name:                rings+version:             0.0.1+synopsis:            basic algebra+description:         Groups, rings, and semirings. +homepage:            https://github.com/cmk/algebras+license:             BSD3+license-file:        LICENSE+author:              Chris McKinlay+maintainer:          chris.mckinlay@gmail.com+category:            Math+build-type:          Simple+extra-source-files:  ChangeLog.md+cabal-version:       >=1.10++library+  exposed-modules:+      Data.Group+      Data.Ring+      Data.Semigroup.Orphan+      Data.Semiring+      Data.Semiring.Property+  default-extensions:+      ScopedTypeVariables+    , TypeApplications+    , MultiParamTypeClasses+    , UndecidableInstances+    , FlexibleInstances++  build-depends:       +      base <5.0+    , containers+    , contravariant+    , property+    , semigroupoids++  hs-source-dirs: src+  default-language: Haskell2010
+ src/Data/Group.hs view
@@ -0,0 +1,20 @@+module Data.Group where++import Prelude hiding (Num(..))++infixl 6 <<++-- |A 'Group' is a 'Monoid' plus a function, 'negate', such that: +--+-- @a << negate a == mempty@+--+-- @negate a << a == mempty@+--+class Monoid a => Group a where+  {-# MINIMAL (negate | (<<)) #-}++  negate :: a -> a+  negate x = mempty << x++  (<<) :: a -> a -> a+  x << y = x <> negate y
+ src/Data/Ring.hs view
@@ -0,0 +1,11 @@+module Data.Ring where++import Data.Group+import Data.Semiring+import Prelude hiding (Num(..))++class (Group a, Semiring a) => Ring a where+  {-# MINIMAL abs, signum #-}+  abs :: a -> a++  signum :: a -> a -- satisfies trichotomy law
+ src/Data/Semigroup/Orphan.hs view
@@ -0,0 +1,37 @@+-- | Orphan instances from base.+module Data.Semigroup.Orphan where++import Control.Applicative+import Data.Complex+import Data.Functor.Alt+import Data.Functor.Plus+import Numeric.Natural (Natural)+++instance Semigroup Word where (<>) = (+)++instance Monoid Word where mempty = 0++instance Semigroup Int where (<>) = (+)++instance Monoid Int where mempty = 0++instance Semigroup Bool where (<>) = (||)++instance Monoid Bool where mempty = False++instance Semigroup Float where (<>) = (+)++instance Monoid Float where mempty = 0++instance Semigroup a => Semigroup (Complex a) where+  (x :+ y) <> (x' :+ y') = (x <> x') :+ (y <> y')++instance Monoid a => Monoid (Complex a) where+  mempty = mempty :+ mempty++instance Semigroup Natural where (<>) = (+)++instance Monoid Natural where mempty = 0++
+ src/Data/Semiring.hs view
@@ -0,0 +1,405 @@+{-# Language ConstrainedClassMethods #-}++{-# Language DeriveFunctor #-}+{-# Language DeriveGeneric #-}++module Data.Semiring where++import Control.Applicative+import Control.Monad+import Data.Foldable hiding (product)+import Data.Functor.Apply+import Data.Functor.Classes+import Data.Functor.Contravariant+import Data.Functor.Contravariant (Predicate(..), Equivalence(..), Op(..))+import Data.Functor.Contravariant.Divisible+import Data.Functor.Identity (Identity(..))+import Data.List (unfoldr)+import Data.List.NonEmpty (NonEmpty(..))+import Data.Semigroup+import Data.Semigroup.Foldable+import Data.Semigroup.Orphan ()+import Data.Typeable (Typeable)+import Foreign.Storable (Storable)+import GHC.Generics (Generic, Generic1)+import GHC.Real (even, quot)+import Numeric.Natural+import Prelude hiding ((^), replicate, sum, product)+import qualified Data.Map as Map+import qualified Data.Sequence as Seq+import qualified Data.Set as Set+import qualified Data.IntMap as IntMap++-- | Right pre-semirings and (non-unital and unital) right semirings.+-- +-- A right pre-semiring (sometimes referred to as a bisemigroup) is a type /R/ endowed +-- with two associative binary (i.e. semigroup) operations: (<>) and (><), along with a +-- right-distributivity property connecting them:+--+-- @(a <> b) >< c = (a >< c) <> (b >< c)@+--+-- A non-unital right semiring (sometimes referred to as a bimonoid) is a pre-semiring +-- with a 'mempty' element that is neutral with respect to both addition and multiplication.+--+-- A unital right semiring is a pre-semiring with two distinct neutral elements, 'mempty' +-- and 'unit', such that 'mempty' is right-neutral wrt addition, 'unit' is right-neutral wrt+--  multiplication, and 'mempty' is right-annihilative wrt multiplication. +--+-- Note that 'unit' needn't be distinct from 'mempty'.+--+-- Instances also need not be commutative nor left-distributive. +--+-- See the properties module for a detailed specification of the laws.+--+class Semigroup r => Semiring r where++  -- Multiplicative operation+  (><) :: r -> r -> r  ++  -- A semiring homomorphism from the Boolean semiring to @r@. +  -- If this map is injective then @r@ has a distinct unit.+  fromBoolean :: Monoid r => Bool -> r+  fromBoolean _ = mempty++unit :: (Monoid r, Semiring r) => r+unit = fromBoolean True++fromBooleanDef :: (Monoid r, Semiring r) => r -> Bool -> r+fromBooleanDef _ False = mempty+fromBooleanDef o True = o+++-- | Fold over a collection using the multiplicative operation of a semiring.+-- +-- @+-- 'product' f ≡ 'Data.foldr'' ((><) . f) 'unit'+-- @+--+-- >>> (foldMap . product) id [[1, 2], [3, (4 :: Int)]] -- 1 >< 2 <> 3 >< 4+-- 14+--+-- >>> (product . foldMap) id [[1, 2], [3, (4 :: Int)]] -- 1 <> 2 >< 3 <> 4+-- 21+--+-- For semirings without a distinct multiplicative unit this is equivalent to @const mempty@:+--+-- >>> product Just [1..(5 :: Int)]+-- Just 0+--+-- In this situation you most likely want to use 'product1'.+--+product :: (Foldable t, Monoid r, Semiring r) => (a -> r) -> t a -> r+product f = foldr' ((><) . f) unit++-- | Fold over a non-empty collection using the multiplicative operation of a semiring.+--+-- As the collection is non-empty this does not require a distinct multiplicative unit:+--+-- >>> product1 Just $ 1 :| [2..(5 :: Int)]+-- Just 120+--+product1 :: (Foldable1 t, Semiring r) => (a -> r) -> t a -> r+product1 f = getProd . foldMap1 (Prod . f)++-- | Cross-multiply two collections.+--+-- >>> cross [1,2,3 ::Int] [1,2,3]+-- 36+--+-- >>> cross [1,2,3 ::Int] []+-- 0+--+cross :: (Foldable t, Applicative t, Monoid r, Semiring r) => t r -> t r -> r+cross a b = fold $ liftA2 (><) a b++-- >>> cross1 (Right 2 :| [Left "oops"]) (Right 2 :| [Right 3]) :: Either [Char] Int+-- Right 4+cross1 :: (Foldable1 t, Apply t, Semiring r) => t r -> t r -> r+cross1 a b = fold1 $ liftF2 (><) a b++-- | Fold with no additive or multiplicative unit.+foldPresemiring :: Semiring r => (a -> r) -> NonEmpty (NonEmpty a) -> r+foldPresemiring = foldMap1 . product1++-- | Fold with no multiplicative unit.+foldNonunital :: (Monoid r, Semiring r) => (a -> r) -> [NonEmpty a] -> r+foldNonunital = foldMap . product1++-- | Fold with additive & multiplicative units.+--+-- This function will zero out if there is no multiplicative unit.+--+foldUnital :: (Monoid r, Semiring r) => (a -> r) -> [[a]] -> r+foldUnital = foldMap . product++-- | A generalization of 'Data.List.replicate' to an arbitrary 'Monoid'. +--+-- Adapted from <http://augustss.blogspot.com/2008/07/lost-and-found-if-i-write-108-in.html>.+--+replicate :: Monoid r => Natural -> r -> r+replicate y0 x0+    | y0 == 0 = mempty+    | otherwise = f x0 y0+    where+        f x y +            | even y = f (x <> x) (y `quot` 2)+            | y == 1 = x+            | otherwise = g (x <> x) ((y - 1) `quot` 2) x+        g x y z +            | even y = g (x <> x) (y `quot` 2) z+            | y == 1 = x <> z+            | otherwise = g (x <> x) ((y - 1) `quot` 2) (x <> z)+{-# INLINE replicate #-}++replicate' :: (Monoid r, Semiring r) => Natural -> r -> r+replicate' n r = getProd $ replicate n (Prod r)++infixr 8 ^++(^) :: (Monoid r, Semiring r) => r -> Natural -> r+(^) = flip replicate'++powers :: (Monoid r, Semiring r) => Natural -> r -> r+powers n a = foldr' (<>) unit . flip unfoldr n $ \m -> +  if m == 0 then Nothing else Just (a^m,m-1)++-------------------------------------------------------------------------------+-- Pre-semirings+-------------------------------------------------------------------------------++-- | 'First a' forms a pre-semiring for any semigroup @a@.+--+-- >>> foldMap1 First $ 1 :| [2..(5 :: Int)] >< 1 :| [2..(5 :: Int)]+-- First {getFirst = 1}+--+-- >>> product1 First $ 1 :| [2..(5 :: Int)]+-- First {getFirst = 15}+--+-- >>> foldMap1 First $ Nothing :| [Just (5 :: Int), Just 6,  Nothing]+-- First {getFirst = Nothing}+--+-- >>> product1 First $ Nothing :| [Just (5 :: Int), Just 6,  Nothing]+-- First {getFirst = Just 11}+--+instance Semigroup a => Semiring (First a) where+  (><) = liftA2 (<>)+  {-# INLINE (><)  #-}++instance Semigroup a => Semiring (Last a) where+  (><) = liftA2 (<>)+  {-# INLINE (><)  #-}++instance Ord a => Semiring (Max a) where+  (><) = min+  {-# INLINE (><)  #-}++instance Ord a => Semiring (Min a) where+  (><) = max+  {-# INLINE (><)  #-}++instance Semigroup a => Semiring (Either e a) where+  (><) = liftA2 (<>)+  {-# INLINE (><) #-}++-- >>> (1 :| [2 :: Int]) >< (3 :| [4 :: Int])+-- 4 :| [5,5,6]+instance Semigroup a => Semiring (NonEmpty a) where+  (><) = liftA2 (<>) +  {-# INLINE (><) #-}++-------------------------------------------------------------------------------+-- Semirings+-------------------------------------------------------------------------------++instance Semiring () where+  (><) _ _ = ()++  fromBoolean _ = ()++instance Semiring Ordering where+  LT >< LT = LT+  LT >< GT = LT+  _  >< EQ = EQ+  EQ >< _  = EQ+  GT >< x  = x++  fromBoolean = fromBooleanDef GT++instance Semiring Bool where+  (><) = (&&)++  fromBoolean = id++instance Semiring Natural where+  (><) = (*)++  fromBoolean = fromBooleanDef 1++instance Semiring Int where+  (><) = (*)++  fromBoolean = fromBooleanDef 1++instance Semiring Word where+  (><) = (*)++  fromBoolean = fromBooleanDef 1++-- >>> (> (0::Int)) >< ((< 10) <> (== 15)) $ 10+-- False+-- >>> (> (0::Int)) >< ((< 10) <> (== 15)) $ 15+-- True+instance (Monoid b, Semiring b) => Semiring (a -> b) where+  (><) = liftA2 (><)+  {-# INLINE (><) #-}++  fromBoolean = const . fromBoolean++instance (Monoid a, Semiring a) => Semiring (Op a b) where+  Op f >< Op g = Op $ \x -> f x >< g x+  {-# INLINE (><) #-}++  fromBoolean = fromBooleanDef $ Op (const unit)++instance (Monoid a, Monoid b, Semiring a, Semiring b) => Semiring (a, b) where+  (a, b) >< (c, d) = (a><c, b><d)+  {-# INLINE (><) #-}++  fromBoolean = liftA2 (,) fromBoolean fromBoolean++instance Monoid a => Semiring [a] where +  (><) = liftA2 (<>)+  {-# INLINE (><) #-}++  fromBoolean = fromBooleanDef $ pure mempty++instance (Monoid a, Semiring a) => Semiring (Maybe a) where +  (><) = liftA2 (><)+  {-# INLINE (><) #-}++  fromBoolean = fromBooleanDef $ pure mempty++instance (Monoid a, Semiring a) => Semiring (Dual a) where+  (><) = liftA2 $ flip (><)+  {-# INLINE (><)  #-}++  fromBoolean = Dual . fromBoolean+  {-# INLINE fromBoolean #-}++instance (Monoid a, Semiring a) => Semiring (Const a b) where+  (Const x) >< (Const y) = Const (x >< y)+  {-# INLINE (><)  #-}++  fromBoolean = Const . fromBoolean+  {-# INLINE fromBoolean #-}++instance (Monoid a, Semiring a) => Semiring (Identity a) where+  (><) = liftA2 (><)+  {-# INLINE (><) #-}++  fromBoolean = fromBooleanDef $ pure mempty++instance Semiring Any where +  Any x >< Any y = Any $ x && y+  {-# INLINE (><) #-}++  fromBoolean = fromBooleanDef $ Any True++instance Semiring All where +  All x >< All y = All $ x || y+  {-# INLINE (><) #-}++  --Note that the truth values are flipped here to create a+  --valid semiring homomorphism. Users should precompose with 'not'+  --where necessary. +  fromBoolean False = All True+  fromBoolean True = All False++instance (Monoid a, Semiring a) => Semiring (IO a) where +  (><) = liftA2 (><)+  {-# INLINE (><) #-}++  fromBoolean = fromBooleanDef $ pure mempty++---------------------------------------------------------------------+--  Instances (contravariant)+---------------------------------------------------------------------++-- Note that due to the underlying 'Monoid' instance this instance+-- has 'All' semiring semantics rather than 'Any'.+instance Semiring (Predicate a) where+  Predicate f >< Predicate g = Predicate $ \x -> f x || g x+  {-# INLINE (><) #-}++  --Note that the truth values are flipped here to create a+  --valid semiring homomorphism. Users should precompose with 'not'+  --where necessary. +  fromBoolean False = Predicate $ const True+  fromBoolean True = Predicate $ const False+++-- Note that due to the underlying 'Monoid' instance this instance+-- has 'All' semiring semantics rather than 'Any'.+instance Semiring (Equivalence a) where+  Equivalence f >< Equivalence g = Equivalence $ \x y -> f x y || g x y+  {-# INLINE (><) #-}++  --Note that the truth values are flipped here to create a+  --valid semiring homomorphism. Users should precompose with 'not'+  --where necessary. +  fromBoolean False = Equivalence $ \_ _ -> True+  fromBoolean True = Equivalence $ \_ _ -> False+++instance Semiring (Comparison a) where+  Comparison f >< Comparison g = Comparison $ \x y -> f x y >< g x y+  {-# INLINE (><) #-}++  fromBoolean = fromBooleanDef $ Comparison $ \_ _ -> GT++---------------------------------------------------------------------+--  Instances (containers)+---------------------------------------------------------------------++instance Ord a => Semiring (Set.Set a) where+  (><) = Set.intersection++instance Monoid a => Semiring (Seq.Seq a) where+  (><) = liftA2 (<>)+  {-# INLINE (><) #-}++  fromBoolean = fromBooleanDef $ Seq.singleton mempty++instance (Ord k, Monoid k, Monoid a) => Semiring (Map.Map k a) where+  xs >< ys = foldMap (flip Map.map xs . (<>)) ys+  {-# INLINE (><) #-}++  fromBoolean = fromBooleanDef $ Map.singleton mempty mempty++instance Monoid a => Semiring (IntMap.IntMap a) where+  xs >< ys = foldMap (flip IntMap.map xs . (<>)) ys+  {-# INLINE (><) #-}++  fromBoolean = fromBooleanDef $ IntMap.singleton 0 mempty++---------------------------------------------------------------------+-- Newtype wrappers+---------------------------------------------------------------------++-- | Monoid under '><'. Analogous to 'Data.Monoid.Product', but uses the+-- 'Semiring' constraint, rather than 'Num'.+newtype Prod a = Prod { getProd :: a }+  deriving (Eq,Ord,Show,Bounded,Generic,Generic1,Typeable,Functor)++instance Applicative Prod where+  pure = Prod+  Prod f <*> Prod a = Prod (f a)++instance Semiring a => Semigroup (Prod a) where+  (<>) = liftA2 (><)+  {-# INLINE (<>) #-}++-- Note that 'unit' must be distinct from 'mempty' for this instance to be legal.+instance (Monoid a, Semiring a) => Monoid (Prod a) where+  mempty = Prod unit+  {-# INLINE mempty #-}
+ src/Data/Semiring/Property.hs view
@@ -0,0 +1,323 @@+{-# Language AllowAmbiguousTypes #-}++module Data.Semiring.Property (+  -- * Properties of pre-semirings & semirings+    neutral_addition_on+  , neutral_addition_on'+  , neutral_multiplication_on+  , neutral_multiplication_on'+  , associative_addition_on +  , associative_multiplication_on +  , distributive_on +  -- * Properties of non-unital (near-)semirings+  , nonunital_on+  -- * Properties of unital semirings+  , annihilative_multiplication_on +  , homomorphism_boolean+  -- * Properties of cancellative semirings +  , cancellative_addition_on +  , cancellative_multiplication_on +  -- * Properties of commutative semirings +  , commutative_addition_on +  , commutative_multiplication_on+  -- * Properties of distributive semirings +  , distributive_finite_on+  , distributive_finite1_on +  , distributive_cross_on+  , distributive_cross1_on +{-+  -- * Properties of closed semirings+  , closed_pstable+  , closed_paffine +  , closed_stable +  , closed_affine +  , idempotent_star+-}+) where++import Data.List.NonEmpty (NonEmpty(..))+import Data.Foldable+import Data.Semiring+import Data.Semigroup.Foldable+import Test.Property.Util+import qualified Test.Property as Prop++------------------------------------------------------------------------------------+-- Properties of pre-semirings & semirings++-- | \( \forall a \in R: (z + a) \sim a \)+--+-- A (pre-)semiring with a right-neutral additive unit must satisfy:+--+-- @+-- 'neutral_addition' 'mempty' ~~ const True+-- @+-- +-- Or, equivalently:+--+-- @+-- 'mempty' '<>' r ~~ r+-- @+--+-- This is a required property.+--+neutral_addition_on :: Semigroup r => Rel r -> r -> r -> Bool+neutral_addition_on (~~) = Prop.neutral_on (~~) (<>)++neutral_addition_on' :: Monoid r => Rel r -> r -> Bool+neutral_addition_on' (~~) = Prop.neutral_on (~~) (<>) mempty++-- | \( \forall a \in R: (o * a) \sim a \)+--+-- A (pre-)semiring with a right-neutral multiplicative unit must satisfy:+--+-- @+-- 'neutral_multiplication' 'unit' ~~ const True+-- @+-- +-- Or, equivalently:+--+-- @+-- 'unit' '><' r ~~ r+-- @+--+-- This is a required property.+--+neutral_multiplication_on :: Semiring r => Rel r -> r -> r -> Bool+neutral_multiplication_on (~~) = Prop.neutral_on (~~) (><) ++neutral_multiplication_on' :: (Monoid r, Semiring r) => Rel r -> r -> Bool+neutral_multiplication_on' (~~) = Prop.neutral_on (~~) (><) unit++-- | \( \forall a, b, c \in R: (a + b) + c \sim a + (b + c) \)+--+-- /R/ must right-associate addition.+--+-- This should be verified by the underlying 'Semigroup' instance,+-- but is included here for completeness.+--+-- This is a required property.+--+associative_addition_on :: Semigroup r => Rel r -> r -> r -> r -> Bool+associative_addition_on (~~) = Prop.associative_on (~~) (<>)++-- | \( \forall a, b, c \in R: (a * b) * c \sim a * (b * c) \)+--+-- /R/ must right-associate multiplication.+--+-- This is a required property.+--+associative_multiplication_on :: Semiring r => Rel r -> r -> r -> r -> Bool+associative_multiplication_on (~~) = Prop.associative_on (~~) (><)++-- | \( \forall a, b, c \in R: (a + b) * c \sim (a * c) + (b * c) \)+--+-- /R/ must right-distribute multiplication.+--+-- When /R/ is a functor and the semiring structure is derived from 'Alternative', +-- this translates to: +--+-- @+-- (a '<|>' b) '*>' c = (a '*>' c) '<|>' (b '*>' c)+-- @  +--+-- See < https://en.wikibooks.org/wiki/Haskell/Alternative_and_MonadPlus >.+--+-- This is a required property.+--+distributive_on :: Semiring r => Rel r -> r -> r -> r -> Bool+distributive_on (~~) = Prop.distributive_on (~~) (<>) (><)++------------------------------------------------------------------------------------+-- Properties of non-unital semirings (aka near-semirings)++-- | \( \forall a, b \in R: a * b \sim a * b + b \)+--+-- If /R/ is non-unital (i.e. /unit/ is not distinct from /mempty/) then it will instead satisfy +-- a right-absorbtion property. +--+-- This follows from right-neutrality and right-distributivity.+--+-- Compare 'codistributive' and 'closed_stable'.+--+-- When /R/ is also left-distributive we get: \( \forall a, b \in R: a * b = a + a * b + b \)+--+-- See also 'Data.Warning' and < https://blogs.ncl.ac.uk/andreymokhov/united-monoids/#whatif >.+--+nonunital_on :: (Monoid r, Semiring r) => Rel r -> r -> r -> Bool+nonunital_on (~~) a b = (a >< b) ~~ (a >< b <> b)+++------------------------------------------------------------------------------------+-- Properties of unital semirings++-- | \( \forall a \in R: (z * a) \sim u \)+--+-- A /R/ is unital then its addititive unit must be right-annihilative, i.e.:+--+-- @+-- 'mempty' '><' a ~~ 'mempty'+-- @+--+-- For 'Alternative' instances this property translates to:+--+-- @+-- 'empty' '*>' a ~~ 'empty'+-- @+--+-- All right semirings must have a right-absorbative addititive unit,+-- however note that depending on the 'Prd' instance this does not preclude +-- IEEE754-mandated behavior such as: +--+-- @+-- 'mempty' '><' NaN ~~ NaN+-- @+--+-- This is a required property.+--+annihilative_multiplication_on :: (Monoid r, Semiring r) => Rel r -> r -> Bool+annihilative_multiplication_on (~~) r = Prop.annihilative_on (~~) (><) mempty r++-- | 'fromBoolean' must be a semiring homomorphism into /R/.+--+-- This is a required property.+--+homomorphism_boolean :: forall r. (Eq r, Monoid r, Semiring r) => Bool -> Bool -> Bool+homomorphism_boolean i j =+  fromBoolean True     == (unit @r)  &&+  fromBoolean False    == (mempty @r) &&+  fromBoolean (i && j) == fi >< fj    && +  fromBoolean (i || j) == fi <> fj ++  where fi :: r = fromBoolean i+        fj :: r = fromBoolean j++------------------------------------------------------------------------------------+-- Properties of cancellative & commutative semirings+++-- | \( \forall a, b, c \in R: b + a \sim c + a \Rightarrow b = c \)+--+-- If /R/ is right-cancellative wrt addition then for all /a/+-- the section /(a <>)/ is injective.+--+cancellative_addition_on :: Semigroup r => Rel r -> r -> r -> r -> Bool+cancellative_addition_on (~~) a = Prop.injective_on (~~) (<> a)+++-- | \( \forall a, b, c \in R: b * a \sim c * a \Rightarrow b = c \)+--+-- If /R/ is right-cancellative wrt multiplication then for all /a/+-- the section /(a ><)/ is injective.+--+cancellative_multiplication_on :: Semiring r => Rel r -> r -> r -> r -> Bool+cancellative_multiplication_on (~~) a = Prop.injective_on (~~) (>< a)+++-- | \( \forall a, b \in R: a + b \sim b + a \)+--+commutative_addition_on :: Semigroup r => Rel r -> r -> r -> Bool+commutative_addition_on (~~) = Prop.commutative_on (~~) (<>)+++-- | \( \forall a, b \in R: a * b \sim b * a \)+--+commutative_multiplication_on :: Semiring r => Rel r -> r -> r -> Bool+commutative_multiplication_on (~~) = Prop.commutative_on (~~) (><)++------------------------------------------------------------------------------------+-- Properties of distributive & co-distributive semirings++-- | \( \forall M \geq 0; a_1 \dots a_M, b \in R: (\sum_{i=1}^M a_i) * b \sim \sum_{i=1}^M a_i * b \)+--+-- /R/ must right-distribute multiplication between finite sums.+--+-- For types with exact arithmetic this follows from 'distributive' & 'neutral_multiplication'.+--+distributive_finite_on :: (Monoid r, Semiring r) => Rel r -> [r] -> r -> Bool+distributive_finite_on (~~) as b = fold as >< b ~~ foldMap (>< b) as++-- | \( \forall M \geq 1; a_1 \dots a_M, b \in R: (\sum_{i=1}^M a_i) * b \sim \sum_{i=1}^M a_i * b \)+--+-- /R/ must right-distribute multiplication over finite (non-empty) sums.+--+-- For types with exact arithmetic this follows from 'distributive' and the universality of 'fold1'.+--+distributive_finite1_on :: (Semiring r) => Rel r -> NonEmpty r -> r -> Bool+distributive_finite1_on (~~) as b = fold1 as >< b ~~ foldMap1 (>< b) as++-- | \( \forall M,N \geq 0; a_1 \dots a_M, b_1 \dots b_N \in R: (\sum_{i=1}^M a_i) * (\sum_{j=1}^N b_j) \sim \sum_{i=1 j=1}^{i=M j=N} a_i * b_j \)+--+-- If /R/ is also left-distributive then it supports cross-multiplication.+--+distributive_cross_on :: (Monoid r, Semiring r) => Rel r -> [r] -> [r] -> Bool+distributive_cross_on (~~) as bs = fold as >< fold bs ~~ cross as bs+++-- | \( \forall M,N \geq 1; a_1 \dots a_M, b_1 \dots b_N \in R: (\sum_{i=1}^M a_i) * (\sum_{j=1}^N b_j) = \sum_{i=1 j=1}^{i=M j=N} a_i * b_j \)+--+-- If /R/ is also left-distributive then it supports (non-empty) cross-multiplication.+--+distributive_cross1_on :: Semiring r => Rel r -> NonEmpty r -> NonEmpty r -> Bool+distributive_cross1_on (~~) as bs = fold1 as >< fold1 bs ~~ cross1 as bs++------------------------------------------------------------------------------------+-- Properties of closed semirings++{-+-- | \( 1 + \sum_{i=1}^{P+1} a^i = 1 + \sum_{i=1}^{P} a^i \)+--+-- If /a/ is p-stable for some /p/, then we have:+--+-- @+-- 'powers' p a ~~ a '><' 'powers' p a '<>' 'unit'  ~~ 'powers' p a '><' a '<>' 'unit' +-- @+--+-- If '<>' and '><' are idempotent then every element is 1-stable:+--+-- @ a '><' a '<>' a '<>' 'unit' = a '<>' a '<>' 'unit' = a '<>' 'unit' @+--+closed_pstable :: (Eq r, Prd r, Monoid r, Semiring r) => Natural -> r -> Bool+closed_pstable p a = powers p a ~~ powers (p <> unit) a++-- | \( x = a * x + b \Rightarrow x = (1 + \sum_{i=1}^{P} a^i) * b \)+--+-- If /a/ is p-stable for some /p/, then we have:+--+closed_paffine :: (Prd r, Monoid r, Semiring r) => Natural -> r -> r -> Bool+closed_paffine p a b = closed_pstable p a ==> x ~~ a >< x <> b +  where x = powers p a >< b++-- | \( \forall a \in R : a^* = a^* * a + 1 \)+--+-- Closure is /p/-stability for all /a/ in the limit as \( p \to \infinity \).+--+-- One way to think of this property is that all geometric series+-- "converge":+--+-- \( \forall a \in R : 1 + \sum_{i \geq 1} a^i \in R \)+--+closed_stable :: (Prd r, Monoid r, Closed r) => r -> Bool+closed_stable a = star a ~~ star a >< a <> unit++closed_stable' :: (Prd r, Monoid r, Closed r) => r -> Bool+closed_stable' a = star a ~~ unit <> a >< star a++closed_affine :: (Prd r, Monoid r, Closed r) => r -> r -> Bool+closed_affine a b = x ~~ a >< x <> b where x = star a >< b++-- If /R/ is closed then 'star' must be idempotent:+--+-- @'star' ('star' a) ~~ 'star' a@+--+idempotent_star :: (Prd r, Monoid r, Closed r) => r -> Bool+idempotent_star = Prop.idempotent star++-- If @r@ is a closed dioid then 'star' must be monotone:+--+-- @x '<~' y ==> 'star' x '<~' 'star' y@+--+monotone_star :: (Prd r, Monoid r, Closed r) => r -> r -> Bool+monotone_star = Prop.monotone_on (<~) star++-}