# Restriction in program algebra

Marcel Jackson  and  Tim Stokes

##  1\. Introduction

Let $P(X,Y)$ be the set of all partial functions having domains in the non-
empty set $X$ and mapping into non-empty $Y$. In Berendsen et al. [2], the
operations of _override_ and _update_ for such partial functions were
considered. Override was defined there as follows: for all $f,g\in P(X,Y)$,

$(f\sqcup g)(x):=\begin{cases}f(x)&\mbox{ if }x\in\text{dom}(f),\\\
g(x)&\mbox{ if }x\in\text{dom}(g)\backslash\text{dom}(f),\\\ \mbox{
undefined}&\mbox{ otherwise}.\end{cases}$

The operation of update $f\diamond g$ is then defined in [2] to be the
restriction of $g\sqcup f$ to the domain of $f$.

We also consider the operations of _domain restriction_ , $\circ$ given by:

$(f\circ g)(x)=\begin{cases}g(x)&\mbox{ if }x\in\text{dom}(f),\\\
\mbox{undefined}&\mbox{ otherwise},\end{cases}$

_minus_ , $-$, given by:

$(f-g)(x)=\begin{cases}f(x)&\mbox{ if
}x\in\text{dom}(f),x\not\in\text{dom}(g),\\\ \mbox{undefined}&\mbox{
otherwise},\end{cases}$

_intersection_ , $\cap$:

$f\cap g=\\{(x,y)\in X\times Y\mid(x,y)\in f\text{ and }(x,y)\in g\\}$

and _difference_ , $\backslash$:

$f\backslash g=\\{(x,y)\in X\times Y\mid(x,y)\in f\text{ and }(x,y)\not\in
g\\}.$

Before we proceed further, we note that the surrounding literature contains a
number of conflicting notations for the operations just introduced. In [2],
the operation we have denoted $\circ$ is referred to in an equivalent form as
“intersection”, with definition and notation $f@g:=g\circ f$. The notation for
$\sqcup$ in [2] is $\triangleright$, however, the notation $\triangleright$ is
well-established for the operation $\circ$ since at least the 1962 work of
Vagner [23] where it is called restrictive multiplication. As the present work
relates to both [2] and [23], we have adopted the neutral operation $\circ$ to
avoid confusion; this was also done in the second author’s work with Hirsch
[9]. We use the term “domain restriction” (as in Borlido and McLean [4]) for
$\circ$, since it is more suggestive of the meaning of the operation than
“restrictive multiplication”, and because the term “intersection” of functions
has another accepted meaning, namely that used above, and widely encountered
since at least the work of Garvac’kiĭ [8]. Our adopted notation $\sqcup$ for
override follows [11] (contemporaneous with [2]), though it is called
_preferential union_ there; $\sqcup$ was also used by the authors in [13].
Finally we use the notation $\diamond$ here for update because it is simpler
to specify in signatures; the notation in [2], and even in the authors’ work
[13], is $f[g]$, in place of $f\diamond g$.

The algebras of partial functions considered in [2] were those closed under
override and minus, and a finite equational axiomatisation was given that was
shown complete for equations. It was subsequently observed in Cvetko-Vah,
Leech and Spinks [6] that these algebras are equivalent to a certain type of
skew Boolean algebra previously considered by Leech in [14], where a complete
axiomatisation of the algebras was given. The axioms were equivalent to those
given in [2], thereby showing those laws to be strongly complete and not just
equationally complete. In the present article, we take strongly complete as
the primary notion of completeness, since in general, the isomorphism class of
functional models is a quasivariety always, and a variety only sometimes. When
completeness is established for equations only, we refer to _complete with
respect to equations_.

Closely related signatures have also been considered. Thus in [15], Leech
shows that algebras of partial functions closed under domain restriction and
override may be axiomatised as certain types of skew lattices; see $3.7$
there, which explains how to view Theorem $3.2$ there as providing such an
axiomatisation. Amongst signatures not including override, that consisting of
domain restriction and difference has recently been considered in [4], where a
finite equational axiomatisation is given.

Note that a number of these operations may be defined in terms of the others;
for example:

  * •

$f\circ g=g-(g-f)$ (as noted in [2]);

  * •

$f\diamond g=f\circ(g\sqcup f)$ (also as noted in [2]);

  * •

$f\circ g=(f\diamond g)\cap g$;

  * •

$f\cap g=f\backslash(g\backslash f)$;

  * •

$f-g=f\backslash(g\circ f)$;

  * •

$f\backslash g=f-(f\cap g)$.

Hence $\circ$ is expressible in any signature containing both $\diamond$ and
$\cap$, and $\diamond$ is expressible in any signature containing both $\circ$
and $\sqcup$. So the following signatures are equivalent in expressive power:

$(\diamond,\sqcup,\cap),\ (\circ,\sqcup,\cap),$

and similarly so are

$(\backslash,\circ),\ (-,\cap)$

as well as

$(\backslash,\sqcup),\ (-,\cap,\sqcup).$

In every case above, $\circ$ is expressible. Other less expressive cases we
consider in which $\circ$ is either in the signature or definable within it
are as follows:

$(-),\ (-,\diamond),\ (\circ),(\circ,\cap),\ (\diamond,\cap).$

The signature $(\backslash,\sqcup)$ can be viewed as a kind of “master
signature”, since all the operations considered here can be expressed within
it. Written directly, we have

$f-g=(g\sqcup f)\backslash g,\ f\cap g=f\backslash(f\backslash g),\ f\circ
g=g\backslash((f\sqcup g)\backslash f),\ f\diamond g=(g\sqcup
f)\backslash[(f\sqcup g)\backslash f].$

This signature is axiomatised by Cirulis [5] (see Theorem $5.6$ there), an
alternative description in terms of skew Boolean intersection algebras being
given in [6], and we give yet another description of it in Section 5. A
further axiomatisation is given by Bignall and Leech [3], where the class is
shown to be the variety generated by the pointed discriminator algebras, which
is the class of pointed comparison algebras as defined in Stokes [21].

However, aside from $(-,\sqcup)$ and $(\backslash,\circ)$, weaker signatures
such as $(\circ,\cap,\sqcup)$ have mostly not been axiomatised; as is pointed
out in [6], this latter signature gives rise to a certain class of skew
lattices with intersection. In this article we axiomatise this case, but also
recover known results such as those in [4] and [5], and obtain new results for
a large range of combinations of the operations previously discussed. In
addition, our methods make possible the modelling of program concatenation,
corresponding to composition of partial functions; in this case, we assume
$Y=X$. Indeed our approach is to model the case with composition first, then
recover the composition-free case for $P(X,Y)$ from it.

For two equivalent signatures, it suffices to finitely axiomatise one in order
to establish a finite axiomatisation of the other: simply translate the needed
laws using the above relations, and add in as additional laws the relations
used in the translation. All the axiomatisations obtained in what follows are
finite, and most are equational, though some are properly quasiequational.
Since $\circ$ is expressible in every signature, we develop an approach based
on it.

The paper is organised as follows. In Section 2 to follow, we introduce each
of the classes of algebras considered, giving axioms for them which we claim
are sound in each case, and in later sections show are complete. The
signatures come in pairs: one without composition and one with, the latter
obtained from the former by the addition of some extra axioms involving
composition. Following that, in Section 3, we develop some important
preliminary facts involving certain fundamental quasiorders and the associated
filters as well as certain equivalence relations, all of which is done at the
“composition-free” level. Then in Section 4, we establish completeness of the
axioms given in Section 2 by using a single unified approach to represent
algebras in each class, applying it to each in turn to show each operation in
the relevant signature is correctly represented. In Section 5, we tidy up some
of the earlier axiomatisations, showing that some quasivarieties are finitely
based varieties, or are not varieties at all. We then present a table in which
the axiomatisation status of a wide range of signatures is given. We conclude
the main body of the article with some open questions in Section 7. Included
after that is some supplementary material in which simplifications of our
various axiom sets are obtained using the Prover9/Mace4 software [16].

Throughout, for a given signature consisting of some of the operations just
described, we use the term “algebra of partial functions” of that signature to
refer to a set of partial functions in $P(X,Y)$ (or $PT(X)$ if composition is
part of the signature) closed under the operations in the signature. When we
speak of the algebras of partial functions of some given signature as being
axiomatised as a class of axiomatically defined algebraic structures, we of
course mean that the isomorphism class of such algebras is that given class.

##  2\. The axioms

###  2.1. Right normal bands and 1-stacks

Recall that a right normal band $(A,\circ)$ is a semigroup satisfying the
following: for all $x,y,z\in A$,

  * •

$x\circ x=x$ (so $(A,\circ)$ is a band), and

  * •

$(x\circ y)\circ z=(y\circ x)\circ z$.

We say the right normal band has a zero if it has a zero as a semigroup;
sufficient for this is that $0\circ x=0$ for all $x$, since if this holds then
$x\circ 0=x\circ(0\circ x)=(x\circ 0)\circ x=(0\circ x)\circ x=0\circ x=0$. We
can append a new element $0$ to any right normal band $(A,\circ)$, defining
$s0=0s=0$ for all $s\in A$ to obtain a semigroup with zero which is clearly a
right normal band with zero; denote this by $A^{0}$.

It is easy to verify that $P(X,Y)$ is a right normal band under the domain
restriction operation $\circ$ (and indeed it has zero the empty function),
whence so is any subsemigroup of it; we call such examples that lie inside
$P(X,Y)$ in this way functional. It was shown in Vagner [23] that every right
normal band is isomorphic to a functional one. A proof of this is quite
straightforward, and we shortly give a proof which also applies to the richer
structures we are interested in here.

The domain restriction operation $\circ$ is defined for partial functions in
$P(X,Y)$. To model composition $\cdot$ as well, we assume $Y=X$. It is easy to
check that the following laws hold on $PT(X)=P(X,X)$ equipped with domain
restriction and composition (where we write $\cdot$ as concatenation):

  1. (1)

the right normal band laws for $\circ$;

  2. (2)

associativity of composition;

  3. (3)

for all $a,b,c$, $a\circ(bc)=(a\circ b)c$, $a(b\circ c)=(ab)\circ(ac)$.

These laws define the class of 1-stacks. The particular axioms just given
appear in Schein [18], where it is noted that they axiomatise algebras of
partial functions under composition and domain restriction.

We say the 1-stack $(A,\circ,\cdot)$ has zero if there is $0\in A$ which is a
zero with respect to both operations.

######  Proposition 2.1.

Every right normal band with zero $(A,\circ)$ can be made into a 1-stack with
zero by setting $st=0$ for all $s,t\in A$.

###### Proof.

With the above definition of $\cdot$, an easy case analysis verifies that the
two identities appearing in (3) above both hold, and $0$ is obviously a zero
with respect to $\cdot$. ∎

######  Corollary 2.2.

Every right normal band $(A,\circ)$ embeds in the right normal band reduct of
a 1-stack with zero.

###### Proof.

Append $0$ to $(A,\circ)$ to form the right normal band with zero $A^{0}$ and
then apply the previous result. ∎

From now on, if it is part of the signature, the semigroup operation intended
to model composition will take notational precedence over all other
operations. For example the law $a(b\circ c)=(ab)\circ(ac)$ can be written
unambiguously as $a(b\circ c)=ab\circ ac$, and so on.

###  2.2. Adding intersection

Algebras of partial functions closed under intersection are abstractly nothing
but semilattices. But intersection of partial functions is also relatively
easily modelled within the setting of right normal bands. Let us say that an
algebra $(A,\circ,\cap)$ equipped with two binary operations is a right normal
band with intersection if $(A,\circ)$ is a right normal band, $(A,\cap)$ is a
semilattice, and for all $x,y,z\in A$:

  * •

$(x\cap y)\circ x=x\cap y$;

  * •

$x\circ(y\cap z)=(x\circ y)\cap z$.

Again, it is routine to check that $P(X,Y)$ is a right normal band with
intersection when equipped with domain restriction and intersection.

Full left distributivity is an easy consequence of the right normal band with
intersection laws:

$(x\circ y)\cap(x\circ z)=x\circ(y\cap(x\circ z))=x\circ((x\circ z)\cap
y)=x\circ(x\circ(z\cap y))=x\circ(y\cap z).$

We introduce composition to the signature. We say $(A,\cdot,\circ,\cap)$ is a
1-stack with intersection if

  1. (1)

$(A,\cdot,\circ)$ is a 1-stack,

  2. (2)

$(A,\circ,\cap)$ is a right normal band with intersection, and

  3. (3)

for all $s,t,u\in A$, $s(t\cap u)=st\cap su$.

The final law is known to be sound for the functional signature $(\cdot,\cap)$
(see [8]). Hence any algebra of functions of signature $(\cdot,\circ,\cap)$ is
certainly a 1-stack with intersection.

######  Proposition 2.3.

Every right normal band with intersection embeds as a reduct in a 1-stack with
intersection.

###### Proof.

Given the right normal band with intersection $(A,\circ,\cap)$, adjoin a zero
element to give $(A^{0},\circ)$, giving a 1-stack with all products zero as in
the proof of Proposition 2.1. Also extend the definition of $\cap$ to
$A^{\prime}$ by defining $s\cap 0=0=0\cap s$ for all $s\in A^{\prime}$. Using
case analyses, the result is easily seen to be a 1-stack with intersection in
which $(A,\circ,\cap)$ embeds as a subreduct. ∎

For each of the sets of axioms to follow involving minus, given in Subsections
2.3, 2.4 and 2.5, we add intersection to the signature by simply adding in the
1-stack with intersection or right normal band with intersection laws, and we
refer to such an enhanced algebra as “with intersection” in all such cases.

###  2.3. Adding minus

We say $(A,\circ,-)$ is a minus-algebra if the following laws hold:

  * •

