Documentation

Constructs a relation \(R \subseteq A \times B \) from a list.

Example

r = build ((0,a),(1,b)) [ ((0,a), true), ((0,b), false)
                        , ((1,a), false), ((1,b), true) ]

The Bit-value for a given element \( (x,y) \in A \times B \) and a given relation \(R \subseteq A \times B \) that indicates if \( (x,y) \in R \) or not.

Example

>>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))]
>>> r ! (0,0)
Var (-1)
>>> r ! (0,1)
Var 1

The bounds of the array that correspond to the matrix representation of the given relation.

Example

>>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false)]
>>> bounds r
((0,0),(1,1))

The list of indices, where each index represents an element \( (x,y) \in A \times B \) that may be contained in the given relation \(R \subseteq A \times B \).

Example

>>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false)]
>>> indices r
[(0,0),(0,1),(1,0),(1,1)]

The list of elements of the array that correspond to the matrix representation of the given relation.

Example

>>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))]
>>> elems r
[Var (-1),Var 1,Var 1,Var (-1)]

The list of tuples for the given relation \(R \subseteq A \times B \), where the first element represents an element \( (x,y) \in A \times B \) and the second element indicates via a Bit , if \( (x,y) \in R \) or not.

Example

>>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false)]
>>> assocs r
[((0,0),Var (-1)),((0,1),Var 1),((1,0),Var 1),((1,1),Var (-1))]

The universe \(A\) of a relation \(R \subseteq A \times A\).

Relation a b represents a binary relation \(R \subseteq A \times B \), where the domain \(A\) is a finite subset of the type a, and the codomain \(B\) is a finite subset of the type b.

A relation is stored internally as Array (a,b) Bit, so a and b have to be instances of Ix, and both \(A\) and \(B\) are intervals.

relation ((amin,bmin),(amax,mbax)) constructs an indeterminate relation \( R \subseteq A \times B \) where \(A\) is {amin .. amax} and \(B\) is {bmin .. bmax}.

Constructs an indeterminate relation \( R \subseteq B \times B \) that is symmetric, i.e., \( \forall x, y \in B: ((x,y) \in R) \rightarrow ((y,x) \in R) \).

Constructs a relation \(R \subseteq A \times B \) from a function.

Constructs an indeterminate relation \(R \subseteq A \times B\) from a function.

Constructs the identity relation \(I = \{ (x,x) ~|~ x \in A \} \subseteq A \times A\).

The domain \(A\) of a relation \(R \subseteq A \times B\).

The codomain \(B\) of a relation \(R \subseteq A \times B\).

The size of the universe \(A\) of a relation \(R \subseteq A \times A\).

Tests if a relation is homogeneous, i.e., if the domain is equal to the codomain.

The number of pairs \( (x,y) \in R \) for the given relation \( R \subseteq A \times B \).

Print a satisfying assignment from a SAT solver, where the assignment is interpreted as a relation. putStrLn $ table <assignment> corresponds to the matrix representation of this relation.

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|\)

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 \} \).

Constructs the union \( R \cup S \) of the relations \( R, S \subseteq A \times B \).

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 \} \).

Constructs the intersection \( R \cap S \) of the relations \( R, S \subseteq A \times B \).

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 \).

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 \)

Constructs the reflexive closure \( R \cup R^{0} \) of the relation \( R \subseteq A \times A \).

Constructs the symmetric closure \( R \cup R^{-1} \) of the relation \( R \subseteq A \times A \).

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 \)

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 \)

Constructs the equivalence closure \( (R \cup R^{-1})^* \) of the relation \( R \subseteq A \times A \).

Formula size: linear in \( |A|^3 \)

Tests if a relation is empty, i.e., the relation doesn't contain any elements.

Tests if two relations are disjoint, i.e., there is no element that is contained in both relations.

Given two relations \( R, S \subseteq A \times B \), check if \(R\) is a subset of \(S\).

Tests if a relation \( R \subseteq A \times A \) is symmetric, i.e., \( R \cup R^{-1} = R \).

Tests if a relation \( R \subseteq A \times A \) is antisymmetric, i.e., \( R \cap R^{-1} \subseteq R^{0} \).

Tests if a relation \( R \subseteq A \times A \) is transitive, i.e., \( R \circ R = R \).

Formula size: linear in \( |A|^3 \)

Tests if a relation \( R \subseteq A \times A \) is irreflexive, i.e., \( R \cap R^{0} = \emptyset \).

Tests if a relation \( R \subseteq A \times A \) is reflexive, i.e., \( R^{0} \subseteq 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.

Given an Int \( n \) and a relation \( R \subseteq A \times B \), check if \( \forall y \in B: | \{ (x,y) \in R \} | = n \) holds.

Given an Int \( n \) and a relation \( R \subseteq A \times B \), check if \( \forall x \in A: | \{ (x,y) \in R \} | = n \) holds.

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.

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.

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.

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.

Tests if a relation \( R \subseteq A \times B \) is complete, i.e., \(R = A \times B \).

Tests if a relation \( R \subseteq A \times A \) is strongly connected, i.e., \( R \cup R^{-1} = A \times A \).

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 \)

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 <- solveWith minisat $ do
    r <- relation ((0,0),(2,2))
    assert $ atleast 3 $ elems r
    assert_terminating r
    return r
  case result of
    (Satisfied, Just r) -> do putStrLn $ table r; return True
    _                   -> return False

Constructs the peak \( R^{-1} \circ S \) of two relations \( R, S \subseteq A \times A \).

Formula size: linear in \( |A|^3 \)

Constructs the valley \( R \circ S^{-1} \) of two relations \( R, S \subseteq A \times A \).

Formula size: linear in \( |A|^3 \)

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 \)

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 \)

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 \)

Tests if a relation \( R \subseteq A \times A \) is convergent, i.e., \( R \) is terminating and confluent.

Formula size: linear in \( |A|^3 \)

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 <- solveWith minisat $ do
    r <- relation ((0,0),(3,3))
    assert $ exactly 3 $ elems r
    assert_convergent r
    assert $ not $ transitive r
    return r
  case result of
    (Satisfied, Just r) -> do putStrLn $ table r; return True
    _                   -> return False

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)} \).

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 \)

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 \)

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| \)

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 \)

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 \)

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 \)