Experimental Investigation of Sufficient Criteria for Relations to Have Kernels

Abstract

We investigate four well-known criteria for the existence of kernels in directed graphs/relations which can be tested efficiently, viz. to be irreflexive and symmetric, to be progressively finite, to be bipartite and to satisfy Richardson’s criterion. The numerical data, obtained by the evaluation of relation-algebraic problem specifications using RelView  show that even the most general of them is very far away from a characterisation of the class of directed graphs/relations having kernels.

1 Introduction

When written as a logical formula, most mathematical theorems have the form

$$\begin{aligned} {\forall }x: \varPhi (x) \Rightarrow \varPsi (x), \end{aligned}$$

where x is a list of variables, each variable ranges over a certain class of mathematical objects, $\varPsi (x)$ describes the property one is actually interested in and $\varPhi (x)$ describes a property that ensures $\varPsi (x)$. Mostly, one tries to get $\varPhi (x)$ as general as possible. Whenever $\varPsi (x)$ is equivalent to $\varPhi (x)$ it characterises the class of mathematical objects for which $\varPsi (x)$ holds. An example is the fixpoint theorem of A. Tarski (see [12]). Here there is only one variable x that ranges over the class of lattices, $\varPhi (x)$ describes that x is complete and $\varPsi (x)$ describes that each monotonic function on x has a least fixpoint. That in this case $\varPhi (x)$ and $\varPsi (x)$ are equivalent is an immediate consequence of a theorem of A. Davis, published in [6]. Other prominent examples are characterisations of classes of mathematical objects by means of forbidden substructures, e.g., that a lattice is modular iff it does not contain a sublattice isomorphic to the pentagon-lattice $N_5$ (R. Dedekind, see [7]) and that a finite graph is planar iff it does not contain a subgraph that is a subdivision of the Kuratowski graph $K_5$ or the Kuratowski graph $K_{3,3}$ (K. Kuratowski, see [9]).

In this paper we investigate kernels within graphs. A kernel of a directed graph is a subset K of the set of vertices such that no pair of vertices of K is connected by an edge and from each vertex outside of K there is an edge to a vertex of K. This concept is introduced in [13] by J. von Neumann and O. Morgenstern as a generalisation of a solution of a cooperative game. In [5] V. Chvatal shows that determining whether a directed graph possesses a kernel is NP-complete.

Mapping kernels the aforementioned formula results in x ranging over the class of directed graphs, $\varPsi (x)$ describes that x has a kernel and $\varPhi (x)$ describes a sufficient criterion for this property. Hence, with $\varPsi (x)$ as just introduced, it is very unlikely to get a $\varPhi (x)$ such that $\varPhi (x)$ and $\varPsi (x)$ are equivalent and $\varPhi (x)$ can be computed efficiently.

There exist a series of sufficient criteria for the existence of kernels which can be tested efficiently. An interesting question is how close these are to a characterisation of the class of directed graphs having kernels. To this end, in this paper we present for all vertex sets X up to 7 vertices the number of directed graphs $g = (X,R)$ having kernels. Then we consider the four most popular criteria for the existence of kernels and present for each criterion the number of directed graphs $g = (X,R)$ which satisfy it. These numerical data show that even in case of the most general of the four criteria, the absence of cycles of odd length (as shown by M. Richardson in [10]), only a very small portion of the directed graphs with kernels satisfy the criterion. We may conclude that the criteria are very far away from a characterisation of the class of directed graphs having kernels.

In case of 7 vertices there are $5.62 \cdot 10^{14}$ directed graphs and $1.88 \cdot 10^{14}$ of them have kernels. Only $1.62 \cdot 10^{10}$ of them satisfy Richardson’s criterion. We have been able to compute the numerical data for such large numbers of directed graphs using only their adjacency relations R, relation-algebraic problem specifications and RelView for the evaluation of the latter. RelView is a tool for the manipulation and visualisation of relations and relational programming. It uses reduced ordered binary decision diagrams (ROBDDs) for implementing relations. See [3, 4] for more details. Besides the excellent and manifold capabilities of relations and relation algebra in problem solving, this paper again demonstrates the amazing computational power of RelView.

2 Relational Preliminaries

If X and Y are given sets, a subset of the direct product ${X\times Y}$ is a relation with source X and target Y. We denote the set of all relations with source X and target Y (i.e., the powerset $2^{X \times Y}$) by $[{{X}\,\leftrightarrow \,{Y}}]$ and write $R : {{X}\,\leftrightarrow \,{Y}}$ instead of $R \in [{{X}\,\leftrightarrow \,{Y}}]$. In such a case ${{X}\,\leftrightarrow \,{Y}}$ is called the type of R. A (typed) relation corresponds to a Boolean matrix. This interpretation is well suited for many purposes and also used as one of the graphical representations of relations within RelView. Therefore, in this paper we also use matrix terminology and notation for relations. In particular, we write $R_{x,y}$ instead of $(x,y) \in R$ or x R y.

We will use the following five basic operations on relations: ${\overline{R}}$ (complementation), $R \cup S$ (union), $R \cap S$ (intersection), ${R}^\mathsf{T}$ (transposition) and $R \text{; }\,S$ (composition). We assume that transposition and complementation bind stronger than composition and composition binds stronger than union and intersection. As derived operation we will use the right residual of two relations with the same source, defined by $R \setminus S := {\overline{{R}^\mathsf{T} \text{; }\,{\overline{S}}}}$. If $R : {{X}\,\leftrightarrow \,{Y}}$ and $S : {{X}\,\leftrightarrow \,{Z}}$, from the typing rules and the point-wise definitions of complementation, transposition and composition we get $R \setminus S : {{Y}\,\leftrightarrow \,{Z}}$ and, given arbitrary $y \in Y$ and $z \in Z$, that $(R \setminus S)_{y,z}$ iff for all $x \in X$ from $R_{x,y}$ it follows $S_{x,z}$.

Besides the just mentioned operations, we will use the three special relations $\mathsf{O}$ (empty relation), $\mathsf{L}$ (universal relation) and $\mathsf{I}$ (identity relation). Here we overload the symbols, i.e., avoid the binding of types to them. Finally, if R is included in S we write $R \subseteq S$ and $R = S$ means their equality.

