Domain Range Semigroups and Finite Representations

Abstract

Relational semigroups with domain and range are a useful tool for modelling nondeterministic programs. We prove that the representation class of domain-range semigroups with demonic composition is not finitely axiomatisable. We extend the result for ordered domain algebras and show that any relation algebra reduct signature containing domain, range, converse, and composition, but no negation, meet, nor join has the finite representation property. That is any finite representable structure of such a signature is representable over a finite base. We survey the results in the area of the finite representation property.

J. Šemrl—The author thanks Professor Robin Hirsch for supervision and insightful conversations about the work presented.

1 Introduction

Formal reasoning about programs and their correctness is an important, yet a demonstrably difficult task and many well known approaches have been proposed. Algebraically speaking, a deterministic program is a partial function mapping from the state space to itself. Generalising this, to account for nondeterminism, we can say that a program (deterministic or nondeterministic) is a binary relation over the state space. This ability to naturally express such concepts motivates the endeavour of formalising the logic of binary relations.

A formalisation of this sort is found in Relation Algebra, obtained by extending the language of Boolean Algebra with operations specific to binary relations. This enables us to reason about the behaviour of binary relations in an abstract manner. However, these algebras are also very badly behaved, with an abundance of undecidability results, see [6, Part V]. A possible way of combating this is by dropping some operations from the language, sacrificing the ability to encapsulate the behaviour of relational calculus in exchange for decidability of certain decision problems. We will formally define some of these and how to prove positive properties later in this section.

Here we examine some of these favourable properties, or lack thereof, for languages containing domain and range, and put them in the bigger context of relation algebra reduct languages. We chose this subset of languages as they were found useful in algebraically reasoning about correctness of nondeterministic programs, see Sect. 2 for more details.

But first, some definitions. Let X be a base set. Domain ($\mathrm {D}$) and range ($\mathrm {R}$) are operations, defined for some relation $R \subseteq X \times X$ as

$$\mathrm {D}(R) = \{(x,x) \mid \exists y: (x,y) \in R\} \quad \;\, \mathrm {R}(R) = \{(y,y) \mid \exists x: (x,y) \in R\}$$

and together with composition, they form the signature of domain-range semigroups. However, relational composition is not always interpreted in the same way. Two examples of interpretations include the angelic or ordinary composition (denoted ; ) and demonic composition (denoted $*$), defined below for $R,S \subseteq X \times X$

$$\begin{aligned} \begin{array}{c} R;S = \{(x,z) \mid \exists y: (x,y) \in R \wedge (y,z) \in S\} \\ R*S = \{(x,y) \in R;S \mid \forall z: (x,z) \in R \Rightarrow (z,z) \in \mathrm {D}(S)\} \end{array} \end{aligned}$$

Whilst the first definition seems pretty intuitive, the second one may appear a bit odd, even arbitrary, so let us have a closer look. The operation is motivated in the behaviour of a nondeterministic machine when the demon is in control of nondeterminism. Imagine the relations R, S were programs over the state space X. The pair $(x,y) \in R;S$ is included in $R*S$ if and only if there is no run from R to some z from which S aborts or loops forever, i.e. $(z,z) \notin \mathrm {D}(S)$. Should such a run exist, the demon will take the opportunity and abort the computation. For more details on this refer to [9].

Any $\{D,R,;\}$- or $\{D,R,*\}$-structure $\mathcal {S}$ with an underlying set $S \subseteq \wp (X \times X)$ for some base X and operations interpreted relationally (as defined above) is proper. Let $\tau$ be a signature of operations that are well defined for binary relations. The representation class for $\tau$, denoted $R(\tau )$, is the class of all proper $\tau$-structures, closed under isomorphic copies. An isomorphism $\theta$ that maps a representable structure to a proper structure is called a representation.

A representation is finite if the base set X of the proper image is finite. If all finite members of $R(\tau )$ have finite representations, we say that the signature has the finite representation property (FRP).

The two properties described above are of special interest to us. This is because they both guarantee the decidability of determining membership in $R(\tau )$ for finite structures, also known as the representability decision problem. Although the properties both ensure decidability of the said decision problem, they in no way follow from each other. This provides us with two non trivial questions for each Relation Algebra reduct language that, given either is answered affirmatively, provide us with a decidability guarantee.

Here, we answer [12, Question 4.9] and show that $R(D,R,*)$ is not finitely axiomatisable. We do so by defining a two-player game that corresponds to a recursively enumerable axiomatisation of the representation class. Then we show that for each finite subset of this axiomatisation has a non-representable model. By compactness of first order logic, we are able to reach a contradiction under the assumption of finite axiomatisability.

Then we show that any relation algebra reduct signature containing domain, range, converse and composition, but no negation, meet, nor join has the finite representation property. This is an extension of a previous finite representation property result for ordered domain algebras [5]. We conclude by putting the result in a larger context of finite representation property for all reduct signatures of relation algebra. We survey the existing results and raise some open questions in the area.

2 Motivation and Context

In this section we take a closer look at the related work and motivate the problems. We have seen that structures of relations provide us with a natural way of formally reasoning about nondeterministic programs [4]. In [3], a good intuition on how to use structures with domain and range to model program control flow using semigroups with domain and range – functional for deterministic, and relational for nondeterministic programs. This allows us to express partial correctness equationally.

However, to extend this to total correctness, we have to turn to the demon. Demonic calculus was introduced to model the behaviour of programs, should the demon be in control of making nondeterministic decisions. Recently, it has been shown we may take this to our advantage and introduce equations to model total correctness. One such approach expresses total correctness using the domain and demonic composition [8] and another using ordinary composition and the bottom element of the demonic lattice [9].

