module Ersatz.Relation.Prop ( implies , symmetric , anti_symmetric , transitive , irreflexive , reflexive , regular , regular_in_degree , regular_out_degree , max_in_degree , min_in_degree , max_out_degree , min_out_degree , empty , complete , total , disjoint , equals ) where import Prelude hiding ( and, or, not, product ) import Ersatz.Bit import Ersatz.Relation.Data import Ersatz.Relation.Op import Ersatz.Counting import Data.Ix implies :: ( Ix a, Ix b ) => Relation a b -> Relation a b -> Bit implies :: Relation a b -> Relation a b -> Bit implies Relation a b r Relation a b s = [Bit] -> Bit forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b and ([Bit] -> Bit) -> [Bit] -> Bit forall a b. (a -> b) -> a -> b $ do (a, b) i <- Relation a b -> [(a, b)] forall a b. (Ix a, Ix b) => Relation a b -> [(a, b)] indices Relation a b r Bit -> [Bit] forall (m :: * -> *) a. Monad m => a -> m a return (Bit -> [Bit]) -> Bit -> [Bit] forall a b. (a -> b) -> a -> b $ [Bit] -> Bit forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b or [ Bit -> Bit forall b. Boolean b => b -> b not (Bit -> Bit) -> Bit -> Bit forall a b. (a -> b) -> a -> b $ Relation a b r Relation a b -> (a, b) -> Bit forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit ! (a, b) i, Relation a b s Relation a b -> (a, b) -> Bit forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit ! (a, b) i ] empty :: ( Ix a, Ix b ) => Relation a b -> Bit empty :: Relation a b -> Bit empty Relation a b r = [Bit] -> Bit forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b and ([Bit] -> Bit) -> [Bit] -> Bit forall a b. (a -> b) -> a -> b $ do (a, b) i <- Relation a b -> [(a, b)] forall a b. (Ix a, Ix b) => Relation a b -> [(a, b)] indices Relation a b r Bit -> [Bit] forall (m :: * -> *) a. Monad m => a -> m a return (Bit -> [Bit]) -> Bit -> [Bit] forall a b. (a -> b) -> a -> b $ Bit -> Bit forall b. Boolean b => b -> b not (Bit -> Bit) -> Bit -> Bit forall a b. (a -> b) -> a -> b $ Relation a b r Relation a b -> (a, b) -> Bit forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit ! (a, b) i complete :: (Ix a, Ix b) => Relation a b -> Bit complete :: Relation a b -> Bit complete Relation a b r = Relation a b -> Bit forall a b. (Ix a, Ix b) => Relation a b -> Bit empty (Relation a b -> Bit) -> Relation a b -> Bit forall a b. (a -> b) -> a -> b $ Relation a b -> Relation a b forall a b. (Ix a, Ix b) => Relation a b -> Relation a b complement Relation a b r total :: ( Ix a) => Relation a a -> Bit total :: Relation a a -> Bit total Relation a a r = Relation a a -> Bit forall a b. (Ix a, Ix b) => Relation a b -> Bit complete (Relation a a -> Bit) -> Relation a a -> Bit forall a b. (a -> b) -> a -> b $ Relation a a -> Relation a a forall a. Ix a => Relation a a -> Relation a a symmetric_closure Relation a a r disjoint :: (Ix a, Ix b) => Relation a b -> Relation a b -> Bit disjoint :: Relation a b -> Relation a b -> Bit disjoint Relation a b r Relation a b s = Relation a b -> Bit forall a b. (Ix a, Ix b) => Relation a b -> Bit empty (Relation a b -> Bit) -> Relation a b -> Bit forall a b. (a -> b) -> a -> b $ Relation a b -> Relation a b -> Relation a b forall a b. (Ix a, Ix b) => Relation a b -> Relation a b -> Relation a b intersection Relation a b r Relation a b s equals :: (Ix a, Ix b) => Relation a b -> Relation a b -> Bit equals :: Relation a b -> Relation a b -> Bit equals Relation a b r Relation a b s = [Bit] -> Bit forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b and [Relation a b -> Relation a b -> Bit forall a b. (Ix a, Ix b) => Relation a b -> Relation a b -> Bit implies Relation a b r Relation a b s, Relation a b -> Relation a b -> Bit forall a b. (Ix a, Ix b) => Relation a b -> Relation a b -> Bit implies Relation a b s Relation a b r] symmetric :: ( Ix a) => Relation a a -> Bit symmetric :: Relation a a -> Bit symmetric Relation a a r = Relation a a -> Relation a a -> Bit forall a b. (Ix a, Ix b) => Relation a b -> Relation a b -> Bit implies Relation a a r ( Relation a a -> Relation a a forall a b. (Ix a, Ix b) => Relation a b -> Relation b a mirror Relation a a r ) anti_symmetric :: ( Ix a) => Relation a a -> Bit anti_symmetric :: Relation a a -> Bit anti_symmetric Relation a a r = Relation a a -> Relation a a -> Bit forall a b. (Ix a, Ix b) => Relation a b -> Relation a b -> Bit implies (Relation a a -> Relation a a -> Relation a a forall a b. (Ix a, Ix b) => Relation a b -> Relation a b -> Relation a b intersection Relation a a r (Relation a a -> Relation a a forall a b. (Ix a, Ix b) => Relation a b -> Relation b a mirror Relation a a r)) (((a, a), (a, a)) -> Relation a a forall a. Ix a => ((a, a), (a, a)) -> Relation a a identity (Relation a a -> ((a, a), (a, a)) forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b)) bounds Relation a a r)) irreflexive :: ( Ix a ) => Relation a a -> Bit irreflexive :: Relation a a -> Bit irreflexive Relation a a r = [Bit] -> Bit forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b and ([Bit] -> Bit) -> [Bit] -> Bit forall a b. (a -> b) -> a -> b $ do let ((a a,a _),(a c,a _)) = Relation a a -> ((a, a), (a, a)) forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b)) bounds Relation a a r a x <- (a, a) -> [a] forall a. Ix a => (a, a) -> [a] range (a a, a c) Bit -> [Bit] forall (m :: * -> *) a. Monad m => a -> m a return (Bit -> [Bit]) -> Bit -> [Bit] forall a b. (a -> b) -> a -> b $ Bit -> Bit forall b. Boolean b => b -> b not (Bit -> Bit) -> Bit -> Bit forall a b. (a -> b) -> a -> b $ Relation a a r Relation a a -> (a, a) -> Bit forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit ! (a x,a x) reflexive :: ( Ix a ) => Relation a a -> Bit reflexive :: Relation a a -> Bit reflexive Relation a a r = [Bit] -> Bit forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b and ([Bit] -> Bit) -> [Bit] -> Bit forall a b. (a -> b) -> a -> b $ do let ((a a,a _),(a c,a _)) = Relation a a -> ((a, a), (a, a)) forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b)) bounds Relation a a r a x <- (a, a) -> [a] forall a. Ix a => (a, a) -> [a] range (a a,a c) Bit -> [Bit] forall (m :: * -> *) a. Monad m => a -> m a return (Bit -> [Bit]) -> Bit -> [Bit] forall a b. (a -> b) -> a -> b $ Relation a a r Relation a a -> (a, a) -> Bit forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit ! (a x,a x) regular, regular_in_degree, regular_out_degree, max_in_degree, min_in_degree, max_out_degree, min_out_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit regular :: Int -> Relation a b -> Bit regular Int deg Relation a b r = [Bit] -> Bit forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b and [ Int -> Relation a b -> Bit forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit regular_in_degree Int deg Relation a b r, Int -> Relation a b -> Bit forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit regular_out_degree Int deg Relation a b r ] regular_out_degree :: Int -> Relation a b -> Bit regular_out_degree = (Int -> [Bit] -> Bit) -> Int -> Relation a b -> Bit forall b b1 a t. (Boolean b, Ix b1, Ix a) => (t -> [Bit] -> b) -> t -> Relation a b1 -> b out_degree_helper Int -> [Bit] -> Bit exactly max_out_degree :: Int -> Relation a b -> Bit max_out_degree = (Int -> [Bit] -> Bit) -> Int -> Relation a b -> Bit forall b b1 a t. (Boolean b, Ix b1, Ix a) => (t -> [Bit] -> b) -> t -> Relation a b1 -> b out_degree_helper Int -> [Bit] -> Bit atmost min_out_degree :: Int -> Relation a b -> Bit min_out_degree = (Int -> [Bit] -> Bit) -> Int -> Relation a b -> Bit forall b b1 a t. (Boolean b, Ix b1, Ix a) => (t -> [Bit] -> b) -> t -> Relation a b1 -> b out_degree_helper Int -> [Bit] -> Bit atleast regular_in_degree :: Int -> Relation a b -> Bit regular_in_degree Int deg Relation a b r = Int -> Relation b a -> Bit forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit regular_out_degree Int deg (Relation b a -> Bit) -> Relation b a -> Bit forall a b. (a -> b) -> a -> b $ Relation a b -> Relation b a forall a b. (Ix a, Ix b) => Relation a b -> Relation b a mirror Relation a b r max_in_degree :: Int -> Relation a b -> Bit max_in_degree Int deg Relation a b r = Int -> Relation b a -> Bit forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit max_out_degree Int deg (Relation b a -> Bit) -> Relation b a -> Bit forall a b. (a -> b) -> a -> b $ Relation a b -> Relation b a forall a b. (Ix a, Ix b) => Relation a b -> Relation b a mirror Relation a b r min_in_degree :: Int -> Relation a b -> Bit min_in_degree Int deg Relation a b r = Int -> Relation b a -> Bit forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit min_out_degree Int deg (Relation b a -> Bit) -> Relation b a -> Bit forall a b. (a -> b) -> a -> b $ Relation a b -> Relation b a forall a b. (Ix a, Ix b) => Relation a b -> Relation b a mirror Relation a b r out_degree_helper :: (Boolean b, Ix b1, Ix a) => (t -> [Bit] -> b) -> t -> Relation a b1 -> b out_degree_helper :: (t -> [Bit] -> b) -> t -> Relation a b1 -> b out_degree_helper t -> [Bit] -> b f t deg Relation a b1 r = [b] -> b forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b and ([b] -> b) -> [b] -> b forall a b. (a -> b) -> a -> b $ do let ((a a,b1 b),(a c,b1 d)) = Relation a b1 -> ((a, b1), (a, b1)) forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b)) bounds Relation a b1 r a x <- (a, a) -> [a] forall a. Ix a => (a, a) -> [a] range ( a a , a c ) b -> [b] forall (m :: * -> *) a. Monad m => a -> m a return (b -> [b]) -> b -> [b] forall a b. (a -> b) -> a -> b $ t -> [Bit] -> b f t deg ([Bit] -> b) -> [Bit] -> b forall a b. (a -> b) -> a -> b $ do b1 y <- (b1, b1) -> [b1] forall a. Ix a => (a, a) -> [a] range (b1 b,b1 d) Bit -> [Bit] forall (m :: * -> *) a. Monad m => a -> m a return (Bit -> [Bit]) -> Bit -> [Bit] forall a b. (a -> b) -> a -> b $ Relation a b1 r Relation a b1 -> (a, b1) -> Bit forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit ! (a x,b1 y) transitive :: ( Ix a ) => Relation a a -> Bit transitive :: Relation a a -> Bit transitive Relation a a r = Relation a a -> Relation a a -> Bit forall a b. (Ix a, Ix b) => Relation a b -> Relation a b -> Bit implies (Relation a a -> Relation a a -> Relation a a forall a b c. (Ix a, Ix b, Ix c) => Relation a b -> Relation b c -> Relation a c product Relation a a r Relation a a r) Relation a a r