Relation algebra as just introduced can express exactly those formulae of first-order predicate logic which contain at most two free variables and all in all at most three variables. The expressive power of full first-order predicate logic is obtained by means of projection relations or equivalent notions. In this paper we always assume that a pair u from a direct product is of the form $u = (u_1, u_2)$. This allows to describe the meaning of the projection relations $\pi$  :  ${{{X \times Y}}\,\leftrightarrow \,{X}}$ and $\rho : {{{X \times Y}}\,\leftrightarrow \,{Y}}$ of a direct product ${X\times Y}$ by $\pi _{u,x}$ iff $u_1 = x$ and $\rho _{u,y}$ iff $u_2 = y$, for all $u \in {X\times Y}$, $x \in X$ and $y \in Y$. Based on the projection relations $\pi$  :  ${{{X \times Y}}\,\leftrightarrow \,{X}}$ and $\rho : {{{X \times Y}}\,\leftrightarrow \,{Y}}$ for $R : {{X}\,\leftrightarrow \,{Z}}$ and $S : {{Y}\,\leftrightarrow \,{Z}}$ their left pairing is defined by ${[\![ {R} , {S}]}$ $:=$ $\pi \text{; }\,R \cap \rho \text{; }\,S$, thereby being of type ${{{X\times Y}}\,\leftrightarrow \,{Z}}$. Using point-wise notation we have ${[\![ {R} , {S}]}_{u,z}$ iff $R_{u_1,z}$ and $S_{u_2,z}$, for all $u \in {X\times Y}$ and $z \in Z$. The counterpart to the left pairing, with now ${{Z}\,\leftrightarrow \,{{X\times Y}}}$ as type, is the right pairing of $R : {{Z}\,\leftrightarrow \,{X}}$ and $S : {{Z}\,\leftrightarrow \,{Y}}$, defined as ${[{R},{S}]\!]} := R \text{; }\,{\pi }^\mathsf{T} \cap S \text{; }\,{\rho }^\mathsf{T}$. Point-wisely we get ${[{R},{S}]\!]}_{z,u}$ iff $R_{z,u_1}$ and $S_{z,u_2}$, for all $u \in {X\times Y}$ and $z \in Z$. The parallel composition (or product) $R \parallel S : {{{X\times X'}}\,\leftrightarrow \,{{Y\times Y'}}}$ of $R : {{X}\,\leftrightarrow \,{Y}}$ and $S : {{X'}\,\leftrightarrow \,{Y'}}$, such that (R $\parallel$ $S)_{u,v}$ iff $R_{u_1,v_1}$ and $S_{u_2,v_2}$, for all $u \in {X\times X'}$ and $v \in {Y\times Y'}$, can be defined by means of the right pairing. We get the desired property if we define $R \parallel S := {[{\pi \text{; }\,R},{\rho \text{; }\,S}]\!]}$, where $\pi$  :  ${{{X\times X'}}\,\leftrightarrow \,{X}}$ and $\rho : {{{X\times X'}}\,\leftrightarrow \,{X'}}$ are the projection relations of ${X\times X'}$ and the right pairing is formed with respect to the projection relations of ${Y\times Y'}$.

Assume the projection relations $\pi$  :  ${{{X \times Y}}\,\leftrightarrow \,{X}}$ and $\rho : {{{X \times Y}}\,\leftrightarrow \,{Y}}$ of ${X\times Y}$ and $R : {{{X\times Y}}\,\leftrightarrow \,{Z}}$ to be given. A property that we will use frequently in Sect. 4 is the equivalence of $({[{\rho },{\pi }]\!]} \text{; }\,R)_{u,z}$ and $R_{(u_2,u_1),z}$, for all $u \in {X\times Y}$ and $z \in Z$.

The relation-level equivalents of the set-theoretic symbol “$\in$” are the membership relations $\mathsf{M}: {{X}\,\leftrightarrow \,{2^X}}$, point-wisely defined by $\mathsf{M}_{x,Y}$ iff $x \in Y$, for all $x \in X$ and $Y \in 2^X$. By means of projection relations and membership relations the expressive power of full second-order predicate logic is obtained and this suffices for our later applications. If the source of a membership relation is a direct product and, hence, its target is a set of relations, we use the symbol $\mathbf{M}$ instead of $\mathsf{M}$. An important property of such a membership relation $\mathbf{M}: {{{X\times Y}}\,\leftrightarrow \,{[{{X}\leftrightarrow {Y}}]}}$ is the equivalence of $\mathbf{M}_{u,R}$ and $R_{u_1,u_2}$, for all $u \in {X\times Y}$ and $R : {{X}\,\leftrightarrow \,{Y}}$, which we also will use frequently later in Sect. 4.

At the end of this section it should be mentioned that – except the parallel composition – all specific relations and all relational operations and tests we have introduced in this section are available in the programming language of RelView. Details will be presented in Sect. 5. See also the Web-site [14].

3 The Experiments and Their Results

In this section we present the numerical data we already have mentioned in the introduction. By means of RelView we have been able to count for a given set X having at most 7 elements the number of directed graphs $g = (X,R)$ possessing kernels. These numbers are presented in the third column in Table 1. In the second column the numbers of all directed graphs with vertex set X are given, i.e., the numbers $2^{|X|^2}$, where $1 \le |X| \le 7$. The percentages of the directed graphs having kernels with regard to the total number of directed graphs are given in the last column of the table. Notice that the last number of the second and the last number of the third column of this table are the exact values of the approximations $5.62 \cdot 10^{14}$ and $1.88 \cdot 10^{14}$ mentioned in the introduction.

Table 1. Occurrences of kernels within graphs having at most 7 vertices.

We investigate four sufficient criteria for the existence of kernels in a directed graph which can be tested efficiently. That each of them indeed ensures the existence of kernels is shown in [11] with relation-algebraic means.

The first criterion is that the adjacency relation R is irreflexive and symmetric, that is, $g = (X,R)$ is the directed version of an undirected graph, where each undirected edge is replaced by two parallel directed edges with opposite directions. The corresponding numbers are presented in the second column of Table 2 corresponding to $2^{\frac{|X|(|X|-1)}{2}}$, where $1 \le |X| \le 7$. The second criterion is that $R : {{X}\,\leftrightarrow \,{X}}$ is a progressively finite relation in the sense of [11] which means that there is no non-empty subset A of X such that for each $x \in A$ there exists a $y \in A$ with $R_{x,y}$. In other words, R is progressively finite iff ${R}^\mathsf{T}$ is Noetherian iff there is no infinite sequence $(x_n)_{n \in \mathbb {N}}$ in X such that $R_{x_n,x_{n+1}}$, for all $n \in \mathbb {N}$. This criterion generalises the criterion “to be cycle-free” of [13] since on a finite set X the relation R is progressively finite iff it is cycle-free; see [11]. The data for this criterion (i.e., the number of cycle-free directed graphs $g = (X,R)$ with $1 \le |X| \le 7$), are presented in the third column. The fourth column of the table shows the number of bipartite directed graphs $g = (X,R)$, with $1 \le |X| \le 7$, since “to be bipartite” is also a sufficient criterion for the existence of kernels. In the introduction we already have mentioned Richardson’s criterion stating that a graph has no cycles of odd length. The data for this fourth criterion can be found in the last column of the table. Notice that the theorem of [10] on the existence of kernels in directed graphs without cycles of odd length assumes finite graphs. In case of an undirected graph the set of kernels equals the set of maximal stable sets such that kernels exist if the vertex set is finite. The other two criteria also hold for infinite graphs.

Each directed graph with a progressively finite relation is cycle-free and, as a consequence, also does not contain cycles of odd length. From a well-known theorem of D. König (see [8]) we immediately get that each bipartite directed graph has no cycles of odd length. Therefore, on finite directed graphs (which are important in practical applications) Richardson’s criterion is more general than the criteria “to be cycle-free” and “to be bipartite”, which also is demonstrated by the numerical data given in Table 2. The last number of the last column is the exact value of the approximation $1.62 \cdot 10^{10}$ mentioned in the introduction. A comparison of the second and the last column shows that Richardson’s criterion is also much more general than the first criterion “R is irreflexive and symmetric”. Notice that, however, neither the first criterion implies Richardson’s criterion nor vice versa.

Table 2. Number of graphs for the four criteria having at most 7 vertices.

At the end of this section it should be mentioned that each of the above four criteria not only can be tested efficiently but also can be used to obtain efficient algorithms for computing a kernel of a graph that satisfies the criterion. In case of Richardson’s criterion such an algorithm is presented in [2]. It is formulated as a relational while-program and formally derived by means of the assertion technique and reconstructing a proof of Richardson’s theorem.

4 Computing Classes of Relations Having Kernels

In this section vectors play a central role. A (relational) vector as introduced in [11] is a relation $s : {{X}\,\leftrightarrow \,{Y}}$ such that $s = s \text{; }\,\mathsf{L}$, for $\mathsf{L}: {{Y}\,\leftrightarrow \,{Y}}$. In the Boolean matrix interpretation this means that each row of s consists only of ones or only of zeros. Consequently, the targets of vectors are irrelevant and we only consider vectors of type ${{X}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}}$, with a specific singleton set $\mathbf{1}{} \mathbf{1}:= \{\bot \}$ as common target. Such vectors correspond to Boolean column vectors and, therefore, as in linear algebra we write $s_x$ instead of $s_{x,\bot }$. For $R : {{\mathbf{1}{} \mathbf{1}}\,\leftrightarrow \,{X}}$ we retain the notation $R_{\bot ,x}$.

Given a set X and a subset S of X, we call $s : {{X}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}}$ a vector model of S (for short s models S) if for all $x \in X$ it holds $x \in S$ iff $s_x$. If X is a direct product, say Y $\times$ Z, then s models a relation $S : {{Y}\,\leftrightarrow \,{Z}}$ and we have $S_{u_1,u_2}$ iff $s_u$, for all $u \in Y$ $\times$ Z. The computation of $s := { vec}(S)$ from S can be done relation-algebraically, as ${ vec}(S) = {[\![ {S} , {\mathsf{I}}]} \text{; }\,\mathsf{L}$, where $\mathsf{I}: {{Z}\,\leftrightarrow \,{Z}}$ and $\mathsf{L}: {{Z}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}}$.

Convention 4.1

For the following we fix a set X. Throughout this section then $\pi : {{{X^2}}\,\leftrightarrow \,{X}}$ and $\rho : {{{X^2}}\,\leftrightarrow \,{X}}$ denote the two projection relations of the direct product ${X^2}$ and $\mathsf{M}: {{X}\,\leftrightarrow \,{2^X}}$ and $\mathbf{M}: {{X^2}\,\leftrightarrow \,{[{{X}\leftrightarrow {X}}]}}$ are membership relations.

