Ersatz.Relation

The type Relation a b represents relations between finite subsets of type a and of type b.

A relation is stored internally as Array (a,b) Bit, and some methods of Data.Array are provided for managing indices and elements.

These are rarely needed, because we provide operations and properties in a point-free style, that is, without reference to individual indices and elements.

The Relation type

data Relation a b

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.

Instances

(Ix a, Ix b) => Codec (Relation a b)

Defined in Ersatz.Relation.Data

Associated Types

type Decoded (Relation a b)

Methods

decode :: MonadPlus f => Solution -> Relation a b -> f (Decoded (Relation a b))

encode :: Decoded (Relation a b) -> Relation a b

type Decoded (Relation a b)

Defined in Ersatz.Relation.Data

type Decoded (Relation a b) = Array (a, b) Bool

Construction

relation :: (Ix a, Ix b, MonadSAT s m) => ((a, b), (a, b)) -> m (Relation a b)

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

symmetric_relation

Arguments

:: (MonadSAT s m, Ix b)

=> ((b, b), (b, b))

Since a symmetric relation must be homogeneous, the domain must equal the codomain. Therefore, given bounds ((p,q),(r,s)), it must hold that p=q and r=s.

-> m (Relation b b)

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

A symmetric relation is an undirected graph, possibly with loops.

build

Arguments

:: (Ix a, Ix b)

=> ((a, b), (a, b))

-> [((a, b), Bit)]

A list of tuples, where the first element represents an element \( (x,y) \in A \times B \) and the second element is a positive Bit if \( (x,y) \in R \), or a negative Bit if \( (x,y) \notin R \).

-> Relation a b

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

buildFrom

Arguments

:: (Ix a, Ix b)

=> (a -> b -> Bit)

A function with the specified signature, that assigns a Bit-value to each element \( (x,y) \in A \times B \).

-> ((a, b), (a, b))

-> Relation a b

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

identity

Arguments

:: Ix a

=> ((a, a), (a, a))

Since the identity relation is homogeneous, the domain must equal the codomain. Therefore, given bounds ((p,q),(r,s)), it must hold that p=q and r=s.

-> Relation a a

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

Components

bounds :: (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))

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

(!) :: (Ix a, Ix b) => Relation a b -> (a, b) -> Bit

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

indices :: (Ix a, Ix b) => Relation a b -> [(a, b)]

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

assocs :: (Ix a, Ix b) => Relation a b -> [((a, b), Bit)]

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

elems :: (Ix a, Ix b) => Relation a b -> [Bit]

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

table :: (Enum a, Ix a, Enum b, Ix b) => Array (a, b) Bool -> String

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.

Operations

mirror :: (Ix a, Ix b) => Relation a b -> Relation b a

Constructs the converse relation \( R^{-1} \subseteq B \times A \) of a relation \( R \subseteq A \times B \), which is defined by \( R^{-1} = \{ (y,x) ~|~ (x,y) \in R \} \).

union :: (Ix a, Ix b) => Relation a b -> Relation a b -> Relation a b

Constructs the union \( R \cup S \) of the relations \( R \) and \( S \).

Note that for \( R \subseteq A \times B \) and \( S \subseteq C \times D \), it must hold that \( A \times B \subseteq C \times D \).

complement :: (Ix a, Ix b) => Relation a b -> Relation a b

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

difference :: (Ix a, Ix b) => Relation a b -> Relation a b -> Relation a b

Constructs the difference \( R \setminus S \) of the relations \(R\) and \(S\), 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 \} \).

Note that if \( R \subseteq A \times B \) and \( S \subseteq C \times D \), then \( A \times B \) must be a subset of \( C \times D \) and \( R \setminus S \subseteq A \times B \).

product :: (Ix a, Ix b, Ix c) => Relation a b -> Relation b c -> Relation a c

Constructs the composition \( R \cdot S \) of the relations \( R \subseteq A \times B \) and \( S \subseteq B \times C \), which is defined by \( R \cdot S = \{ (a,c) ~|~ ((a,b) \in R) \land ((b,c) \in S) \} \).

power

Arguments

:: Ix a

=> Int

\(n\)

-> Relation a a

-> Relation a 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_{R} = \{ (x,x) ~|~ x \in A \} \) of \(R\).

intersection :: (Ix a, Ix b) => Relation a b -> Relation a b -> Relation a b

Constructs the intersection \( R \cap S \) of the relations \( R \) and \( S \).

Note that for \( R \subseteq A \times B \) and \( S \subseteq C \times D \), it must hold that \( A \times B \subseteq C \times D \).

reflexive_closure :: Ix a => Relation a a -> Relation a a

Constructs the reflexive closure \( R \cup I_{R} \) of the relation \( R \subseteq A \times A \), where \( I_{R} = \{ (x,x) ~|~ x \in A \} \) is the identity relation of \(R\).

symmetric_closure :: Ix a => Relation a a -> Relation a a

Constructs the symmetric closure \( R \cup R^{-1} \) of the relation \( R \subseteq A \times A \), where \( R^{-1} = \{ (y,x) ~|~ (x,y) \in R \} \) is converse relation of \(R\).

Properties

implies :: (Ix a, Ix b) => Relation a b -> Relation a b -> Bit

Tests if the first relation \(R\) is a subset of the second relation \(S\), i.e., every element that is contained in \(R\) is also contained in \(S\).

Note that if \( R \subseteq A \times B \) and \( S \subseteq C \times D \), then \( A \times B \) must be a subset of \( C \times D \).

symmetric :: Ix a => Relation a a -> Bit

Tests if a relation \( R \subseteq A \times A \) is symmetric, i.e., \( \forall x, y \in A: ((x,y) \in R) \rightarrow ((y,x) \in R) \).

anti_symmetric :: Ix a => Relation a a -> Bit

Tests if a relation \( R \subseteq A \times A \) is antisymmetric, i.e., \( \forall x, y \in A: ((x,y) \in R) \land ((y,x) \in R)) \rightarrow (x = y) \).

transitive :: Ix a => Relation a a -> Bit

Tests if a relation \( R \subseteq A \times A \) is transitive, i.e., \( \forall x, y \in A: ((x,y) \in R) \land ((y,z) \in R) \rightarrow ((x,z) \in R) \).

irreflexive :: Ix a => Relation a a -> Bit

Tests if a relation \( R \subseteq A \times A \) is irreflexive, i.e., \( \forall x \in A: (x,x) \notin R \).

reflexive :: Ix a => Relation a a -> Bit

Tests if a relation \( R \subseteq A \times A \) is reflexive, i.e., \( \forall x \in A: (x,x) \in R \).

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 x \in A: | \{ (x,y) \in R \} | = n \) and \( \forall y \in B: | \{ (x,y) \in R \} | = n \) hold.

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 y \in B: | \{ (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 x \in A: | \{ (x,y) \in R \} | = 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 \} | \leq 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 y \in B: | \{ (x,y) \in R \} | \geq 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 \} | \leq n \) holds.

min_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.

empty :: (Ix a, Ix b) => Relation a b -> Bit

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

complete :: (Ix a, Ix b) => Relation a b -> Bit

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

total :: Ix a => Relation a a -> Bit

Tests if a relation \( R \subseteq A \times A \) is strongly connected, i.e., \( \forall x, y \in A: ((x,y) \in R) \lor ((y,x) \in R) \).

disjoint :: (Ix a, Ix b) => Relation a b -> Relation a b -> Bit

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

equals :: (Ix a, Ix b) => Relation a b -> Relation a b -> Bit

Tests if two relations \( R, S \subseteq A \times B \) are equal, i.e., they contain the same elements.