$x\circ y=y-(y-x)$;

  * •

$(A,\circ)$ is a right normal band;

  * •

$x-x=0$ (this effectively defines $0$);

  * •

$x\circ 0=0\circ x=0$;

  * •

$(x-y)\circ x=x-y$;

  * •

$(x-y)\circ y=0$;

  * •

$(x-y)\circ z=(x\circ z)-y$;

  * •

$s-x=t-x\And x\circ s=x\circ t\Rightarrow s=t$.

(As in other cases to follow in this section, we return to the question of
more elegant axioms later.) Fix the minus-algebra $(A,-)$ for the remainder of
this section.

As in previous cases, we can add composition to the signature. We say
$(A,\cdot,-)$ is a minus-semigroup if

  1. (1)

$(A,-)$ is a minus-algebra,

  2. (2)

$(A,\cdot)$ is a semigroup,

  3. (3)

$s(t-u)=st-su$ for all $s,t,u\in A$.

All of these laws are functionally sound, and most follow easily from Figure 3
in [2]. In particular, the final quasiequational law for minus-algebras states
that two functions $s,t$ that agree both on the domain of $x$ and outside of
the domain of $x$ must be equal. Law (3) above involving composition can
easily be checked by case analysis (both sides being subsets of $st$).

Since $0$ is already in the signature of a minus-algebra, we do not need to
adjoin one.

######  Proposition 2.4.

Every minus-algebra is a minus-semigroup if we define $st=0$ for all $s,t$.

###### Proof.

Let $(A,-)$ be a minus-algebra. Defining $s\cdot t=0$ for all $s,t\in A$ gives
a semigroup $(A,\cdot)$, and because $0-0=0$, $(A,-,\cdot)$ satisfies the law
$s(t-u)=(st)-(su)$ for all $s,t,u\in A$. All other laws remain satisfied since
no new elements have been introduced. ∎

It is now trivial to add $\cap$ to the signature of both minus-algebras and
minus-semigroups, using finitely many more equations as in Subsection 2.2.

###  2.4. Minus and override

We next turn to the signature considered in [2], in which update can be
defined as a term. A finite equational axiomatisation was given there that was
shown complete for equations. The associated class of algebras was
subsequently shown in [6] to be equivalent to certain types of skew Boolean
algebras (SBAs) previously considered by Leech in [14], and because of this
the axiomatisation was established as complete. We here present a third
axiomatisation, but go further by introducing function composition to the
signature as well.

We say an algebra $(A,-,\sqcup)$ is a minus-algebra with override if it is a
minus-algebra that additionally satisfies the following laws:

  * •

$(x\sqcup y)-x=y-x$;

  * •

$x\circ(x\sqcup y)=x$.

It is straightforward to check that override in $P(X,Y)$ satisfies these two
laws.

We say an algebra $(A,-,\sqcup,\cdot)$ is a minus-semigroup with override if:

  1. (1)

$(A,-,\cdot)$ is a minus-semigroup; and

  2. (2)

$(A,-,\sqcup)$ is a minus-algebra with override.

Again, it is routine to verify that $(PT(X),-,\sqcup,\cdot)$ is a minus-
semigroup with override, whence so is any subalgebra.

We have our usual result, which follows from Proposition 2.4.

######  Proposition 2.5.

Every minus-algebra with override is a minus-semigroup with override if we
define $st=0$ for all $s,t$.

###  2.5. Minus and update

We say $(A,-,\diamond)$ is a minus-algebra with update if

  1. (1)

$(A,-)$ is a minus-algebra,

  2. (2)

$(x\diamond y)-x=x-(x\diamond y)=0$,

  3. (3)

$((x\diamond y)-y)\circ x=(x\diamond y)-y$, and

  4. (4)

$x\circ y=y\circ(x\diamond y)$.

We say $(A,\cdot,-,\diamond)$ is a minus-semigroup with update if

  1. (1)

$(A,-,\diamond)$ is a minus-algebra with update, and

  2. (2)

$(A,\cdot,-)$ is a minus-semigroup.

Again, the usual functional models satisfy these various laws, establishing
soundness, and again from Proposition 2.4 we obtain the following.

######  Proposition 2.6.

Every minus-algebra with update is a minus-semigroup with update if we define
$st=0$ for all $s,t$.

###  2.6. Intersection and override

In previous cases, we could simply add “with intersection” to each set of
axioms by just adding the relevant axioms from Subsection 2.2 to an existing
axiom set. In this signature and the one after, that is no longer possible:
using our methods, we cannot obtain axioms for domain restriction together
with either just override or just update without first assuming intersection
is present as well.

We say the algebra $(A,\circ,\cap,\sqcup)$ is a right normal band with
intersection and override if the following laws are satisfied:

  1. (1)

$(A,\circ,\cap)$ is a right normal band with intersection;

  2. (2)

$s\circ(s\sqcup t)=s$;

  3. (3)

$((s\sqcup t)\cap t)\sqcup s=s\sqcup t$;

  4. (4)

$(s\sqcup t)\circ u=(s\circ u)\sqcup(t\circ u)$.

As usual, it is a routine process to verify that $P(X,Y)$ equipped with domain
restriction, intersection and override is a right normal band with
intersection and override (and hence so are all its subalgebras).

We add composition to the signature. We say the algebra
$(A,\circ,\cap,\sqcup,\cdot)$ is a 1-stack with intersection and override if
the following laws are satisfied:

  1. (1)

$(A,\circ,\cap)$ is a right normal band with intersection and override;

  2. (2)

$(A,\cdot,\circ,\cap)$ is a 1-stack with intersection;

  3. (3)

for all $s,t,u\in A$, $s(t\sqcup u)=st\sqcup su$.

######  Proposition 2.7.

Every right normal band with intersection and override embeds in a reduct of a
1-stack with intersection and override.

###### Proof.

If $(A,\circ,\cap,\sqcup)$ is a right normal band with intersection and
override, adjoin a zero element as in Proposition 2.3, also assuming that
$s\sqcup 0=s$ and $0\sqcup s=s$ for all $s\in A\cup\\{0\\}$. It follows from
that result that $(A,\cdot,\circ,\cap)$ is a 1-stack with intersection, and
routine case analysis shows that all three new laws for right normal bands
with intersection and override as well as the third law above for 1-stacks
with intersection and override are satisfied, so the result is a 1-stack with
intersection and override into which $(A,\circ,\cap,\sqcup)$ embeds as a
subreduct. ∎

###  2.7. Intersection and update

We say the algebra $(A,\circ,\cap,\diamond)$ is a right normal band with
intersection and update if and the following laws are satisfied:

  1. (1)

$(A,\circ,\cap)$ is a right normal band with intersection;

  2. (2)

$s=(s\diamond t)\circ s$;

  3. (3)

$s\diamond t=s\diamond(s\diamond t)$;

  4. (4)

$s\circ t=t\circ(s\diamond t)$;

  5. (5)

$(x\cap(x\diamond y))\circ a=(x\cap(x\diamond y))\circ b$ and $y\circ a=y\circ
b$; imply $x\circ a=x\circ b$.

As usual, there is a version involving composition as well. We say the algebra
$(A,\cdot,\circ,\cap,\diamond)$ is a 1-stack with intersection and update if

  1. (1)

$(A,\circ,\cap,\diamond)$ is a right normal band with intersection and update,

  2. (2)

$(A,\cdot,\circ,\cap)$ is a 1-stack with intersection, and

  3. (3)

$s(t\diamond u)=st\diamond su$ for all $s,t,u\in A$.

And as usual, we have an embedding result.

######  Proposition 2.8.

Every right normal band with intersection and update embeds in a reduct of a
1-stack with intersection and update.

###### Proof.

If $(A,\circ,\cap,\diamond)$ is a right normal band with intersection and
update, adjoin a zero element as in Proposition 2.3, also assuming that
$s\diamond 0=s$ and $0\diamond s=0$ for all $s\in A\cup\\{0\\}$. Then argue as
for Proposition 2.7. ∎

###  2.8. Override only

The signature $(\circ,\sqcup)$ does not lend itself to axiomatisation using
the methods presented here. For completeness, we here list axioms for this
case, based on those presented in [15] for certain types of skew lattices,
which we now define.

The algebra $(A,\circ,\sqcup)$ is a right handed strongly distributive skew
lattice if the following laws are satisfied:

  1. (1)

$(A,\circ)$ is a right normal band (indeed it suffices that it be a band
satisfying the law $x\circ y\circ x=y\circ x$);

  2. (2)

$(A,\sqcup)$ is a band (idempotent semigroup);

  3. (3)

the absorption laws $x\circ(x\sqcup y)=x=(y\sqcup x)\circ x$ and
$x\sqcup(x\circ y)=x=(y\circ x)\sqcup x=x$ hold;

  4. (4)

the distributive laws $s\circ(t\sqcup u)=(s\circ t)\sqcup(s\circ u)$ and
$(s\sqcup t)\circ u=(s\circ u)\sqcup(t\circ u)$ hold.

##  3\. Quasiorders and filters

###  3.1. Right normal bands in general

For the rest of this section, let $(A,\circ)$ be a fixed right normal band. We
may define two quasiorders on $(A,\circ)$ as follows:

  * •

$f\lesssim g$ if and only if $g\circ f=f$; in $P(X,Y)$ this asserts that the
domain of $f$ is contained in that of $g$, so $\lesssim$ is the first
projection quasiorder, which was axiomatised within function semigroups by
Schein in [19];

  * •

$f\leq g$ if and only if $f=f\circ g$; in $P(X,Y)$ this asserts that
$f\subseteq g$, or $f$ is a domain restriction of $g$, and we call it the
natural order, and we apply the same terminology to right normal bands in
general. The natural order was also axiomatised within function semigroups by
Schein in [19].

The next facts follow from Vagner’s representation theorem as in [23], but
direct proofs are straightforward.

######  Proposition 3.1.

On $(A,\circ)$, $\lesssim$ is a quasiorder and $\leq$ is a partial order, and
$a\leq b$ implies $a\lesssim b$ for all $a,b\in A$. Moreover the equivalence
relation $\sim$ determined by $\lesssim$ is a congruence, and
$(A/{\sim},\circ)$ is a semilattice.

###### Proof.

Both relations are quasiorders because $(A,\circ)$ is a band. If $a\leq b$ and
$b\leq a$, then $a=a\circ b$ and $b=b\circ a$, so

$a=a\circ b=a\circ(b\circ a)=(a\circ b)\circ a=(b\circ a)\circ a=b\circ a=b.$

So $\leq$ is a partial order. If $a\leq b$ then $a=a\circ b$ and so

$b\circ a=b\circ(a\circ b)=(b\circ a)\circ b=(a\circ b)\circ b=a\circ(b\circ
b)=a\circ b=a,$

so $a\lesssim b$.

Suppose $a\sim b$ and $c\sim d$. Then $a\circ b=b$, $b\circ a=a$, $c\circ
d=d$, $d\circ c=c$. So

$(a\circ c)\circ(b\circ d)=a\circ b\circ c\circ d=b\circ d,$

so $b\circ d\lesssim a\circ c$. By symmetry, $a\circ c\lesssim b\circ d$, so
$a\circ c\sim b\circ d$.

Now $(b\circ c)\circ(c\circ b)=b\circ c\circ b=c\circ b\circ b=c\circ b$ so
$b\circ c\lesssim c\circ b$; so by symmetry $b\circ c\sim c\circ b$. So
$(A/{\sim},\circ)$ is a commutative band, hence a semilattice. ∎

Let $(A,\circ)$ be a fixed right normal band throughout the remainder of this
section. Let $F\subseteq A$ be a filter, meaning a non-empty subset of $A$
such that for all $a,b\in F$, $a\circ b\in F$, and if $a\in F$ and $a\lesssim
b$, then $b\in F$ (so $F$ is an up-set under $\lesssim$). (So in other words,
$F/{\sim}$ is a filter in $A/{\sim}$ in the usual sense for semilattices.)

The next observation is useful in what follows.

######  Lemma 3.2.

Let $F$ be a proper filter of $A$ and $a\in A\backslash F$. Then

$F_{a}=\\{b\in A\mid f\circ a\lesssim b\mbox{ for some }f\in F\\}$

is a filter of $A$ containing $a$ and $F$.

###### Proof.

If $b_{1},b_{2}\in F_{a}$ then there are $f_{1},f_{2}\in F$ such that
$f_{1}\circ a\lesssim b_{1}$ and $f_{2}\circ a\lesssim b_{2}$, so letting
$f=f_{1}\circ f_{2}\in F$, we have

$b_{1}\circ b_{2}\circ f\circ a=b_{2}\circ f_{2}\circ b_{1}\circ f_{1}\circ
a=b_{2}\circ f_{2}\circ f_{1}\circ a=f_{1}\circ b_{2}\circ f_{2}\circ
a=f_{1}\circ f_{2}\circ a=f\circ a,$

so $f\circ a\lesssim b_{1}\circ b_{2}$, so $b_{1}\circ b_{2}\in F_{a}$.
Obviously $F_{a}$ is an up-set, hence it is a filter. Since $f\circ a\lesssim
a$ for any $f\in F$, we have $a\in F_{a}$, and since also $f\circ a\lesssim f$
for all $f\in F$, we have $F\subseteq F_{a}$. ∎

Let $(A,\circ)$ be a right normal band. Suppose $a,b\in A$ are such that
$a\not\leq b$. We say the filter $F$ of $A$ is $(a,b)$-separating if (i) $a\in
F$, and (ii) there is no $e\in F$ for which $e\circ a=e\circ b$.