Instead of working with directed graphs $g = (X,R)$ in the following we work with their adjacency relations $R : {{X}\,\leftrightarrow \,{X}}$ (in [11] called associated relation) and use the notions kernel, cycle, bipartite etc. for R in an obvious way. The computations we will present consist of relation-algebraic specifications of vector models of those sets of relations on X which satisfy the first, second, third respectively fourth of the four sufficient criteria for the existence of kernels we have mentioned in Sect. 3. In Sect. 5 we will demonstrate how these specifications rather straightforwardly can be implemented in the programming language of RelView and the executions of these RelView-programs led to the numerical data of Sect. 3.

Given $R : {{X}\,\leftrightarrow \,{X}}$, from the description of kernels in Sect. 1 we get that a subset K of X is a kernel of R iff the following two formulae hold, where the variables x and y range over X:

$$\begin{aligned} \lnot {\exists }x, y : x \in K \wedge y \in K \wedge R_{x,y} \qquad \qquad {\forall }x: x \not \in K \Rightarrow {\exists }y: y \in K \wedge R_{x,y} \end{aligned}$$

The first formula defines K as R-stable and the second one as R-absorbant. As a consequence, kernels of R are precisely those subsets of X which are R-stable and R-absorbant at the same time. Based on two auxiliary specifications for R-stable and R-absorbant subsets, in the following theorem we specify relation-algebraically a vector model $\mathfrak {kernel} : {{[{{X}\leftrightarrow {X}}]}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}}$ for the set of relations on X having kernels. Besides the relations of Convention 4.1 the second projection relation $\beta : {{{X\times 2^X}}\,\leftrightarrow \,{2^X}}$ of the direct product ${X\times 2^X}$ is used. Notice that the backslash-symbol used in the second auxiliary specification $\mathfrak {absorb}$ denotes the right residual operation.

Theorem 4.1

We consider the following three relation-algebraic specifications:

$$\begin{aligned} \mathfrak {stable}&:= {\overline{ {[{{\mathsf{M}}^\mathsf{T}},{{\mathsf{M}}^\mathsf{T}}]\!]} \text{; }\,\mathbf{M}}} : {{2^X}\,\leftrightarrow \,{[{{X}\leftrightarrow {X}}]}} \\ \mathfrak {absorb}&:= (\beta \cap { vec}({\overline{\mathsf{M}}}) \text{; }\,\mathsf{L}) \setminus ( (\mathsf{I}\parallel {\mathsf{M}}^\mathsf{T}) \text{; }\,\mathbf{M}) : {{2^X}\,\leftrightarrow \,{[{{X}\leftrightarrow {X}}]}} \\ \mathfrak {kernel}&:= {(\mathsf{L}\text{; }\,(\mathfrak {stable} \cap \mathfrak {absorb}) )}^\mathsf{T} : {{[{{X}\leftrightarrow {X}}]}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}} \end{aligned}$$

For all $A \in 2^X$ and $R : {{X}\,\leftrightarrow \,{X}}$ then $\mathfrak {stable}_{A,R}$ iff A is R-stable, $\mathfrak {absorb}_{A,R}$ iff A is R-absorbant and $\mathfrak {kernel}_{R}$ iff R has a kernel.

Proof

Assume arbitrary $A \in 2^X$ and $R : {{X}\,\leftrightarrow \,{X}}$. Then the first claim is shown by the following calculation, where the variable u ranges over ${X^2}$:

$$\begin{aligned} \mathfrak {stable}_{A,R}&\,\Longleftrightarrow \,{\overline{ {[{{\mathsf{M}}^\mathsf{T}},{{\mathsf{M}}^\mathsf{T}}]\!]} \text{; }\,\mathbf{M}}}_{A,R} \\&\,\Longleftrightarrow \,\lnot {\exists }u : {[{{\mathsf{M}}^\mathsf{T}},{{\mathsf{M}}^\mathsf{T}}]\!]}_{A,u} \wedge \mathbf{M}_{u,R} \\&\,\Longleftrightarrow \,\lnot {\exists }u : {\mathsf{M}}^\mathsf{T}_{A,u_1} \wedge {\mathsf{M}}^\mathsf{T}_{A,u_2} \wedge R_{u_1,u_2} \\&\,\Longleftrightarrow \,\lnot {\exists }u : u_1 \in A \wedge u_2 \in A \wedge R_{u_1,u_2} \\&\,\Longleftrightarrow \,A \text{ is } \text{ R-stable } \end{aligned}$$

To prove the second claim, we calculate as follows, where the variables x and y range over X, the variable u ranges over ${X^2}$ and the variable B ranges over $2^X$:

$$\begin{aligned} \mathfrak {absorb}_{A,R}&\,\Longleftrightarrow \,((\beta \cap { vec}({\overline{\mathsf{M}}}) \text{; }\,\mathsf{L}) \setminus ( (\mathsf{I}\parallel {\mathsf{M}}^\mathsf{T}) \text{; }\,\mathbf{M}) )_{A,R} \\&\,\Longleftrightarrow \,{\forall }x, B: (\beta \cap { vec}({\overline{\mathsf{M}}}) \text{; }\,\mathsf{L})_{(x,B),A} \Rightarrow ((\mathsf{I}\parallel {\mathsf{M}}^\mathsf{T}) \text{; }\,\mathbf{M})_{(x,B),R} \\&\,\Longleftrightarrow \,{\forall }x, B: B = A \wedge {\overline{\mathsf{M}}}_{x,B} \Rightarrow {\exists }u: (\mathsf{I}\parallel {\mathsf{M}}^\mathsf{T})_{(x,B),u} \wedge \mathbf{M}_{u,R} \\&\,\Longleftrightarrow \,{\forall }x, B: B = A \wedge x \not \in B \Rightarrow {\exists }u: x = u_1 \wedge {\mathsf{M}}^\mathsf{T}_{B,u_2} \wedge R_{u_1,u_2} \\&\,\Longleftrightarrow \,{\forall }x: x \not \in A \Rightarrow {\exists }y: y \in A \wedge R_{x,y} \\&\,\Longleftrightarrow \,A \text{ is } R\text{-absorbant } \end{aligned}$$

Finally, we calculate as follows, where the variable A ranges over $2^X$:

$$\begin{aligned} \mathfrak {kernel}_R&\,\Longleftrightarrow \,(\mathsf{L}\text{; }\,(\mathfrak {stable} \cap \mathfrak {absorb}) )_{\bot ,R} \\&\,\Longleftrightarrow \,{\exists }A: \mathsf{L}_{\bot ,A} \wedge (\mathfrak {stable} \cap \mathfrak {absorb})_{A,R} \\&\,\Longleftrightarrow \,{\exists }A: \mathfrak {stable}_{A,R} \wedge \mathfrak {absorb}_{A,R} \end{aligned}$$

Together with the first two claims this implies the third claim. $\square$

We have used the prevalent mathematical theorem-proof-style to emphasise the result of this theorem and to enhance readability. However, in fact, we have obtained the relation-algebraic specifications by developing them formally from the corresponding logical specifications by replacing step-by-step logical constructions by equivalent relational ones. This remark also holds for the other theorems of this section.

The next theorem presents relation-algebraic specifications of vector models $\mathfrak {irrefl} : {{[{{X}\leftrightarrow {X}}]}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}}$ and $\mathfrak {sym} : {{[{{X}\leftrightarrow {X}}]}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}}$ for the set of irreflexive respectively symmetric relations on X such that the intersection $\mathfrak {irrefl} \cap \mathfrak {sym}$ models the set of relations on X which satisfy the first sufficient criterion for the existence of kernels we have mentioned in Sect. 3. Only the three relations $\pi : {{{X^2}}\,\leftrightarrow \,{X}}$ and $\rho : {{{X^2}}\,\leftrightarrow \,{X}}$ and $\mathbf{M}: {{X^2}\,\leftrightarrow \,{[{{X}\leftrightarrow {X}}]}}$ of Convention 4.1 are used.

Theorem 4.2

We consider the following relation-algebraic specifications:

$$\begin{aligned} \mathfrak {irrefl}&:= {{\overline{\mathsf{L}\text{; }\,( \mathbf{M}\cap { vec}(\mathsf{I}) \text{; }\,\mathsf{L}) }}}^\mathsf{T} : {{[{{X}\leftrightarrow {X}}]}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}} \\ \mathfrak {sym}&:= {{\overline{\mathsf{L}\text{; }\,( \mathbf{M}\cap {\overline{{[{\rho },{\pi }]\!]} \text{; }\,\mathbf{M}}} ) }}}^\mathsf{T} : {{[{{X}\leftrightarrow {X}}]}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}} \end{aligned}$$