These applications motivate our search for computational guarantees. As we have discussed, this includes looking for finite axiomatisability of the representation class and the finite representation property. A major negative result is shown with $R(\mathrm {D},\mathrm {R},;)$ and $R(\mathrm {D}, ;)$ having no finite axiomatisation [7].

Both of these two signatures have the finite representation property open. However, one may add the partial ordering, converse, the identity, and the empty relation to obtain the signature of ordered domain algebras. Surprisingly, this signature has both the finite representation property, as well as a finitely axiomatisable representation class [5]. Another interesting result is the axiomatisation of $R(\mathrm {D}, *)$ is not only finite, but also the same as that of representable domain semigroups of partial functions [11]. Furthermore, the equational theories of both $R(\mathrm {D}, \mathrm {R}, ;)$ and $R(\mathrm {D}, \mathrm {R}, *)$ are finitely axiomatisable [12].

Finally, it is important to note that although the finite axiomatisability of the representation class and the finite representation property both guarantee the decidability of the representation decision problem, neither is stronger or weaker than the other. We have seen an example of a signature with both properties in the ordered domain algebras, as well as the full signature of relation algebras with neither property. However, you can find signatures with finitely axiomatisable representation class but no FRP, like meet-lattice semigroups [2, 14], and semigroups with demonic refinement [10] with FRP, but non finitely axiomatisable representation class.

3 Networks and Representation by Games

In this section we outline a representation game that will help us prove the non finite axiomatisability result of $R(\mathrm {D},\mathrm {R},*)$. This argument is based on [6], but defined for this specific signature. The proofs presented are outlines, however, they are more detailed in parts where it is necessary to show the argument can be feasibly used to show results for demonic composition. For full details of proofs, see [6, Chapter 7].

On an intuitive level, this approach entails defining a game where a player is challenged to build a representation, on a step by step basis over a predetermined number of moves. The design of our game must be such that the player challenged will have a winning strategy if and only if they can survive the game of any length.

We then, for every natural number, define a formula that corresponds to a winning strategy for a game of that length. This means that we have defined a recursively enumerable theory that axiomatises the representation class.

In later sections we define, for each length of the game, an unrepresentable structure where the player challenged has got the winning strategy. This will enable us to use the compactness of first order logic to reach a contradiction under the assumption of finite axiomatisability.

Now, we will define these concepts more formally. A network $\mathcal {N} = (N, \bot , \top )$ where $\bot , \top : N \times N \rightarrow \wp (\mathcal {S})$ and $\mathcal {S}$ is some $\{\mathrm {D}, \mathrm {R}, *\}$-structure. We say it is consistent if and only if

$$\begin{aligned} \begin{array}{c} \forall x,y \in N: \top (x,y) \cap \bot (x,y) = \emptyset \\ \forall x, y \in N, \forall s,t \in \mathcal {S}: \Big ( s \in \top (x,y) \wedge \big (s = \mathrm {D}(t) \vee s = \mathrm {R}(t)\big )\Big ) \Rightarrow x=y \end{array} \end{aligned}$$

Now, let us define for any $a,b \in \mathcal {S}$ the two networks $\mathcal {N}_{ref}[a,b]$ and $\mathcal {N}_{nref}[a,b]$ as follows

$$\begin{aligned} \begin{array}{c} \mathcal {N}_{ref}[a,b] = (\{x\}, \{(x,x) \mapsto \{b\}\}, \{(x, x) \mapsto \{a\}\})\\ \mathcal {N}_{nref}[a,b] = (\{x,y\}, \{(x,y) \mapsto \{b\}\}, \{(x,y) \mapsto \{a\}\}) \end{array} \end{aligned}$$

And all other pairs map to $\emptyset$ for $\top ,\bot$.

We also define two operations $+_\top [\mathcal {N},x,y,a], +_\bot [\mathcal {N},x,y,a]$ which take a network $\mathcal {N}= (N,\bot , \top )$, some $x,y \in N \dot{\cup }\{x_+\}$ and some $a \in \mathcal {S}$ and return

$$\begin{aligned} +_\top [\mathcal {N},x,y,a] = (N \cup \{x,y\}, \bot , \top ^+)\\ +_\bot [\mathcal {N},x,y,a] = (N \cup \{x,y\}, \bot ^+, \top ) \end{aligned}$$

where $\top ^+(v,w)$ is the same as $\top (v,w)$, or $\emptyset$ (if $\top (v,w)$ is undefined), for all v, w, except for x, y where a is also added to $\top ^+(x,y)$. Similarly for $\bot ^+$.

A network $\mathcal {N}' = (N',\top ', \bot ')$ is said to extend $\mathcal {N}= (N, \top , \bot )$, denoted $\mathcal {N}\subseteq \mathcal {N}'$ if and only $N \subseteq N'$ and for all $x,y \in N$ we have $\top (x,y) \subseteq \top '(x,y), \bot (x,y) \subseteq \bot '(x,y)$. Clearly, both $+_\top , +_\bot$ for $\mathcal {N}$ with any operands are extensions of $\mathcal {N}$. Furthermore, observe how inconsistency is inherited under extensions.

We can now define a game for a $\{D,R,*\}$-structure $\mathcal {S}$. It is played by two players $\forall , \exists$, we will call them Abelard and Eloise. The game, denoted $\varGamma _n(\mathcal {S})$, starts with the initialisation (zeroth) move and then continues for n moves where $0 < n \le \omega$. Let $k \le n$. At kth move $\forall$ challenges $\exists$ to return a $\mathcal {N}_k$ such that $\mathcal {N}_0 \subseteq \mathcal {N}_1 \subseteq ... \subseteq \mathcal {N}_n$. $\forall$ wins the game if and only if $\exists$ introduces an inconsistent network.