For $a\in A$, denote by $a^{\uparrow}$ the principal filter of $A$ generated
by $a$, so $a^{\uparrow}=\\{e\in A\mid a\lesssim e\\}$. Clearly this is an up-
set under $\lesssim$, and if $e,f\in a^{\uparrow}$, then $e\circ a=f\circ
a=a$, so $(e\circ f)\circ a=e\circ(f\circ a)=e\circ a=a$, and so $e\circ f\in
F$.

######  Lemma 3.3.

If $a,b\in S$ with $a\not\leq b$, then $F=a^{\uparrow}$ is $(a,b)$-separating.

###### Proof.

Evidently $a\in F$. Suppose there is $e\in F$ for which $e\circ a=e\circ b$.
Since $a\lesssim e$, $a=e\circ a$. So $a\circ b=e\circ a\circ b=a\circ e\circ
b=a\circ e\circ a=e\circ a\circ a=e\circ a=a$, and so $a\leq b$, a
contradiction. So $F$ is $(a,b)$-separating. ∎

Let $F$ be a proper filter of $(A,\circ)$. Define a binary relation
$\epsilon_{F}$ on $A$ by setting

$\mathrel{\epsilon_{F}}=\\{(a,b)\in A\times A\mid e\circ a=e\circ b\mbox{ for
some }e\in F\\}.$

######  Proposition 3.4.

If $F$ is a proper filter of $A$, then $\epsilon_{F}$ is a congruence on
$(A,\circ)$, and both $F$ and $\overline{F}$ (the complement of $F$ in $A$)
are unions of $\epsilon_{F}$-classes.

###### Proof.

Reflexivity and symmetry are immediate. If $a,b,c\in F$, and $e\circ a=e\circ
b$ and $f\circ b=f\circ c$ for some $e,f\in F$, then letting $g=e\circ f\in
F$, we have

$g\circ a=e\circ f\circ a=f\circ e\circ a=f\circ e\circ b=e\circ f\circ
b=e\circ f\circ c=g\circ c.$

Suppose $(a,b),(c,d)\in\epsilon_{F}$. Then there must be $e,f\in F$ such that
$e\circ a=e\circ b$ and $f\circ c=f\circ d$. Again, letting $g=e\circ f\in F$,
we have that

$(e\circ f)\circ(a\circ c)=f\circ e\circ a\circ c=f\circ e\circ b\circ
c=f\circ b\circ e\circ c=f\circ b\circ e\circ d=(e\circ f)\circ(b\circ d).$

So $(a\circ c,b\circ d)\in\epsilon_{F}$.

If $x\in\overline{F}$ and $(x,y)\in\epsilon_{F}$, then $e\circ x=e\circ y$ for
some $e\in F$, so if $y\in F$, then $e\circ y$ and hence $e\circ x$ are in
$F$, so $x\in F$, a contradiction, so $y\in\overline{F}$. Hence $\overline{F}$
is a union of $\epsilon_{F}$-classes, and so $F$ must be as well. ∎

Let $X$ be a set of filters of $A$ with the property that for every $a,b\in A$
with $a\not\leq b$, there exists $F\in X$ that is $(a,b)$-separating. We call
such $X$ separating. Lemma 3.3 now gives the following.

######  Proposition 3.5.

The set of all filters of $A$ is separating.

Suppose $a,b\in A$, with $a\not\leq b$. We say the filter $F$ of $(A,\circ)$
is maximally $(a,b)$-separating if it is maximal with respect to the property
of being $(a,b)$-separating. Because $F=a^{\uparrow}$ is $(a,b)$-separating by
Lemma 3.3, we readily obtain the following from Zorn’s Lemma.

######  Lemma 3.6.

For any $a,b\in S$ for which $a\not\leq b$, there is a maximally
$(a,b)$-separating filter in $A$.

It is immediate that the set ${\mathcal{F}}$ of all filters of $A$ that is
maximally $(a,b)$-separating, ranging over all $a,b\in A$ for which $a\not\leq
b$, is separating.

Another useful fact is the following.

######  Lemma 3.7.

If $(A,\circ)$ is a right normal band with $a\not\leq b$ in $A$, and $F$ a
maximally $(a,b)$-separating filter in $A$ with $y\in A\backslash F$, then
there exists $f\in F$ for which $(f\circ y)\circ a=(f\circ y)\circ b$.

###### Proof.

Now $F_{y}=\\{g\in A\mid y\circ f\lesssim g\mbox{ for some }f\in F\\}$ as in
Lemma 3.2 properly contains $y$ and $F$, hence is not $(a,b)$-separating by
maximality of $F$, and so there exists $e\in F_{y}$, that is $f\circ y\lesssim
e$ for some $f\in F$, such that $e\circ a=e\circ b$. Hence also $(f\circ
y)\circ a=(f\circ y)\circ b$ (because if $e\lesssim f$ and $f\circ s=f\circ t$
then $e\circ s=(e\circ g)\circ s=e\circ(g\circ s)=e\circ(g\circ t)=(e\circ
g)\circ t=e\circ t$). ∎

###  3.2. Right normal bands with intersection

Throughout this subsection, let $(A,\circ,\cap)$ be a fixed right normal band
with intersection. In this case, the natural order on $(A,\circ)$ coincides
with the partial order determined by the meet-semilattice $(A,\cap)$.

######  Proposition 3.8.

For $x,y\in A$, $a\leq b$ if and only if $a=a\cap b$.

###### Proof.

Suppose $a\leq b$, so that $a=a\circ b$. Then

$a\cap b=(a\circ b)\cap(b\circ b)=(a\circ b)\cap b=a\circ(b\cap b)=a\circ
b=a.$

Conversely, suppose $a=a\cap b$. Then $a\circ b=(a\cap b)\circ b=a\cap b=a$,
so $a\leq b$. ∎

######  Lemma 3.9.

For any filter $F$ of $A$ and $x,y\in A$, it is the case that $x,y\in F$ and
$(x,y)\in\epsilon_{F}$ if and only if $x\cap y\in F$.

###### Proof.

Suppose $x\cap y\in F$. Then $x,y\in F$ since $x\cap y\leq x,y$ by Proposition
3.8, and so $x\cap y\lesssim x,y$. But also, $(x\cap y)\circ x=x\cap y=(x\cap
y)\circ y$, so $(x,y)\in\epsilon_{F}$.

Conversely, suppose $x,y\in F$ and $(x,y)\in\epsilon_{F}$, so there exists
$e\in A$ for which $e\circ x=e\circ y$. So $e\circ(x\cap y)=(e\circ
x)\cap(e\circ y)=(e\circ x)\cap(e\circ x)=e\circ x$, and so $F\ni e\circ
x\lesssim x\cap y$, so $x\cap y\in F$. ∎

###  3.3. Minus-algebras

We begin with a useful result.

######  Lemma 3.10.

In any minus-algebra, the following law holds:

$(z-x)\circ s=(z-x)\circ t\And x\circ s=x\circ t\Rightarrow z\circ s=z\circ
t.$

###### Proof.

Assume that $(z-x)\circ s=(z-x)\circ t$ and $x\circ s=x\circ t$ hold; we must
show that $z\circ s=z\circ t$. Now $x\circ s=x\circ t$ implies that $z\circ
x\circ s=z\circ x\circ t$, which in turn gives

(1) $x\circ(z\circ s)=x\circ(z\circ t),$

using the laws of domain restriction. Next $(z-x)\circ s=(z\circ s)-x$ and
$(z-x)\circ t=(z\circ t)-x$ so that

(2) $(z\circ s)-x=(z\circ t)-x.$

Applying the final law for minus-algebras to (1) and (2) gives $z\circ
s=z\circ t$ as required. ∎

For reasons that will become more plain later, let us say that a filter $F$ of
the minus-algebra $(A,-)$ (viewed as a right normal band) is prime if,
whenever $a\in F$, for all $b\in A$, either $b\in F$ or $a-b\in F$.

######  Lemma 3.11.

Let $F$ be maximally $(a,b)$-separating, for some $a,b\in A$ with $a\not\leq
b$. Then $F$ is prime.

###### Proof.

First suppose that $x\in F$ and $y\not\in F$, and for a contradiction that
$x-y\not\in F$. Then by Lemma 3.7, there exists $f\in F$ for which $(f\circ
y)\circ a=(f\circ y)\circ b$. Similarly, there exists $h\in F$ for which
$(h\circ(x-y))\circ a=(h\circ(x-y))\circ b$. So letting $k=f\circ h\in F$, we
have $y\circ(k\circ a)=y\circ(k\circ b)$ and $(x-y)\circ(k\circ
a)=(x-y)\circ(k\circ b)$, so $(x\circ k)\circ a=x\circ(k\circ a)=x\circ(k\circ
b)=(x\circ k)\circ b$ by Lemma 3.10. But $x\circ k\in F$, so this contradicts
the $(a,b)$-separating property of $F$. Hence in fact $x-y\in F$. ∎

######  Corollary 3.12.

The set of all prime filters of $(A,-)$ is separating.

###  3.4. Minus-algebras with override

Of interest is the following alternative way of looking at prime filters in
minus-algebras with override, making clear that the termionology is natural.

######  Proposition 3.13.

Let $(A,-,\sqcup)$ be a minus-algebra with override. A filter $F$ of the
minus-algebra $(A,-)$ is prime if and only if it satisfies the following: for
all $a,b\in A$, if $a\sqcup b\in F$ then $a\in F$ or $b\in F$.

###### Proof.

Suppose $F$ is prime, and that $a\sqcup b\in F$. Suppose $b\not\in F$. Then by
primeness, $F\ni(a\sqcup b)-b\lesssim a$ (as follows from the functional
interpretation afforded by Proposition 3), and so $a\in F$.

Conversely, suppose that for all $a,b\in A$, if $a\sqcup b\in F$ then $a\in F$
or $b\in F$. Suppose $a\in F$, and $b\in A$. Then because
$a\lesssim(a-b)\sqcup b$ (again from the functional interpretation), we have
$(a-b)\sqcup b\in F$ and so $a-b\in F$ or $b\in F$. So $F$ is prime. ∎

###  3.5. Right normal bands with intersection and update

Again we need a relevant notion of “prime” for filters in this case. Suppose
$(A,\circ,\cap,\diamond)$ is a right normal band with intersection and update.
This time we say the filter $F$ of $(A,\circ)$ is weakly prime if whenever
$a\in F$, for all $b\in A$, either $b\in F$ or $a\cap(a\diamond b)\in F$.

######  Lemma 3.14.

Suppose $(A,\circ,\cap,\diamond)$ is a right normal band with intersection and
update. Pick $a,b\in A$ with $a\not\leq b$, and let $F$ be maximally
$(a,b)$-separating in $(A,\circ)$. Then $F$ is weakly prime.

###### Proof.

First suppose that $x\in F$ and $y\not\in F$, and for a contradiction that
$x\cap(x\diamond y)\not\in F$. Then by Lemma 3.7, there is $f\in F$ for which
$(f\circ y)\circ a=(f\circ y)\circ b$. Similarly, there exists $h\in F$ for
which $(h\circ(x\cap(x\diamond y)))\circ a=(h\circ(x\cap(x\diamond y)))\circ
b$. So letting $k=f\circ h\in F$, we have $y\circ(k\circ a)=y\circ(k\circ b)$
and $(x\cap(x\diamond y))\circ(k\circ a)=(x\cap(x\diamond y))\circ(k\circ b)$,
so $(x\circ k)\circ a=x\circ(k\circ a)=x\circ(k\circ b)=(x\circ k)\circ b$ by
the implication law for right normal bands with intersection and update. But
$x\circ k\in F$, so this contradicts the $(a,b)$-separating property of $F$.
Hence indeed $x\cap(x\diamond y)\in F$. ∎

######  Corollary 3.15.

The set of all weakly prime filters of a right normal band with intersection
and update is separating.

###  3.6. Right normal bands with intersection and override

Let $(A,\circ,\cap,\sqcup)$ be a fixed right normal band with intersection and
override. Following Proposition 3.13, we say a filter $F$ of
$(A,\circ,\cap,\sqcup)$ is prime if and only if it satisfies the following:
for all $a,b\in A$, if $a\sqcup b\in F$ then $a\in F$ or $b\in F$.

######  Lemma 3.16.

For $a,b\in A$ with $a\not\leq b$, every maximally $(a,b)$-separating filter
of $A$ is prime.

###### Proof.

Let $F$ be maximally $(a,b)$-separating. Suppose $s\sqcup t\in F$ and for a
contradiction that $s\not\in F$ and $t\not\in F$. Then the filter
$F_{s}=\\{g\in A\mid s\circ f\lesssim g\mbox{ for some }f\in F\\}$ as in Lemma
3.2 contains $F$ and $s\not\in F$ (and $a$), so by maximality of $F$, there
exists $g_{1}\in F_{s}$ for which $g_{1}\circ a=g_{1}\circ b$. So arguing as
in the proof of Lemma 3.11, $s\circ f_{1}\circ a=s\circ f_{1}\circ b$ for some
$f_{1}\in F$. Similarly, there is $f_{2}\in F$ for which $t\circ f_{2}\circ
a=t\circ f_{2}\circ b$. So letting $f=f_{1}\circ f_{2}\in F$, we have

$s\circ f\circ a=s\circ f\circ b,\ t\circ f\circ a=t\circ f\circ b.$

So

$\displaystyle(s\sqcup t)\circ f\circ a$ $\displaystyle=$
$\displaystyle(s\circ f\circ a)\sqcup(t\circ f\circ a)$ by the third law for
1-stacks with intersection and override $\displaystyle=$ $\displaystyle(s\circ
f\circ b)\sqcup(t\circ f\circ b)$ $\displaystyle=$ $\displaystyle(s\sqcup
t)\circ f\circ b,$