For all $R : {{X}\,\leftrightarrow \,{X}}$ then $\mathfrak {irrefl}_{R}$ iff R is irreflexive and $\mathfrak {sym}_{R}$ iff R is symmetric.

Proof

Assume an arbitrary $R : {{X}\,\leftrightarrow \,{X}}$. Then the following calculation shows the first claim, where the variable u ranges over ${X^2}$:

$$\begin{aligned} \mathfrak {irrefl}_R&\,\Longleftrightarrow \,{\overline{\mathsf{L}\text{; }\,(\mathbf{M}\cap { vec}(\mathsf{I}) \text{; }\,\mathsf{L})}}_{\bot ,R} \\&\,\Longleftrightarrow \,\lnot {\exists }u: \mathsf{L}_{\bot ,u} \wedge \mathbf{M}_{u,R} \wedge { vec}(\mathsf{I})_u \\&\,\Longleftrightarrow \,\lnot {\exists }u: R_{u_1,u_2} \wedge \mathsf{I}_{u_1,u_2} \\&\,\Longleftrightarrow \,\lnot {\exists }u: R_{u_1,u_2} \wedge u_1 = u_2 \\&\,\Longleftrightarrow \,R \text{ is } \text{ irreflexive } \end{aligned}$$

Also in the following calculation the variable u ranges over ${X^2}$:

$$\begin{aligned} \mathfrak {sym}_R&\,\Longleftrightarrow \,{\overline{\mathsf{L}\text{; }\,( \mathbf{M}\cap {\overline{{[{\rho },{\pi }]\!]} \text{; }\,\mathbf{M}}})}}_{\bot ,R} \\&\,\Longleftrightarrow \,\lnot {\exists }u: \mathsf{L}_{\bot ,u} \wedge \mathbf{M}_{u,R} \wedge \lnot ({[{\rho },{\pi }]\!]} \text{; }\,\mathbf{M})_{u,R} \\&\,\Longleftrightarrow \,{\forall }u: \mathbf{M}_{u,R} \Rightarrow ({[{\rho },{\pi }]\!]} \text{; }\,\mathbf{M})_{u,R} \\&\,\Longleftrightarrow \,{\forall }u: R_{u_1,u_2} \Rightarrow \mathbf{M}_{(u_2,u_1),R} \\&\,\Longleftrightarrow \,{\forall }u: R_{u_1,u_2} \Rightarrow R_{u_2,u_1} \\&\,\Longleftrightarrow \,R \text{ is } \text{ symmetric } \end{aligned}$$

With this verification of the second claim the proof is complete. $\square$

The second sufficient criterion for the existence of kernels we have mentioned in Sect. 3 is “to be progressively finite”. In the following we show how to specify relation-algebraically a vector model $\mathfrak {progFin} : {{[{{X}\leftrightarrow {X}}]}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}}$ of the set of progressively finite relations on X. As in the case of Theorem 4.1 besides the relations of Convention 4.1 we use the second projection relation $\beta : {{{X\times 2^X}}\,\leftrightarrow \,{2^X}}$ of the direct product ${X\times 2^X}$.

Theorem 4.3

We consider the following relation-algebraic specification:

$$\begin{aligned} \mathfrak {progFin}&:= { {\overline{\mathsf{L}\text{; }\,\mathsf{M}\text{; }\,{\overline{({\beta }^\mathsf{T} \cap \mathsf{L}\text{; }\,{{ vec}(\mathsf{M})}^\mathsf{T} ) \text{; }\,{\overline{{{[{\pi },{\rho \text{; }\,\mathsf{M}}]\!]}}^\mathsf{T} \text{; }\,\mathbf{M}}} }} }}}^\mathsf{T} : {{[{{X}\leftrightarrow {X}}]}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}} \end{aligned}$$

For all $R : {{X}\,\leftrightarrow \,{X}}$ then $\mathfrak {progFin}_{R}$ iff R is progressively finite.

Proof

To structure the proof, we define the following auxiliary relation:

$$\begin{aligned} \mathfrak {R}&:= {\overline{ ({\beta }^\mathsf{T} \cap \mathsf{L}\text{; }\,{{ vec}(\mathsf{M})}^\mathsf{T} ) \text{; }\,{\overline{{{[{\pi },{\rho \text{; }\,\mathsf{M}}]\!]}}^\mathsf{T} \text{; }\,\mathbf{M}}} }} : {{2^X}\,\leftrightarrow \,{[{{X}\leftrightarrow {X}}]}} \end{aligned}$$

Now, assume an arbitrary $R : {{X}\,\leftrightarrow \,{X}}$. For all $A \in 2^X$ we then calculate as follows, where the variables x and y range over X, the variable B ranges over $2^X$ and the variable u ranges over ${X^2}$:

$$\begin{aligned} \mathfrak {R}_{A,R}&\,\Longleftrightarrow \,{\overline{ ({\beta }^\mathsf{T} \cap \mathsf{L}\text{; }\,{{ vec}(\mathsf{M})}^\mathsf{T} ) \text{; }\,{\overline{{{[{\pi },{\rho \text{; }\,\mathsf{M}}]\!]}}^\mathsf{T} \text{; }\,\mathbf{M}}} }}_{A,R} \\&\,\Longleftrightarrow \,\lnot {\exists }x, B: ({\beta }^\mathsf{T} \cap \mathsf{L}\text{; }\,{{ vec}(\mathsf{M})}^\mathsf{T} )_{A,(x,B)} \wedge {\overline{{{[{\pi },{\rho \text{; }\,\mathsf{M}}]\!]}}^\mathsf{T} \text{; }\,\mathbf{M}}}_{(x,B),R} \\&\,\Longleftrightarrow \,\lnot {\exists }x, B: A = B \wedge { vec}(\mathsf{M})_{(x,B)} \wedge \lnot ({{[{\pi },{\rho \text{; }\,\mathsf{M}}]\!]}}^\mathsf{T} \text{; }\,\mathbf{M})_{(x,B),R} \\&\,\Longleftrightarrow \,\lnot {\exists }x: { vec}(\mathsf{M})_{(x,A)} \wedge \lnot {\exists }u: {{[{\pi },{\rho \text{; }\,\mathsf{M}}]\!]}}^\mathsf{T}_{(x,A),u} \wedge \mathbf{M}_{u,R} \\&\,\Longleftrightarrow \,\lnot {\exists }x: \mathsf{M}_{x,A} \wedge \lnot {\exists }u: {[{\pi },{\rho \text{; }\,\mathsf{M}}]\!]}_{u,(x,A)} \wedge R_{u_1,u_2} \\&\,\Longleftrightarrow \,{\forall }x: x \in A \Rightarrow {\exists }u: u_1 = x \wedge u_2 \in A \wedge R_{u_1,u_2} \\&\,\Longleftrightarrow \,{\forall }x: x \in A \Rightarrow {\exists }y: y \in A \wedge R_{x,y} \end{aligned}$$

Using this result, we now calculate as follows, where the variable A ranges over $2^X$ and, as above, the variables x and y range over X:

$$\begin{aligned} \mathfrak {progFin}_R&\,\Longleftrightarrow \,{\overline{\mathsf{L}\text{; }\,\mathsf{M}\text{; }\,\mathfrak {R}}}_{\bot ,R} \\&\,\Longleftrightarrow \,\lnot \exists A : (\mathsf{L}\text{; }\,\mathsf{M})_{\bot ,A} \wedge \mathfrak {R}_{A,R} \\&\,\Longleftrightarrow \,\lnot \exists A : ({\mathsf{M}}^\mathsf{T} \text{; }\,\mathsf{L})_A \wedge {\forall }x: x \in A \Rightarrow {\exists }y: y \in A \wedge R_{x,y} \\&\,\Longleftrightarrow \,\lnot \exists A : A \not = \emptyset \wedge {\forall }x: x \in A \Rightarrow {\exists }y: y \in A \wedge R_{x,y} \end{aligned}$$

The last formula is the logical specification of R being progressively finite; see the definition given in Sect. 3. $\square$