Initialisation. $\forall$ picks a pair $a \ne b \in \mathcal {S}$ and $\exists$ returns $\mathcal {N}_0$ that is an extension of $\mathcal {N}_{ref}[a,b]$, $\mathcal {N}_{nref}[a,b]$, $\mathcal {N}_{ref}[b,a]$ or $\mathcal {N}_{nref}[b,a]$.

Witness Move. $\forall$ picks a pair of nodes x, z in the network $\mathcal {N}_k$ and a pair of elements $a,b \in \mathcal {S}$ such that $a * b \in \top (x,z)$. $\exists$ picks a $y \in N \dot{\cup }\{x_+\}$ and returns $\mathcal {N}_{k+1} \supseteq +_\top [+_\top [\mathcal {N},x,y,a],y,z,b]$, see Fig. 1 left.

Fig. 1.

Witness move (left) and composition-domain move (right)

Composition-Domain Move. $\forall$ picks, some x, y, z with $a \in \top (x,y)$ and $a * b \in \top (x,z)$ and $\exists$ must return $\mathcal {N}_{k+1} \supseteq +_\top [\mathcal {N}, y, y, \mathrm {D}(b)]$, see Fig. 1 right.

Composition Move. $\forall$ picks some $x,y,z \in \mathcal {N}_k$ along with a, b such that $a \in \top (x,y)$ and $b \in \top (y,z)$. $\exists$ has a choice between returning $\mathcal {N}_{k+1} \supseteq +_\top [\mathcal {N}, x, z, a * b]$ (Fig. 2 left) and $\mathcal {N}_{k+1} \supseteq +_\bot [+_\top [\mathcal {N},x,w,a],w,w,\mathrm {D}(b)]$ where she picks a $w \in N \dot{\cup }\{x_+\}$ (Fig. 2 right).

Fig. 2.

Composition move

Domain-Range Move. $\forall$ picks $x,y \in N_n, a \in \mathcal {S}$ such that $a \in \top (x,y)$ and $\exists$ must return $\mathcal {N}_{k+1} \supseteq +_\top [+_\top [\mathcal {N},x,x,\mathrm {D}(a)],y,y, \mathrm {R}(a)]$.

Domain Move. $\forall$ picks a node x and an $a \in \mathcal {S}$ such that $\mathrm {D}(a) \in \top (x,x)$ and $\exists$ must pick a node $y \in N \dot{\cup }\{x_+\}$ and return $\mathcal {N}_{k+1} \supseteq +_\top [\mathcal {N},x,y,a]$

Range Move. $\forall$ picks a node y and an $a \in \mathcal {S}$ such that $\mathrm {R}(a) \in \top (y,y)$ and $\exists$ must pick a node $x \in N \dot{\cup }\{x_+\}$ and return $\mathcal {N}_{k+1} \supseteq +_\top [\mathcal {N},x,y,a]$

Lemma 1

A countable $\{\mathrm {D}, \mathrm {R}, *\}$-structure is representable if and only if $\exists$ has a winning strategy for $\varGamma _\omega (S)$.

Proof

If the structure is representable, $\exists$ can play the game by mapping the responses from the representation. Conversely, if $\exists$ has a winning strategy for $\varGamma _\omega (\mathcal {S})$, she must also have the winning strategy for any length of the game where $\forall$ schedules moves in the way that eventually every move will be called and the $\top$ label of the network will in the limit be closed under composition, domain-range moves and saturated under witness, domain and range moves. Since the structure is countable, $\forall$ can schedule moves in this manner. Take the limit network, call it $\mathcal {N}_\omega [a \ne b]$, after such a play with the initialisation pair $a \ne b$. Observe how due to saturation and closure, the $\top$ outlines a mapping from $\mathcal {S}$ to $N \times N$ that represents $\mathrm {D}, \mathrm {R}, *$ correctly and ensures that a, b map to different relations. Thus a disjoint union $\dot{\bigcup }_{a \ne b} \mathcal {N}_\omega [a \ne b]$ is a representation of $\mathcal {S}$.    $\square$

Lemma 2

For every $n<\omega$, there exists a first order formula $\sigma _n$ such that $\exists$ has a winning strategy for $\varGamma _n(\mathcal {S})$ if and only if $\mathcal {S}\models \sigma _n$. Furthermore, the first order theory $\varSigma = \{\sigma _i \mid i < \omega \}$ axiomatises $R(\mathrm {D}, \mathrm {R}, *)$.

Proof

Let us define a variable network in a slightly different manner with the mappings $\top , \bot : N \times N \rightarrow \wp (\mathrm {Vars})$. A valuation $v: \mathrm {Vars} \rightarrow \mathcal {S}$ defines a conventional network $v(\mathcal {N})$. This allows us to define a formula $\phi _n(\mathcal {N})$ in a way that, together with a valuation $v: \mathcal {S}\rightarrow \mathrm {Vars}$, $\exists$ can survive the conservative play of the game for n more moves, starting from $v(\mathcal {N})$. By conservative, we mean that $\exists$ plays the network requested without proper extensions.

In the base case, observe how $v(\mathcal {N})$ only needs to be consistent and thus

$$ \phi _0(\mathcal {N}) = \bigwedge _{{\begin{array}{cc} x \ne y \in N \\ s \in \top (x,y) \end{array}}} \lnot \exists t: s = \mathrm {D}(t) \vee s = \mathrm {R}(t) \;\;\wedge \bigwedge _{{\begin{array}{cc} x, y \in N \\ s \in \top (x,y) \\ t \in \bot (x,y) \end{array}}} s \ne t $$

In the induction case, if $\phi _n[\mathcal {N}]$ signifies that $\exists$ can survive for n more moves, simply define $\phi _{n+1}$ as