so $g\circ a=g\circ b$ where $g=(s\sqcup t)\circ f\in F$, contradicting the
fact that $F$ is $(a,b)$-separating. So $F$ is prime. ∎

######  Corollary 3.17.

The set of all prime filters of $(A,\circ,\cap,\sqcup)$ is separating.

Of course every right normal band with intersection and override is a right
normal band with intersection and update, which we define via $a\diamond
b=a\circ(a\sqcup b)$ as usual. We do not know if the weakly prime filters in a
right normal band with intersection and override viewed in this way as a right
normal band with intersection and update are nothing but its prime filters.
However in general we have the following, which justifies use of the “weakly”
epithet.

######  Proposition 3.18.

Every prime filter of the right normal band with intersection and override
$(A,\circ,\cap,\sqcup)$ is weakly prime.

###### Proof.

Suppose $F$ is a prime filter, with $x\in F$ and $y\not\in F$. Now
$x=(x\cap(x\diamond y))\sqcup y\circ x$ as follows from the functional
interpretation (and so must follow from the laws), so as $y\circ x\lesssim y$
we have $y\circ x\not\in F$ also, and then by primeness, we obtain
$x\cap(x\diamond y)\in F$. ∎

##  4\. The representations

The same basic construction is used throughout in what follows. The main
advantage of this is that it is relatively straightforward to enrich the
signature of domain restriction by including other operations defined on
partial functions in $P(X,Y)$, such as minus, intersection, override, but
especially function composition when $Y=X$, since the construction will
represent these operations correctly also for some choice of separating
filters ${\mathcal{F}}$. Indeed our approach is to represent algebras with
signature containing an operation modelling composition first, and use this to
obtain the analogous results for those without composition.

Let $S$ be a 1-stack, and let $F$ be a filter of $A$, viewed as a right normal
band. Let $A^{1}$ be $A$ with adjoined identity element $1$, so that $1a=a1=a$
for all $a\in A$, and extend $\epsilon_{F}$ to $A^{1}$ by putting $\\{1\\}$ in
a class by itself, and then let $A_{F}=(F\cup\\{1\\})/\epsilon_{F}$ (recalling
that $F$ is a union of $\epsilon_{F}$-classes by Proposition 3.4, so the
quotient is defined). For $x\in A^{1}$, denote by $\overline{x}^{F}$ the
$\epsilon_{F}$-class containing $x$. For any $a\in A$, define
$\phi^{F}_{a}:A_{F}\rightarrow A_{F}$, by setting, for $\overline{x}^{F}\in
A$,

$\phi^{F}_{a}(\overline{x}^{F}):=\begin{cases}\overline{xa}^{F}&\mbox{
providing }xa\in F,\\\ \mbox{undefined}&\mbox{ otherwise.}\end{cases}$

So $\phi^{F}_{a}$ is a partial function in $PT(A_{F})$, for each $a\in A$.

Now for ${\mathcal{F}}$ any separating set of filters of $A$, view the $A_{F}$
($F\in{\mathcal{F}}$) as mutually disjoint, let $X=\bigcup\\{A_{F}\mid
F\in{\mathcal{F}}\\}$ be their disjoint union, and let
$\phi_{a}=\bigcup\\{\phi^{F}_{a}\mid F\in{\mathcal{F}}\\}$ be the disjoint
union of the $\phi^{F}_{a}$ as $F$ ranges across ${\mathcal{F}}$; so
$\phi_{a}\in PT(X)$ for all $a\in A$.

######  Proposition 4.1.

With the above definitions, the mapping $\Phi:A\rightarrow PT(X)$ given by
$\Phi(a)=\phi_{a}$ for all $a\in S$ is a 1-stack embedding, mapping any zero
element to the empty function.

###### Proof.

We first show that if $x,y\in A$ and $(x,y)\in\epsilon_{F}$, then for all
$a\in A$, $(xa,ya)\in\epsilon_{F}$ (noting that if $x=1$, this is true also).
If $e\circ x=e\circ y$ then $e\circ(xa)=e\circ x\circ(xa)=e\circ
y\circ(xa)=y\circ e\circ(xa)=y\circ((e\circ x)a)=y\circ((e\circ y)a)=y\circ
e\circ(ya)=e\circ y\circ(ya)=e\circ(ya)$, so $(xa,ya)\in\epsilon_{F}$.

Next we show that $\overline{F}$, the complement of $F$ in $A$, is a right
ideal if non-empty. For $s\in\overline{F}$, because $s\circ(st)=st$ for all
$t\in A$, it follows that $st\lesssim s$, so if $st\in F$ then $s\in F$, a
contradiction, so $st\in\overline{F}$ also. We note also that $\overline{F}$
is a union of $\epsilon_{F}$-classes, from Proposition 3.4.

It now follows from the theory of determinative pairs (due to Boris Schein and
since used in many settings) that the mapping $A\rightarrow PT(A_{F})$ given
by $a\mapsto\psi^{F}_{a}$ is a semigroup homomorphism, and indeed that $\Phi$
is a homomorphism as well, since the computation of the operations takes place
independently on each $A_{F}$-patch of $X$, for those elements of $PT(X)$ in
the range of $\Phi$.

If $s\not\leq t$, there exists $F\in{\mathcal{F}}$ that is $(s,t)$-separating.
So $\psi^{F}_{s}(1)$ is defined, and even if $\psi^{F}_{t}(1)$ is defined as
well, so that $t\in F$, it would be the case that $(s,t)\not\in\epsilon_{F}$
and so $\psi^{F}_{s}(1)\neq\psi^{F}_{t}(1)$. So
$\psi^{F}(s)\not\subseteq\psi^{F}(t)$, and so $\Phi(s)\not\subseteq\Phi(t)$.
This shows that $\Phi$ is an embedding.

Next we show $\Phi$ respects domain restriction. Now for $s,t\in A$,
$\Phi(s\circ t)$ is defined at $\overline{x}^{F}\in A_{F}$, if and only if
$\psi^{F}(s\circ t)$ is defined at $\overline{x}^{F}$, if and only if
$(xs)\circ(xt)=x(s\circ t)\in F$, that is, $xs,xt\in F$ (since $xs\circ
xt\lesssim xs,xt$), or $\psi^{F}(s),\psi^{F}(t)$ are both defined at
$\overline{x}^{F}$, so $\Phi(s),\Phi(t)$ are both defined at
$\overline{x}^{F}$. For such $\overline{x}^{F}$, $x(s\circ t)=xs\circ(xs\circ
xt)=xs\circ xt$, so since $xs\in F$, we have $(x(s\circ
t),xt)\in\epsilon_{F}$, and so $\psi^{F}_{s\circ
t}(\overline{x})=\psi^{F}_{t}(\overline{x})$, and so $\Phi(s\circ
t)(\overline{x}^{F})=\Phi(t)(\overline{x}^{F})$. So by definition,
$\Phi(s\circ t)=\Phi(s)\circ\Phi(t)$.

If $(S,\circ)$ has a zero element $0$, then it is a smallest element under
$\lesssim$, so $0\not\in F$ for any filter $F\in{\mathcal{F}}$, and so
$\Phi(0)=\varnothing$. ∎

######  Corollary 4.2.

The algebras of partial functions of signature $(\cdot,\circ)$ are axiomatised
as the class of 1-stacks, and the algebras of partial functions of signature
$(\circ)$ are axiomatised as the class of right normal bands.

Each of these facts is well-known; see [18] and [23]. The value of the
construction just used is that it is sufficiently versatile to admit
representation theorems for richer signatures as well, including the one
considered in [2]. We now present a single result that addresses every one of
the cases so far considered.

######  Theorem 4.3.

Let $(A,\cdot,\circ,\ldots)$ be a 1-stack that is enriched in one of the ways
described in Section 2, and recall the 1-stack embedding $\Phi:A\rightarrow
PT(X)$ as in Proposition 4.1.

  1. (1)

If $(A,\cdot,\circ,\cap)$ is a 1-stack with intersection, then for any choice
of separating ${\mathcal{F}}$, $\Phi$ respects intersection.

  2. (2)

If $(A,\cdot,-)$ is a minus-semigroup, with ${\mathcal{F}}$ the set of all
prime filters of $(A,-)$, then $\Phi$ respects minus.

  3. (3)

If $(A,\cdot,-,\sqcup)$ is a minus-semigroup with override, with
${\mathcal{F}}$ the set of all prime filters of $(A,-)$, then $\Phi$ respects
minus and override.

  4. (4)

If $(A,\cdot,-,\diamond)$ is a minus-semigroup with update, with
${\mathcal{F}}$ the set of all prime filters of $(A,-)$, then $\Phi$ respects
minus and update.

  5. (5)

If $(A,\cdot,-,\ldots)$ is any of the last three cases involving minus, and
has intersection added to it by assuming the 1-stack with intersection laws,
then $\Phi$ respects intersection.

  6. (6)

If $(A,\circ,\cap,\sqcup,\cdot)$ is a 1-stack with intersection and override,
and ${\mathcal{F}}$ is the set of all prime filters of
$(A,\circ,\cap,\sqcup)$, then $\Phi$ respects $\cap$ and $\sqcup$.

  7. (7)

If $(A,\cdot,\circ,\cap,\diamond)$ is a 1-stack with intersection and update,
and ${\mathcal{F}}$ is the set of all weakly prime filters of
$(A,\diamond,\cap)$, then $\Phi$ respects $\cap$ and $\diamond$.

###### Proof.

For (1), note that $\overline{x}^{F}$ is in the domain of $\Phi(s)\cap\Phi(t)$
if and only if it is in the domain of $\psi^{F}_{s}\cap\psi^{F}_{t}$, that is,
$xs\in F$, $xt\in F$, and $(xs,xt)\in\epsilon_{F}$, which by the previous
lemma is equivalent to saying that $x(s\cap t)=xs\cap xt\in F$ (using 3 in the
definition if $x\in A$, and the fact that if $x=1$, this is trivially true),
which is to say that $\overline{x}^{F}$ is in the domain of $\psi^{F}_{s\cap
t}=\Phi(s\cap t)$. So the domains of $\Phi(s\cap t)$ and $\Phi(s)\cap\Phi(t)$
coincide. But for such $\overline{x}^{F}$ in this common domain,
$(xs)\cap(xs\cap xt)=xs\cap xt\in F$, so $(xs,xs\cap xt)\in\epsilon_{F}$ by
Lemma 3.9, and so

$\Phi(s\cap t)(\overline{x}^{F})=\psi^{F}_{s\cap
t}(\overline{x}^{F})=\overline{x(s\cap t)}^{F}=\overline{(xs\cap
xt)}^{F}=\overline{xs}^{F}=\psi^{F}_{s}(\overline{x}^{F})=\Phi(s)(\overline{x}^{F}),$

and similarly $\Phi(s\cap t)(\overline{x}^{F})=\Phi(t)(\overline{x}^{F})$. So
$\Phi(s\cap t)=\Phi(s)\cap\Phi(t)$.

For (2), $\overline{x}^{F}\in X$ is in the domain of $\Phi(s)-\Phi(t)$ if and
only if $xs\in F$ and $xt\not\in F$, which implies that $x(s-t)=xs-xt\in F$ by
primeness, and the minus-semigroup law if $x\in A$, with it being trivial if
$x=1$; indeed it is equivalent to this since if $xs-xt\in F$ then $xs\in F$
since $xs-xt\lesssim xs$ (as $xs\circ(xs-xt)=xs-xt$ by the second additional
law for minus-semigroups), and if $xt\in F$ then by the third law for minus-
algebras, $(xs-xt)\circ(xt)=0\in F$, a contradiction. But $xs-xt\in F$ simply
states that $\Phi(s-t)$ is defined at $\overline{x}^{F}$. When this happens,
$(xs-xt)\circ(xs-xt)=xs-xt=(xs-xt)\circ xs$, so $(xs,xs-xt)\in\epsilon_{F}$,
and so $\Phi(s-t)=\Phi(s)$. So by definition, $\Phi(s-t)=\Phi(s)-\Phi(t)$.

For (3), it suffices to show that a minus-algebra $(A,-)$ of functions
equipped with an operation $\sqcup$ satisfying the additional two laws for
minus-algebras with override that involve $\sqcup$ must have $\sqcup$ equal to
override. (In [13], the general idea behind this is called abstract
definability, in this case of $\sqcup$ from minus and domain restriction.) The
second law says that restricting the partial function $x\sqcup y$ to the
domain of $x$ yields $x$, while the first says that if this part of $x\sqcup
y$ is removed, the remainder is the same as what one obtains by restricting
$y$ to where $x$ is undefined. So in summary, $x\sqcup y$ is the union of $x$
with the restriction of $y$ to where $x$ is undefined, which is nothing but
their preferential union, or override of $y$ by $x$. The proof of (4) is very
similar.

For each of the signatures involving minus as in (5), if the 1-stack with
intersection axioms are added, then $\Phi$ respects intersection by (1)
(already shown).