We continue with the third sufficient criterion for the existence of kernels we have mentioned in Sect. 3, viz. “to be bipartite”. A corresponding relation-algebraic specification of a vector model $\mathfrak {bipartite} : {{[{{X}\leftrightarrow {X}}]}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}}$ of the set of bipartite relations on X is given in the theorem below. In this theorem only the two membership relations of Convention 4.1 are used.

Theorem 4.4

We consider the following relation-algebraic specification:

$$\begin{aligned} \mathfrak {bipartite}&:= (\mathbf{M}\setminus ( {[{\mathsf{M}},{{\overline{\mathsf{M}}}}]\!]} \cup {[{{\overline{\mathsf{M}}}},{\mathsf{M}}]\!]} ) ) \text{; }\,\mathsf{L}: {{[{{X}\leftrightarrow {X}}]}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}} \end{aligned}$$

For all $R : {{X}\,\leftrightarrow \,{X}}$ then $\mathfrak {bipartite}_{R}$ iff R is bipartite.

Proof

Assume an arbitrary $R : {{X}\,\leftrightarrow \,{X}}$. Then we calculate as follows, where the variable A ranges over $2^X$ and the variable u ranges over ${X^2}$:

$$\begin{aligned} \mathfrak {bipartite}_R&\,\Longleftrightarrow \,((\mathbf{M}\setminus ({[{\mathsf{M}},{{\overline{\mathsf{M}}}}]\!]} \cup {[{{\overline{\mathsf{M}}}},{\mathsf{M}}]\!]}) ) \text{; }\,\mathsf{L})_R \\&\,\Longleftrightarrow \,{\exists }A: (\mathbf{M}\setminus ({[{\mathsf{M}},{{\overline{\mathsf{M}}}}]\!]} \cup {[{{\overline{\mathsf{M}}}},{\mathsf{M}}]\!]}) )_{R,A} \wedge \mathsf{L}_A \\&\,\Longleftrightarrow \,{\exists }A: {\forall }u: \mathbf{M}_{u,R} \Rightarrow {[{\mathsf{M}},{{\overline{\mathsf{M}}}}]\!]}_{u,A} \vee {[{{\overline{\mathsf{M}}}},{\mathsf{M}}]\!]}_{u,A} \\&\,\Longleftrightarrow \,{\exists }A: {\forall }u: R_{u_1,u_2} \Rightarrow (\mathsf{M}_{u_1,A} \wedge {\overline{\mathsf{M}}}_{u_2,A}) \vee ({\overline{\mathsf{M}}}_{u_1,A} \wedge \mathsf{M}_{u_2,A}) \\&\,\Longleftrightarrow \,{\exists }A: {\forall }u: R_{u_1,u_2} \Rightarrow (u_1 \in A \wedge u_2 \not \in A) \vee (u_1 \not \in A \wedge u_2 \in A) \\&\,\Longleftrightarrow \,R \text{ is } \text{ bipartite } \end{aligned}$$

This completes the proof. $\square$

Concerning Richardson’s criterion, we have not been able to specify a vector model of the set of relations on X without cycles of odd length with purely relation-algebraic means. Experiments with the RelView tool have shown that the RelView-implementation of the vector model $\mathfrak {kernel}$ of Theorem 4.1 seems to be successfully executable up to $|X| = 7$ only. For $|X| = 8$ we cancelled the computation after about 20 h. Based on this fact, we have decided to consider one after the other the lengths 1, 3, 5 and 7 of cycles. If $|X| \le 2$, then a relation on X has no cycle of odd length iff it is irreflexive. As a consequence, the first two numbers of the last column of the second table of Sect. 3, i.e., the numbers for $|X| = 1$ and $|X| = 2$, are $2^{|X|(|X|-1)}$, since this expression specifies the number of irreflexive relations on X. The next three theorems present relation-algebraic specifications of three vector models with the following meanings:

• a) $\mathfrak {cyc3} : {{[{{X}\leftrightarrow {X}}]}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}}$ models the set of relations on X which have a cycle of length 3.

• b) $\mathfrak {cyc5} : {{[{{X}\leftrightarrow {X}}]}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}}$ models the set of relations on X which have a cycle of length 5.

• c) $\mathfrak {cyc7} : {{[{{X}\leftrightarrow {X}}]}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}}$ models the set of relations on X which have a cycle of length 7.

Since the complement ${\overline{\mathfrak {cyc3}}}$ models the set of relations on X without cycles of length 3 and for the complements ${\overline{\mathfrak {cyc5}}}$ and ${\overline{\mathfrak {cyc7}}}$ the same applies for length 5 and 7, respectively, the vector

$$\begin{aligned} \mathfrak {irrefl} \cap {\overline{\mathfrak {cyc3}}} \cap {\overline{\mathfrak {cyc5}}} \cap {\overline{\mathfrak {cyc7}}} : {{[{{X}\leftrightarrow {X}}]}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}} \end{aligned}$$

models the set of relations on X which have no cycles of length 1, 3, 5 and 7. Consequently, we get for $|X| \le 8$ that it models the set of relations on X without cycles of odd length. This way we have obtained the numbers of the last column of Table 2 for $3 \le |X| \le 7$.

The following relation-algebraic specification of the vector model $\mathfrak {cyc3}$ uses the relations of Convention 4.1 except the membership relation $\mathsf{M}: {{X}\,\leftrightarrow \,{2^X}}$. Furthermore, it uses the two projection relations of the direct product ${X^2}$ $\times$ ${X^2}$, which we denote as $\gamma : {{{{X^2}\times {X^2}}}\,\leftrightarrow \,{{X^2}}}$ and $\delta : {{{{X^2}\times {X^2}}}\,\leftrightarrow \,{{X^2}}}$.

Theorem 4.5

We consider the following relation-algebraic specification:

$$\begin{aligned} \mathfrak {cyc3}&:= {( \mathsf{L}\text{; }\,({[{\delta },{\gamma }]\!]} \text{; }\,(\rho \parallel \pi ) \text{; }\,\mathbf{M}\cap {[\![ {\mathbf{M}} , {\mathbf{M}}]} \cap { vec}(\rho \text{; }\,{\pi }^\mathsf{T}) \text{; }\,\mathsf{L}) )}^\mathsf{T} : {{[{{X}\leftrightarrow {X}}]}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}} \end{aligned}$$

For all $R : {{X}\,\leftrightarrow \,{X}}$ then $\mathfrak {cyc3}_{R}$ iff R has a cycle of length 3.

Proof

Assume an arbitrary $R : {{X}\,\leftrightarrow \,{X}}$. Furthermore, let $u, v \in {X^2}$. Then we have

$$\begin{aligned} ({[{\delta },{\gamma }]\!]} \text{; }\,(\rho \parallel \pi ) \text{; }\,\mathbf{M})_{(u,v),R} \,\Longleftrightarrow \,((\rho \parallel \pi ) \text{; }\,\mathbf{M})_{(v,u),R} \,\Longleftrightarrow \,\mathbf{M}_{(v_2,u_1),R} \,\Longleftrightarrow \,R_{v_2,u_1} \end{aligned}$$

and

