{-# language FlexibleInstances, MultiParamTypeClasses #-}

module Ersatz.Relation.Op

(
-- * Operations
  mirror
, union
, complement
, difference
, product, power
, intersection
, reflexive_closure
, symmetric_closure
, transitive_closure
, transitive_reflexive_closure
, equivalence_closure
)

where

import Ersatz.Relation.Data

import Prelude hiding ( (&&), (||), and, or, not, product )
import Ersatz.Bit

import qualified Data.Array as A
import Data.Ix

-- | Constructs the converse relation \( R^{-1} \) of a relation
-- \( R \subseteq A \times B \), which is defined by \( R^{-1} = \{ (y,x) ~|~ (x,y) \in R \} \subseteq B \times A \).
mirror :: ( Ix a , Ix b ) => Relation a b -> Relation b a
mirror :: forall a b. (Ix a, Ix b) => Relation a b -> Relation b a
mirror Relation a b
r =
    let ((a
a,b
b),(a
c,b
d)) = 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
    in  ((b, a), (b, a)) -> [((b, a), Bit)] -> Relation b a
forall a b.
(Ix a, Ix b) =>
((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
build ((b
b,a
a),(b
d,a
c)) ([((b, a), Bit)] -> Relation b a)
-> [((b, a), Bit)] -> Relation b a
forall a b. (a -> b) -> a -> b
$ do (a
x,b
y) <- Relation a b -> [(a, b)]
forall a b. (Ix a, Ix b) => Relation a b -> [(a, b)]
indices Relation a b
r ; ((b, a), Bit) -> [((b, a), Bit)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ((b
y,a
x), Relation a b
rRelation a b -> (a, b) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
!(a
x,b
y))

-- | Constructs the complement relation \( \overline{R} \)
-- of a relation \( R \subseteq A \times B \), which is defined by
-- \( \overline{R}  = \{ (x,y) \in A \times B ~|~ (x,y) \notin R \} \).
complement :: ( Ix a , Ix b ) => Relation a b -> Relation a b
complement :: forall a b. (Ix a, Ix b) => Relation a b -> Relation a b
complement Relation a b
r =
    ((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
forall a b.
(Ix a, Ix b) =>
((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
build (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), Bit)] -> Relation a b)
-> [((a, b), Bit)] -> Relation a b
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 ; ((a, b), Bit) -> [((a, b), Bit)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ( (a, b)
i, Bit -> Bit
forall b. Boolean b => b -> b
not (Bit -> Bit) -> Bit -> Bit
forall a b. (a -> b) -> a -> b
$ Relation a b
rRelation a b -> (a, b) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
!(a, b)
i )

-- | Constructs the difference \( R \setminus S \) of the relations
-- \(R, S \subseteq A \times B \), that contains all elements that are in \(R\) but not in \(S\), i.e.,
-- \( R \setminus S = \{ (x,y) \in R ~|~ (x,y) \notin S \} \).
difference :: ( Ix a , Ix b )
        => Relation a b -> Relation a b ->  Relation a b
difference :: forall a b.
(Ix a, Ix b) =>
Relation a b -> Relation a b -> Relation a b
difference Relation a b
r Relation a b
s =
    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 -> Relation a b) -> Relation a b -> Relation a b
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
s

-- | Constructs the union \( R \cup S \) of the relations \( R, S \subseteq A \times B \).
union :: ( Ix a , Ix b )
        => Relation a b -> Relation a b -> Relation a b
union :: forall a b.
(Ix a, Ix b) =>
Relation a b -> Relation a b -> Relation a b
union 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 = ((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
forall a b.
(Ix a, Ix b) =>
((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
build ( 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), Bit)] -> Relation a b)
-> [((a, b), Bit)] -> Relation a b
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
        ((a, b), Bit) -> [((a, b), Bit)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ((a, b)
i, Relation a b
rRelation 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
sRelation a b -> (a, b) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
!(a, b)
i)
    | Bool
otherwise = [Char] -> Relation a b
forall a. HasCallStack => [Char] -> a
error [Char]
"Relations don't have the same bounds!"

-- | Constructs the composition \( R \circ S \) of the relations
-- \( R \subseteq A \times B \) and \( S \subseteq B \times C \), which is
-- defined by \( R \circ S = \{ (a,c) ~|~ (a,b) \in R \land (b,c) \in S \} \).
--
-- Formula size: linear in \(|A|\cdot|B|\cdot|C|\)
product :: ( Ix a , Ix b, Ix c )
        => Relation a b -> Relation b c -> Relation a c
product :: forall a b c.
(Ix a, Ix b, Ix c) =>
Relation a b -> Relation b c -> Relation a c
product Relation a b
a Relation b c
b =
    let ((a
ao,b
al),(a
au,b
ar)) = 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
a
        ((b
bo,c
bl),(b
bu,c
br)) = Relation b c -> ((b, c), (b, c))
forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation b c
b
        bnd :: ((a, c), (a, c))
bnd = ((a
ao,c
bl),(a
au,c
br))
    in  if (b
al,b
ar) (b, b) -> (b, b) -> Bool
forall a. Eq a => a -> a -> Bool
== (b
bo,b
bu)
            then ((a, c), (a, c)) -> [((a, c), Bit)] -> Relation a c
forall a b.
(Ix a, Ix b) =>
((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
build ((a, c), (a, c))
bnd ([((a, c), Bit)] -> Relation a c)
-> [((a, c), Bit)] -> Relation a c
forall a b. (a -> b) -> a -> b
$ do
                i :: (a, c)
i@(a
x,c
z) <- ((a, c), (a, c)) -> [(a, c)]
forall a. Ix a => (a, a) -> [a]
range ((a, c), (a, c))
bnd
                ((a, c), Bit) -> [((a, c), Bit)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ((a, c)
i, [Bit] -> Bit
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
forall (t :: * -> *). Foldable t => t Bit -> Bit
or ([Bit] -> Bit) -> [Bit] -> Bit
forall a b. (a -> b) -> a -> b
$ do
                        b
y <- (b, b) -> [b]
forall a. Ix a => (a, a) -> [a]
range ( b
al, b
ar )
                        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 (t :: * -> *). (Boolean b, Foldable t) => t b -> b
forall (t :: * -> *). Foldable t => t Bit -> Bit
and [ Relation a b
aRelation a b -> (a, b) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
!(a
x,b
y), Relation b c
bRelation b c -> (b, c) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
!(b
y,c
z) ]
                        )
            else [Char] -> Relation a c
forall a. HasCallStack => [Char] -> a
error [Char]
"Codomain of first relation must equal domain of second relation!"

-- | Constructs the relation \( R^{n} \) that results if a relation
-- \( R \subseteq A \times A \) is composed \(n\) times with itself.
--
-- \( R^{0} \) is the identity relation \( I = \{ (x,x) ~|~ x \in A \} \).
--
-- Formula size: linear in \( |A|^3 \cdot  \log n \)
power  :: ( Ix a ) => Int -> Relation a a -> Relation a a
power :: forall a. Ix a => Int -> Relation a a -> Relation a a
power Int
0 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 )
power Int
1 Relation a a
r = Relation a a
r
power Int
e Relation a a
r =
    let (Int
d,Int
m) = Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
divMod Int
e Int
2
        s :: Relation a a
s = Int -> Relation a a -> Relation a a
forall a. Ix a => Int -> Relation a a -> Relation a a
power Int
d Relation a a
r
        s2 :: Relation a a
s2 = 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
s Relation a a
s
    in  case Int
m of
        Int
0 -> Relation a a
s2
        Int
_ -> 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
s2 Relation a a
r

-- | Constructs the intersection \( R \cap S \) of the relations \( R, S \subseteq A \times B \).
intersection :: ( Ix a , Ix b )
      => Relation a b -> Relation a b
      -> Relation a b
intersection :: 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
    | 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 = ((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
forall a b.
(Ix a, Ix b) =>
((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
build ( 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), Bit)] -> Relation a b)
-> [((a, b), Bit)] -> Relation a b
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
        ((a, b), Bit) -> [((a, b), Bit)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ((a, b)
i, [Bit] -> Bit
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
forall (t :: * -> *). Foldable t => t Bit -> Bit
and [ Relation a b
rRelation a b -> (a, b) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
!(a, b)
i, Relation a b
sRelation a b -> (a, b) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
!(a, b)
i ] )
    | Bool
otherwise = [Char] -> Relation a b
forall a. HasCallStack => [Char] -> a
error [Char]
"Relations don't have the same bounds!"

-- | Constructs the reflexive closure \( R \cup R^{0} \) of the relation
-- \( R \subseteq A \times A \).
reflexive_closure :: Ix a => Relation a a -> Relation a a
reflexive_closure :: forall a. Ix a => Relation a a -> Relation a a
reflexive_closure Relation a a
t =
    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
union Relation a a
t (Relation a a -> Relation a a) -> Relation a a -> Relation a a
forall a b. (a -> b) -> a -> b
$ ((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
t

-- | Constructs the symmetric closure \( R \cup R^{-1} \) of the relation
-- \( R \subseteq A \times A \).
symmetric_closure :: Ix a => Relation a a -> Relation a a
symmetric_closure :: forall a. Ix a => Relation a a -> Relation a a
symmetric_closure Relation a a
r =
    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
union Relation a a
r (Relation a a -> Relation a a) -> Relation a a -> Relation a a
forall a b. (a -> b) -> a -> b
$ Relation a a -> Relation a a
forall a b. (Ix a, Ix b) => Relation a b -> Relation b a
mirror Relation a a
r

-- | Constructs the transitive closure \( R^{+} \) of the relation
-- \( R \subseteq A \times A \), which is defined by
-- \( R^{+} = \bigcup^{\infty}_{i = 1} R^{i} \).
--
-- Formula size: linear in \( |A|^3 \)
transitive_closure :: Ix a => Relation a a -> Relation a a
transitive_closure :: forall a. Ix a => Relation a a -> Relation a a
transitive_closure Relation a a
r =
  let n :: Int
n = Relation a a -> Int
forall a. Ix a => Relation a a -> Int
universeSize Relation a a
r
      -- @a' ! (0,p,q)@ is true if and only if @r ! (p,q)@ is true
      a' :: Array (Int, Int, Int) Bit
a' = ((Int, Int, Int), (Int, Int, Int))
-> [Bit] -> Array (Int, Int, Int) Bit
forall i e. Ix i => (i, i) -> [e] -> Array i e
A.listArray ((Int
0,Int
1,Int
1),(Int
n,Int
n,Int
n)) (Relation a a -> [Bit]
forall a b. (Ix a, Ix b) => Relation a b -> [Bit]
elems Relation a a
r)
      -- @a ! (0,p,q)@ is true if and only if @a' ! (0,p,q)@ is true
      a :: Array (Int, Int, Int) Bit
a = Array (Int, Int, Int) Bit
a' Array (Int, Int, Int) Bit
-> [((Int, Int, Int), Bit)] -> Array (Int, Int, Int) Bit
forall i e. Ix i => Array i e -> [(i, e)] -> Array i e
A.// do
        -- If x > 0, then @a ! (p,x,q)@ is true if and only if there is a path from p to q via nodes {1,...,x} in r
        i :: (Int, Int, Int)
i@(Int
x,Int
p,Int
q) <- ((Int, Int, Int), (Int, Int, Int)) -> [(Int, Int, Int)]
forall a. Ix a => (a, a) -> [a]
A.range ((Int
1,Int
1,Int
1),(Int
n,Int
n,Int
n))
        ((Int, Int, Int), Bit) -> [((Int, Int, Int), Bit)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Int, Int, Int)
i, Array (Int, Int, Int) Bit
a Array (Int, Int, Int) Bit -> (Int, Int, Int) -> Bit
forall i e. Ix i => Array i e -> i -> e
A.! (Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1,Int
p,Int
q) Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
|| Array (Int, Int, Int) Bit
a Array (Int, Int, Int) Bit -> (Int, Int, Int) -> Bit
forall i e. Ix i => Array i e -> i -> e
A.! (Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1,Int
p,Int
x) Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
&& Array (Int, Int, Int) Bit
a Array (Int, Int, Int) Bit -> (Int, Int, Int) -> Bit
forall i e. Ix i => Array i e -> i -> e
A.! (Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1,Int
x,Int
q))
  in ((a, a), (a, a)) -> [((a, a), Bit)] -> Relation a a
forall a b.
(Ix a, Ix b) =>
((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
build (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, a), Bit)] -> Relation a a)
-> [((a, a), Bit)] -> Relation a a
forall a b. (a -> b) -> a -> b
$ [(a, a)] -> [Bit] -> [((a, a), Bit)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Relation a a -> [(a, a)]
forall a b. (Ix a, Ix b) => Relation a b -> [(a, b)]
indices Relation a a
r) [Array (Int, Int, Int) Bit
a Array (Int, Int, Int) Bit -> (Int, Int, Int) -> Bit
forall i e. Ix i => Array i e -> i -> e
A.! (Int, Int, Int)
i | (Int, Int, Int)
i <- ((Int, Int, Int), (Int, Int, Int)) -> [(Int, Int, Int)]
forall a. Ix a => (a, a) -> [a]
A.range ((Int
n,Int
1,Int
1),(Int
n,Int
n,Int
n))]

-- | Constructs the transitive reflexive closure \( R^{*} \) of the relation
-- \( R \subseteq A \times A \), which is defined by
-- \( R^{*} = \bigcup^{\infty}_{i = 0} R^{i} \).
--
-- Formula size: linear in \( |A|^3 \)
transitive_reflexive_closure :: Ix a => Relation a a -> Relation a a
transitive_reflexive_closure :: forall a. Ix a => Relation a a -> Relation a a
transitive_reflexive_closure Relation a a
r =
    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
union (Relation a a -> Relation a a
forall a. Ix a => Relation a a -> Relation a a
transitive_closure Relation a a
r) (((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)

-- | Constructs the equivalence closure \( (R \cup R^{-1})^* \) of the relation
-- \( R \subseteq A \times A \).
--
-- Formula size: linear in \( |A|^3 \)
equivalence_closure :: Ix a => Relation a a -> Relation a a
equivalence_closure :: forall a. Ix a => Relation a a -> Relation a a
equivalence_closure Relation a a
r =
  Relation a a -> Relation a a
forall a. Ix a => Relation a a -> Relation a a
transitive_reflexive_closure (Relation a a -> Relation a a) -> Relation a a -> Relation a a
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