Now we turn to (6). Let $s,t\in A$. We must show that $\Phi(s\sqcup
t)=\Phi(s)\sqcup\Phi(t)$ as partial functions. First we show their domains are
equal. Now $\overline{x}^{F}\in\text{dom}(\Phi(s\sqcup t))$ says that
$x(s\sqcup t)\in F$. But $x(s\sqcup t)=xs\sqcup xt$ by 3 in the definition of
1-stacks with intersection and override if $x\in A$, and trivially if $x=1$,
so this is equivalent to saying that $xs\in F$ or $xt\in F$, which is
equivalent to saying that $\overline{x}^{F}$ is in
$\text{dom}(\Phi(s))\cup\text{dom}(\Phi(t))$. So the domains are equal. For
$\overline{x}^{F}$ in this common domain, we consider two cases. (i) If
$\Phi(s)$ is defined at $\overline{x}$, so that $xs\in F$, then
$xs\circ(xs\sqcup xt)=xs=xs\circ xs$ by the first law for right normal bands
with intersection and override, so $\Phi(s\sqcup t)$ and $\Phi(s)$ agree at
$\overline{x}$. (ii) If $\Phi(s)$ is not defined at $\overline{x}$, so that
$xs\not\in F$, then necessarily $xt\in F$, and also $F\ni xs\sqcup
xt=((xs\sqcup xt)\cap xt)\sqcup xs$ by (3) in the definition of right normal
bands with intersection and override, so by primeness of $F$, $(xs\sqcup
xt)\cap xt\in F$, and so by Lemma 3.9, $x(s\sqcup t)=xs\sqcup xt\
\epsilon_{F}\ xt$, and so $\Phi(s\sqcup t)$ and $\Phi(t)$ agree at
$\overline{x}^{F}$. Overall then $\Phi(s\sqcup t)$ and $\Phi(s)\sqcup\Phi(t)$
agree at all $\overline{x}^{F}$ in their (equal) domains, hence are the same
partial functions.

Finally, we consider (7). Pick $s,t\in A$. Now $\overline{x}^{F}\in X$ is in
the domain of $\Phi(s)\diamond\Phi(t)$ if and only if $\overline{x}^{F}$ is in
the domain of $\Phi(s)$, that is, $xs\in F$, or equivalently (even if $x=1$ as
for $\sqcup$ above), $x(s\diamond t)=xs\diamond xt\in F$ (since $xs\diamond
xt\sim xs$), that is, $\overline{x}^{F}$ is in the domain of $\Phi(s\diamond
t)$. For such $\overline{x}^{F}$, we consider cases. (i) If $\overline{x}^{F}$
is in the domain of $\Phi(t)$, then $xt\in F$ and so $xt\circ xs\in F$, so
$(xt\circ xs)\circ xt=xs\circ xt=xt\circ(xs\diamond
xt)=xt\circ(xs\circ(xs\diamond xt))=(xt\circ xs)\circ(xs\diamond xt)$, we have
$(x(s\diamond t),xt)\in\epsilon_{F}$, and so $\Phi(s\diamond
t)(\overline{x}^{F})=\Phi(t)(\overline{x}^{F})$. (ii) If $\overline{x}^{F}$ is
not in the domain of $\Phi(t)$, then $xt\not\in F$ and so by the weakly prime
property, $xs\cap(xs\diamond xt)\in F$, and so because $xs\diamond
xt=x(s\diamond t)$, we have $(xs,x(s\diamond t))\in\epsilon_{F}$ by Lemma 3.9,
and so $\Phi(s\diamond t)=\Phi(s)$ at $\overline{x}^{F}$. So $\Phi(s\diamond
t)$ and $\Phi(s)\diamond\Phi(t)$ agree on their common domain and hence are
equal. ∎

From this theorem we obtain the following.

######  Theorem 4.4.

The algebras of partial functions of each of the signatures containing domain
restriction and composition listed below are axiomatised as the indicated
class of enriched 1-stacks.

  1. (1)

$(\cdot,\circ,\cap)$ $\leftrightarrow$ 1-stacks with intersection.

  2. (2)

$(\cdot,-)$ $\leftrightarrow$ minus-semigroups.

  3. (3)

$(\cdot,-,\sqcup)$ $\leftrightarrow$ minus-semigroups with override.

  4. (4)

$(\cdot,-,\diamond)$ $\leftrightarrow$ minus-semigroups with update.

  5. (5)

Any of the last three with intersection added $\leftrightarrow$ the relevant
axioms plus those for 1-stacks with intersection.

  6. (6)

$(\cdot,\circ,\cap,\sqcup)$ $\leftrightarrow$ 1-stacks with intersection and
override.

  7. (7)

$(\cdot,\circ,\cap,\diamond)$ $\leftrightarrow$ 1-stacks with intersection and
update.

Then from this and using the relevant one of Propositions 2.3, 2.4, 2.5, 2.6,
2.7 and 2.8, we obtain the following further consequence.

######  Corollary 4.5.

The algebras of partial functions of each of the signatures containing domain
restriction but not composition listed below are axiomatised as the indicated
class of enriched right normal bands.

  1. (1)

$(\circ,\cap)$ $\leftrightarrow$ right normal bands with intersection.

  2. (2)

$(-)$ $\leftrightarrow$ minus-algebras.

  3. (3)

$(-,\sqcup)$ $\leftrightarrow$ minus-algebras with override.

  4. (4)

$(-,\diamond)$ $\leftrightarrow$ minus-algebras with update.

  5. (5)

Any of the last three with intersection added $\leftrightarrow$ the relevant
axioms plus those for right normal bands with intersection.

  6. (6)

$(\circ,\cap,\sqcup)$ $\leftrightarrow$ right normal bands with intersection
and override.

  7. (7)

$(\circ,\cap,\diamond)$ $\leftrightarrow$ right normal bands with intersection
and update.

Of these nine cases, we believe all are new except for three. One is the
signature $(-,\sqcup)$: see [2] for a proof of completness of an equivalent
set of axioms for the equational theory, and [5] and [6] for full completeness
proofs of a different set of equivalent axioms. Another is the signature
$(-,\sqcup,\cap)$: see the discussion below on comparison algebras and
semigroups, and how they relate to pointed discriminator varieties. The third
is the signature $(-,\cap)$: as discussed earlier, this signature is
equivalent to the signature $(\circ,\backslash)$, which is finitely
axiomatised in [4].

In a minus-algebra $(A,-)$, the relation $\sim$ actually respects minus as
well: under the available functional interpretation, $a\sim b$ asserts that
$a,b$ have the same domains, so it follows that $a\sim b$ and $c\sim d$ imply
that $a-c\sim b-d$. Given the functional interpretation, it is easy to check
that $(A,-)/{\sim}$ is the dual of an implication algebra in the sense of [1],
hence is an implicative BCK-algebra by [17].

Note that in the minus-algebra with override $(A,\circ,-,\sqcup)$,
${A/{\sim}}$ is a distributive lattice with operations induced by
$\circ,\sqcup$ on $A$ (as follows easily from the functional interpretation),
and then $F$ is a prime filter in a minus-algebra with override precisely when
$F/{\sim}$ is a prime filter of this distributive lattice in the usual sense
for distributive lattices.

Finally, the next result appears in Section $3$ of [15].

######  Proposition 4.6.

The algebras of partial functions of signature $(\circ,\sqcup)$ are
axiomatised as the class of right handed strongly distributive skew lattices.

##  5\. Tidying up the axioms

We now spend time re-considering the sets of axioms given in Section 2, which
were purpose-built to facilitate the subsequent completeness proofs in terms
of partial functions. For some of the quasi-equational axiomatisations it is
possible to find an equivalent equational one or else show that this is
impossible. We also relate some of our axioms to other known axiomatisations.
(We defer consideration of the most parsimonious possible axiomatisations to
the supplementary Section 8.)

First note that the operation of “intersection” is abstractly defined in a
skew Boolean intersection algebra (SBIA) in the sense of [3] in terms of the
property that any two elements in a right normal band have a greatest lower
bound under the natural order. It turns out that this notion is relevant also
in the case of right normal bands with intersection.

######  Proposition 5.1.

If $(A,\circ)$ is a right normal band in which every two elements $s,t\in A$
have a greatest lower bound $s\wedge t$ under the natural order, then
$(A,\circ,\wedge)$ is a right normal band with intersection. Moreover ever
right normal band with intersection arises in this way.

Hence the class of right normal bands with intersection $(A,\circ,\cap)$ may
be axiomatised as follows.

  1. (1)

$(A,\circ)$ is a right normal band;

  2. (2)

the following law holds:

$x=x\circ y\And x=x\circ z\Leftrightarrow x=x\circ(y\cap z).$

###### Proof.

Recall that $\leq$ is the natural order on $A$, given by $x\leq y$ if and only
if $x=x\circ y$. Note that for all $x,y\in A$, $x\circ y\leq y$, and if $y\leq
z$ then $x\circ y\leq x\circ z$. (Direct proofs are easy but also follow
easily from the available functional interpetation.)

Assume $(A,\circ)$ is a right normal band in which every two elements $s,t\in
A$ have a greatest lower bound $s\wedge t$ under the natural order. Then of
course $(A,\wedge)$ is a semilattice, and by definition of the natural order
it satisfies the law $(x\wedge y)\circ x=x\wedge y$. It remains to check the
law $x\circ(y\wedge z)=(x\circ y)\wedge z$.

But for all $x,y,z\in A$, $x\circ(y\wedge z)\circ(x\circ y)=x\circ(y\wedge
z)\circ y=x\circ(y\wedge z)$, so $x\circ(y\wedge z)\leq x\circ y$. Moreover
$x\circ(y\wedge z)\leq y\wedge z\leq z$. So $x\circ(y\wedge z)\leq(x\circ
y)\wedge z$.

For the opposite inequality, since $x\circ y\leq y$, we have $(x\circ y)\wedge
z\leq y\wedge z$, and so $x\circ((x\circ y)\wedge z)\leq x\circ(y\wedge z)$.
Now suppose that $u\leq x\circ y$; then $x\circ u=x\circ u\circ x\circ
y=u\circ x\circ x\circ y=u\circ x\circ y=u$. Letting $u=(x\circ y)\wedge z$
gives that

$(x\circ y)\wedge z=x\circ((x\circ y)\wedge z)\leq x\circ(y\wedge
z)\leq(x\circ y)\wedge z,$

and the law follows.

Conversely, if $(A,\circ,\cap)$ is a right normal band with intersection, then
$(x\cap y)\circ x=x$ so $x\cap y\leq x$, and by symmmetry (since $x\cap
y=y\cap x$), $x\cap y\leq y$. If $u\leq x,y$ then $u\circ(x\cap y)=(u\circ
x)\cap(u\circ y)=x\cap y$, so $u\leq x\cap y$. So $\cap$ is meet in
$(A,\leq)$. ∎

Moving on to minus, recall that one of the laws of minus-algebras is an
equational implication. In fact it cannot be replaced by any purely equational
laws.

######  Proposition 5.2.

The class of minus-algebras is properly quasi-equational.

###### Proof.

We give an example of a minus-algebra that has a quotient that is not a minus-
algebra: specifically we show that necessary law

(3) $(x-y)\circ s=(x-y)\circ t\And y\circ s=y\circ t\Rightarrow x\circ
s=x\circ t$

fails. The example is essentially that used in the proof of [11, Proposition
11] to show that the class of modal restriction semigroups is a proper
quasivariety. We give the details as they are brief, and the law is different
to the direct translation of the property considered in [11]. We consider the
minus-algebra $A$ of functions on $\\{1,2,3\\}$ consisting of the empty
function along with the following six functions

$\displaystyle a:=\left(\begin{matrix}1&2&3\\\ 1&2&2\end{matrix}\right)$
$\displaystyle b:=\left(\begin{matrix}1&2&3\\\ 1&3&3\end{matrix}\right)$
$\displaystyle c:=\left(\begin{matrix}2&3\\\ 2&3\end{matrix}\right)$
$\displaystyle d:=\left(\begin{matrix}1\\\ 1\end{matrix}\right)$
$\displaystyle e:=\left(\begin{matrix}2&3\\\ 3&3\end{matrix}\right)$
$\displaystyle f:=\left(\begin{matrix}2&3\\\ 2&2\end{matrix}\right)$

It is routine to verify that this is closed under minus. Observe that

(4) $\displaystyle(c-d)\circ a$ $\displaystyle=c\circ a=a-(a-c)=a-d=e\text{
and}$ (5) $\displaystyle(c-d)\circ b$ $\displaystyle=c\circ b=b-(b-c)=b-d=f.$

It is also easily verified that

(6) $\displaystyle d\circ a=d\circ b=d$

Moreover, the equivalence relation $\theta$ that identifies $e$ and $f$ is a
congruence. Indeed, for every $x$ we have $e-x$ is equivalent modulo $\theta$
to $f-x$, and similarly for $x-e$ and $x-f$. As $\\{e,f\\}$ is the unique
nontrivial block of $\theta$, this verifies the stability of $\theta$ under
$-$. In the quotient $A/\theta$ we have $((c-d)\circ
a)/\theta=e/\theta=f/\theta((c-d)\circ b)/\theta$ by (4) and (5). By (6) we
have $d\circ a=d\circ b$. But $(c\circ a,c\circ b)=(a,b)\notin\theta$, so that
the law (3) fails when $(x,y,s,t)=(c,d,a,b)$. ∎

Proposition 5.2 extends to cover a corresponding result for the class of
minus-semigroups, as defining $st=0$ (the empty function) for all $s,t$ in the
above example gives a minus-semigroup with $\theta$ still a congruence on it.

As already noted, the class of minus-algebras with intersection is a finitely
based variety; this follows from the main result of [4], which is that the
class of algebras of functions of signature $(\circ,\backslash)$ is a finitely
axiomatised variety, given by the following laws:

  * •

$x\backslash(y\backslash x)=x$;

  * •

$x\cap y=y\cap x$;

  * •

$x\backslash y)\backslash z=(x\backslash z)\backslash y$;

  * •

$(x\circ z)\cap(y\circ z)=(x\backslash y)\backslash z$;

  * •

$(x\cap y)\circ x=x\cap y$.

(Here, as usual $s\cap t$ is defined to be $s\backslash(s\backslash t)$.) This
implies a finite equational axiomatisation for the equivalent signature
$(-,\cap)$. However, staying with the signature of $(\circ,\backslash)$, we
are easily able to extend the above result appearing in [4] to the signature
in which composition is added.

######  Proposition 5.3.