$$\begin{aligned} {[\![ {\mathbf{M}} , {\mathbf{M}}]}_{(u,v),R} \,\Longleftrightarrow \,\mathbf{M}_{u,R} \wedge \mathbf{M}_{v,R} \,\Longleftrightarrow \,R_{u_1,u_2} \wedge R_{v_1,v_2} \end{aligned}$$

and

$$\begin{aligned} ({ vec}(\rho \text{; }\,{\pi }^\mathsf{T}) \text{; }\,\mathsf{L})_{(u,v),R} \,\Longleftrightarrow \,{ vec}(\rho \text{; }\,{\pi }^\mathsf{T})_{(u,v)} \,\Longleftrightarrow \,(\rho \text{; }\,{\pi }^\mathsf{T})_{u,v} \,\Longleftrightarrow \,u_2 = v_1. \end{aligned}$$

From these equivalences we get

$$\begin{aligned} \mathfrak {cyc3}_R&\,\Longleftrightarrow \,(\mathsf{L}\text{; }\,({[{\delta },{\gamma }]\!]} \text{; }\,(\rho \parallel \pi ) \text{; }\,\mathbf{M}\cap {[\![ {\mathbf{M}} , {\mathbf{M}}]} \cap { vec}(\rho \text{; }\,{\pi }^\mathsf{T}) \text{; }\,\mathsf{L}) )_{\bot ,R} \\&\,\Longleftrightarrow \,{\exists }u, v: \mathsf{L}_{\bot ,(u,v)} \wedge R_{v_2,u_1} \wedge R_{u_1,u_2} \wedge R_{v_1,v_2} \wedge u_2 = v_1\\&\,\Longleftrightarrow \,{\exists }x, y, z: R_{x,y} \wedge R_{y,z} \wedge R_{z,x}, \end{aligned}$$

where the variables u and v range over ${X^2}$ and the variables x, y and z range over X. The last formula of this calculation is the logical description of R having a cycle of length 3. $\square$

In the next theorem we present a relation-algebraic specification of the vector model $\mathfrak {cyc5}$. Precisely, it is based on the same projection relations and membership relations as Theorem 4.5 and uses two auxiliary specifications for the construction of paths.

Theorem 4.6

We consider the following relation-algebraic specifications:

$$\begin{aligned} \mathfrak {R}&:= (\pi \text{; }\,{\pi }^\mathsf{T} \parallel \rho \text{; }\,{\rho }^\mathsf{T}) \text{; }\,({[\![ {\mathbf{M}} , {\mathbf{M}}]} \cap { vec}(\rho \text{; }\,{\pi }^\mathsf{T}) \text{; }\,\mathsf{L}) : {{{{X^2}\times {X^2}}}\,\leftrightarrow \,{[{{X}\leftrightarrow {X}}]}} \\ \mathfrak {S}&:= {[\![ {{[{\rho },{\pi }]\!]} \text{; }\,\mathbf{M}} , {{[{\rho },{\pi }]\!]} \text{; }\,\mathbf{M}}]} \cap {[{\delta },{\gamma }]\!]} \text{; }\,(\pi \parallel \rho ) \text{; }\,\mathbf{M}: {{{{X^2}\times {X^2}}}\,\leftrightarrow \,{[{{X}\leftrightarrow {X}}]}} \\ \mathfrak {cyc5}&:= {( \mathsf{L}\text{; }\,(\mathfrak {R} \cap \mathfrak {S}) )}^\mathsf{T} : {{[{{X}\leftrightarrow {X}}]}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}} \end{aligned}$$

For all $R : {{X}\,\leftrightarrow \,{X}}$ then $\mathfrak {cyc5}_{R}$ iff R has a cycle of length 5.

Proof

Assume an arbitrary $R : {{X}\,\leftrightarrow \,{X}}$. Furthermore, let $u, v \in {X^2}$. First, we treat $\mathfrak {R}$ and calculate as given below, where the variables a and b range over ${X^2}$ and the variable x ranges over X:

$$\begin{aligned} \mathfrak {R}_{(u,v),R}&\,\Longleftrightarrow \,{\exists }a, b: (\pi \text{; }\,{\pi }^\mathsf{T} \parallel \rho \text{; }\,{\rho }^\mathsf{T})_{(u,v),(a,b)} \wedge ({[\![ {\mathbf{M}} , {\mathbf{M}}]} \cap { vec}(\rho \text{; }\,{\pi }^\mathsf{T}) \text{; }\,\mathsf{L})_{(a,b),R} \\&\,\Longleftrightarrow \,{\exists }a, b: (\pi \text{; }\,{\pi }^\mathsf{T})_{u,a} \wedge (\rho \text{; }\,{\rho }^\mathsf{T})_{v,b} \wedge {[\![ {\mathbf{M}} , {\mathbf{M}}]}_{(a,b),R} \wedge { vec}(\rho \text{; }\,{\pi }^\mathsf{T})_{(a,b)} \\&\,\Longleftrightarrow \,{\exists }a, b: u_1 = a_1 \wedge v_2 = b_2 \wedge \mathbf{M}_{a,R} \wedge \mathbf{M}_{b,R} \wedge a_2 = b_1 \\&\,\Longleftrightarrow \,{\exists }x: \mathbf{M}_{(u_1,x),R} \wedge \mathbf{M}_{(x,v_2),R} \\&\,\Longleftrightarrow \,{\exists }x: R_{u_1,x} \wedge R_{x,v_2} \end{aligned}$$

Hence, $\mathfrak {R}_{(u,v),R}$ specifies that there exists a path $(u_1,x,v_2)$ in R. With regard to $\mathfrak {S}$ we calculate as follows:

$$\begin{aligned} \mathfrak {S}_{(u,v),R}&\,\Longleftrightarrow \,{[\![ {{[{\rho },{\pi }]\!]} \text{; }\,\mathbf{M}} , {{[{\rho },{\pi }]\!]} \text{; }\,\mathbf{M}}]}_{(u,v),R} \wedge ({[{\delta },{\gamma }]\!]} \text{; }\,(\pi \parallel \rho ) \text{; }\,\mathbf{M})_{(u,v),R} \\&\,\Longleftrightarrow \,({[{\rho },{\pi }]\!]} \text{; }\,\mathbf{M})_{u,R} \wedge ({[{\rho },{\pi }]\!]} \text{; }\,\mathbf{M})_{v,R} \wedge ((\pi \parallel \rho ) \text{; }\,\mathbf{M})_{(v,u),R} \\&\,\Longleftrightarrow \,\mathbf{M}_{(u_2,u_1),R} \wedge \mathbf{M}_{(v_2,v_1),R} \wedge \mathbf{M}_{(v_1,u_2),R} \\&\,\Longleftrightarrow \,R_{v_2,v_1} \wedge R_{v_1,u_2} \wedge R_{u_2,u_1} \end{aligned}$$

So, $\mathfrak {S}_{(u,v),R}$ specifies that $(v_2,v_1,u_2,u_1)$ is a path in R. After these preparations we now prove the claim. We start with the following calculation, where the variables u and v range over ${X^2}$ and the variable x ranges over X:

$$\begin{aligned} \mathfrak {cyc5}_R&\,\Longleftrightarrow \,( \mathsf{L}\text{; }\,(\mathfrak {R} \cap \mathfrak {S}) )_{\bot ,R} \\&\,\Longleftrightarrow \,{\exists }u, v: \mathsf{L}_{\bot ,(u,v)} \wedge \mathfrak {R}_{(u,v),R} \wedge \mathfrak {S}_{(u,v),R} \\&\,\Longleftrightarrow \,{\exists }u, v: \mathfrak {R}_{(u,v),R} \wedge \mathfrak {S}_{(u,v),R} \\&\,\Longleftrightarrow \,{\exists }u, v: ({\exists }x: R_{u_1,x} \wedge R_{x,v_2}) \wedge (v_2,v_1,u_2,u_1) \text{ is } \text{ a } \text{ path } \text{ in } R \end{aligned}$$

It remains to verify that the last formula holds iff R has a cycle of length 5. For the direction “$\Longrightarrow$”, let the formula be true. Then $(u_1,x,v_2,v_1,u_2,u_1)$ is a cycle of length 5 in R. For the converse, suppose that R possesses a cycle $(c_1,c_2,c_3,c_4,c_5,c_1)$ of length 5. We define $u := (c_1,c_5)$, $v := (c_4,c_3)$ and $x := c_2$. Then $(u_1,x,v_2)$ and $(v_2,v_1,u_2,u_1)$ are paths in R and the formula holds. $\square$

The relation-algebraic specification of the vector model $\mathfrak {cyc7}$ is given in the next theorem. We follow the ideas of Theorem 4.6, but the realisation is far more complex. We use a further projection relation, viz. the second projection relation of the direct product $({{X^2}\times {X^2}})^2$, which we denote as $\mu : {{({{X^2}\times {X^2}})^2}\,\leftrightarrow \,{{{X^2}\times {X^2}}}}$. Furthermore, we use the auxiliary specification $\mathfrak {R}$ of Theorem 4.6 and three further auxiliary specifications.

Theorem 4.7

With $\mathfrak {R} : {{{{X^2}\times {X^2}}}\,\leftrightarrow \,{[{{X}\leftrightarrow {X}}]}}$ as defined in Theorem 4.6 we consider the following relation-algebraic specifications:

