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 :: forall a b. (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
implies Relation a b
r Relation a b
s = forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
and forall a b. (a -> b) -> a -> b
$ do
(a, b)
i <- forall a b. (Ix a, Ix b) => Relation a b -> [(a, b)]
indices Relation a b
r
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
or [ forall b. Boolean b => b -> b
not forall a b. (a -> b) -> a -> b
$ Relation a b
r forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
! (a, b)
i, Relation a b
s 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 :: forall a b. (Ix a, Ix b) => Relation a b -> Bit
empty Relation a b
r = forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
and forall a b. (a -> b) -> a -> b
$ do
(a, b)
i <- forall a b. (Ix a, Ix b) => Relation a b -> [(a, b)]
indices Relation a b
r
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall b. Boolean b => b -> b
not forall a b. (a -> b) -> a -> b
$ Relation a b
r 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 :: forall a b. (Ix a, Ix b) => Relation a b -> Bit
complete Relation a b
r = forall a b. (Ix a, Ix b) => Relation a b -> Bit
empty forall a b. (a -> b) -> 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 :: forall a. Ix a => Relation a a -> Bit
total Relation a a
r = forall a b. (Ix a, Ix b) => Relation a b -> Bit
complete forall a b. (a -> b) -> a -> b
$ 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 :: forall a b. (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
disjoint Relation a b
r Relation a b
s = forall a b. (Ix a, Ix b) => Relation a b -> Bit
empty forall a b. (a -> b) -> 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 :: forall a b. (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
equals Relation a b
r Relation a b
s = forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
and [forall a b. (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
implies Relation a b
r Relation a b
s, 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 :: forall a. Ix a => Relation a a -> Bit
symmetric Relation a a
r = forall a b. (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
implies Relation a a
r ( 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 :: forall a. Ix a => Relation a a -> Bit
anti_symmetric Relation a a
r = forall a b. (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
implies (forall a b.
(Ix a, Ix b) =>
Relation a b -> Relation a b -> Relation a b
intersection Relation a a
r (forall a b. (Ix a, Ix b) => Relation a b -> Relation b a
mirror Relation a a
r)) (forall a. Ix a => ((a, a), (a, a)) -> Relation a a
identity (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 :: forall a. Ix a => Relation a a -> Bit
irreflexive Relation a a
r = forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
and forall a b. (a -> b) -> a -> b
$ do
let ((a
a,a
_),(a
c,a
_)) = forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a a
r
a
x <- forall a. Ix a => (a, a) -> [a]
range (a
a, a
c)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall b. Boolean b => b -> b
not forall a b. (a -> b) -> a -> b
$ Relation a a
r 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 :: forall a. Ix a => Relation a a -> Bit
reflexive Relation a a
r = forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
and forall a b. (a -> b) -> a -> b
$ do
let ((a
a,a
_),(a
c,a
_)) = forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a a
r
a
x <- forall a. Ix a => (a, a) -> [a]
range (a
a,a
c)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Relation a a
r forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
! (a
x,a
x)
regular :: (Ix a, Ix b) => Int -> Relation a b -> Bit
regular_in_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit
regular_out_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit
max_in_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit
min_in_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit
max_out_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit
min_out_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit
regular :: forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit
regular Int
deg Relation a b
r = forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
and [ forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit
regular_in_degree Int
deg Relation a b
r, forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit
regular_out_degree Int
deg Relation a b
r ]
regular_out_degree :: forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit
regular_out_degree = 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 :: forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit
max_out_degree = 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 :: forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit
min_out_degree = 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 :: forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit
regular_in_degree Int
deg Relation a b
r = forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit
regular_out_degree Int
deg forall a b. (a -> b) -> a -> b
$ forall a b. (Ix a, Ix b) => Relation a b -> Relation b a
mirror Relation a b
r
max_in_degree :: forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit
max_in_degree Int
deg Relation a b
r = forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit
max_out_degree Int
deg forall a b. (a -> b) -> a -> b
$ forall a b. (Ix a, Ix b) => Relation a b -> Relation b a
mirror Relation a b
r
min_in_degree :: forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit
min_in_degree Int
deg Relation a b
r = forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit
min_out_degree Int
deg forall a b. (a -> b) -> a -> b
$ 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 :: forall b b1 a t.
(Boolean b, Ix b1, Ix a) =>
(t -> [Bit] -> b) -> t -> Relation a b1 -> b
out_degree_helper t -> [Bit] -> b
f t
deg Relation a b1
r = forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
and forall a b. (a -> b) -> a -> b
$ do
let ((a
a,b1
b),(a
c,b1
d)) = forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a b1
r
a
x <- forall a. Ix a => (a, a) -> [a]
range ( a
a , a
c )
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ t -> [Bit] -> b
f t
deg forall a b. (a -> b) -> a -> b
$ do
b1
y <- forall a. Ix a => (a, a) -> [a]
range (b1
b,b1
d)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Relation a b1
r 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 :: forall a. Ix a => Relation a a -> Bit
transitive Relation a a
r = forall a b. (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
implies (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