The class of algebras of functions of signature $(\cdot,\circ,\backslash)$ is
a finitely axiomatised variety, given by the following laws:

  * •

the above laws for algebras of signature $(\circ,\backslash)$ as in [4];

  * •

the laws for 1-stacks with intersection;

  * •

$s(t\backslash u)=st\backslash su$.

###### Proof.

The above laws are all sound for partial functions (for the final one, see
[20]). Conversely, given an algebra $(S,\cdot,\circ,\backslash)$ satisfying
these laws, define $s-t$ and $s\cap t$ in terms of $\circ,\backslash$ as in
Section 1. Then all the laws for minus-algebras with intersection must hold,
since we are assuming the complete laws involving $\circ,\backslash$ as in
[4]. We verify the minus-semigroup law: for all $s,t,u$,

$\displaystyle s(t-u)$ $\displaystyle=$ $\displaystyle s(t\backslash(u\circ
t))$ $\displaystyle=$ $\displaystyle st\backslash s(u\circ t)$
$\displaystyle=$ $\displaystyle st\backslash(su\circ st)$ $\displaystyle=$
$\displaystyle st-su,$

as required. So by (5) in Theorem 4.4 applied to (2) there, $(S,\cdot,-,\cap)$
can be represented as an algebra of partial functions. It only remains to
check that $\backslash,\circ$ are correctly represented. They will be
providing $s\backslash t=s-(s\cap t)$ and $s\circ t-t-(t-s)$ (since as in
Section 1, this is how they are definable in terms of $-,\cap$ as operations
on partial functions), with $s-t,s\cap t$ as defined in Section 1. But this
again follows from the completeness of the laws for $\backslash,\circ$ in [4].
∎

We also have the following new result.

######  Proposition 5.4.

The class of minus-algebras with override is a finitely based variety,
obtained by replacing the quasiequational law for minus-algebras by the
equational law $x=(y\circ x)\sqcup(x-y)$; hence so is the class of minus-
semigroups with override.

###### Proof.

Observe that the new equational law is sound. Conversely, if $s-x=t-x$ and
$x\circ s=x\circ t$ then

$s=(x\circ s)\sqcup(s-x)=(x\circ t)\sqcup(t-x)=t,$

as required. ∎

Right handed strongly distributive skew lattices as in Subsection 2.8 provide
an alternative route to the axiomatisation of minus-algebras with override,
the class considered in [2]. This is because minus is abstractly definable
from override and domain restriction in the sense used in [13, §3.1].

######  Proposition 5.5.

The class of algebras of functions of signature $(\circ,\sqcup,-)$ is
axiomatised as the class of right handed strongly distributive skew lattices
equipped with an operation $-$ satisfying the following:

  1. (1)

$0\circ x=0$;

  2. (2)

$(x-y)\circ y=0$;

  3. (3)

$(y\circ x)\sqcup(x-y)=x$.

###### Proof.

The three laws are easily seen to be sound, so it suffices to show that a
right handed strongly distributive skew lattice of functions
$(A,\circ,\sqcup)$ equipped with an operation $-$ satisfying the additional
three laws for minus just given must have $-$ equal to minus. Represent
$(A,\circ,\sqcup)$ as an algebra of functions. The law $0\circ x=0$ forces $0$
to be a subset of every function. Modify the representation by removing this
common part of every function: the result is easily seen to still be a
faithful representation of $A$, but now $0$ is represented as the empty
function. The second law then guarantees that under this representation, the
domain of $x-y$ lies outside that of $y$, and the third forces it to be minus
applied to $x,y$. ∎

This provides a nice counterpoint to the previously noted fact that override
is abstractly definable from minus. In this case, the abstract definability of
minus is from override, domain restriction and $0$.

The axiomatisation of the signature $(\circ,\sqcup,-)$ obtained by Leech in
[14] is very similar. A right-handed skew Boolean algebra is an algebra
$(A,\circ,\sqcup,-)$ satisfying the following laws:

  * •

$(A,\circ,\sqcup)$ is a right-handed strongly distributive skew lattice;

  * •

$x\circ 0=0\circ x=0$, $x\sqcup 0=0\sqcup x=x$;

  * •

$(x-y)\sqcup(y\circ x)=(y\circ x)\sqcup(x-y)=x$;

  * •

$(x-y)\circ y\circ x=y\circ x\circ(x-y)=0$.

In [14], the author showed that the algebras of partial functions of signature
$(\circ,\sqcup,-)$ are axiomatised as the class of right-handed skew Boolean
algebras. It follows that the axioms given in Proposition 5.5 for minus-
algebras with override must be equivalent to the rather more complex axioms
for right-handed skew Boolean algebras (something we have verified directly
using Prover9). The result in [14] was published prior to the axiomatisation
of the functional signature $(\circ,\sqcup)$ as right normal distributive
symmetric skew lattices given in [15] by the same author; we have just shown
that one can easily obtain the richer axiomatisation involving minus from the
one without it.

It follows from the third part of Corollary 4.5 that the axioms just given are
equivalent to those given earlier for minus-algebras with override, and so we
may use the former in place of the latter to obtain an alternative
axiomatisation for 1-stacks with minus and override.

Because adding intersection to the signature of minus-algebras with override
requires only the addition of two equational laws as in Subsection 2.2, we
obtain the following.

######  Corollary 5.6.

The class of minus-algebras with intersection and override is a variety; hence
so is the class of minus-semigroups with intersection and override.

######  Proposition 5.7.

The class of minus-algebras with update is a finitely based variety; hence so
is the class of minus-semigroups with update.

###### Proof.

It suffices to show that the one quasiequation in the definition of minus-
algebras follows from finitely many sound equations (which could therefore be
added to that axiomatisation in place of it to give a finite equational
axiomatisation).

Suppose $(A,\circ,-,\diamond)$ is a minus-algebra with update; hence it is
functionally representable. Suppose $a,b,c\in A$ are such that $c-b=a-b$ and
$b\circ c=b\circ a$. Our goal is to show that $a=c$.

Then using the sound law $x-y=(x-(y-z))-y$, we obtain

$c-a=(c-(a-b))-a=(c-(c-b))-a=(b\circ c)-a=b\circ a-a=0,$

on using the sound law $x\circ y-y=0$. So using the sound laws $x\circ
y=(x\diamond y)-(x-y)$ and $x-0=x$, we obtain

$c\circ a=(c\diamond a)-(c-a)=(c\diamond a)-0=c\diamond a.$

Now using the law $(x-y)\circ z=(x\circ z)-y$ for minus-algebras and again
using the law $(x\circ y)-y=0$, we have

$(b-c)\circ a=(b\circ a)-c=(b\circ c)-c=0.$

Hence $a-(b-c)=a-((b-c)\circ a))=a-0=a,$ upon using the further sound law
$x-y=x-(y\circ x)$. So again using the law $x-y=(x-(y-z))-y$, we see that

$a-c=(a-(c-b))-c=(a-(a-b))-c=(b\circ a)-c=0$

from earlier. So $c\diamond a=c\circ a=a-(a-c)=a-0=a$.

Now we note the following laws are sound:

$((y\diamond x)\diamond(y-z))\diamond(z\circ y)=y,\ x\diamond(x-y)=x.$

(The first is, because $(y\diamond x)\diamond(y-z)$ has domain the same as
$y$, and agrees with $y$ outside of the domain of $z$, so updating with $y$ on
the domain of $z$ forces it to equal $y$. The second is obvious.) Hence,

$c=((c\diamond a)\diamond(a-b))\diamond(b\circ
a)=(a\diamond(a-b))\diamond(b\circ a)=a\diamond(b\circ
a)=a\diamond(a-(a-b))=a,$

as required. ∎

######  Corollary 5.8.

The class of minus-algebras with intersection and update is a finitely based
variety.

For the signature consisting of minus, override and intersection, we saw
earlier that it was trivial to add $\cap$ to the signature of minus-algebras
with override using finitely many more equations as in Subsection 2.2,
yielding a finitely based variety with three binary operations. Alternatively,
we can use Proposition 5.1 and simply add the law

$x=x\circ y\And x=x\circ z\Leftrightarrow x=x\circ(y\circ z).$

Now recalling that the class of minus-algebras with override is the same as
the class of right handed skew Boolean algebras, this last observation leads
us to infer that the class of minus-algebras with intersection and override is
nothing but the class of right handed skew Boolean intersection algebras in
the sense of [3], which as noted in [6] is also the same as the class of
associative Boolean NLOs as defined by Cirulis in [5].

From the remarks made in the first section, any of these axioms for the
signature $(-,\sqcup,\cap)$ can then give a finite axiomatisation of the
algebras of signature $(\backslash,\sqcup)$, which as noted above is a natural
enrichment of the signature $(-,\sqcup)$ considered in [2] and is the richest
composition-free signature considered here. This richest signature may
usefully be thought of in yet another equivalent way.

The operation of generalised comparison for partial functions was defined in
[21], (at least for the case $Y=X$ but the definition is identical in the
general case). Its definition is as follows: for $f,g,h,k\in P(X,Y)$ and $x\in
X$,

$(f,g)[h,k](x):=\begin{cases}h(x)&\mbox{ if }f(x)=g(x)\mbox{ or neither is
defined}\\\ k(x)&\mbox{ otherwise.}\end{cases}$

In short, $(f,g)[h,k]$ is $h$ when $f,g$ do not disagree and $k$ otherwise. As
follows easily from what is observed there for the special case in which
$Y=X$, it is easy enough to see that

$f\backslash g=(f,f\cap g)[0,f]\mbox{ and }f\sqcup g=(f,g)[g,f].$

Indeed we may explicitly write

  * •

$f\cap g=(f,g)[f,0]$

  * •

$f\circ g=(f,0)[0,g]$

  * •

$g-f=(f,0)[g,0]$.

Conversely, it is straightforward to verify that

$(f,g)[h,k]=(f\cap g)\circ h\sqcup((h-f)-g)\sqcup k\mbox{ and }0=f-f,$

so the signature consisting of generalised comparison and zero is also
equivalent to $(\backslash,\sqcup)$ and hence to $(-,\cap,\sqcup)$. A
functional representation of generalised comparison semigroups with zero was
given in [21], which therefore provides a prior proof of the special case case
of (5) in Theorem 4.3 applied to (3), and similarly for the corresponding
parts of Corollary 4.5.

On this topic, it is shown in [3] that the variety $PD_{0}$ generated by the
so-called pointed discriminator algebras is equivalent to the variety of skew
Boolean intersection algebras. A special case of this gives that the class of
right handed skew Boolean intersection algebras (hence also of these various
other classes) is term equivalent to the variety of generalised comparison
algebras with zero as in [21], something which follows immediately from the
above remarks (since both are term equivalent to the variety of minus-algebras
with intersection and override).

We turn to the remaining signatures, which do not include minus.

As we have seen, the class of minus-semigroups with intersection and override
axiomatises the algebras of functions under the signature $(-,\sqcup,\cap)$,
and in fact these axioms are equivalent to those of right handed skew Boolean
intersection algebras. This latter class consists of those right handed skew
Boolean algebras in which every two elements have a meet $\cap$ under the
natural order. This follows from the fact that the class of right normal bands
with intersection is nothing but the class of right normal bands such that
every two elements have a meet under the natural order. Since partial
functions under signature $(\circ,\sqcup)$ are axiomatisable as the class of
right handed strongly distributive skew lattices, one might imagine by analogy
that the class of right normal bands with intersection and override may be
axiomatisable as those right handed strongly distributive skew lattices in
which every two elements have a meet under the natural order. But this is not
the case.

######  Example 5.9.

Consider the set of partial functions $A=\\{1,i,e,f,0\\}$ on $X=\\{a,b\\}$
defined as follows:

$1=\\{(a,a),(b,b)\\},\ i=\\{(a,b),(b,b)\\},\ e=\\{(a,a)\\},\ f=\\{(a,b)\\},\
0=\varnothing.$

It is easily checked that $A$ is closed under domain restriction and override,
so is a right handed strongly distributive skew lattice. Further, any two
elements $x,y\in A$ have a least upper bound $x\wedge y$ under the natural
order. However,

$((e\sqcup i)\wedge i)\sqcup e=(1\wedge i)\sqcup e=0\sqcup e=e\neq 1=e\sqcup
i,$

so the axiom $((x\sqcup y)\cap y)\sqcup x=x\sqcup y$ for right normal bands
with intersection and override does not hold.

We remark that this example is a right normal band having meet with respect to
its natural order, so by Proposition 5.1, it must be faithfully representable
in terms of partial functions as such. This may be achieved by adjusting the
definition of its elements so that $i$ becomes $\\{(a,b),(b,a)\\}$ with all
others unchanged. However, once this is done, $\sqcup$ is no longer correctly
represented since $e\sqcup i$ no longer equals $1$.

One remedy is to add to the laws for right-handed strongly distributive skew
lattices all of the laws for right normal bands with intersection and override
as in Subsection 2.6 (which by the sixth part of Corollary 4.5 are complete
for this signature), although the result contains repetitions and probably
further redundancy. These redundancies are explored in the supplementary
material in Section 8.

The class of right normal bands with intersection and update includes a
quasiequation in its axiomatic definition. This cannot be replaced by
equations.

######  Proposition 5.10.

The class of right normal bands with intersection and update is properly
quasi-equational, and so is the class of 1-stacks with intersection and
update.

###### Proof.

