module Ersatz.Relation.Prop

( 
-- * Properties
  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

-- | Tests if the first relation \(R\) is a subset of the second relation \(S\), 
-- i.e., every element that is contained in \(R\) is also contained in \(S\).
--
-- Note that if \( R \subseteq A \times B \) and \( S \subseteq C \times D \),
-- then \( A \times B \) must be a subset of \( C \times D \).
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 ]

-- | Tests if a relation is empty, i.e., the relation doesn't contain any elements.
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

-- | Tests if a relation \( R \subseteq A \times B \) is complete,
-- i.e., \(R = A \times B \).
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

-- | Tests if a relation \( R \subseteq A \times A \) is strongly connected, i.e.,
-- \( \forall x, y \in A: ((x,y) \in R) \lor ((y,x) \in 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

-- | Tests if two relations are disjoint, i.e., 
-- there is no element that is contained in both relations.
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

-- | Tests if two relations \( R, S \subseteq A \times B \) are equal, 
-- i.e., they contain the same elements.
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]

-- | Tests if a relation \( R \subseteq A \times A \) is symmetric,
-- i.e., \( \forall x, y \in A: ((x,y) \in R) \rightarrow ((y,x) \in 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 )


-- | Tests if a relation \( R \subseteq A \times A \) is antisymmetric,
-- i.e., \( \forall x, y \in A: ((x,y) \in R) \land ((y,x) \in R)) \rightarrow (x = y) \).
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))

-- | Tests if a relation \( R \subseteq A \times A \) is irreflexive, i.e.,
-- \( \forall x \in A: (x,x) \notin 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)

-- | Tests if a relation \( R \subseteq A \times A \) is reflexive, i.e.,
-- \( \forall x \in A: (x,x) \in R \).
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)

-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if
-- \( \forall x \in A: | \{ (x,y) \in R \} | = n \) and
-- \( \forall y \in B: | \{ (x,y) \in R \} | = n \) hold.
regular :: (Ix a, Ix b) => Int -> Relation a b -> Bit

-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if
-- \( \forall y \in B: | \{ (x,y) \in R \} | = n \) holds.
regular_in_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit

-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if
-- \( \forall x \in A: | \{ (x,y) \in R \} | = n \) holds.
regular_out_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit

-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if
-- \( \forall y \in B: | \{ (x,y) \in R \} | \leq n \) holds.
max_in_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit

-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if
-- \( \forall y \in B: | \{ (x,y) \in R \} | \geq n \) holds.
min_in_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit

-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if
-- \( \forall x \in A: | \{ (x,y) \in R \} | \leq n \) holds.
max_out_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit

-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if
-- \( \forall x \in A: | \{ (x,y) \in R \} | \geq n \) holds.
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)

-- | Tests if a relation \( R \subseteq A \times A \) is transitive, i.e.,
-- \( \forall x, y \in A: ((x,y) \in R) \land ((y,z) \in R) \rightarrow ((x,z) \in R) \).
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