module Ersatz.Relation.ARS (
-- * Abstract rewriting
  terminating, assert_terminating
, peak, valley
, locally_confluent
, confluent, semiconfluent
, convergent, assert_convergent
, point_symmetric
, relative_to
, connected
, is_nf
, nf_property
, unique_nfs, unique_nfs_reduction
)

where

import Prelude hiding ( (&&), not, or, and, all, product )

import Ersatz.Bit
import Ersatz.Equatable
import Ersatz.Problem ( MonadSAT )

import Ersatz.Relation.Data
import Ersatz.Relation.Op
import Ersatz.Relation.Prop

import Data.Ix
import Control.Monad ( guard )


-- | Tests if a relation \( R \subseteq A \times A \) is terminating, i.e.,
-- there is no infinite sequence \( x_1, x_2, ... \) with \( x_i \in A \)
-- such that \( (x_i, x_{i+1}) \in R \) holds.
--
-- Formula size: linear in \( |A|^3 \)
terminating :: Ix a => Relation a a -> Bit
terminating :: forall a. Ix a => Relation a a -> Bit
terminating Relation a a
r = Relation a a -> Bit
forall a. Ix a => Relation a a -> Bit
irreflexive (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
transitive_closure Relation a a
r

-- | Monadic version of 'terminating'.
--
-- Note that @assert_terminating@ cannot be used for expressing non-termination of a relation,
-- only for expressing termination.
--
-- Formula size: linear in \( |A|^3 \)
--
-- ==== __Example__
--
-- @
-- example = do
--   result <- 'Ersatz.Solver.solveWith' 'Ersatz.Solver.Minisat.minisat' $ do
--     r <- 'relation' ((0,0),(2,2))
--     'Ersatz.Bit.assert' $ 'Ersatz.Counting.atleast' 3 $ 'elems' r
--     'assert_terminating' r
--     return r
--   case result of
--     (Satisfied, Just r) -> do putStrLn $ 'table' r; return True
--     _                   -> return False
-- @
assert_terminating :: (Ix a, MonadSAT s m) => Relation a a -> m ()
assert_terminating :: forall a s (m :: * -> *).
(Ix a, MonadSAT s m) =>
Relation a a -> m ()
assert_terminating Relation a a
r = do
  Relation a a
s <- ((a, a), (a, a)) -> m (Relation a a)
forall a b s (m :: * -> *).
(Ix a, Ix b, MonadSAT s m) =>
((a, b), (a, b)) -> m (Relation a b)
relation (((a, a), (a, a)) -> m (Relation a a))
-> ((a, a), (a, a)) -> m (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
  Bit -> m ()
forall s (m :: * -> *). MonadSAT s m => Bit -> m ()
assert (Bit -> m ()) -> Bit -> m ()
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 a -> Bit
forall a. Ix a => Relation a a -> Bit
transitive Relation a a
s
    , Relation a a -> Bit
forall a. Ix a => Relation a a -> Bit
irreflexive Relation a a
s
    , 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
s ]

-- | Constructs the peak \( R^{-1} \circ S \) of two relations
-- \( R, S \subseteq A \times A \).
--
-- Formula size: linear in \( |A|^3 \)
peak :: Ix a => Relation a a -> Relation a a -> Relation a a
peak :: forall a. Ix a => Relation a a -> Relation a a -> Relation a a
peak Relation a a
r = 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 -> Relation a a
forall a b. (Ix a, Ix b) => Relation a b -> Relation b a
mirror Relation a a
r)

-- | Constructs the valley \( R \circ S^{-1} \) of two relations
-- \( R, S \subseteq A \times A \).
--
-- Formula size: linear in \( |A|^3 \)
valley :: Ix a => Relation a a -> Relation a a -> Relation a a
valley :: forall a. Ix a => Relation a a -> Relation a a -> Relation a a
valley Relation a a
r Relation a a
s = 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 -> Relation a a
forall a b. (Ix a, Ix b) => Relation a b -> Relation b a
mirror Relation a a
s)