In $P(X_{1},X_{2})$, where $X_{1}=\\{x,y\\}$ and
$X_{2}=\\{x^{\prime},y^{\prime}\\}$, with all four of
$x,y,x^{\prime},y^{\prime}$ distinct, let $I$ denote the function
$\\{(x,x^{\prime}),(y,y^{\prime})\\}$, $b=\\{(y,x^{\prime})\\}$,
$c=\\{(y,y^{\prime})\\}$, $d=\\{(x,x^{\prime}),(y,x^{\prime})\\}$,
$e=\\{(x,x^{\prime})\\}$ and let $0$ denote the empty function. Let
$A=\\{1,b,c,d,e,0\\}$. It is routine to check that $A$ is closed under
$\circ,\diamond,\cap$ and is therefore a right normal band with intersection
and update. It is even closed under composition, with all composites equalling
$0$, and so is a 1-stack with intersection and update. The various Cayley
tables for the operations (other than composition) are as follows.

$\circ$ | $1$ | $b$ | $c$ | $d$ | $e$ | $0$
---|---|---|---|---|---|---
$1$ | $1$ | $b$ | $c$ | $d$ | $e$ | $0$
$b$ | $c$ | $b$ | $c$ | $b$ | $0$ | $0$
$c$ | $c$ | $b$ | $c$ | $b$ | $0$ | $0$
$d$ | $a$ | $b$ | $c$ | $d$ | $e$ | $0$
$e$ | $e$ | $0$ | $0$ | $e$ | $e$ | $0$
$0$ | $0$ | $0$ | $0$ | $0$ | $0$ | $0$
$\diamond$ | $1$ | $b$ | $c$ | $d$ | $e$ | $0$
---|---|---|---|---|---|---
$1$ | $1$ | $d$ | $1$ | $d$ | $1$ | $1$
$b$ | $c$ | $b$ | $c$ | $b$ | $b$ | $b$
$c$ | $c$ | $b$ | $c$ | $b$ | $c$ | $c$
$d$ | $a$ | $d$ | $a$ | $d$ | $d$ | $d$
$e$ | $e$ | $e$ | $e$ | $e$ | $e$ | $e$
$0$ | $0$ | $0$ | $0$ | $0$ | $0$ | $0$

$\cap$ | $1$ | $b$ | $c$ | $d$ | $e$ | $0$
---|---|---|---|---|---|---
$1$ | $1$ | $0$ | $c$ | $e$ | $e$ | $0$
$b$ | $0$ | $b$ | $0$ | $b$ | $0$ | $0$
$c$ | $c$ | $0$ | $c$ | $0$ | $0$ | $0$
$d$ | $e$ | $b$ | $0$ | $d$ | $e$ | $0$
$e$ | $e$ | $0$ | $0$ | $e$ | $e$ | $0$
$0$ | $0$ | $0$ | $0$ | $0$ | $0$ | $0$

From these, it is easy to see that the equivalence relation $\theta$ in which
$(e,0)\in\theta$, with all other elements of $A$ in their own
$\theta$-classes, is a congruence with respect to all of these three
operations, and trivially with respect to composition as well. However, in the
quotient algebra $A/\theta$ equipped with the induced operations, the one
quasiequation in the definition of right normal bands with update fails. This
is because

$(a\cap(a\diamond b))\circ a=(a\cap d)\circ a=e\circ a=e$

and

$(a\cap(a\diamond b)))\circ c=e\circ c=0\ \theta\ e,$

and moreover $b\circ a=c=b\circ c$. However, $a\circ a=a$ while $b\circ a=c$
and $(a,c)\not\in\theta$. ∎

Here is a table summarizing what is known. In it, if the status of a case is
known, there is an axiomatisation witnessing that status that is finitely
based. The cases shown here for the first time (as far as we know) are
indicated with a “$*$”.

signature | composition-free | with composition
---|---|---
$(\circ)$ | variety (right normal bands) | variety (1-stacks)
$(\circ,\cap)$ | variety $*$ | variety $*$
$(-)$ | proper quasivariety $*$ | proper quasivariety $*$
$(-,\cap)$ | variety ([4]) | variety $*$
$(-,\sqcup)$ | variety (RH SBAs) | variety $*$
$(-,\sqcup,\cap)$ | variety (RH SBIAs) | variety (comparison semis with zero)
$(-,\diamond)$ | variety $*$ | variety $*$
$(-,\diamond,\cap)$ | variety $*$ | variety $*$
$(\circ,\sqcup)$ | variety (RH strongly dist. skew lattices) | unknown
$(\circ,\diamond)$ | unknown | unknown
$(\circ,\sqcup,\cap)$ | variety $*$ | variety $*$
$(\circ,\diamond,\cap)$ | proper quasivariety $*$ | proper quasivariety $*$

##  6\. Left restriction semigroups and their enrichments

In this section we connect the classes of algebras considered here with left
restriction semigroups and their enrichments. This material only applies to
the cases in which composition is being modelled, so at least 1-stacks.

A left restriction semigroup is a unary semigroup with unary operation $D$
satisfying the following laws:

  * •

$D(x)x=x$;

  * •

$D(x)D(y)=D(y)D(x)$;

  * •

$D(D(x)y)=D(D(x)D(y))$;

  * •

$xD(y)=D(xy)x$.

It is well-known that the laws for left restriction semigroups axiomatise the
subalgebras of $PT(X)$ under composition and domain, defined as follows:

$D(f)=\\{(x,x)\in X\times X\mid x\in dom(f)\\}.$

This was first shown by [22], albeit using slightly different axioms and
terminology.

The following consequences of these laws are easily shown and in any case
well-known.

######  Lemma 6.1.

If $(A,\cdot,D)$ is a left restriction semigroup, then for $x,y\in A$,

  1. (1)

$D(x)^{2}=D(x)$,

  2. (2)

$D(x)D(y)=D(y)D(x)=D(D(x)y)$,

  3. (3)

$D(xy)D(x)=D(xy)$,

  4. (4)

$D(xy)=D(xD(y))$.

It is well-known, and in any case follows from the well-known representation
theorem for left restriction semigroups, that every left restriction semigroup
$(A,\cdot,D)$ gives a 1-stack $(A,\cdot,\circ)$ if we define $s\circ t=D(s)t$;
call this the derived 1-stack of the left restriction semigroup. However, in
general 1-stacks are not equivalent to left restriction semigroups, since
there are 1-stacks of functions containing no restrictions of the identity
map.

One situation in which 1-stacks and left restriction semigroups do correspond
arises when the operation modelling composition in a 1-stack has an identity
element $1$, for then we may define $D(s)=s\circ 1$ and obtain a left
restriction semigroup from which the original 1-stack may be derived. In fact,
if an identity is present, every type of enriched 1-stack so far considered
can be viewed as being a type of enriched left restriction semigroup with
identity. By modifying the representation $\Phi$ used in Proposition 4.1 by
not adjoining a new identity element $e$ to $A$ and making other small tweaks,
it is possible to ensure the resulting $\Phi$ is still a faithful
representation, but one in which $1$ is represented as the identity function.
We could then go on to obtain results for enriched left restriction monoids
corresponding to our earlier results for enriched 1-stacks.

We note that each of the operations considered here can be expressed in the
language of the modal restriction semigroups considered in [11]. There,
algebras of partial functions in $PT(X)$ equipped with at least composition
and “antidomain” $A$, where $A(t)$ is the identity map on $X$ restricted to
the complement of $\text{dom}(t)$, $t\in PT(X)$ together with some or all of
intersection and override (there called “preferential union”) in all possible
combinations, were axiomatised. Thus:

$D(s):=A(A(s)),\ s\circ t:=D(s)t,\ s-t:=A(t)s,\ s\diamond t:=D(s)(t\sqcup s).$

Conversely, the signature $(\cdot,1,A)$, where $1$ is the identity function,
is easily seen to be equivalent to $(\cdot,1,-)$, since $A(s)=1-s$ for all
$s\in PT(X)$, so modal restriction semigroups are nothing but minus-semigroups
with identity. This then extends to the various other signatures. The above
fairly straightforward adjustment to the definition of $\Phi$ in Proposition
4.1 does represent $1\in A$ correctly, and all else still works, so we could
thereby recover the axiomatisations obtained in [11].

However, the signatures considered in this article do not include the identity
function, so axiomatiations for algebras different to those considered in [11]
may be obtained. Instead, we start with an arbitrary left restriction
semigroup $(A,\cdot,D)$, possibly without identity, and represent its derived
1-stack using $\Phi$ as in Proposition 4.1.

######  Proposition 6.2.

Let $(A,\cdot,D)$ be a left restriction semigroup with $(A,\cdot,\circ)$ the
derived 1-stack, and suppose ${\mathcal{F}}$ is any separating set of filters
of $A$. Then $\Phi$ respects $D$.

###### Proof.

Now $\overline{x}_{F}\in\text{dom}(\Phi(D(a)))$ if and only if $xD(a)\in F$,
that is, $D(xa)x\in F$, or $(xa)\circ x\in F$, that is, $xa\in F$, or
$\overline{x}^{F}\in\text{dom}\Phi(a)$. For such $\overline{x}^{F}$, note that
$(xa)\circ x=D(xa)x=xD(a)=D(xD(a))xD(a)=D(xa)xD(a)=(xa)\circ(xD(a))$, so
$(x,xD(a))\in\epsilon_{F}$. Hence
$\Phi(D(a))(\overline{x}^{F})=\overline{xD(a)}^{F}=\overline{x}^{F}$, and so
$\Phi(D(a))$ is the identity function on $\text{dom}(\Phi(a))$, that is,
$\Phi(D(a))=D(\Phi(a))$. ∎

It now follows that we can obtain further axiomatisations of algebras of
partial functions, one for each of those considered so far, in which $D$ is
part of the signature. To obtain the new axioms, simply include the left
restriction semigroup axioms and interpret every occurrence of “$s\circ t$” in
an axiom as “$D(s)t$”. In this way, we immediately recover the familiar fact
that left restriction semigroups axiomatise algebras of partial functions
under composition and domain, and can go on to recover some previously known
axiomatisations as well as to uncover some new ones.

Here is a summary of the results applied to enriched left restriction
semigroups in the way just described. In each case, axioms follow via the
axioms for the relevant class of enriched 1-stacks given in Section 2,
modified to accommodate $D$ as above, and using the relevant part of Theorem
4.4 as well as Proposition 6.2 above.

  1. (1)

Signature $(\cdot,D,\cap)$. The resulting variety of enriched left restriction
semigroups was first axiomatised in [10] and [7].

  2. (2)

Signature $(\cdot,D,-)$. These have not previously been considered. Note that
the class of minus-semigroups is a proper quasivariety, as noted earlier. When
we introduce left restriction semigroup structure to induce the right normal
band structure, then adding an identity element $1$ with respect to the
composition operation, we obtain the class of modal restriction semigroups in
which $A(x)=1-x$, as in [11]. These form a proper quasivariety, as shown
there, so the current class must also.

  3. (3)

Signature $(\cdot,D,-,\cap)$. Not previously considered, but a variety,
following Proposition 5.3. With an identity element under composition added,
we obtain modal restriction semigroups with intersection as in [11].

  4. (4)

Signature $(\cdot,D,-,\sqcup)$. Again, not previously considered, but yields a
finitely based variety, as did $(\cdot,\circ,-,\sqcup)$. With an identity
element under composition added, we obtain modal restriction semigroups with
preferential union as in [11].

  5. (5)

Signature $(\cdot,D,-,\diamond)$. This is a new signature not previously
considered, even with an identity element present, and is a finitely based
variety due to Proposition 5.7. With a composition identity added, the
resulting class of modal restriction semigroups is a new one enriched with the
addition of update.

  6. (6)

Signature $(\cdot,D,\cap,\sqcup)$. This is a signature not previously
considered, again a finitely based variety. Since minus is not present, adding
a composition identity does not give a class of enriched modal restriction
semigroups.

  7. (7)

Signature $(\cdot,D,\cap,\diamond)$. Again, a new signature. We are uncertain
whether it is a variety.

##  7\. Open questions

This work considers signatures that can express domain restriction of
functions $\circ$. As already noted, Leech showed in [15] that the functional
algebras of signature $(\circ,\sqcup)$, or equivalently
$(\circ,\sqcup,\diamond)$, are finitely axiomatised as the variety of right
handed strongly distributive skew lattices. However, despite the fact that the
concept of a prime filter as in Subsection 3.6 makes sense in this setting,
our representation method as in Proposition 4.1 does not seem to represent
$\sqcup$ correctly when ${\mathcal{F}}$ is chosen to be the prime filters.
Hence the extended version of this signature in which composition is present
remains unaxiomatised.

We showed in Proposition 5.10 that the signature $(\circ,\diamond,\cap)$, with
and without composition added, gives a properly quasiequational
axiomatisation. However, although it seems likely, we are yet to confirm that
the class of functional algebras of signature $(\cdot,D,-,\diamond)$ is a
proper quasivariety. (The example in the proof of Proposition 5.10 does not
readily adapt to this setting.)

The set $P(X,Y)$ has a relational generalisation $R(X,Y)$, consisting of all
binary relations that are subsets of the power set of $X\times Y$. The various
operations described in this work all generalise to $R(X,Y)$ (within which
$P(X,Y)$ is a subalgebra). There is interest in axiomatising algebras of
binary relations under these operations. It is noted in Remark $3.5$ of [13]
that for signatures chosen from the operations $(\circ,\sqcup,-,\diamond)$, up
to isomorphism, the relational models are precisely the same as the functional
ones. Hence the algebras of binary relations under such signatures have the
same axiomatisations as the algebras of functions of the same signature.
However, when adding in either intersection or composition to these
signatures, this is no longer the case in general. There is interest in
whether finite axiomatisations exist for such signatures, and if so what they
are.

