ersatz-0.6: src/Ersatz/Relation/ARS.hs

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 r = irreflexive $ transitive_closure 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 r = do
  s <- relation $ bounds r
  assert $ and [
      transitive s
    , irreflexive s
    , implies r 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 r = product (mirror 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 r s = product r (mirror 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 r =
  let r' = transitive_reflexive_closure r
  in implies (peak r r) (valley r' 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 r =
  let r' = transitive_reflexive_closure r
  in implies (peak r' r') (valley r' 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 r =
  let r' = transitive_reflexive_closure r
  in implies (peak r r') (valley r' 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 r = and [terminating r, locally_confluent 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 r = do
  s <- relation $ bounds r
  t <- relation $ bounds r
  let u = universe r
      i = indices r
  assert $ and [
      transitive s
    , irreflexive s
    , implies r s
    , all (\x -> is_nf x r ==> t ! (x,x)) u
    , all (\(x,y) -> s!(x,y) && t!(y,y) ==> t!(x,y)) i
    , nor $ do
        (x,y) <- i; z <- u; guard $ y /= z
        return $ t ! (x,y) && t ! (x,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 r
  | is_homogeneous r = elems r === reverse (elems r)
  | otherwise = error "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
r `relative_to` s =
  let s' = transitive_reflexive_closure s
  in foldl1 product [ s', r , 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 r = complete $ equivalence_closure 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 x r =
  let ((_,b),(_,d)) = bounds r
  in nor $ map (r !) $ range ((x,b),(x,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 r = and $ do
  let trc = transitive_reflexive_closure r
      ec = equivalence_closure r
  (x,y) <- indices r
  return $ and [is_nf y r, ec ! (x,y)] ==> trc ! (x,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 r = and $ do
  let ec = equivalence_closure r
  (x,y) <- indices r
  guard $ x < y
  return $ and [is_nf x r, is_nf y r] ==> not $ ec ! (x,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 r = and $ do
  let trc = transitive_reflexive_closure r
  (x,y) <- indices r
  guard $ x < y
  return $ and [is_nf x r, is_nf y r] ==> not $ peak trc trc ! (x,y)