-- | Tests if a relation \( R \subseteq A \times A \) is locally confluent, i.e.,
-- \( \forall a,b,c \in A: ((a,b) \in R) \land ((a,c) \in R) \rightarrow \exists d \in A: ((b,d) \in R^*) \land ((c,d)\in R^*) \).
--
-- Formula size: linear in \( |A|^3 \)
locally_confluent :: Ix a => Relation a a -> Bit
locally_confluent :: forall a. Ix a => Relation a a -> Bit
locally_confluent Relation a a
r =
  let r' :: 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
r
  in 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. Ix a => Relation a a -> Relation a a -> Relation a a
peak Relation a a
r Relation a a
r) (Relation a a -> Relation a a -> Relation a a
forall a. Ix a => Relation a a -> Relation a a -> Relation a a
valley Relation a a
r' Relation a a
r')

-- | Tests if a relation \( R \subseteq A \times A \) is confluent, i.e.,
-- \( \forall a,b,c \in A: ((a,b) \in R^*) \land ((a,c) \in R^*) \rightarrow \exists d \in A: ((b,d) \in R^*) \land ((c,d)\in R^*) \).
--
-- Formula size: linear in \( |A|^3 \)
confluent :: Ix a => Relation a a -> Bit
confluent :: forall a. Ix a => Relation a a -> Bit
confluent Relation a a
r =
  let r' :: 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
r
  in 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. Ix a => Relation a a -> Relation a a -> Relation a a
peak Relation a a
r' Relation a a
r') (Relation a a -> Relation a a -> Relation a a
forall a. Ix a => Relation a a -> Relation a a -> Relation a a
valley Relation a a
r' Relation a a
r')

-- | Tests if a relation \( R \subseteq A \times A \) is semi-confluent, i.e.,
-- \( \forall a,b,c \in A: ((a,b) \in R) \land ((a,c) \in R^*) \rightarrow \exists d \in A: ((b,d) \in R^*) \land ((c,d)\in R^*) \).
--
-- @semiconfluent@ is equivalent to 'confluent'.
--
-- Formula size: linear in \( |A|^3 \)
semiconfluent :: Ix a => Relation a a -> Bit
semiconfluent :: forall a. Ix a => Relation a a -> Bit
semiconfluent Relation a a
r =
  let r' :: 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
r
  in 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. Ix a => Relation a a -> Relation a a -> Relation a a
peak Relation a a
r Relation a a
r') (Relation a a -> Relation a a -> Relation a a
forall a. Ix a => Relation a a -> Relation a a -> Relation a a
valley Relation a a
r' Relation a a
r')

-- | Tests if a relation \( R \subseteq A \times A \) is convergent, i.e.,
-- \( R \) is 'terminating' and 'confluent'.
--
-- Formula size: linear in \( |A|^3 \)
convergent :: Ix a => Relation a a -> Bit
convergent :: forall a. Ix a => Relation a a -> Bit
convergent Relation a a
r = [Bit] -> Bit
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
forall (t :: * -> *). Foldable t => t Bit -> Bit
and [Relation a a -> Bit
forall a. Ix a => Relation a a -> Bit
terminating Relation a a
r, Relation a a -> Bit
forall a. Ix a => Relation a a -> Bit
locally_confluent Relation a a
r]

-- | Monadic version of 'convergent'.
--
-- Note that @assert_convergent@ cannot be used for expressing non-convergence of a relation,
-- only for expressing convergence.
--
-- Formula size: linear in \( |A|^3 \)
--
-- ==== __Example__
--
-- @
-- example = do
--   result <- 'Ersatz.Solver.solveWith' 'Ersatz.Solver.Minisat.minisat' $ do
--     r <- 'relation' ((0,0),(3,3))
--     'Ersatz.Bit.assert' $ 'Ersatz.Counting.exactly' 3 $ 'elems' r
--     'assert_convergent' r
--     'Ersatz.Bit.assert' $ 'Ersatz.Bit.not' $ 'transitive' r
--     return r
--   case result of
--     (Satisfied, Just r) -> do putStrLn $ 'table' r; return True
--     _                   -> return False
-- @
assert_convergent :: (Ix a, MonadSAT s m) => Relation a a -> m ()
assert_convergent :: forall a s (m :: * -> *).
(Ix a, MonadSAT s m) =>
Relation a a -> m ()
assert_convergent Relation a a
r = do
  Relation a a
s <- ((a, a), (a, a)) -> m (Relation a a)
forall a b s (m :: * -> *).
(Ix a, Ix b, MonadSAT s m) =>
((a, b), (a, b)) -> m (Relation a b)
relation (((a, a), (a, a)) -> m (Relation a a))
-> ((a, a), (a, a)) -> m (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
t <- ((a, a), (a, a)) -> m (Relation a a)
forall a b s (m :: * -> *).
(Ix a, Ix b, MonadSAT s m) =>
((a, b), (a, b)) -> m (Relation a b)
relation (((a, a), (a, a)) -> m (Relation a a))
-> ((a, a), (a, a)) -> m (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
  let u :: [a]
u = Relation a a -> [a]
forall a. Ix a => Relation a a -> [a]
universe Relation a a
r
      i :: [(a, a)]
i = Relation a a -> [(a, a)]
forall a b. (Ix a, Ix b) => Relation a b -> [(a, b)]
indices Relation a a
r
  Bit -> m ()
forall s (m :: * -> *). MonadSAT s m => Bit -> m ()
assert (Bit -> m ()) -> Bit -> m ()
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 a -> Bit
forall a. Ix a => Relation a a -> Bit
transitive Relation a a
s
    , Relation a a -> Bit
forall a. Ix a => Relation a a -> Bit
irreflexive Relation a a
s
    , 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
s
    , (a -> Bit) -> [a] -> Bit
forall b (t :: * -> *) a.
(Boolean b, Foldable t) =>
(a -> b) -> t a -> b
forall (t :: * -> *) a. Foldable t => (a -> Bit) -> t a -> Bit
all (\a
x -> a -> Relation a a -> Bit
forall a. Ix a => a -> Relation a a -> Bit
is_nf a
x Relation a a
r Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
==> Relation a a
t Relation a a -> (a, a) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
! (a
x,a
x)) [a]
u
    , ((a, a) -> Bit) -> [(a, a)] -> Bit
forall b (t :: * -> *) a.
(Boolean b, Foldable t) =>
(a -> b) -> t a -> b
forall (t :: * -> *) a. Foldable t => (a -> Bit) -> t a -> Bit
all (\(a
x,a
y) -> Relation a a
sRelation a a -> (a, a) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
!(a
x,a
y) Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
&& Relation a a
tRelation a a -> (a, a) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
!(a
y,a
y) Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
==> Relation a a
tRelation a a -> (a, a) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
!(a
x,a
y)) [(a, a)]
i
    , [Bit] -> Bit
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
forall (t :: * -> *). Foldable t => t Bit -> Bit
nor ([Bit] -> Bit) -> [Bit] -> Bit
forall a b. (a -> b) -> a -> b
$ do
        (a
x,a
y) <- [(a, a)]
i; a
z <- [a]
u; Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ a
y a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
z
        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 a
t Relation a a -> (a, a) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
! (a
x,a
y) Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
&& Relation a a
t Relation a a -> (a, a) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
! (a
x,a
z) ]

-- | Tests if the matrix representation (i.e. the array) of a relation
-- \( R \subseteq A \times A \) is point symmetric, i.e., for the matrix representation
-- \( \begin{pmatrix} a_{11} & \dots & a_{1n} \\ \vdots & \ddots & \vdots \\ a_{n1} & \dots & a_{nn} \end{pmatrix} \)
-- holds \( a_{ij} = a_{(n-i+1)(n-j+1)} \).
point_symmetric :: Ix a => Relation a a -> Bit
point_symmetric :: forall a. Ix a => Relation a a -> Bit
point_symmetric Relation a a
r
  | Relation a a -> Bool
forall a. Ix a => Relation a a -> Bool
is_homogeneous Relation a a
r = Relation a a -> [Bit]
forall a b. (Ix a, Ix b) => Relation a b -> [Bit]
elems Relation a a
r [Bit] -> [Bit] -> Bit
forall t. Equatable t => t -> t -> Bit
=== [Bit] -> [Bit]
forall a. [a] -> [a]
reverse (Relation a a -> [Bit]
forall a b. (Ix a, Ix b) => Relation a b -> [Bit]
elems Relation a a
r)
  | Bool
otherwise = [Char] -> Bit
forall a. HasCallStack => [Char] -> a
error [Char]
"The domain must equal the codomain!"

-- | Given two relations \( R, S \subseteq A \times A \),
-- construct \( R \) relative to \( S \) defined by \( R/S = S^* \circ R \circ S^* \).
--
-- Formula size: linear in \( |A|^3 \)
relative_to :: Ix a => Relation a a -> Relation a a -> Relation a a
Relation a a
r relative_to :: forall a. Ix a => Relation a a -> Relation a a -> Relation a a
`relative_to` Relation a a
s =
  let s' :: Relation a a
s' = Relation a a -> Relation a a
forall a. Ix a => Relation a a -> Relation a a
transitive_reflexive_closure Relation a a
s
  in (Relation a a -> Relation a a -> Relation a a)
-> [Relation a a] -> Relation a a
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 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
r , Relation a a
s' ]

-- | Tests if a relation \( R \subseteq A \times A \) is connected,
-- i.e., \( (R \cup R^{-1})^* = A \times A \).
--
-- Formula size: linear in \( |A|^3 \)
connected :: Ix a => Relation a a -> Bit
connected :: forall a. Ix a => Relation a a -> Bit
connected 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
equivalence_closure Relation a a
r

-- | Given an element \( x \in A \) and a relation \( R \subseteq A \times A \),
-- check if \( x \) is a normal form, i.e., \( \forall y \in A: (x,y) \notin R \).
--
-- Formula size: linear in \( |A| \)
is_nf :: Ix a => a -> Relation a a -> Bit
is_nf :: forall a. Ix a => a -> Relation a a -> Bit
is_nf a
x Relation a a
r =
  let ((a
_,a
b),(a
_,a
d)) = 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
  in [Bit] -> Bit
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
forall (t :: * -> *). Foldable t => t Bit -> Bit
nor ([Bit] -> Bit) -> [Bit] -> Bit
forall a b. (a -> b) -> a -> b
$ ((a, a) -> Bit) -> [(a, a)] -> [Bit]
forall a b. (a -> b) -> [a] -> [b]
map (Relation a a
r Relation a a -> (a, a) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
!) ([(a, a)] -> [Bit]) -> [(a, a)] -> [Bit]
forall a b. (a -> b) -> a -> b
$ ((a, a), (a, a)) -> [(a, a)]
forall a. Ix a => (a, a) -> [a]
range ((a
x,a
b),(a
x,a
d))

-- | Tests if a relation \( R \subseteq A \times A \) has the normal form property,
-- i.e., \( \forall a,b \in A \) holds: if \(b\) is a normal form and
-- \( (a,b) \in (R \cup R^{-1})^{*} \), then \( (a,b) \in R^{*} \).
--
-- Formula size: linear in \( |A|^3 \)
nf_property :: Ix a => Relation a a -> Bit
nf_property :: forall a. Ix a => Relation a a -> Bit
nf_property Relation a a
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
  let trc :: Relation a a
trc = Relation a a -> Relation a a
forall a. Ix a => Relation a a -> Relation a a
transitive_reflexive_closure Relation a a
r
      ec :: Relation a a
ec = Relation a a -> Relation a a
forall a. Ix a => Relation a a -> Relation a a
equivalence_closure Relation a a
r
  (a
x,a
y) <- Relation a a -> [(a, a)]
forall a b. (Ix a, Ix b) => Relation a b -> [(a, b)]
indices Relation a a
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 (t :: * -> *). (Boolean b, Foldable t) => t b -> b
forall (t :: * -> *). Foldable t => t Bit -> Bit
and [a -> Relation a a -> Bit
forall a. Ix a => a -> Relation a a -> Bit
is_nf a
y Relation a a
r, Relation a a
ec Relation a a -> (a, a) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
! (a
x,a
y)] Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
==> Relation a a
trc Relation a a -> (a, a) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
! (a
x,a
y)

-- | Tests if a relation \( R \subseteq A \times A \) has the unique normal form property,
-- i.e., \( \forall a,b \in A \) with \( a \neq b \) holds: if \(a\) and \(b\) are normal forms,
-- then \( (a,b) \notin (R \cup R^{-1})^{*} \).
--
-- Formula size: linear in \( |A|^3 \)
unique_nfs :: Ix a => Relation a a -> Bit
unique_nfs :: forall a. Ix a => Relation a a -> Bit
unique_nfs Relation a a
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
  let ec :: Relation a a
ec = Relation a a -> Relation a a
forall a. Ix a => Relation a a -> Relation a a
equivalence_closure Relation a a
r
  (a
x,a
y) <- Relation a a -> [(a, a)]
forall a b. (Ix a, Ix b) => Relation a b -> [(a, b)]
indices Relation a a
r
  Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
y
  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 [a -> Relation a a -> Bit
forall a. Ix a => a -> Relation a a -> Bit
is_nf a
x Relation a a
r, a -> Relation a a -> Bit
forall a. Ix a => a -> Relation a a -> Bit
is_nf a
y Relation a a
r] Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
==> Bit -> Bit
forall b. Boolean b => b -> b
not (Bit -> Bit) -> Bit -> Bit
forall a b. (a -> b) -> a -> b
$ Relation a a
ec Relation a a -> (a, a) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
! (a
x,a
y)

-- | Tests if a relation \( R \subseteq A \times A \) has the unique normal form property
-- with respect to reduction, i.e., \( \forall a,b \in A \) with \( a \neq b \) holds:
-- if \(a\) and \(b\) are normal forms, then \( (a,b) \notin ((R^{*})^{-1} \circ R^{*}) \).
--
-- Formula size: linear in \( |A|^3 \)
unique_nfs_reduction :: Ix a => Relation a a -> Bit
unique_nfs_reduction :: forall a. Ix a => Relation a a -> Bit
unique_nfs_reduction Relation a a
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
  let trc :: Relation a a
trc = Relation a a -> Relation a a
forall a. Ix a => Relation a a -> Relation a a
transitive_reflexive_closure Relation a a
r
  (a
x,a
y) <- Relation a a -> [(a, a)]
forall a b. (Ix a, Ix b) => Relation a b -> [(a, b)]
indices Relation a a
r
  Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
y
  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 [a -> Relation a a -> Bit
forall a. Ix a => a -> Relation a a -> Bit
is_nf a
x Relation a a
r, a -> Relation a a -> Bit
forall a. Ix a => a -> Relation a a -> Bit
is_nf a
y Relation a a
r] Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
==> Bit -> Bit
forall b. Boolean b => b -> b
not (Bit -> Bit) -> Bit -> Bit
forall a b. (a -> b) -> a -> b
$ Relation a a -> Relation a a -> Relation a a
forall a. Ix a => Relation a a -> Relation a a -> Relation a a
peak Relation a a
trc Relation a a
trc Relation a a -> (a, a) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
! (a
x,a
y)