## References

  * [1] J.C. Abbott, Implication algebra, Bull. Math. Soc. Math. R. S. Roumania, 11:59 (1967), 1.
  * [2] J. Berendsen, D.N. Jansen, J. Schmaltz and F.W. Vaandrager, The axiomatization of override and update, Journal of Applied Logic 8 (2010), 141–150.
  * [3] R.J. Bignall and J.E. Leech, Skew Boolean algebras and discriminator varieties, Algebra Universalis 33 (1995), 387–398.
  * [4] C. Borlido and B. McLean, Difference-restriction algebras of partial functions: axiomatisations and representations, arxiv.org/abs/2011.15108v1.
  * [5] J. Cirulis, Nearlattices with an overriding operation, Order 28 (2011), 33–51.
  * [6] K. Cvetko-Vah, J. Leech, M. Spinks, Skew lattices and binary operations on functions, Journal of Applied Logic 11 (2013), 253–265.
  * [7] W. Dudek and V.S. Trokhimenko, Functional Menger $\mathcal{P}$-algebras, Comm. Algebra 30 (2002), 5921–5931.
  * [8] V.S. Garvac’kiĭ, $\cap$-semigroups of transformations, Theory of Semigroups and its Applications, No. 2, pp.2–13, Izdat. Saratov. Uni., Saratov, 1971. (Russian)
  * [9] R. Hirsch and T. Stokes, Axioms for signatures with domain and demonic composition, Algebra Universalis 82 (2021), Paper No. 24, 19 pp.
  * [10] M. Jackson and T. Stokes, Agreeable semigroups, J. Algebra 266 (2003), 393–417.
  * [11] M. Jackson and T. Stokes, Modal restriction semigroups: towards an algebra of functions, Internat. J. Algebra Comput. 21 (2011), 1053–1095.
  * [12] M. Jackson and T. Stokes, Monoids with tests and the algebra of possibly non-halting programs, Journal of Logic and Algebraic Programming 84 (2015), 259–275.
  * [13] M. Jackson and T. Stokes, Override and Update, J. Pure Appl. Algebra 225 (2021), Paper No. 106532, 17 pp.
  * [14] J. Leech, Skew Boolean algebras, Algebra Universalis 27 (1990), 497–506.
  * [15] J. Leech, Normal skew lattices, Semigroup Forum 44 (1992), 1–8.
  * [16] W. McCune, Prover9 and Mace4, version LADR-Dec-2007, (http://www.cs.unm.edu/mccune/prover9/).
  * [17] J. Meng, Implication algebras are dual to implicative BCK-algebras, Soochow J. Math. 22 (1996), 567–571.
  * [18] B.M. Schein, Relation algebras and function semigroups, Semigroup Forum 1 (1970), 1–62.
  * [19] B.M. Schein, Lectures on semigroups of transformations, Amer. Math. Soc. Translat. Ser. 2. 113 (1979), 123–181.
  * [20] B.M. Schein, Difference Semigroups, Comm. Alg. 20 (1992), 2153–2169.
  * [21] T. Stokes, Comparison semigroups and algebras of transformations, Semigroup Forum 81 (2010), 325–334.
  * [22] V.S Trokhimenko, Menger’s function systems. Izv. Vysš. Učebn. Zaved. Matematika 11 (1973) 71–78. (Russian)
  * [23] V.V. Vagner, Right normal bands, Izv. Vysš. Učebn. Zaved. Matematika 31 (1962), 19–27. (Russian)

##  8\. Supplementary material

There are many more simplifications to axioms that can be obtained, mostly
with the aid of Prover9/Mace4, but as these distract somewhat from the flow of
the main results of the article, and are often mechanical in nature, we
collect them here as supplementary material. Proofs obtained mechanically are
omitted, but can be easily verified using Prover9/Mace4 by entering the given
laws and testing for derivation of the relevant axioms obtained in the main
body of the paper.

In Proposition 5.1 we gave a simplification of the axioms in Subsection 2.2
for right normal bands with intersection. Using Prover9 and Mace4, it is
straightforward to verify the following significant trimming of the eight
equations implicit in the definition of right normal bands with intersection.

######  Proposition 8.1.

An irredundant equational axiomatisation for the class of right normal bands
with intersection is the following.

  * •

$(x\circ y)\circ z=(y\circ x)\circ z$

  * •

$x\cap x=x$

  * •

$x\cap y=y\cap x$

  * •

$(x\cap y)\circ x=x\cap y$

  * •

$x\circ(y\cap z)=(x\circ y)\cap z$

Use of Prover9 establishes that many of the laws for minus-algebras given in
Subsection 2.3 are redundant. We omit the rather long human proof, and instead
present a sufficient irredundant set of axioms in the next result.

######  Proposition 8.2.

The axioms for minus-algebras are equivalent to the following ones.

  * •

$(x\circ y)\circ z=(y\circ x)\circ z$

  * •

$x\circ y=y-(y-x)$

  * •

$0\circ x=0$

  * •

$(x-y)\circ z=(x\circ z)-y$

  * •

$s-x=t-x\And x\circ s=x\circ t\Rightarrow s=t$.

We note that if one uses the streamlined axioms for minus-algebras given in
Proposition 8.2, just adding the two for override as in Subsection 2.6, and
replacing the quasiequation for minus-algebras by the equational law
$x=(y\circ x)\sqcup(x-y)$, we find (at length) that the final right normal
band law is redundant. This gives the following.

######  Proposition 8.3.

The class of minus-algebras with override may be axiomatised as follows.

  * •

$x\circ y=y-(y-x)$

  * •

$0\circ x=0$

  * •

$(x-y)\circ z=(x\circ z)-y$

  * •

$x=(y\circ x)\sqcup(x-y)$

  * •

$(x\sqcup y)-x=y-x$

  * •

$x\circ(x\sqcup y)=x$

By eliminating $\circ$ using the first law, we obtain five laws, the same
number given in [2], the latter an axiomatisation shown equationally complete
there and subsequently shown complete in [6]. Introducing an operation
modelling composition as in Subsection 2.4, Prover9 shows that associativity
of composition is redundant, so only the law $x(y-z)=(xy)-(xz)$ need be added.

The axioms of Proposition 5.5 for minus-algebras with override, built from
those for right handed strongly distributive skew lattices, also contain
redundancies. With the aid of Prover9 we obtain the following simplification
in which 14 axioms are reduced to five.

######  Proposition 8.4.

The class of minus-algebras with override may be irredudantly axiomatised as
follows.

  * •

$x\circ(y\sqcup z)=(x\circ y)\sqcup(x\circ z)$

  * •

$(x\sqcup y)\circ z=(x\circ z)\sqcup(y\circ z)$

  * •

$x\circ(x\sqcup y)=x$

  * •

$(x-y)\circ y=0$

  * •

$(y\circ x)\sqcup(x-y)=x$

For the signature of domain restriction and override, starting with Leech’s
axioms for right handed strongly distributive skew lattices, Prover9/Mace4
showed that the following somewhat less impressive paring back of axioms is
possible.

######  Proposition 8.5.

For the algebras of functions of signature $(\circ,\sqcup)$, the following
axiomatisation is irredundant.

  * •

$(x\circ y)\circ x=y\circ x$

  * •

$(x\sqcup y)\sqcup z=x\sqcup(y\sqcup z)$

  * •

$x\circ(x\sqcup y)=x$

  * •

$(y\sqcup x)\circ x=x$

  * •

$x\circ(y\sqcup z)=(x\circ y)\sqcup(x\circ z)$

  * •

$(x\sqcup y)\circ z=(x\circ z)\sqcup(y\circ z)$

In Example 5.9 of the main text, we showed that a possibly simpler set of laws
for the signature $\\{\circ,\sqcup,\cap\\}$ was not complete, and subsequently
observed the required extra laws: add to the laws for right-handed strongly
distributive skew lattices all of the laws for right normal bands with
intersection and override as in Subsection 2.6. It was noted that these laws
would contain considerable redundancy including repetitions, and indeed
Prover9/Mace4 shows that of these additional laws added to those for right-
handed strongly distributive skew lattices, it is sufficient to add only the
law shown to fail in Example 5.9; moreover the laws for right-handed strongly
distributive skew lattice given in Proposition 8.5 also simplify.

######  Proposition 8.6.

The class of right normal bands with intersection and override may be
axiomatised as those algebras $(A,\circ,\sqcup,\cap)$ such that:

  * •

$x\circ(x\sqcup y)=x$

  * •

$(y\sqcup x)\circ x=x$

  * •

$x\circ(y\sqcup z)=(x\circ y)\sqcup(x\circ z)$

  * •

$(x\sqcup y)\circ z=(x\circ z)\sqcup(y\circ z)$

  * •

$x=x\circ y\And x=x\circ z\Leftrightarrow x=x\circ(y\cap z)$

  * •

$((x\sqcup y)\cap y)\sqcup x=x\sqcup y$

Starting instead with the axioms given in Subsection 2.6, Prover9/Mace4
revealed that the following set of axioms is minimally complete; note that it
contains none of the right normal band laws.

######  Proposition 8.7.

For the class of right normal bands with intersection and override, the
following axiomatisation is irredundant.

  * •

$x\cap y=y\cap x$

  * •

$x\circ(y\cap z)=(x\circ y)\cap z$

  * •

$x\circ(x\sqcup y)=x$

  * •

$((x\sqcup y)\cap y)\sqcup x=x\sqcup y$

  * •

$(x\sqcup y)\circ z=(x\circ z)\sqcup(y\circ z)$

As discussed in the introduction, it is possible to entirely eliminate $\circ$
from the signature, instead replacing it by update, using the facts that
$x\circ y=(x\diamond y)\cap y$ and $x\diamond y=x\circ(y\sqcup x)$, thereby
giving an equational axiomatisation for the algebras of partial functions of
signature $(\sqcup,\diamond,\cap)$. We could do this directly for the above
axioms. However, instead it seemed of more interest to start from the axioms
for override and update found in [13] and to attempt to augment them with
enough of the above axioms to incorporate intersection into that
axiomatisation. Here are those axioms from [13], proved complete there.

  * •

$x\sqcup(y\sqcup z)=(x\sqcup y)\sqcup z$

  * •

$x\sqcup x=x$

  * •

$x=x\diamond(x\sqcup y)$

  * •

$x\sqcup y=(y\diamond x)\sqcup x$

  * •

$(x\diamond y)\diamond z=x\diamond(z\sqcup y)$

  * •

$(x\sqcup y)\diamond z=(x\diamond z)\sqcup(y\diamond z)$

We then added translated versions of the laws in Proposition 8.7 to these,
eliminating as many as possible relative to those in [13], and only then
turning to elimination of any redundant laws in the above axioms for override
and update, all done using Prover9/Mace4. The result of this was that we were
only able to eliminate one of our translated laws. We also realised that, on
translation, the third law above was equivalent to the combination of the two
laws $x\diamond(x\sqcup y)=x$ and $x\cap(x\sqcup y)=x$, the former of which
proved redundant. With this noted, of the above laws for override and update,
most then proved redundant, leaving us with the following.

######  Proposition 8.8.

An irredundant axiomatisation for the algebras of functions of signature
$(\sqcup,\diamond,\cap)$ is as follows:

  * •

$x=x\diamond(x\sqcup y)$

  * •

$(x\diamond y)\diamond z=x\diamond(z\sqcup y)$

  * •

$x\cap y=y\cap x$

  * •

$(x\diamond(y\cap z))\cap(y\cap z)=((x\diamond y)\cap y)\cap z$

  * •

$x\cap(x\sqcup y)=x$

  * •

$((x\sqcup y)\cap y)\sqcup x=x\sqcup y$

  * •

$(x\sqcup y)\circ z=(x\circ z)\sqcup(y\circ z)$

For the class of 1-stacks with intersection and override, one further axiom
may be omitted, namely $x(y\circ z)=xy\circ xz$.

Next, for update and intersection, the software showed the following. (Proving
that the axiom $(x\circ y)\circ z=(y\circ x)\circ z$ is redundant was very
slow.)

######  Proposition 8.9.

For the class of right normal bands with intersection and update, the
following axiomatisation is irredundant.

  * •

$x\cap y=y\cap x$

  * •

$(x\cap y)\circ x=x\cap y$

  * •

$x\circ(y\cap z)=(x\circ y)\cap z$

  * •

$(x\diamond y)\circ x=x$

  * •

$x\diamond(x\diamond y)=x\diamond y$

  * •

$y\circ(x\diamond y)=x\circ y$

  * •

$(x\cap(x\diamond y))\circ u=(x\cap(x\diamond y))\circ v\And y\circ u=y\circ
v\Rightarrow x\circ u=x\circ v$

Again, it is possible to eliminate $\circ$ entirely, giving axioms involving
$\diamond,\cap$ that axiomatise algebras of partial functions of this
signature.

Finally we turn our attention to the axioms of Section 6 in the main text.
_Prover9/Mace4_ showed the following two results.

######  Proposition 8.10.

The following axiomatisation is irredundant for the functional signature
$(\cdot,D,\cap)$:

  * •

$x(yz)=(xy)z$

  * •

$xD(y)=D(xy)x$

  * •

$x\cap x=x$

  * •

$x\cap y=y\cap x$

  * •

$D(x\cap y)x=x\cap y$

  * •

$D(x)(y\cap z)=(D(x)y)\cap z$

  * •

$x(y\cap z)=(xy)\cap(xz)$

######  Proposition 8.11.

The following axiomatisation is irredundant for the signature
$(\cdot,D,\cap,\sqcup)$:

  * •

$x(yz)=(xy)z$

  * •

$xD(y)=D(xy)x$

  * •

$x\cap y=y\cap x$

  * •

$D(x)(y\cap z)=(D(x)y)\cap z$

  * •

$x(y\cap z)=(xy)\cap(xz)$

  * •

$D(x)(x\sqcup y)=x$

  * •

$((x\sqcup y)\cap y)\sqcup x=x\sqcup y$

  * •

$D(x\sqcup y)z=(D(x)z)\sqcup D(y)z$