$$\begin{aligned} \mathfrak {S}&:= {[\![ {{[{\rho },{\pi }]\!]} \text{; }\,\mathbf{M}} , {{[{\rho },{\pi }]\!]} \text{; }\,\mathbf{M}}]} : {{{{X^2}\times {X^2}}}\,\leftrightarrow \,{[{{X}\leftrightarrow {X}}]}} \\ \mathfrak {T}&:= {[\![ {{[\![ {\rho \text{; }\,{\rho }^\mathsf{T}} , {\rho \text{; }\,{\pi }^\mathsf{T}}]} \text{; }\,\mathbf{M}} , {{[\![ {\pi \text{; }\,{\pi }^\mathsf{T}} , {\pi \text{; }\,{\rho }^\mathsf{T}}]} \text{; }\,\mathbf{M}}]} : {{({{X^2}\times {X^2}})^2}\,\leftrightarrow \,{[{{X}\leftrightarrow {X}}]}} \\ \mathfrak {U}&:= ({\gamma }^\mathsf{T} \parallel {\gamma }^\mathsf{T}) \text{; }\,(\mathfrak {T} \cap \mu \text{; }\,\delta \text{; }\,\mathbf{M}\cap { vec}(\delta \text{; }\,{\delta }^\mathsf{T}) \text{; }\,\mathsf{L}) : {{{{X^2}\times {X^2}}}\,\leftrightarrow \,{[{{X}\leftrightarrow {X}}]}} \\ \mathfrak {cyc7}&:= {( \mathsf{L}\text{; }\,(\mathfrak {R} \cap \mathfrak {S} \cap \mathfrak {U}) )}^\mathsf{T} : {{[{{X}\leftrightarrow {X}}]}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}} \end{aligned}$$

For all $R : {{X}\,\leftrightarrow \,{X}}$ then $\mathfrak {cyc7}_{R}$ iff R has a cycle of length 7.

Proof

Assume an arbitrary $R : {{X}\,\leftrightarrow \,{X}}$. Furthermore, let $u, v \in {X^2}$. From the proof of Theorem 4.6 we already know the following facts, where the variable x of the left equivalence ranges over X:

$$\begin{aligned} \mathfrak {R}_{(u,v),R} \,\Longleftrightarrow \,{\exists }x: R_{u_1,x} \wedge R_{x,v_2} \qquad \qquad \mathfrak {S}_{(u,v),R} \,\Longleftrightarrow \,R_{u_2,u_1} \wedge R_{v_2,v_1} \end{aligned}$$

So, we have $(\mathfrak {R} \cap \mathfrak {S})_{(u,v),R}$ iff there exists a path $(u_2,u_1,x,v_2,v_1)$ in R. In the remainder of the proof we show that $\mathfrak {U}_{(u,v),R}$ iff there is a path $(v_1,w_1,w_2,u_2)$ in R, from which then the claim follows similarly to the last step of the proof of Theorem 4.6.

First, we concentrate on $\mathfrak {T}$. Guided by its source we assume arbitrary pairs $(a, b) \in {{X^2}\times {X^2}}$ and $(c,d) \in {{X^2}\times {X^2}}$ to be given. For all $e \in {X^2}$ we then have

$$\begin{aligned} {[\![ {\rho \text{; }\,{\rho }^\mathsf{T}} , {\rho \text{; }\,{\pi }^\mathsf{T}}]}_{(a,b),e} \,\Longleftrightarrow \,(\rho \text{; }\,{\rho }^\mathsf{T})_{a,e} \wedge (\rho \text{; }\,{\pi }^\mathsf{T})_{b,e} \,\Longleftrightarrow \,a_2 = e_2 \wedge b_2 = e_1 \end{aligned}$$

and this implies

$$\begin{aligned} ({[\![ {\rho \text{; }\,{\rho }^\mathsf{T}} , {\rho \text{; }\,{\pi }^\mathsf{T}}]} \text{; }\,\mathbf{M})_{(a,b),R} \,\Longleftrightarrow \,\mathbf{M}_{(b_2,a_2),R} \,\Longleftrightarrow \,R_{b_2,a_2}. \end{aligned}$$

In the same way we show that

$$\begin{aligned} ({[\![ {\pi \text{; }\,{\pi }^\mathsf{T}} , {\pi \text{; }\,{\rho }^\mathsf{T}}]} \text{; }\,\mathbf{M})_{(c,d),R} \,\Longleftrightarrow \,\mathbf{M}_{(c_1,d_1),R} \,\Longleftrightarrow \,R_{c_1,d_1}. \end{aligned}$$

So, altogether, we get:

$$\begin{aligned} \mathfrak {T}_{((a,b),(c,d)),R}&\,\Longleftrightarrow \,{[\![ {{[\![ {\rho \text{; }\,{\rho }^\mathsf{T}} , {\rho \text{; }\,{\pi }^\mathsf{T}}]} \text{; }\,\mathbf{M}} , {{[\![ {\pi \text{; }\,{\pi }^\mathsf{T}} , {\pi \text{; }\,{\rho }^\mathsf{T}}]} \text{; }\,\mathbf{M}}]}_{((a,b),(c,d)),R} \\&\,\Longleftrightarrow \,({[\![ {\rho \text{; }\,{\rho }^\mathsf{T}} , {\rho \text{; }\,{\pi }^\mathsf{T}}]} \text{; }\,\mathbf{M})_{(a,b),R} \wedge ({[\![ {\pi \text{; }\,{\pi }^\mathsf{T}} , {\pi \text{; }\,{\rho }^\mathsf{T}}]} \text{; }\,\mathbf{M})_{(c,d),R} \\&\,\Longleftrightarrow \,R_{b_2,a_2} \wedge R_{c_1,d_1} \end{aligned}$$

Second, we concentrate on $\mathfrak {U}$ and calculate as follows, where the variables a, b, c, d and w range over ${X^2}$:

$$\begin{aligned} \mathfrak {U}_{(u,v),R}&\,\Longleftrightarrow \,( ({\gamma }^\mathsf{T} \parallel {\gamma }^\mathsf{T}) \text{; }\,(\mathfrak {T} \cap \mu \text{; }\,\delta \text{; }\,\mathbf{M}\cap { vec}(\delta \text{; }\,{\delta }^\mathsf{T}) \text{; }\,\mathsf{L}) )_{(u,v),R} \\&\,\Longleftrightarrow \,{\exists }a, b, c,d: ({\gamma }^\mathsf{T} \parallel {\gamma }^\mathsf{T})_{(u,v),((a,b),(c,d))} \\&~~~~~~~~~~~~~~ \wedge (\mathfrak {T} \cap \mu \text{; }\,\delta \text{; }\,\mathbf{M}\cap { vec}(\delta \text{; }\,{\delta }^\mathsf{T}) \text{; }\,\mathsf{L})_{((a,b),(c,d)),R} \\&\,\Longleftrightarrow \,{\exists }a, b, c,d: ({\gamma }^\mathsf{T} \parallel {\gamma }^\mathsf{T})_{(u,v),((a,b),(c,d))} \wedge \mathfrak {T}_{((a,b),(c,d)),R} \\&~~~~~~~~~~~~~~ \wedge (\mu \text{; }\,\delta \text{; }\,\mathbf{M})_{((a,b),(c,d)),R} \wedge { vec}(\delta \text{; }\,{\delta }^\mathsf{T})_{((a,b),(c,d))} \\&\,\Longleftrightarrow \,{\exists }a, b, c,d: \gamma _{(a,b),u} \wedge \gamma _{(c,d),v} \wedge R_{b_2,a_2} \wedge R_{c_1,d_1} \\&~~~~~~~~~~~~~~ \wedge (\delta \text{; }\,\mathbf{M})_{(c,d),R} \wedge (\delta \text{; }\,{\delta }^\mathsf{T})_{(a,b),(c,d)} \\&\,\Longleftrightarrow \,{\exists }a, b, c, d: a = u \wedge c = v \wedge R_{b_2,a_2} \wedge R_{c_1,d_1} \wedge \mathbf{M}_{d,R} \wedge b = d \\&\,\Longleftrightarrow \,{\exists }w: R_{w_2,u_2} \wedge R_{v_1,w_1} \wedge \mathbf{M}_{w,R} \\&\,\Longleftrightarrow \,{\exists }w: R_{v_1,w_1} \wedge R_{w_1,w_2} \wedge R_{w_2,u_2} \end{aligned}$$

Hence, we have $\mathfrak {U}_{(u,v),R}$ iff there exists a path $(v_1,w_1,w_2,u_2)$ in R as required to conclude the proof. $\square$

5 Implementation in RelView

RelView is a specific purpose computer algebra system for the manipulation and visualisation of relations, relational prototyping and relational programming. Computational tasks can be described by short and concise programs, which frequently consist of only a few lines that present the relation-algebraic expressions or formulae of the notions in question. At the beginning of Sect. 4 we have mentioned that all relation-algebraic specifications of the section rather straightforwardly can be implemented in the programming language of RelView. In the following we will demonstrate this by means of the specifications $\mathfrak {kernel}$, $\mathfrak {progFin}$ and $\mathfrak {bipartite}$.

Projection relations play a decisive role. Therefore, we start with the following two RelView-programs pr1 and pr2, which implement the two projection relations $\pi : {{{X\times Y}}\,\leftrightarrow \,{X}}$ and $\rho : {{{X\times Y}}\,\leftrightarrow \,{Y}}$ of the direct product ${X\times Y}$.

RelView knows relations as the only data type. In the above programs the parameters X and Y stand for homogeneous relations and X is assumed as carrier set of X and Y as carrier set of Y. The declaration XY = PROD(X,Y) introduces XY as name for the relational direct product $({X\times Y},\pi ,\rho )$ in the sense of [11]. In pr1 the return-clause yields the first projection relation $\pi : {{{X\times Y}}\,\leftrightarrow \,{X}}$ by means of the pre-defined RelView-operation p-1 and in pr2 the second projection relation $\rho : {{{X\times Y}}\,\leftrightarrow \,{X}}$ is obtained via the pre-defined RelView-operation p-2.

The following RelView-program par implements the parallel composition of relations. It immediately is obtained from the definition $R \parallel S := {[{\pi \text{; }\,R},{\rho \text{; }\,S}]\!]}$ using the above RelView-programs pr1 and pr2. A comparison with the definition of the parallel composition shows that * is the RelView-notation for composition, that for transposition and [ $\cdot$ , $\cdot$ |] that for right pairing.

Also the following RelView-function vec immediately follows from the definition ${ vec}(R) = {[\![ {R} , {\mathsf{I}}]} \text{; }\,\mathsf{L}$, where the pre-defined RelView-operation I computes the identity relation of the same type as its argument, the pre-defined RelView-operation dom computes the composition of its argument with an universal vector of appropriate type (i.e., a vector that models the domain of the argument) and [| $\cdot$ , $\cdot$ ] is the RelView-notation for left pairing.

We now implement $\mathfrak {kernel}$ as follows, where the parameter X of the RelView-program kernel stands for a homogeneous relation and the set X of Convention 4.1 is defined as the carrier set of X.

By means of the pre-defined RelView-operation epsi and the first two assignments the two membership relations $\mathsf{M}: {{X}\,\leftrightarrow \,{2^X}}$ and $\mathbf{M}: {{X^2}\,\leftrightarrow \,{[{{X}\leftrightarrow {X}}]}}$ are computed and stored in the variables M and MM. The third assignment computes the second projection relation $\beta : {{{X\times 2^X}}\,\leftrightarrow \,{2^X}}$ of the direct product ${X\times 2^X}$ and stores it in the variable beta. The right-hand sides of the following two assignments are the RelView-versions of the relation-algebraic specifications of $\mathfrak {stable}$ and $\mathfrak {absorb}$ of Theorem 4.1. Finally, the expression of the return-clause is the RelView-version of the relation-algebraic specification of $\mathfrak {kernel}$ of Theorem 4.1, where & means intersection, - means complementation and the pre-defined RelView-operation L1n computes a transposed universal vector $\mathsf{L}: {{\mathbf{1}{} \mathbf{1}}\,\leftrightarrow \,{Y}}$ with the target Y equal to that of the argument.

In the same way the relation-algebraic specifications of $\mathfrak {progFin}$ and $\mathfrak {bipartite}$ of Theorem 4.3 and Theorem 4.4 immediately lead to the following two RelView-programs for their computation. In progFin the variable R corresponds to the auxiliary relation $\mathfrak {R}$ of the proof of Theorem 4.3 and in bipartite the symbol | denotes union of relations.

When RelView computes a relation and displays it in the relation window, it shows in the window’s frame the number of rows, of columns and of 1-entries. Using this feature, we have obtained the numerical data of Sect. 3. The running times (in seconds) of the computations are given in Table 3. A computation of the vector model of the set of relations on X means the computation of the universal vector $\mathsf{L}: {{[{{X}\leftrightarrow {X}}]}\,\leftrightarrow \,{\mathbf{1}{} \mathbf{1}}}$. In RelView this is possible via the expression and practically needs no time (see last column of the table). For the computation of the numerical data we have used a PC with 2 CPUs of type Intel$^{\textregistered }$ Xeon$^{\textregistered }$ E5-2698, each with 20 cores and 3.60 GHz base frequency, 512 GByte RAM and running Arch Linux 5.2.0, and version 8.2 of RelView. This newest version of the tool is described at the Web-site [14] and the source code is available from Github via [15] and from Zenodo via [16]. The virtual machine of [16] was built to ease running RelView not only using Linux but also Microsoft Windows and Mac OSX.

Table 3. Running times within RelView.

The amazing computational power obtained by the use of ROBDDs and RelView becomes clear if we compare the running times of Table 3 with the times needed in case of a “classical” brute-force approach. If we assume that some algorithm could generate every relation on a given finite set X and test the existence of a kernel in, say, $10^{-6}$ seconds, it would take $5.62 \cdot 10^{14} \cdot 10^{-6}$ seconds, i.e., more than 17 years, for this task in the case of $|X| = 7$.

6 Concluding Remarks

There exist some extensions of Richardson’s theorem which allow the existence of cycles of odd length but demand certain properties for them to hold. In [1] C. Berge and P. Duchet prove that a finite directed graph $g = (X,R)$ has a kernel if every cycle of odd length has all its arcs belonging to pairs of parallel arcs, meaning for each cycle $(c_1,c_2,\ldots ,c_n,c_1)$ of odd length of g also the reversed list $(c_1,c_n,\ldots ,c_2,c_1)$ is a cycle of g, that is, all cycles of odd length are symmetric.

Although not explicitly mentioned, this criterion of Berge and Duchet includes g to be irreflexive. This becomes clear if one studies the proof of Proposition 1.1 of [1] in detail. Roughly the idea is as follows. Suppose $X = \{x_1,\ldots ,x_n\}$. From g then construct a graph $g'$ by removing all edges $(x_i,x_j)$ for which $i > j$ and also $(x_j,x_i)$ is an edge of g. Since cycles of length 1 do not occur and all cycles of odd length are assumed as symmetric, this way each cycle of odd length is split into non-cyclic paths. Hence, the graph $g'$ has no cycles of odd length. Richardson’s theorem implies that it has a kernel K and K is also a kernel of g.

In contrast to the four criteria we have mentioned in Sect. 3, testing the criterion of Berge and Duchet seems to be rather expensive since it requires to check all cycles of odd length in view of symmetry. The same holds for all other extensions of Richardson’s theorem mentioned in [1]. We also have been concerned with the question whether such weaker criteria are satisfied by much more graphs/relations with kernels than Richardson’s criterion.

To get at least a feeling for their behaviour, we have applied our approach to the criterion of Berge and Duchet and computed, again for small sets X, the set of all irreflexive relations on X such that all cycles of odd length are symmetric. In case of $1 \le |X| \le 2$ the criterion of Berge and Duchet is equivalent to that of Richardson and, hence, is satisfied by 1 respectively 4 relations on X. For $|X| = 3$ the number of relations on X which satisfy the criterion of Berge and Duchet is 50; this are 2.04% more than the 49 relations on X which satisfy Richardson’s criterion. For $4 \le |X| \le 6$ the numbers of relations on X which satisfy the criterion of Berge and Duchet are 1 778 (or 4.64% more than those which satisfy Richardson’s criterion), 161 254 (or 6.97% more than those which satisfy Richardson’s criterion) and 35 280 286 (or 8.89% more than those which satisfy Richardson’s criterion). Hence, the criterion of Berge and Duchet seems to be only slightly more general than Richardson’s criterion.

In [1] it is also mentioned that the existence of kernels already follows from the fact that (besides irreflexivety) every cycle of odd length has at least two arcs belonging to pairs of parallel arcs. This criterion is ascribed to P. Duchet. We also have checked it and RelView computed for $1 \le |X| \le 6$ the following numbers of relations on X which satisfy it: 1, 4, 56, 2 534, 348 064 and 138 636 886. Compared with Richardson’s criterion we get for $1 \le |X| \le 6$ that Duchet’s criterion is satisfied by 0%, 0%, 14.28%, 49.14%, 130.90% respectively 327.91% more relations on X than Richardson’s criterion. Despite these better percentages it still seems to be very far away from a characterisation of the class of directed graphs having kernels. E.g., in case $|X| = 6$ it is satisfied by only 0.9% of the graphs of this class.