{-# OPTIONS_GHC -Wno-orphans #-}
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
)

where

import Prelude hiding ( and, or, not, product )
import Ersatz.Bit
import Ersatz.Relation.Data
import Ersatz.Relation.Op
import Ersatz.Counting
import Ersatz.Equatable

import Data.Ix


instance (Ix a, Ix b) => Equatable (Relation a b) where
  Relation a b
r === :: Relation a b -> Relation a b -> Bit
=== Relation a b
s = [Bit] -> Bit
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
forall (t :: * -> *). Foldable t => t Bit -> Bit
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]
  Relation a b
r /== :: Relation a b -> Relation a b -> Bit
/== Relation a b
s = 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 -> Relation a b -> Bit
forall t. Equatable t => t -> t -> Bit
=== Relation a b
s

-- | Given two relations \( R, S \subseteq A \times B \), check if \(R\) is a subset of \(S\).
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
  | Relation a b -> ((a, b), (a, b))
forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a b
r ((a, b), (a, b)) -> ((a, b), (a, b)) -> Bool
forall a. Eq a => a -> a -> Bool
== Relation a b -> ((a, b), (a, b))
forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a b
s = [Bit] -> Bit
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
forall (t :: * -> *). Foldable t => t Bit -> Bit
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 a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (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) Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
==> (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)
  | Bool
otherwise = [Char] -> Bit
forall a. HasCallStack => [Char] -> a
error [Char]
"Relations don't have the same bounds!"

-- | 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 = [Bit] -> Bit
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
forall (t :: * -> *). Foldable t => t Bit -> Bit
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 a. a -> [a]
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

-- | 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 = 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

-- | Tests if a relation \( R \subseteq A \times A \) is strongly connected, i.e.,
-- \( R \cup R^{-1} = A \times A \).
total :: ( Ix a ) => Relation a a -> Bit
total :: forall a. Ix a => 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

-- | 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 = 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

-- | Tests if a relation \( R \subseteq A \times A \) is symmetric,
-- i.e., \( R \cup R^{-1} = R \).
symmetric :: ( Ix a ) => Relation a a -> Bit
symmetric :: forall a. Ix a => 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 )


-- | Tests if a relation \( R \subseteq A \times A \) is antisymmetric,
-- i.e., \( R \cap R^{-1} \subseteq R^{0} \).
anti_symmetric :: ( Ix a ) => Relation a a -> Bit
anti_symmetric :: forall a. Ix a => 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))

-- | Tests if a relation \( R \subseteq A \times A \) is irreflexive, i.e.,
-- \( R \cap R^{0} = \emptyset \).
irreflexive :: ( Ix a ) => Relation a a -> Bit
irreflexive :: forall a. Ix a => Relation a a -> Bit
irreflexive Relation a a
r = Relation a a -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> Bit
empty (Relation a a -> Bit) -> Relation a a -> Bit
forall a b. (a -> b) -> a -> b
$ 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 (((a, a), (a, a)) -> Relation a a
forall a. Ix a => ((a, a), (a, a)) -> Relation a a
identity (((a, a), (a, a)) -> Relation a a)
-> ((a, a), (a, a)) -> Relation a a
forall a b. (a -> b) -> a -> b
$ 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) Relation a a
r

-- | Tests if a relation \( R \subseteq A \times A \) is reflexive, i.e.,
-- \( R^{0} \subseteq R \).
reflexive :: ( Ix a ) => Relation a a -> Bit
reflexive :: forall a. Ix a => Relation a a -> Bit
reflexive 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 (((a, a), (a, a)) -> Relation a a
forall a. Ix a => ((a, a), (a, a)) -> Relation a a
identity (((a, a), (a, a)) -> Relation a a)
-> ((a, a), (a, a)) -> Relation a a
forall a b. (a -> b) -> a -> b
$ 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) Relation a a
r

-- | 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 = [Bit] -> Bit
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
forall (t :: * -> *). Foldable t => t Bit -> Bit
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 :: forall a b. (Ix a, Ix b) => 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 :: forall a b. (Ix a, Ix b) => 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 :: forall a b. (Ix a, Ix b) => 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 :: forall a b. (Ix a, Ix b) => 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 :: forall a b. (Ix a, Ix b) => 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 :: forall a b. (Ix a, Ix b) => 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 :: 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 = [b] -> b
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
forall (t :: * -> *). 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 a. a -> [a]
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 a. a -> [a]
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)

-- | Tests if a relation \( R \subseteq A \times A \) is transitive, i.e.,
-- \( R \circ R = R \).
--
-- Formula size: linear in \( |A|^3 \)
transitive :: ( Ix a )
           => Relation a a -> Bit
transitive :: forall a. Ix a => 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