$$\begin{aligned} \phi _{n+1}(\mathcal {N}) =&\bigwedge _{{\begin{array}{cc} x,z \in N \\ s \in \top (x,z) \end{array}}} \!\forall t,u: s = t * u \Rightarrow \bigvee _{y \in N \dot{\cup }\{x_+\}} \phi _n(+_\top [+_\top [\mathcal {N}, x,y,a],y,z,b])\\&\wedge \bigwedge _{{\begin{array}{cc} x,y,z \in N \\ t \in \top (x,y), u \in \top (y,z) \end{array}}} \forall s: s = t * u \rightarrow \Bigg ( \phi _n(+_\top [\mathcal {N}, x,z, s] \\&\quad \;\,\vee \; \forall v: v = \mathrm {D}(t) \Rightarrow \bigvee _{w \in N\dot{\cup }\{x_+\}}\phi _n(+_\bot [+_\top [\mathcal {N},x,w,t],w,w,v]) \Bigg )\\&\wedge \bigwedge _{{\begin{array}{cc} x,y,z \in N \\ t \in \top (x,y) \\ s \in \top (x,z) \end{array}}} \forall u,v: (s = t * u \wedge v = \mathrm {D}(u)) \Rightarrow \phi _n(+_\top [\mathcal {N},y,y,v])\\&\wedge \bigwedge _{{\begin{array}{cc} x,y \in N \\ s \in \top (x,y) \end{array}}} \forall t,u: \Big (t = \mathrm {D}(s) \wedge u = \mathrm {R}(s)) \Rightarrow \\&\qquad \qquad \qquad \qquad \qquad \phi _n(+_\top [+_\top [\mathcal {N},x,x,t],y,y,u]\Big )\\&\wedge \bigwedge _{{\begin{array}{cc} x \in N \\ s \in \top (x,x) \end{array}}} \forall t: \mathrm {D}(t) = s \Rightarrow \bigvee _{y \in N\dot{\cup }\{x_+\}}\phi _n(+_\top [\mathcal {N},x,y,t])\\&\wedge \bigwedge _{{\begin{array}{cc} y \in N \\ s \in \top (y,y) \end{array}}} \forall t: \mathrm {R}(t) = s \Rightarrow \bigvee _{x \in N\dot{\cup }\{x_+\}} \phi _n(+_\top [\mathcal {N},x,y,t]) \end{aligned}$$

Thus $\exists$ can win a conservative game $\varGamma _n(\mathcal {S})$ if and only if $\mathcal {S}\models \sigma _n$ where

$$\begin{aligned} \sigma _n = \forall s,t: s \ne t \Rightarrow \bigg (&\phi _n(\mathcal {N}_{ref}[a,b]) \vee \phi _n(\mathcal {N}_{nref}[a,b])\\ {}&\vee \phi _n(\mathcal {N}_{ref}[b,a]) \vee \phi _n(\mathcal {N}_{nref}[b,a])\bigg ) \end{aligned}$$

Since inconsistencies in networks are inherited in extensions, it is true that for countable structures if $\exists$ has a winning strategy for conservative plays of $\varGamma _n(\mathcal {S})$, she will also have a winning strategy for any play of $\varGamma _n(\mathcal {S})$. Furthermore, as inconsistency is inherited in extensions, if $\mathcal {S}\models \varSigma$, $\exists$ has a winning strategy for $\varGamma _\omega (\mathcal {S})$. Thus for all countable $\mathcal {S}$, $\mathcal {S}\in R(\mathrm {D}, \mathrm {R}, *)$ if and only if $\mathcal {S}\models \varSigma$. As the representation class is pseudoelementary, it is closed under elementary equivalence, and by Löwenheim-Skolem Theorem, we conclude $\mathcal {S}\models \varSigma$ is both sufficient and necessary for membership, even for uncountable structures.    $\square$

4 Demonic Refinement

Before we move on to defining structures used to prove non finite axiomatisability, we will quickly have a look at the demonic lattice. We discuss in Sect. 2 that the demonic lattice has found use in algebraically modelling total correctness. However, in this section, it will help us show that the structures we will use in the argument are in fact non-representable.

We do so by defining demonic refinement, the partial ordering predicate arising from the demonic lattice. Furthermore, we observe that even though the predicate is not in the signature, some pairs of elements of a representable $\{\mathrm {D},\mathrm {R},*\}$-structure will always be represented as demonic refinement pairs.

Now assume that a $\{\mathrm {D}, \mathrm {R}, *\}$-structure has a cycle of elements where each element is a demonic refinement of its successor. As the predicate is a partial order, it means by antisymmetry and transitivity that these distinct elements will map the same binary relation in any representation and thus the structure is not representable.

Now let us define demonic refinement for $R,S \subseteq X \times X$ as

$$R \sqsubseteq S \Longleftrightarrow (\mathrm {D}(S) \subseteq \mathrm {D}(R) \wedge \mathrm {D}(S);R \subseteq S)$$

This is motivated, again, with the demon in control of nondeterminism. Imagine R, S were programs over the state space X. If the demon is given the choice to run R or S, he will always run S. This is because when we are outside the domain of S, running S rather than R will result abort and when in the domain of S it will maximise the odds of reaching an erroneous state.

Now we recursively define a predicate $\preceq$ using infinitary $\{\mathrm {D},\mathrm {R},*\}$-formula such that for every structure $\mathcal {S}$ with a representation $\theta$ we will have $\forall s,t \in \mathcal {S}: s \preceq t \Rightarrow s^\theta \sqsubseteq t^\theta$. We take advantage of the fact that sometimes non domain elements may compose to a domain element, and define $\preceq _1$. Then we inductively close the predicate under monotonicity and transitivity. More formally, we say that

$$s \preceq _1 t \Longleftrightarrow \exists u,v: \mathrm {D}(u * v) = u * v \wedge s = \mathrm {R}(u * \mathrm {D}(v)) \wedge t = s * v * u$$

$$s \preceq _{n+1} t \Longleftrightarrow \left( \begin{array}{rl} &{} \exists s',t',u,v: s' \preceq _n t' \wedge s = u * s' * v \wedge t = u * t' * v\\ \vee &{} \exists v: s \preceq _n v \wedge v \preceq _{n} t \end{array}\right) $$

and $\preceq = \bigcup _{n<\omega } \preceq _n$

Lemma 3

For any $s,t \in \mathcal {S}$, if $s \preceq t$, it is true that for any representation $\theta$ we have $s^\theta \sqsubseteq t^\theta$.

Proof

We show this by induction over n.

In the base case, we see that there exists a u, v such that $u * v = \mathrm {D}(u * v)$ and $s = \mathrm {R}(u * \mathrm {D}(v))$ and $t = s * v * u$. First see how if $(x,x) \in t^\theta$, there must exist a witness for $s * v * u$ and since s is a range element, it must hold that $(x,x) \in s^\theta$. Since $\mathrm {D}(s^\theta ) = s^\theta$, we have $\mathrm {D}(t^\theta ) \subseteq \mathrm {D}(s^\theta )$. Furthermore, assume that $(x,x) \in \mathrm {D}(t^\theta )$ and $(x,x) \in s^\theta$. See how there must exist a y such that $(y,x) \in (u * \mathrm {D}(v))^\theta$. There must also exist a z such that $(x,z) \in v^\theta$. Since $(y,y) \in \mathrm {D}(u * \mathrm {D}(v))^\theta$, we can see that $(y,z) \in (u * v)^\theta$ and since $u * v$ is a domain element, $y = z$. And because $(x,x) \in \mathrm {D}(t)^\theta$ and because $(x,z) \in (s * v)^\theta$ and $(z,x) \in u^\theta$, we conclude $(x,x) \in (s * v * u)^\theta = t^\theta$.

The induction case follows from the fact that $\sqsubseteq$ is transitive as well as left and right monotone for $*$ as discussed in [10].    $\square$

The use of refinement cycles may seem similar to [7] where the predicate $\triangleleft$ is defined as the monotone, transitive closure of $\mathrm {D}(s); \mathrm {D}(t) \triangleleft \mathrm {D}(t)$ to signify ordinary inclusion ($\le$) for the angelic signature. However, for the demonic signature, $\triangleleft$ can be simply described as $\mathrm {D}(s) * t \triangleleft t$ as the following axiom is sound

$$\begin{aligned} \forall s,t: \mathrm {D}(s * \mathrm {D}(t)) * s = s * \mathrm {D}(t)\end{aligned}$$

Thus, $\triangleleft$ does not show useful when trying to show $R(\mathrm {D}, \mathrm {R}, *)$ is not finitely axiomatisable, as avoiding cycles of $\triangleleft$ can be described in a single axiom.

5 $R(\mathrm {D},\mathrm {R},*)$ is Not Finitely Axiomatisable

We can now define the non representable structures for every $n<\omega$ for which $\exists$ will have a winning strategy in $\varGamma _n$. First we use the demonic refinement predicate, defined in Sect. 4, to show these are not representable as they include a refinement cycle. Then we show by induction that $\exists$ will have a winning strategy for n moves in the representation game. Using the compactness trick, we show that the representation class is not finitely axiomatisable.

For every $n < \omega$, let $N=2n+1$. Define a $\{\mathrm {D}, \mathrm {R}, *\}$-structure $\mathcal {S}_n$, with the following underlying set

$$\{0,d,r\} \cup \{m_i,\varepsilon _i, a_i,b_i,c_i,d_i,ac_i,acd_i,cdb_i, db_i, ab_i \mid 0 \le i < N \}$$

$0,d,r,m_i, \varepsilon _i$ are the domain-range elements, idempotent with respect to composition, and disjoint, i.e. composition of two distinct domain-range elements evaluates to 0. We now examine domain-range elements, see visualisation in Fig. 3. For all $i < N$, we have

$$\begin{aligned} \begin{array}{c} d = \mathrm {D}(a_i) = \mathrm {D}(ac_i) = \mathrm {D}(acd_i) = \mathrm {D}(ab_i) \\ m_i = \mathrm {D}(c_i) = \mathrm {D}(b_i) = \mathrm {D}(cdb_i) = \mathrm {R}(a_i) = \mathrm {R}(d_i) = \mathrm {R}(cd_i)\\ \varepsilon _i = \mathrm {D}(d_i) = \mathrm {D}(db_i) = \mathrm {R}(c_i) = \mathrm {R}(ac_i)\\ r = \mathrm {R}(ab_i) = \mathrm {R}(cdb_i) = \mathrm {R}(db_i) = \mathrm {R}(b_i) \end{array} \end{aligned}$$

The reader may find it helpful to pay close attention to Fig. 3 while we define the compositions. First, we say that

$$ d_i* c_i = \varepsilon _i \qquad \quad c_i * d_i = cd_i \qquad \quad cd_i * cd_i = cd_i $$

for every $i<N$. Furthermore, some elements will result in a composition with an index increasing by one, namely

$$a_i * cdb_i = ab_{i+1} \quad \;\, acd_i * cdb_i = ab_{i+1} \quad \;\, ac_i * db_i = ab_{i+1} \quad \;\, acd_i * b_i = ab_{i+1} $$

for $i<N$ where $+$ denotes addition modulo N. Composition results below are defined more naturally

$$ \begin{array}{ccccc} cd_i * c_i = c_i \;\;\,&{}\;\;\, d_i * cd_i = d_i \;\;\,&{}\;\;\, a_i * b_i = ab_i \;\;\,&{}\;\;\, a_i * c_i = ac_i \;\;\,&{}\;\;\, a_i * cd_i = acd_i \\ c_i * db_i = cdb_i &{} d_i* b_i = db_i &{} ac_i * d_i = acd_i &{} acd_i * c_i = ac_i &{} cd_i * b_i = cdb_i \end{array} $$

All other compositions are either the mandatory domain-range compositions or they evaluate to 0.

The following two Lemmas will now show that although $\mathcal {S}_n$ is not representable, $\exists$ will be able to maintain consistency in the network for n moves.

Fig. 3.

Visualisation of $\mathcal {S}_n$

Lemma 4

$\mathcal {S}_n$ is not $\{\mathrm {D}, \mathrm {R}, *\}$-representable.

Proof

Observe how $m_i \preceq c_i * d_i$ and thus $ab_i = a_i * m_i * b_i \preceq a_i * c_i * d_i * b_i = ab_{i+1}$ for all $i < N$. This means by transitivity of $\preceq$ that for all $i,j < N$ we have $ab_i \preceq ab_j$. Now assume that there existed a representation $\theta$. We would have $ab_i^\theta \sqsubseteq ab_j^\theta , ab_j^\theta \sqsubseteq ab_i^\theta$, even where $i \ne j$. Since $\sqsubseteq$ is antisymmetric, we would have $ab_i^\theta = ab_j^\theta$ for $i \ne j$. Therefore, no such $\theta$ can exist.    $\square$

Lemma 5

For all $n < \omega$, $\exists$ has a winning strategy for $\varGamma _n(\mathcal {S}_n)$

Proof

First see how $\exists$ may play in a way that she returns a network that is closed under composition, composition domain and domain-range moves. For composition moves, she always chooses to add $a*b$ to the label, rather than adding a node with D(b) in its $\bot$ label. Furthermore, she may set the $\top$ label in a way that for all (x, y)

$$\top _{k+1} \subseteq \top _{k}(x,y) \cup \{ ab_{i+1} \mid ab_i \in \top _k(x,y) \}$$

where $+$ is modulo N and

$$\begin{array}{cc} a_i \in \top _k(x,y) \Rightarrow acd_i \in \top _k(x,y)\;\; &{}\;\; m_i \in \top _k(x,y) \Rightarrow cd_i \in \top _k(x,y)\\ b_i \in \top _k(x,y) \Rightarrow cdb_i \in \top _k(x,y)\;\; &{}\;\; 0 \notin \top (x,y) \end{array}$$

as well as ensure that domain-range elements are only added to reflexive edge $\top$ labels. If $m_i \in \top (x,x)$, there exists at most one y such that $c_i \in \top (x,y) \vee d_i \in \top (y,x)$ and if $cd_i \in \top (x,x')$, the y must be the same for $x, x'$. to prevent compositional closure from adding $m_i$ to a $\top (z,w), z \ne w$.

In the base case, observe how for every $s \ne t$, it is possible to find either s or t to put in $\top (x,y)$ of the initialisation network. Without loss, if $s = 0$ or $s=a_i, t=acd_i$ or $s=m_i, t = cd_i$ or $s=b_i, t=cdb_i$ she has to play t. Otherwise, she is free to play either s or t, making sure that she plays the reflexive network if and only if she opts to play a domain-range element.

Fig. 4.

Compositions with $cd_i$

In the induction case, as the network is closed under domain-range, composition and composition-domain moves, $\forall$’s only non-redundant move options are composition, domain, and range.

For the domain move, $\exists$ may add a new node unless $c_i$ is requested on some x. In that case, she must pick to add $c_i$ to $\top (x,y)$ to the designated y if such y exists, otherwise create such a y and close it under all the necessary moves to maintain the induction hypothesis. All the compositions resulting in $cd_i, acd_i, cdb_i$ are included in the appropriate labels due to her strategy, see Fig. 4. Otherwise the move can be satisfied with a new node, satisfying all the properties in $\exists$’s strategy. Similarly, the argument can be constructed for range moves including $d_i$ or otherwise.

In case a witness move is called and the left operand is $c_i$ or the right operand is $d_i$ (or both), the witness node returned must be the designated y and the induction hypothesis is maintained (again, see Fig. 4). If the witness move has $cd_i$ as an operand, she makes sure to designate the appropriate y, again preserving the induction hypothesis. All other non-redundant operations result in $ab_i$. If the index of the operands is $i-1$, $\exists$ may ensure she does not include $a_{i-1}*b_{i-1}$ witness (see Fig. 5 left). Finally, for operands with index i she adds a witness node with $m_i, cd_i$ in the reflexive label, $a_i, acd_i$ on the left and $b_i, cdb_i$ on the right (see Fig. 5 right). This covers all the possible non-redundant witness moves, but results in $ab_{i+1}$ being added to the label. In any case, the induction hypothesis is maintained.

Fig. 5.

Witness moves for $ab_i$ with $i-1$ left and i on the right

We have now seen that $\exists$ can play a game in a way that the only possible inconsistency that can arise is from $ab_i \in \top (x,y)$ and also in $\bot (x,y)$. Without loss, this situation can only arise when the initialisation pair is $ab_0, ab_{n+1}$. In this case she plays the initial non-reflexive network with $ab_0 \in \top (x,y), ab_{n+1} \in \bot (x,y)$. As she can only increase the maximal i such that $ab_i \in \top (x,y)$ by 1 each move, she introduces an inconsistency at the $n+1$st move at the earliest. Thus she can win $\varGamma _n(\mathcal {S}_n)$.    $\square$

This gives us all we need to conclude

Theorem 1

$R(\mathrm {D}, \mathrm {R}, *)$ cannot be axiomatised by a finite first order theory.

Proof

Suppose such a theory existed, call it $\varPsi$. Then $R(\mathrm {D}, \mathrm {R}, *)$ is axiomatised by a single axiom $\psi = \bigwedge _{\psi ' \in \varPsi } \psi '$. Thus $\varSigma \cup \{\lnot \psi \}$ is not consistent as, by Lemma 2, $\varSigma$ ensures that any model of it is representable and $\lnot \psi$ ensures it is not. Now look at any finite subtheory $\varOmega \subseteq \varSigma \cup \{\lnot \psi \}$. Observe how, since it is finite, there exists $n < \omega$ such that for all $m>n$ we have $\sigma _m \not \in \varOmega$. Thus $\mathcal {S}_n \models \varOmega$ as by Lemmas 5, 2 we have $\mathcal {S}_n \models \sigma _i, i\le n$, and by Lemmas 1, 4 we have $\mathcal {S}_n \models \lnot \psi$. By compactness of first order logic, we conclude the Theory $\varSigma \cup \{\lnot \psi \}$ is consistent and we have reached a contradiction.    $\square$

6 Finite Representation Property

We have now seen that both the angelic and demonic representable domain-range semigroups cannot be axiomatised finitely. However, it remains unknown if all finite members of $R(\mathrm {D}, \mathrm {R}, ;)$ and $R(\mathrm {D}, \mathrm {R}, *)$ have the finite representation property. Although the finite axiomatisability (or lack thereof) is known for a number of representation classes [13], FRP remains largely unknown for signatures with composition. In this section we discuss some existing results and extend FRP result for ordered domain algebras [5].

The known results regarding FRP are summarised in Table 1. The signatures $\{;\}, \{1',;\}, \{\mathrm {D}, *\}$ are well known examples where Cayley representation for groups can be used to represent the structure over a finite base. Neuzerling shows that any signature containing meet and composition fails to have FRP using Point Algebra [14]. In [10] we show that this structure can also be used to show that FRP fails for any signature containing negation, partial order and composition. In a forthcoming paper, we extend this result to any signature containing $\{-, ;\}$.

Table 1. Signatures with composition where FRP is known

A simple approach to constructing a finite representation of a relational partially ordered semigroup was proposed by Zareckiĭ in [16] where one may amend a representable $\{\le , ;\}$-structure $\mathcal {S}$ with a compositional identity element e and only add the mandatory (e, e) to $\le$ to then define a simple representation $\theta$ over the base $\mathcal {S}$ with

$$(s,t) \in a^\theta \Longleftrightarrow t \le s;a$$

The inclusion of e ensures faithfulness as for $a \not \le b$ $(e,a) \in a^\theta \setminus b^\theta$ and the associativity and monotonicity ensure that $\le , ;$ are correctly represented.

Egrot and Hirsch [5] amend the idea to represent the ordered domain algebras, the signature $\{0, \mathrm {D}, \mathrm {R}, \le , 1', \smile , ;\}$ where 0 is the empty relation (bottom element of the Boolean lattice), $1'$ is the relational identity and $\smile$ is the relational converse. They represent the structures in $R(0, \mathrm {D}, \mathrm {R}, \le , 1', \smile , ;)$ over the base of subsets of the structure, rather than its elements.

However, their result can be adapted for a wider range of signatures. Below we present an outline of the proof for the following theorem.

Proposition 1

For any signature $\{\mathrm {D}, \mathrm {R}, \smile , ;\} \subseteq \tau \subseteq \{ 0, 1, \mathrm {D}, \mathrm {R},\le , 1', \smile , ;\}$, $R(\tau )$ has the finite representation property.

Proof

We can, for any representable $\tau$-structure $\mathcal {S}$, define a partial ordering $\le$ (even if $\le \; \notin \tau$) as the set of all pairs where $s \le t$ if and only if for all representations $\theta$, $s^\theta \le t^\theta$. Similarly, one can define at most one element 0 (again even if $0 \notin \tau$) that will always be represented as an empty relation.

This means that we can define the set of closed sets $\mathcal {G}$ as the set of all $\emptyset \subsetneq S \subseteq \mathcal {S}\setminus \{0\}$ such that for $\mathrm {D}(S) = \prod _{s \in S} \mathrm {D}(s)$ and similarly $\mathrm {R}(S)$, we have $(\mathrm {D}(S);S;\mathrm {R}(S))^\uparrow = S$ where $\uparrow$ is upward closure with respect to $\le$. Then define a mapping $\rho : \mathcal {S}\rightarrow \wp (\mathcal {G}\times \mathcal {G})$ such that $(S,T) \in a^\rho$ if and only if $S;a \subseteq T$ and $T;\breve{a} \subseteq S$.

The mapping is faithful as for $a \nleq b$, $(\mathrm {D}(a), a) \in a^\rho$ as $a;\breve{a} \ge \mathrm {D}(a)$, but not in b as that would mean $a \le \mathrm {D}(a);b \le b$. It represents $\le$ correctly by monotonicity of ;  over $\le$ and 0, 1 correctly as 1 is the top element with respect to ordering and $a;0 = 0;a = 0$, for all a. Domain and range are correctly represented as if there is an outgoing/incoming edge from S with a/$\breve{a}$, then $S;a;\breve{a} \subseteq S$ and since $\mathrm {R}(\breve{a}) = \mathrm {R}(a;\breve{a}) = \mathrm {D}(a)$, $S;\mathrm {D}(a) \subseteq S$ and thus $\mathrm {D}(a) = \mathrm {R}(\breve{a})$ is included in (S, S). Furthermore if $\mathrm {R}(a) = \mathrm {D}(\breve{a})$ is included in (S, S) then $(S;\breve{a})^\uparrow$ ensures that there is an incoming edge with a and an outgoing edge with $\breve{a}$. Finally, domain elements are only on reflexive nodes as if $(S;\mathrm {D}(a))^\uparrow = S$ so if $(S,T) \in \mathrm {D}(a)$ then $S \subseteq T \subseteq S$ and similarly $(S,T) \in (1')^\rho$ if and only $S = T$. Converse is correctly represented as $\breve{\breve{a}} = a$. Finally $a^\rho ;b^\rho \le (a;b)^\rho$ by monotonicity and $(a;b)^\smile = \breve{a};\breve{b}$ and $(a;b)^\rho \le a^\rho ;b^\rho$ as if $(S,T) \in (a;b)^\rho$, $\Big (S;a;\mathrm {D}(\breve{a};\breve{T}) \cup T;a;\mathrm {R}(S;a)\Big )^\uparrow$ is an appropriate witness for the composition.    $\square$

Note that the second part of the proof where we show that $\rho$ is indeed a representation is an outline. This is because the argument closely follows that in [5, Section 6], refer to it for more detail.

Finally, Rogozin shows that one can embed residuated semigroups into relational quantales in [15] and we show in [10] that a Zareckiĭ representation can be modified in a way to represent semigroups with demonic refinement. The latter was the first example of a signature with composition without a finitely axiomatisable representation class, but with FRP.

7 Problems

In this section we look at some open problems and outline the difficulties with showing the finite representation property.

We begin with the observation that e in the Zareckiĭ representation, as defined in Sect. 6, is not represented as the true relational identity element, i.e. $1' = \{(x,x) \mid x \in X\}$, as for some $a \lneq a'$ we will have $(a', a) \in e^\theta$. Thus this good behaviour does not extend to the signature of $\{1', \le , ;\}$, with $R(\le , 1', ;)$ non-finitely axiomatisable [7] and FRP unknown.

$R(\le , 1', ;)$ suffers from the same problem as $R(\mathrm {D}, \mathrm {R}, *)$ and $R(\mathrm {D}, \mathrm {R}, ;)$. That is, some elements are always represented as partial functions, that is, for any representation $\theta$ over X, if $(x,y) \in f^\theta , (x,z) \in f^\theta$ then $y = z$. Simple examples of that include the domain-range elements, as well as those $f \le 1'$. However, composition makes for some more interesting examples, like $c_i$ in $\mathcal {S}_n$ in Sect. 5 or in $R(\mathrm {D}, \mathrm {R}, ;)$, $\mathrm {R}(a);b$ will always be represented as a partial function if $\mathrm {D}(a;b) = a;b$. This is illustrated in Fig. 6, from left to right, observe how for any representation $\theta$ if $(x,y) \in (R(a);b)^\theta$ then $(x,x) \in R(a)^\theta$, so there must exist a z such that $(z,x) \in a^\theta$. As $a;b = \mathrm {D}(a;b)$ and by composition, z must be the same as y. Similarly, for any outgoing z with $(x,z) \in (R(a);b)^\theta$, it has to be the case that $y=z$.

Fig. 6.

Partial-functional nature of R(a); b when $a;b = \mathrm {D}(a;b)$

Every function in the signature of domain-range algebras comes with a converse. More specifically, if $D(a;b) = a;b$ then not only is R(a); b a function, but a; D(b) is its well defined converse. Unfortunately, this does not enable us to use represent structures over a finite base in the same way as the structures in Proposition 1.

It is true that partial functions, their converses and arbitrary compositions of those have their converse well defined. But take an a with its converse defined and say $a = b;c$ and $\mathrm {R}(b) = \mathrm {D}(c)$. Observe that converses of b, c not defined. Both b and c have a partial converse. That is, for every representation $\theta$, $(b^\theta )^\smile \le (c;\breve{a})^\theta$ and $(c^\theta )^\smile \le (\breve{a};b)^\theta$, but the $\ge$ inclusions do not necessarily hold, see Fig. 7.

Fig. 7.

Partial converse of b, i.e. $b \le c;\breve{a}$, but $\breve{c};a \not \le b$, where a, b, c are elements of a domain range semigroup

This enables us to define the partial converse of $s \in \mathcal {S}$ to be the set $\mathrm {C}(s) \subseteq \mathcal {S}$ where $\mathrm {C}(s)$ is the set of all $s' \in \mathcal {S}$ such that $(s^\theta )^\smile \le (s')^\theta$, for any representation $\theta$. However, as we have seen there is no guarantee that $\mathrm {C}(\mathrm {C}(s))=s^\uparrow$. Furthermore, $\mathrm {C}(t);\mathrm {C}(s) \subseteq \mathrm {C}(s;t)$ but not necessarily $\mathrm {C}(t);\mathrm {C}(s) \supseteq \mathrm {C}(s;t)$. As the proof of FRP for ordered domain algebras heavily relies on both $\breve{\breve{a}} = a$ and $(a;b)^\smile = \breve{b};\breve{a}$, the same representation cannot be used for converse-free signatures.

Adding join ($+$) to the signature adds additional difficulty. The class of representable join-lattice semigroups $R(+, ;)$ was shown non-finitely axiomatisable in [1], with the finite representation property remaining open. Similar to the case where $1'$ is added to the signature of $\{\le , ;\}$, this slight modification completely breaks the Zareckiĭ representation. That is because $+$ is not necessarily distributive, i.e. if $a \le b+c$ there exists some $b' \le b$ and $c' \le c$ such that $a = b' + c'$.

For distributive lattices, one can define the Zareckiĭ representation over the set of minimal non-0 elements and preserve all operations in a faithful manner. However, no signature including $\{+, ;\}$ has been shown to have the finite representation property for its representation class thus far.

The problems raised in this section can be summarised below

Problem 1

Do converse-free (ordered) domain-range semigroups have the finite representation property? How about their demonic counterparts?

Problem 2

Do signatures containing the join-semilattice and composition have the finite representation property?

Problem 3

Does $R(\le , 1', ;)$ have FRP? How about $R(\le , 1', \smile , ;)$ or $R(\le , \smile , ;)$?