Override and update

TL;DR

This paper establishes a complete set of axioms for the first order theory of override and update operations on partial functions, connecting these concepts with combinatorial geometry to solve a longstanding problem.

Contribution

It introduces a novel connection between override/update operations and combinatorial geometry, providing the first comprehensive axiomatization for their theory.

Findings

Complete finite axiomatization of override and update theory

Connection between partial functions and combinatorial geometry

Resolution of a major open problem in the area

Abstract

Override and update are natural constructions for combining partial functions, which arise in various program specification contexts. We use an unexpected connection with combinatorial geometry to provide a complete finite system of equational axioms for the first order theory of the override and update constructions on partial functions, resolving the main unsolved problem in the area.

Equations

$$(f\bigsqcup g)(x):=\{\begin{array}{ll}f(x)& \text{mbox}ifx\in \text{dom}(f),\\ g(x)& \text{mbox}ifx\in \text{dom}(g)\backslash \text{dom}(f),\\ \text{mbox}undefined& \text{mbox}otherwise.\end{array}$$

$$x$$

$$x\bigsqcup y$$

$$x[y][z]$$

$$(x\bigsqcup y)[z]$$

$$f-g=g\text{ where f is undefined}.$$

$$f@g=f\text{ where g is defined}$$

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

$$\cdot$$

$$f_1,f_2\text{ are defined at x but take different values to f(x),}$$

$$f_1,f_2\text{ are undefined at x,}$$

$$f_1(x)=f_2(x)=f(x)\text{ otherwise.}$$

$$x\bigsqcup x_1$$

$$x\bigsqcup x_2$$

$$x_2\bigsqcup x_1$$

$$\cdot$$

$$x(yz)$$

$$xx$$

$$xyx$$

$$\left\{\begin{array}{c}xy=x\&yx=y\\ \&z_{1}x=x\&z_{2n+1}y=y\end{array}\right\}\&$$

$${\chi }_F(H)=\{\begin{array}{ll}\text{undefined}& \text{ if }F\subseteq H\\ +& \text{ if }F\subseteq H^{+}\\ -& \text{ if }F\subseteq H^{-}\end{array}$$

$$x[y[x[z]]]=x[y[x][z]].$$

$$w[x[y[w[z]]]]=w[x[y[w][z]]].$$

$$x[y]\bigsqcup x$$

$$x\bigsqcup x[y]$$

$$x[y]\bigsqcup y$$

$$y\bigsqcup x[y]$$

$$x[y][z]$$

$$x[y]=x$$

$$x\bigsqcup z=z\&y\bigsqcup z=z$$

$$x\bigsqcup y=x\&y\bigsqcup x=y$$

$$x\bigsqcup y=x\&y\bigsqcup x=y\&v\bigsqcup x=v\bigsqcup y$$

$$x[y][z]\stackrel{\text{eqref}eq:leftdist}{=}x[z\bigsqcup y]\stackrel{\text{eqref}eq:absorb2}{=}x[y[z]\bigsqcup z]\stackrel{\text{eqref}eq:leftdist}{=}x[z][y[z]].$$

$$\ast$$

$$\underset{1\le i\le n-1}{\&}{x}_i[x_{i+1}]=x_i\to x_1[x_2[x_3[\dots [x_n[u]]\dots ]]]=x_1[x_2[x_3[\dots [x_n[x_1[u]]]\dots ]]]$$

$$\begin{gathered} \underset{1\le i\le n-1}{\&}{x}_i[x_{i+1}]=x_i \\ \to x_1[x_2[x_3[\dots [x_n[u]]\dots ]]]=x_1[(x_2[x_1])[(x_3[x_1])[\dots [(x_n[x_1])[u]]\dots ]]] \end{gathered}$$

$$x_1[x_2[x_3[\dots [x_{k+1}[u]]\dots ]]]=$$

$$=$$

$$\stackrel{\text{eqref}eq:special2}{=}$$

Full text

The first author was partially supported by ARC Future Fellowship FT120100666

1. Introduction

The constructions of override and update on partial functions were analysed by Berendsen, Jansen, Schmaltz, Vaandrager [1], with a view to giving a complete system of axioms. Formally, let $\mathcal{P}(X,Y)$ be the set of all functions having domains in the non-empty set $X$ and mapping into non-empty $Y$; these are to be viewed as modelling programs with inputs from $X$ and outputs in $Y$, with partiality reflecting the fact that the programs may abort or not halt for certain input values from $X$. The override operation is defined111We here use the notation “$\sqcup$” rather than $\triangleright$ as in [1], as $\triangleright$ conflicts with some well-established notation in the algebraic theory of functions, and $\sqcup$ has some current usage as override, under the name “preferential union” [8]. in [1] as follows: for all $f,g\in\mathcal{P}(X,Y)$,

[TABLE]

The operation of update $f[g]$ is then defined in [1] to be the restriction of $g\sqcup f$ to the domain of $f$. These constructions are natural enough in their own right, but are also widely encountered in formal methods for program specification and correctness, such as in the the specification language Z [16] and VDM-SL [9] amongst others; see [1] for further examples. The operations also have a natural interpretation as constructions on “patterned” Venn diagrams, where each partial function $f:X\to Y$ is thought of as a region of definition (a set, corresponding to $\text{dom}(f)$) and a “pattern” or “colour” (the action: thinking of $Y$ as a set of colours, each point in $\text{dom}(f)$ is assigned a colour by $f$, which collectively pattern the region $\text{dom}(f)$). The $\sqcup$ operation returns the union of the regions, with the pattern of the first region dominating the pattern of the second, while the $\underline{\phantom{a}}[\underline{\phantom{a}}]$ operation returns the first region, but with the pattern of the second region dominating where it overlaps; see Figure 1. This interpretation can also be recast in terms of choice functions on powersets – see Sections 3 and 6 – and in fact represents the free algebra for the class of representable algebras; see Theorem 3.4. A further manifestation of $\sqcup$ arises in combinatorial geometry, but we postpone discussion of this until Section 4.

A complete system of axioms in the signature $\{\sqcup,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$ is left as an open problem in [1]. A possible system is presented:

[TABLE]

along with associativity and idempotence of $\sqcup$. We have in [1, pp. 149]:

“Are these laws complete? If not, which laws should be added? Does there exist a finite equational axiomatization of override and update without auxiliary operators?”

The issue is subsequently revisited by Cvetko-Vah, Leech and Spinks [4] where similar questions are reiterated; see [4, pp. 262] (the penultimate paragraph of Section 6).

In this article we will resolve these questions by showing

• •

there is a valid equational law that does not follow from the speculated axiomatisations in both [1] and [4] and

• •

with the addition of this extra law, a full completeness result can be obtained.

In particular, the full first order theory of override and update on functions can be completely axiomatised by a finite set of equations.

After some preliminary development and investigation, we uncover the unexpected connection with combinatorial geometry and semigroup theory and use this to note an infinite axiomatisation for the signature of override alone (Corollary 4.1). No finite axiomatisation is possible for this signature. We then show how to extend this to an infinite complete axiomatisation for the main signature of interest $\{\sqcup,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$, but then provide an argument to show that these infinitely many laws are consequences of a finite set (Theorem 5.1). During this proof we make frequent reference to the automated theorem prover Prover9 and its companion counterexample program Mace4 (see [14]), although only Remark 5.2, which observes redundancies in axiom systems, states facts that are not proved directly in the article. There is also one counterexample obtained from Mace4, though this is in principle human-checkable.

Finally, in Section 6 we provide a description of the expressive power of update, from which various other similar results follow. In terms of patterned Venn diagrams, the result shows that any conceivable patterning of the subregions of a single global region can be achieved by applications of update alone.

2. Preliminaries: other operations and algebras of functions

Throughout, we refer to elements of $\mathcal{P}(X,Y)$ as “functions” (rather than partial functions or maps), and to subalgebras of $\mathcal{P}(X,Y)$ (with respect to some signature of operations $\tau$) as $\tau$-algebras of functions.

The authors of [1] embed the signature $\{\sqcup,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$ into a more expressive signature $\{\sqcup,-\}$, where the “minus” operation is defined by

[TABLE]

The operation of restrictive multiplication:

[TABLE]

arises as a term function by way of $f\mathbin{@}g=f-(f-g)$, and then $\underline{\phantom{a}}[\underline{\phantom{a}}]$ arises by way of $f[g]=(g\sqcup f)\mathbin{@}f$. In [1] restrictive multiplication is refered to as intersection, but we prefer to reserve this name for actual intersection, which applies to functions as

[TABLE]

and which goes back at least to the work of Garvac*′kiĭ [5]. Restrictive multiplication itself also has interest in its own right, and has been considered as far back as the pioneering work of Vagner [17]. The symbol $\triangleright$ is quite standard in abstract treatments of restrictive multiplication (see Schein [15] for one of many examples), albeit in reverse form as $f\mathbin{@}g=g\triangleright f$. As noted in the introduction, there is potential confusion here, as the $\triangleright$ symbol is used in [1] to denote override, though in the present article we have adopted $\sqcup$. We note that restrictive multiplication and minus also have natural interpretations in terms of patterned Venn diagrams; see Figure 2. (Amusingly, the Tik*Z command \clip used to produce the diagram for restrictive multiplication, and other diagrams in this article, is itself an example of the operation of restrictive multiplication: the command restricts a patterned circle centred to the left to the domain of a circle to the right.)

In [1, §6] it is shown that the pair of operations $\{-,\sqcup\}$ is expressive enough to produce all possible patternings over any Boolean combination of domains; here Boolean complementation is interpreted within the union of the master regions, and each subregion has a pattern consistent with that of a master region containing it. We revisit this in Section 6 of the present article, by showing that update alone is already capable of all possible patternings within a given domain.

A succinct set of equations is shown in [1] to be complete for the equational theory of functions with $\{\sqcup,-\}$, therefore obtaining laws to reason with $\{\sqcup,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$. We refer to the notion of completeness for equations as weak completeness, reserving completeness for the situation where all first order properties are consequences (rather than only equational properties). In general the setting of weak completeness still allows for a high level of incompleteness on nonequational properties: witness for example, Kozen’s axiom system KA which is complete for the equational theory of regular languages [10], versus the strong incompleteness result given in [11]. In the particular case of $\{\sqcup,-\}$, however, it was subsequently shown by Cvetko-Vah, Leech and Spinks [4] that full completeness holds anyway, as the system turns out to be term-equivalent to certain types of skew Boolean algebras previously considered by Leech in [12], where a complete axiomatisation of the algebras was given, and shown to be a variety. In fact both the signatures $\{\sqcup,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$ and $\{\sqcup,-\}$ are already expressible in the richer theory described in Cirulis [3] or indeed in the authors’ work [8], where completeness results are also obtained.

In subsequent work we will consider many of the remaining combinations of $\{\sqcup,\underline{\phantom{a}}[\underline{\phantom{a}}],\mathbin{@},-\}$, as well as operations of functional intersection $\cap$, set difference and even composition. In these cases we are able to find a unified approach that can be adjusted to obtain complete axiomatisations in each case, provided that restrictive multiplication is expressible. The original signature of interest $\{\sqcup,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$, which is the subject of the present article, distinguishes itself from these by seemingly requiring a different approach.

3. Preliminaries: representation basics and finite generation

In this preliminary section we observe some elementary facts concerning representable algebras: algebras that are faithfully representable as algebras of functions. Throughout, when $\tau$ is a signature of operations on functions, by a $\tau$-algebra of functions we mean an algebra whose elements are functions, and whose fundamental operations are the operations in $\tau$. We let $\operatorname{Rep}(\tau)$ denote the class of algebras isomorphic to $\tau$-algebras of functions.

The following easy observation (whose proof is omitted) details some of the flexibility available in choosing the set $Y$ when representing in an algebra of functions $\mathcal{P}(X,Y)$.

Lemma 3.1**.**

Let $X,Y$ be nonempty sets and $Z$ denote the disjoint union $X\times\{1\}\cup Y\times\{2\}$. For any subset $\tau\subseteq\{\sqcup,\underline{\phantom{a}}[\underline{\phantom{a}}],\mathbin{@},-\}$, the algebra $\langle\mathcal{P}(X,Y),\tau\rangle$ is isomorphic to $\langle\mathcal{P}(X\times\{1\},Y\times\{2\}),\tau\rangle$ which is a subalgebra of $\langle\mathcal{P}(Z,Z),\tau\rangle$.

The following lemma is also trivial.

Lemma 3.2**.**

Let $\tau\subseteq\{\sqcup,\underline{\phantom{a}}[\underline{\phantom{a}}],\mathbin{@},-\}$. Let $X,Y$ be sets, let $\theta$ be an equivalence relation on $Y$ and let $X^{\prime}$ be a subset of $X$.

1. (1)

Any function $f$ in $\mathcal{P}(X,Y)$ determines a function $f/\theta$ in $\mathcal{P}(X,Y/\theta)$ via $(f/\theta):x\mapsto f(x)/\theta$ and (as a $\tau$-algebra of functions) $\mathcal{P}(X,Y/\theta)$ is a quotient of $\mathcal{P}(X,Y)$. 2. (2)

Any function $f$ in $\mathcal{P}(X,Y)$ determines a function $f^{\prime}$ in $\mathcal{P}(X^{\prime},Y)$ by restricting its domain to $X^{\prime}$ and (as a $\tau$-algebra of functions) $\mathcal{P}(X^{\prime},Y)$ is a quotient of $\mathcal{P}(X,Y)$.

The following algebra ${\bf 3}$ and its reducts will play a prominent role.

[TABLE]

The algebra is isomorphic to $\langle\mathcal{P}(\{x\},\{+,-\});\sqcup,-\rangle$, where [math] is the empty function, $1$ maps $x$ to $+$ and $2$ maps $x$ to $-$. It is shown in [4] that the variety generated by ${\bf 3}$ coincides with the quasivariety generated by ${\bf 3}$, which in turn is precisely the class of representable $\{\sqcup,-\}$-algebras. We now give an alternative proof of this second fact, extending it to all reduct signatures as well.

Let $\tau\subseteq\{\sqcup,\mathbin{@},-,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$, and let ${\bf 3}_{\tau}$ be the reduct of ${\bf 3}$ to $\tau$. In the present article we are interested primarily in the signature $\{\sqcup\}$ and $\{\sqcup,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$, but the other cases are used in subsequent work and it is easier to prove one general result than to prove two specific ones. The arguments also work for term reducts of $\{\sqcup,\mathbin{@},-,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$ as well as reducts, but we omit this more general statement for notational brevity. There is also an extension to signatures including $\cap$, however we do not need this here and it requires replacement of ${\bf 3}$ by an infinite family of structures.

Theorem 3.3**.**

For any set of operations $\tau\subseteq\{\sqcup,\mathbin{@},-,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$ and any sets $X,Y$, the algebra ${\bf S}=\langle\mathcal{P}(X,Y),\tau\rangle$ is isomorphic to a subalgebra of a direct power of ${\bf 3}_{\tau}$, and hence $\operatorname{Rep}(\tau)$ coincides exactly with the class $\mathsf{SP}({\bf 3}_{\tau})$ of isomorphic copies of subalgebras of direct powers of ${\bf 3}_{\tau}$.

Proof.

First observe that as ${\bf 3}_{\tau}$ is representable, so too are all members of $\mathsf{SP}({\bf 3}_{\tau})$ (see [8, pp. 1062] for an example of the simple argument). Thus it remains to show that all representable algebras lie in $\mathsf{SP}({\bf 3}_{\tau})$. For this, it suffices to show that for $f\neq g$ in $\mathcal{P}(X,Y)$ there is a $\tau$-homomorphism $\phi:{\bf S}\to{\bf 3}_{\tau}$ (preserving $\sqcup$ as $\cdot$) such that $\phi(f)\neq\phi(g)$. Indeed, in this case we have that $\langle\mathcal{P}(X,Y),\tau\rangle$ embeds into $({\bf 3}_{\tau})^{\operatorname{hom}({\bf S},{\bf 3}_{\tau})}$ by the map sending $h\in\mathcal{P}(X,Y)$ to the tuple $\varepsilon_{h}(\phi)=\phi(h)$ (for each $\phi\in\operatorname{hom}({\bf S},{\bf 3}_{\tau})$).

So let $f\neq g$, and consider some point $x\in X$ where $f$ and $g$ disagree. Without loss of generality, assume that $f$ is defined at $x$ and either $g$ is not defined at $x$, or the value of $g$ is distinct from that of $f$ at $x$. Define an equivalence $\theta$ by $f_{1}\mathrel{\theta}f_{2}$ if

[TABLE]

This equivalence is a congruence in the signature $\{\sqcup,\mathbin{@},-,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$, and hence also in the signature $\tau$: indeed it is a combination of the two items in Lemma 3.2 (restrict to domain $\{x\}$, then identify all points in the range not equal to $f(x)$). The quotient ${\bf S}/\theta$ is isomorphic to a subsemigroup of ${\bf 3}_{\tau}$ (which is an isomorphism unless one of the three cases in the definition of $\theta$ does not occur). Also, $f$ is not $\theta$-related to $g$, so that the required separation property holds. ∎

A well-known theorem of Birkhoff (see [2, Corollary II.11.10] for example) shows that the free algebras for an $\mathsf{SP}$-closed class are contained within the class, and hence the free algebras for $\operatorname{Rep}(\tau)=\mathsf{SP}({\bf 3}_{\tau})$ are isomorphic to algebras of functions. As we now show, the free agebras have a natural representation as choice functions on families of subsets of a set. Recall that a choice function for a family $\{S_{i}\mid i\in I\}$ of sets is a map $\gamma:\{S_{i}\mid i\in I\}\to\bigcup_{i\in I}S_{i}$ with the property $\gamma(S_{i})\in S_{i}$ for each $i\in I$. For any nonempty set $S$, the set of all choice functions with domains equal to nonempty subsets of the powerset $\wp(S)$ is easily seen to form a $\tau$-subalgebra of $\mathcal{P}(\wp(S),S)$, which we will denote by $\operatorname{Choice}(S)$. The next theorem shows that the $S$-generated free algebra for $\operatorname{Rep}(\tau)$ can be represented in $\operatorname{Choice}(S)\leq\mathcal{P}(\wp(S),S)$, with the constant choice functions as free generators.

Theorem 3.4**.**

Fix a signature $\tau\subseteq\{\sqcup,\mathbin{@},-,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$ and let $F_{\tau}(S)$ denote the free algebra in $\mathsf{SP}({\bf 3}_{\tau})$ with free generators $S$. Then $F_{\tau}(S)$ embeds into $\operatorname{Choice}(S)$ via the map sending each $s\in S$ to the choice function with domain $\{A\subseteq S\mid s\in A\}$ and definition $A\mapsto s$.

The proof is via a series of applications of Lemma 3.2, but is postponed until Section 6 to maintain the flow of these preliminary sections. Theorem 3.4 shows that Venn diagram interpretations of $\tau$ terms are simply a diagrammatic visualisation of the free algebras (where each individual pattern denotes the generator chosen for that subregion). However, Theorem 3.4 itself does not describe exactly which choice functions appear in $F_{\tau}(S)$, only what the free generators are. When $\tau$ has the full strength of $\{\sqcup,\mathbin{@},-,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$, it is relatively straightforward to see that $F_{\tau}(S)$ coincides with $\operatorname{Choice}(S)$, and a result equivalent to this is given in Berendsen et al. [1, Proposition 14]. In contrast, the operation of $\underline{\phantom{a}}[\underline{\phantom{a}}]$ preserves domains, so for this signature, all choice functions in $F_{\{\underline{\phantom{a}}[\underline{\phantom{a}}]\}}(S)$ (as a subalgebra of $\operatorname{Choice}(S)$) must have domains identical to the domain of a free generator. We return to this in Section 6 where we show that $F_{\tau}(S)$ consists of all such choice functions; similar classifications for remaining signatures in $\{\sqcup,\mathbin{@},-,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$ then follow.

We did not describe relational semantics for the operations in $\{\sqcup,\mathbin{@},-,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$, however the given functional definitions extend to the case of relations (replacing statements such as $f(x)=y$ by $(x,y)\in f$).

Remark 3.5**.**

The proof of Theorem 3.3 continues to hold if binary relations are considered instead of functions. Thus there is no algebraic distinction between the relational case and the functional case for reducts of $\{\sqcup,\mathbin{@},-,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$.

3.1. Abstract definability

We now expand on some of the basic term function relationships between the operations as in the introduction. Each of the operations has been given a natural definition in the language of algebras of functions, but we now observe that sometimes this definition can be made solely in terms of the abstract algebraic properties. Rather than introduce all of the necessary terminology to make this precise, observe that each of the operations has been defined by formulæ in the multi-sorted language of concrete function. But often we will discover that some of the operations may be defined in terms of the others, without recourse to the full language of function. All of the following concepts can be generalised from function to other forms of binary (and higher arity) relations.

Suppose that $\{\divideontimes_{i}\mid i\in I\}$ is a signature of operation and relation symbols, but with each $\divideontimes_{i}$ having some agreed interpretation as an operation or relation on functions (more formally we would associate each $\divideontimes_{i}$ with a formula in the multi-sorted language of concrete algebras of functions). Similarly, let $\divideontimes$ (of arity $n$, say) be an operation, with some agreed definition on functions. We say that $\divideontimes$ is abstractly definable from $\{\divideontimes_{i}\mid i\in I\}$ (for functions) if there is a first order formula $\phi(x,x_{1},\dots,x_{n})$ in the signature $\{\divideontimes_{i}\mid i\in I\}$ such that in any concrete algebra of functions in the signature $\{\divideontimes_{i}\mid i\in I\}$, we have $h=\divideontimes(f_{1},\dots,f_{n})$ if and only if $\phi(h,f_{1},\dots,f_{n})$ holds. Note that we do not require that the algebra be closed under $\divideontimes$. The simplest instance of abstract definability is when $\divideontimes$ is simply a term function in $\{\divideontimes_{i}\mid i\in I\}$. Thus for example, $f[g]=(g\sqcup f)\mathbin{@}f$ so that $\underline{\phantom{a}}[\underline{\phantom{a}}]$ is a term function in $\{\mathbin{@},\sqcup\}$ and the formula $\phi(x,x_{1},x_{2})$ defining $\underline{\phantom{a}}[\underline{\phantom{a}}]$ is simply $x=(x_{2}\sqcup x_{1})\mathbin{@}x_{1}$. In this situation, every functional model of $\{\divideontimes_{i}\mid i\in I\}$ is automatically a model of $\divideontimes$. A familiar example of the more general form of abstract definability (albeit concerning algebras of permutations rather than algebras of functions) is the definability of inverse in semigroups of permutations by way of composition and identity: the defining formula $\phi(x,x_{1})$ is $x_{1}x=1\And xx_{1}=1$. Earlier work of the authors and their coauthors [8, §3.3], [6, §3.4], used examples of abstract definability to extend a representations for function composition and the antidomain operations to include the operation $\sqcup$. The following lemma gives a further example that plays an important role in our main proof.

Lemma 3.6**.**

The update operation $\underline{\phantom{a}}[\underline{\phantom{a}}]$ is abstractly definable from override $\sqcup$ by the formula $\phi_{1}(x,x_{1},x_{2})$ consisting of the conjunction of the following equalities:**

[TABLE]

Proof.

The parenthetical remarks are easily verified as true statements when $x,x_{1},x_{2}$ are functions, and $x=x_{1}[x_{2}]$. It is also trivial that these properties uniquely define the value of $x_{1}[x_{2}]$, so any function $x$ satisfying the equalities must coincide with $x_{1}[x_{2}]$. ∎

The following theorem demonstrates the utility of abstract definability in finding axiomatisations. We include the easy proof for completeness.

Theorem 3.7**.**

If $\divideontimes$ is abstractly definable by $\phi(x,x_{1},\dots,x_{n})$ from $\{\divideontimes_{i}\mid i\in I\}$ for functions and $\Sigma$ is a sound and complete axiomatisation for $\operatorname{Rep}(\{\divideontimes_{i}\mid i\in I\})$, then $\Sigma\cup\{\forall x_{1}\dots\forall x_{n}\,\phi(\divideontimes(x_{1},\dots,x_{n}),x_{1},\dots,x_{n})\}$ is a sound and complete axiomatisation for $\operatorname{Rep}(\{\divideontimes_{i}\mid i\in I\}\cup\{\divideontimes\})$.

Proof.

Certainly $\Sigma\cup\{\forall x_{1}\dots\forall x_{n}\,\phi(\divideontimes(x_{1},\dots,x_{n}),x_{1},\dots,x_{n})\}$ is a sound set of laws for $\{\divideontimes_{i}\mid i\in I\}\cup\{\divideontimes\}$ on functions, as we assumed that $\phi$ defined $\divideontimes$ from $\{\divideontimes_{i}\mid i\in I\}$. For completeness, we need to show that any model is representable. Now any model of $\Sigma\cup\{\forall x_{1}\dots\forall x_{n}\,\phi(\divideontimes(x_{1},\dots,x_{n}),x_{1},\dots,x_{n})\}$ is a model of $\Sigma$, and as $\Sigma$ is complete for representability of the operations $\{\divideontimes_{i}\mid i\in I\}$, it follows that there is a representation in this signature. But $\divideontimes$ is abstractly definable by $\phi(x,x_{1},\dots,x_{n})$, so that law $\forall x_{1}\dots\forall x_{n}\,\phi(\divideontimes(x_{1},\dots,x_{n}),x_{1},\dots,x_{n})$ ensures that $\divideontimes$ is also correctly represented, as required. ∎

4. Starting from override

We now explore a connection between override and combinatorial geometry, leading to an inherently infinite axiomatization.

Let $\mathcal{H}$ denote a finite set of hyperplanes in $\mathbb{R}^{n}$ (that is, subspaces of dimension $n-1$), each including the origin. Each $H\in\mathcal{H}$ partitions the space $\mathbb{R}^{n}$ into three regions: the set $H$ itself, along with two “sides”. If these sides are assigned values $+,-$ arbitrarily, then the family $\mathcal{H}$ (with, say, $|\mathcal{H}|=m$) partitions $\mathbb{R}^{n}$ into $3^{m}$ regions – or “faces” – with two points in the same region according to whether or not they satisfy the same relationships with respect to every $H\in\mathcal{H}$ (namely, for each $H\in\mathcal{H}$, either both lie in $H^{+}$, both in $H^{-}$, or both on $H$). Such a family of regions carries a natural multiplication, with $F\cdot G$ denoting the region reached from any point $p$ of $F$ by travelling any sufficiently small distance in a straight line toward any point $q$ of $G$. Note that if $F$ consists of a region that does not intersect any of the hyperplanes in $\mathcal{H}$, then $F\cdot G=F$.

This algebra is known as a hyperplane face monoid: the operation $\cdot$ is associative, and in fact is a left regular band operation; see Howie [7, §4.4]. Subsemigroups of hyperplane face monoids correspond to families of hyperplane faces closed under $\cdot$; we refer to these as hyperplane face semigroups. In Margolis, Saliola and Steinberg [13] it was shown that the class of semigroups isomorphic to hyperplane semigroups corresponds to the quasivariety generated by the three element monoid ${\bf L}$:

[TABLE]

(Note that ${\bf L}$ would usually be denoted by $L^{1}$ in semigroup theory, as it is the result of adjoining an identity element $1$ to the two-element left zero semigroup, but in our case the element [math] is notationally playing the role of $1$. However ${\bf L}$ is used in [13], and it is notationally convenient to continue this in the present article.) The article [13] also shows that the following infinite set $\Sigma_{\bf L}$ of axioms completely axiomatises the quasivariety generated by ${\bf L}$ (and no finite axiomatisation exists).

[TABLE]

We will refer to the $2n+3$ variable quasi-equation in $\Sigma_{\bf L}$ by $\lambda_{n}$.

Note that ${\bf L}$ is (isomorphic to) ${\bf 3}_{\{\sqcup\}}$, the $\sqcup$-reduct of ${\bf 3}$, and hence is representable as a $\sqcup$-algebra of functions. Moreover, because all hyperplane monoids embed into a power of ${\bf L}$, it follows that all hyperplane monoids are representable as $\sqcup$-algebras of functions. It is convenient to make this representation explicit. For a family of hyperplanes $\mathcal{H}$ (with each $H$ having $H^{+}$ and $H^{-}$ fixed), and a face $F$, define the partial characteristic function $\chi_{F}:\mathcal{H}\to\{+,-\}$ by

[TABLE]

It is essentially trivial to verify that the operation $\cdot$ on faces corresponds precisely to $\sqcup$ on the corresponding partial characteristic functions.

Corollary 4.1**.**

The class $\operatorname{Rep}(\sqcup)$ of algebras representable as $\sqcup$-algebras of functions is precisely the class of semigroups in the quasivariety of ${\bf L}$, and coincides at the finite level with the class of semigroups isomorphic to hyperplane face semigroups. The class is completely axiomatised by $\Sigma_{\bf L}$, and no complete finite axiomatisation is possible in first order logic.

Proof.

Note that ${\bf 3}_{\{\sqcup\}}$ is ${\bf L}$, so that the first statement is just the $\tau=\{\sqcup\}$ case of Theorem 3.3. The remaining statements are from the main results of [13]. ∎

An alternative proof of Corollary 4.1, based on the work of [13] is as follows, and may be useful in aiding the reader to understand the laws in $\Sigma_{\bf L}$ and some of the effort used to prove them in the next section. First, the quasivariety generated by ${\bf L}$ consists of representable algebras, so it suffices to show that every representable algebra lies in this quasivariety. Next verify that the laws $\Sigma_{\bf L}$ are sound for representable $\sqcup$-algebras. Indeed, the equational laws are easily verified. For the implications $\lambda_{n}$, observe that $x\sqcup y=y$ and $y\sqcup x=x$ together assert that $x$ and $y$ have the same domain. The laws $z_{i}\sqcup x=z_{i}\sqcup y$ ensure that $x$ and $y$ agree outside of the places where each $z_{i}$ are defined. In particular, $x$ and $y$ agree outside of the intersection of the domains of the $z_{i}$; let us denote this intersection by $D$. Now, all the $z_{i}$ are in agreement on $D$ because they are alternately extensions and restrictions of each other: $z_{1}\sqcup z_{2}=z_{2}$ asserts that $z_{1}$ is a restriction of $z_{2}$, $z_{3}\sqcup z_{2}=z_{2}$ asserts that $z_{2}$ extends $z_{3}$, and so on. But also, $x$ extends $z_{1}$ by $z_{1}\sqcup x=x$ and $y$ extends $z_{2n+1}$ by $z_{2n+1}\sqcup y=y$. So $x$ and $y$ also agree with all the $z_{i}$ on $D$, and hence they agree everywhere that they are both defined. Then $x=y$ as they have the same domain.

The variety generated by ${\bf L}$ is the variety of left regular bands, which is well known to be axiomatised by the first three laws of $\Sigma_{\bf L}$. So we have the following corollary.

Corollary 4.2**.**

The first three laws of $\Sigma_{\bf L}$ are weakly complete:* they are sound and complete for the equational theory of $\sqcup$-algebras of functions.*

5. Override and update

We now turn to the main signature of interest – override and update, $\{\sqcup,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$ – and solve the fundamental problem stated in [1] and [4].

To begin with we observe that axioms (1)–(4) (along with associativity and idempotence of $\sqcup$) that are presented in [1] are not complete; similarly with those given in [4, pp. 262]. Indeed, the following valid law is not a consequence:

[TABLE]

Validity is easily proved; see Figure 3.

Mace4 quickly finds a 16-element counterexample demonstrating the underivability of (8) from (1)–(4). A further law of similar structure to that of (8) is

[TABLE]

Equation (9) is also routinely shown to be sound, however we use it only to simplify our proof and note in Remark 5.2 that it is in fact redundant.

Theorem 5.1**.**

The laws (1)–(4), (8), (9) along with idempotence and associativity of $\sqcup$ constitute a complete equational axiomatisation for the class $\operatorname{Rep}(\{\sqcup,\underline{\phantom{a}}[\underline{\phantom{a}}]\})$ of algebras in the signature $\{\sqcup,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$ representable as systems of functions.

Remark 5.2**.**

There are redundancies in the axioms given in Theorem 5.1 and a complete axiomatisation for $\{\sqcup,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$ can be given by the laws (1), (2), (3), (8) along with idempotence and associativity of $\sqcup$. These redundancies can be easily established using Prover9. We have stated Theorem 5.1 with the larger redundant set, as these are the laws used in the proof presented here. The Prover9 proofs for the redundancy claim are not excessively complex, and human readable proofs could be obtained, but would add unnecessary routine technical tedium to the article. The reader wishing to avoid further technical deductions can omit Lemmas 5.4 and 5.5, provided that the laws proved there are added to the list of axioms in Theorem 5.1.

The proof of Theorem 5.1 covers the rest of the section. We prove completeness by first deriving a complete axiomatisation from the results of Section 4. This axiomatisation is infinite and involves quasiequations as well as equations. We then show that these infinitely many laws are consequences of the axioms in Theorem 5.1.

We begin by recalling that by Lemma 3.6, the update operation is abstractly definable from override, using the formula $\phi_{1}(x,y,z)$. Thus by Theorem 3.7, any complete axiomatisation of $\sqcup$ (such as $\Sigma_{\bf L}$) can be expanded to a complete axiomatisation of $\sqcup,\underline{\phantom{a}}[\underline{\phantom{a}}]$ by the addition of the law $\phi_{1}(x[y],x,y)$, which as a conjunction of equations, is equivalent to the following axioms (replacing the solution $x$ in (5), (6), (7) by the value $x_{1}[x_{2}]$, and renaming $x_{1}$ as $x$ and $x_{2}$ as $y$):

[TABLE]

We state this as a proposition.

Proposition 5.3**.**

A sound and complete axiomatisation for $\operatorname{Rep}(\{\sqcup,\underline{\phantom{a}}[\underline{\phantom{a}}]\})$ is obtained by adjoining (10)–(13) to $\Sigma_{\bf L}$.

Our goal now is to show that the laws in Proposition 5.3 follow from the laws in Theorem 5.1. A consequence of this is that there is a finite subset of $\Sigma_{L}$ which in the presence of (10)–(13) are sufficient to yield all of $\Sigma_{L}$, though we are unsure at this point which finite subset is sufficient. Surprisingly, Prover9 finds that $\lambda_{1}$ and $\lambda_{2}$ are consequences of (1)–(4), yet $\lambda_{3}$ is not. We were able to use Prover9 to demonstrate proofs that $\lambda_{3}$–$\lambda_{7}$ were consequences of the full axiom system in Theorem 5.1 (which involves the extra law (8)), and even decipher very long human-readable proofs from these in the case of $\lambda_{3}$ and $\lambda_{4}$. These intricate proofs did not provide many hints for a general proof for arbitrary $\lambda_{n}$. The main influence on the final approach we present (for all $\lambda_{n}$) was confidence that the axioms in Theorem 5.1 were likely correct, and that deep nesting of $\underline{\phantom{a}}[\underline{\phantom{a}}]$ may play a role.

Lemma 5.4**.**

The laws in Theorem 5.1 imply (10)–(13) as well as the equational laws in $\Sigma_{L}$ (associativity, idempotence and $x\sqcup y\sqcup x=x\sqcup y$).

Proof.

Idempotence and associativity of $\sqcup$ are immediate as they are included in Theorem 5.1. For $x\sqcup y\sqcup x=x\sqcup y$, observe that $(x\sqcup y)\sqcup x\stackrel{{\scriptstyle\eqref{eq:absorb2}}}{{=}}y[x]\sqcup x\sqcup x=y[x]\sqcup x\stackrel{{\scriptstyle\eqref{eq:absorb2}}}{{=}}x\sqcup y$. Next, law (11) follows by way of $x=x\sqcup x\stackrel{{\scriptstyle\eqref{eq:absorb}}}{{=}}x[x\sqcup y]\sqcup x\stackrel{{\scriptstyle\eqref{eq:leftdist}}}{{=}}x[y][x]\sqcup x\stackrel{{\scriptstyle\eqref{eq:absorb2}}}{{=}}x\sqcup x[y]$. For (13) use $x\sqcup y\stackrel{{\scriptstyle\eqref{eq:absorb}}}{{=}}(x\sqcup y)[(x\sqcup y)\sqcup y]\stackrel{{\scriptstyle\eqref{eq:rightdist}}}{{=}}x[(x\sqcup y)\sqcup y]\sqcup y[(x\sqcup y)\sqcup y]\stackrel{{\scriptstyle\eqref{eq:absorb}}}{{=}}x\sqcup y[(x\sqcup y)\sqcup y]\stackrel{{\scriptstyle\eqref{eq:leftdist}}}{{=}}x\sqcup y[y\sqcup y][x]\stackrel{{\scriptstyle\eqref{eq:absorb}}}{{=}}x\sqcup y[x]$. For (12) we have $y\sqcup x[y]\stackrel{{\scriptstyle\eqref{eq:absorb2}}}{{=}}x[y][y]\sqcup y\stackrel{{\scriptstyle\eqref{eq:leftdist}}}{{=}}x[y\sqcup y]\sqcup y=x[y]\sqcup y$. For (10) note that $x[y]\stackrel{{\scriptstyle\eqref{eq:absorb}}}{{=}}x[y][x[y]\sqcup x]\stackrel{{\scriptstyle\eqref{eq:leftdist}}}{{=}}x[x[y]\sqcup x\sqcup y]\stackrel{{\scriptstyle\eqref{eq:leftdist}}}{{=}}x[x\sqcup y][x[y]]\stackrel{{\scriptstyle\eqref{eq:absorb}}}{{=}}x[x[y]]$. Using this we obtain $x[y]\sqcup x\stackrel{{\scriptstyle\eqref{eq:absorb2}}}{{=}}x[x[y]]\sqcup x[y]=x[y]\sqcup x[y]=x[y]$, as required. ∎

We also need the following consequences.

Lemma 5.5**.**

The following laws are consequences of the axioms in Theorem 5.1.

[TABLE]

Proof.

For Equation (14) we have

[TABLE]

For (15), assume $x[y]=x$ and use $y\stackrel{{\scriptstyle\eqref{eq:absorb}}}{{=}}y[y\sqcup x]\stackrel{{\scriptstyle\eqref{eq:leftdist}}}{{=}}y[x][y]\stackrel{{\scriptstyle\eqref{eq:updateright}}}{{=}}y[y][x[y]]=y[x]$ with the last step using $x[y]=x$ and $y[y]=y[y\sqcup y]\stackrel{{\scriptstyle\eqref{eq:absorb}}}{{=}}y$. Now for (17), assume

[TABLE]

and obtain $y\stackrel{{\scriptstyle\eqref{eq:assumption}}}{{=}}y\sqcup x\stackrel{{\scriptstyle\eqref{eq:absorb2}}}{{=}}x[y]\sqcup y=x[y]\sqcup y[y]\stackrel{{\scriptstyle\eqref{eq:rightdist}}}{{=}}(x\sqcup y)[y]\stackrel{{\scriptstyle\eqref{eq:assumption}}}{{=}}x[y]\stackrel{{\scriptstyle\eqref{eq:absorb}}}{{=}}x[x\sqcup u][y]\stackrel{{\scriptstyle\eqref{eq:leftdist}}}{{=}}x[y\sqcup x\sqcup u]\stackrel{{\scriptstyle\eqref{eq:assumption}}}{{=}}x[y\sqcup u]\stackrel{{\scriptstyle\eqref{eq:leftdist}}}{{=}}x[u][y]$.

For (16) assume that $x,y,z$ satisfy the premise of (16). Then $x[z]=x[x\sqcup z]\stackrel{{\scriptstyle\eqref{eq:absorb}}}{{=}}x$ so that $x[y]=x[z][y]\stackrel{{\scriptstyle\eqref{eq:leftdist}}}{{=}}x[y\sqcup z]=x[z]=x$.

Finally, we prove (18). Note that the premise of the implication easily leads to $v[z]\sqcup x=v[z]\sqcup y$ for any $z$. Applying (3) twice gives $u[x][v[y][w]]=u[v[w\sqcup y]\sqcup x]$, and as $v[z]\sqcup x=v[z]\sqcup y$ for any $z$, we have $u[v[w\sqcup y]\sqcup x]=u[v[w\sqcup y]\sqcup y]\stackrel{{\scriptstyle\eqref{eq:leftdist}}}{{=}}u[y][v[y][w]]$ as required. ∎

We need further preliminary lemmas.

Lemma 5.6**.**

The following two implication schema are consequences of the axioms in Theorem 5.1:**

[TABLE]

and

[TABLE]

Proof.

We first prove the $\eta_{n}$ family, then the $\eta_{n}^{\prime}$ family. The proof is by induction on $n$. The base case is straightforward using $x_{2}=x_{2}[x_{1}]$ (by (15), from $x_{1}[x_{2}]=x_{1}$) as $x_{1}[x_{2}[u]]=x_{1}[x_{2}[x_{1}][u]]\stackrel{{\scriptstyle\eqref{eq:special}}}{{=}}x_{1}[x_{2}[x_{1}[u]]]$. Now let $k\geq 2$ and assume $\eta_{k}$ is true. Assume $x_{1},\dots,x_{k+1}$ satisfy the premise of $\eta_{k+1}$.

Then

[TABLE]

Now we look at the $\eta_{n}^{\prime}$ family. Let $n\geq 2$ be an arbitrary integer and assume that $x_{1},\dots,x_{n}$ satisfy the premise of $\eta_{n}^{\prime}$. We have

[TABLE]

This completes the proof of $\eta_{n}^{\prime}$, and hence of the lemma. ∎

Proof of Theorem 5.1.

It remains to show that the laws $\lambda_{n}$ are a consequence of the axioms in Theorem 5.1. We will assume that $x,y,z_{1},\dots,z_{2n+1}$ satisfy the premise of $\lambda_{n}$. The law $\lambda_{n}$ refers only to $\sqcup$, however there are number of atomic formulæ within the premise that are more conveniently expressed in terms of $\underline{\phantom{a}}[\underline{\phantom{a}}]$. First observe that the properties $z_{2i-1}\sqcup z_{2i}=z_{2i}$ and $z_{2i+1}\sqcup z_{2i}=z_{2i}$ imply $z_{2i-1}[z_{2i+1}]=z_{2i-1}$ by Equation (16) (and then $z_{2i+1}[z_{2i-1}]=z_{2i+1}$ by symmetry, or by (15)). It turns out we need only this simpler property (essentially: the expression $z_{2i-1}\sqcup z_{2i+1}$ could be shown to replace the role of $z_{2i}$, though we do not need this fact in the proof). Thus we need only the odd index $z$-variables, which we now label as $v_{1}:=z_{1}$, $v_{2}:=z_{3}$,…, $v_{n+1}=z_{2n+1}$, and so can now assume that for each $i$ we have $v_{i}\sqcup x=v_{i}\sqcup y$ as well as $v_{i}[v_{i+1}]=v_{i}$ and that $v_{1}\sqcup x=x$ and $v_{n+1}\sqcup y=y$. Our goal is to show that $x=y$. Note that (17) implies that $x[u][y]=y$ (for any $u$) and by symmetry $y[u][x]=x$. Also, the property $v_{1}\sqcup x=x$ implies that $x\stackrel{{\scriptstyle\eqref{eq:absorb}}}{{=}}x[x]=x[v_{1}\sqcup x]\stackrel{{\scriptstyle\eqref{eq:leftdist}}}{{=}}x[x][v_{1}]=x[v_{1}]$, which by symmetry gives $y=y[v_{n+1}]$ and then by (15) gives $v_{n+1}[y]=v_{n+1}$.

Now we have

[TABLE]

as required. ∎

6. Choice functions

We now return to the unproved claims in Section 3. We begin by proving Theorem 3.4, which gives a canonical representation of the free algebras for the class $\operatorname{Rep}(\tau)$.

Proof of Theorem 3.4.

By Theorem 3.3 we may assume that $F_{\tau}(S)$ is a subalgebra of $\mathcal{P}(A,B)$ for some sets $A,B$. Recall that $S$ denotes the free generators, which then are functions from $A$ to $B$. Let $\bar{S}=\{\bar{s}\mid s\in S\}$ be a disjoint copy of $S$ and let each $\bar{s}$ denote a function from $A$ to $B\times S$ defined by $a\mapsto(s(a),s)$ for each $a$ in the domain of $s$. Let $F^{\prime}_{\tau}(S)$ denote the subalgebra of $\mathcal{P}(A,B\times S)$ generated by $\bar{S}$. Using the first projection from $B\times S$, Lemma 3.2(1) shows that $F^{\prime}_{\tau}(S)$ maps homomorphically onto $F_{\tau}(S)$. This homomorphism maps $\bar{s}\mapsto s$ and so is bijective from the generators $\bar{S}$ to the free generators $S$. By the universal mapping property for $F_{\tau}(S)$, it follows that $F^{\prime}_{\tau}(S)$ is isomorphic to $F_{\tau}(S)$, with free generators $\bar{S}$.

Now consider the quotient of $B\times S$ corresponding to the second projection. This induces a proper quotient of $\mathcal{P}(A,B\times S)$, however it separates the elements of $F^{\prime}_{S}$. To see this, first note that the natural map described in Lemma 3.2(1) does not change the domain of any function, only the range. Second, note that two distinct elements $f\neq g$ of $F^{\prime}_{S}$ with the same domain must differ at some element $a\in A$. By a trivial induction argument on applications of operations from $\{\sqcup,\mathbin{@},-,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$ on elements from $\bar{S}$, it follows that there are $s_{f},s_{g}\in S$ with $f(a)=\bar{s}_{f}(a)$ and $g(a)=\bar{s}_{g}(a)$. But $\bar{s}_{f}(a)=(s_{f}(a),s_{f})$ and $\bar{s}_{g}(a)=(s_{g}(a),s_{g})$. Because $f(a)\neq g(a)$ we have $s_{f}\neq s_{g}$ and then the second projection from $B\times S$ to $S$ separates $f(a)=(s_{f}(a),s_{f})\mapsto s_{f}$ from $g(a)=(s_{g}(a),s_{g})\mapsto s_{g}$, as required. It now follows that $F_{\tau}(S)$ is isomorphic to the subalgebra of $\mathcal{P}(A,S)$ with each free generator $s\in S$ corresponding to a function from $A$ that maps its domain constantly to $s$. To avoid cumbersome notation, we now identify $F_{\tau}(S)$ with this subalgebra of $\mathcal{P}(A,S)$.

Define an equivalence relation $\equiv$ on $A$ by stating $x\equiv y$ if for all $s\in S$ either both $x,y\in\text{dom}(s)$ or $x,y\notin\text{dom}(s)$. It is clear that on each block of this equivalence, each element of $F_{\tau}(S)$ acts identically: it is either completely undefined, or maps the entire block to some $s\in S$. If we select a transversal $A^{\prime}$ of $\equiv$ (that is, one element is selected from each block of $\equiv$) and then replace $A$ by the subset $A^{\prime}$, then Lemma 3.2(2) shows that we have taken a quotient of $\mathcal{P}(A,S)$. As each element of $F_{\tau}(S)$ is either entirely undefined or entirely constant on each block of $\equiv$, it follows that this quotient separates the elements of $F_{\tau}(S)$; without loss of generality then, we will assume that $A=A^{\prime}$, or equivalently that $\equiv$ is the equality relation. Now we may identify $A$ with a subset of the powerset $\wp(S)$: indeed, we may label each element $a$ of $A$ by the subset of elements of $S$ defined at $a$. The assumption that $\equiv$ is the equality relation implies that this labelling is an injective function from $A$ into $\wp(S)$. Without loss of generality, we may identify $A$ with this subset of $\wp(S)$. Note then that each free generator $s\in S$ is defined at precisely those elements of $A$ that contain $s$. This nearly completes the proof, except that $A$ might possibly only contain some of the subsets of $S$. Applying Lemma 3.2(2) again (with $X=\wp(S)$ and $X^{\prime}=A$), we find that $F_{\tau}(S)$ is a homomorphic image of the subalgebra of $\mathcal{P}(\wp(S),S)$ described in the theorem statement, with generators mapping bijectively to the free generators of $F_{\tau}(S)$. The desired conclusion now follows by the universal mapping property for $F_{\tau}(S)$. ∎

As mentioned in Section 3, Berendsen et al. [1, §6] prove a completeness result for the operations of $\{-,\sqcup\}$ with respect to the patterned Venn diagram interpretation (over finitely many variables): any legitimate patterning of any set of regions can be achieved using $\{-,\sqcup\}$; see Proposition 14 of [1]. Under the canonical representation for the $\operatorname{Rep}(\{-,\sqcup\})$-free algebras (given in Theorem 3.4), this means that $F_{\{-,\sqcup\}}(S)$ coincides with $\operatorname{Choice}(S)$ as a $\{-,\sqcup\}$-algebra of functions. The update operation in contrast appears quite weak, as it is incapable of even changing the domain of a function. We now show that in any other sense it is the most expressive of the operations discussed above, since by using update alone we may achieve any legitimate patterning of the domain of a function. More formally: under the canonical representation given by Theorem 3.4, we show that when $S$ is finite, $F_{\underline{\phantom{a}}[\underline{\phantom{a}}]}(S)$ equals the family of all choice functions with domains $\{A\subseteq S\mid s\in A\}$, for $s\in S$. It will be convenient to denote a domain of this form by $D_{s}$, or $D_{i}$ in the case that the free generator is indexed as $s_{i}$.

We fix finitely many free generators $s_{1},\dots,s_{k}$. To avoid cumbersome notation in indexing we use the set $S=\{1,\dots,k\}$ in place of $\{s_{1},\dots,s_{k}\}$ and represent each free generator $s_{i}$ as the (unique) constant choice function on domain $D_{i}=\{A\subseteq\{1,\dots,k\}\mid i\in A\}$. If $t(x_{1},\dots,x_{k})$ denotes a term in the language $\{\underline{\phantom{a}}[\underline{\phantom{a}}]\}$, with left-most variable $x_{p}$, say, then $t(s_{1},\dots,s_{k})$ determines a choice function on $D_{p}$: on each $A=\{i_{1},\dots,i_{m}\}$ containing $p$, the function $t(s_{1},\dots,s_{k})$ must take one of the values $j\in\{i_{1},\dots,i_{m}\}$ (in agreement with a free generator $s_{j}$). Note that the Venn-diagrammatic representation of the set $\{i_{1},\dots,i_{m}\}$ is the subregion $\left(\bigcap_{j\in A}x_{j}\right)\cap\overline{\left(\bigcup_{j\notin A}x_{j}\right)}$ (where overline denotes complementation); see Figure 4 for an example with $k=4$. A term corresponding to the choice function in this figure is given after the proof of Theorem 6.1, as an example of the inductive process used in the proof.

Theorem 6.1**.**

Let $s_{1},\dots,s_{k}$ be the free generators for $F_{\{\underline{\phantom{a}}[\underline{\phantom{a}}]\}}(S)$ in its canonical representation in $\operatorname{Choice}(\{1,\dots,k\})$;* thus each $s_{i}$ is the constant choice function on domain $D_{i}$. Then for $p\in\{1,\dots,k\}$ and any choice function $\gamma$ with domain $D_{p}$, there is a term $t(x_{1},\dots,x_{k})$ in the language $\{\underline{\phantom{a}}[\underline{\phantom{a}}]\}$ with $t(s_{1},\dots,s_{k})=\gamma$.*

Proof.

We work slightly more generally, by taking any choice function $\gamma$ on the domain $\wp^{+}(\{1,\dots,k\})$ of all nonempty subsets of $\{1,\dots,k\}$. We aim to construct an update term that agrees with the restriction of $\gamma$ to $D_{p}$. We work inductively down $L:=\wp^{+}(\{1,\dots,k\})$. For each $A\in L$, let $\gamma|_{A}$ denote the restriction of $\gamma$ to the upset ${\uparrow}A$ of $A$ in $L$. For each $j$ in such an $A$ we will construct a term $t_{j\in A}$ with leftmost variable $x_{j}$ and such that the choice function $t_{j\in A}(s_{1},\dots,s_{k})$ agrees with $\gamma|_{A}$ on the elements of the upset of $A$ in $L$.

The base case of the induction will be the top element $\top:=\{1,\dots,k\}$. For each $j\in\{1,\dots,k\}$ we let $t_{j\in\top}$ be the term $x_{j}[x_{\gamma(\top)}]$. The function $t_{j\in\top}(s_{1},\dots,s_{k})=s_{j}[s_{\gamma(\top)}]$ has domain $D_{j}$, and coincides with $s_{\gamma(\top)}$ on $\bigcap_{1\leq i\leq k}D_{i}=\{\top\}$. Hence $t_{j\in\top}(s_{1},\dots,s_{k})$ agrees with $\gamma$ on $\top$.

Now assume that for some $i\geq 0$ and every subset $A\subseteq\{1,\dots,k\}$ with $|A|=k-i$, and every $j\in A$ we have defined a term $t_{j\in A}$ that agrees with $\gamma|_{A}$ on ${\uparrow}A$ and has leftmost variable $x_{j}$. If $i=k-1$ we are done, as then the $(k-i)$-element subsets are the singleton subsets, and $t_{p\in\{p\}}(s_{1},\dots,s_{k})$ agrees with $\gamma$ on the upset of $\{p\}$ (that is, on $D_{p}$), which completes the proof. So now assume $i<k-1$ and consider some set $A\subseteq\{1,\dots,k\}$ with $|A|=k-(i+1)\geq 1$. For each $j\notin A$, the set $A_{j}:=A\cup\{j\}$ has size $k-i$, so the induction hypothesis gives a term $t_{j\in A_{j}}$ agreeing with $\gamma$ on $\operatorname{\uparrow}(A\cup\{j\})$. There are precisely $i+1$ such choices for $j\notin A$, and we will enumerate them as $j_{1},\dots,j_{i+1}$. The induction step is based over the observation that

[TABLE]

For each $\ell\in A$, define

[TABLE]

The function $t_{\ell\in A}(s_{1},\dots,s_{k})$ has domain $D_{\ell}$ and agrees with $s_{\gamma(A)}$ on the region $\bigcap_{j\in A}D_{j}\cap\overline{\bigcup_{j\notin A}D_{j}}=\{A\}$ (that is, $t_{\ell\in A}(s_{1},\dots,s_{k})$ agrees with $\gamma$ at the point $A$) and by the induction hypothesis determines the same choice function as $\gamma$ on each set in ${\uparrow}A_{j_{1}},\dots,{\uparrow}A_{j_{i+1}}$. Thus $\gamma_{t_{\ell\in A}}(s_{1},\dots,s_{k})$ agrees with $\gamma_{A}$ on ${\uparrow}A$, as required. ∎

As example of the proof method, we work through the example choice function in Figure 4$(d,f)$, which has domain $D_{1}$ corresponding to $x_{1}$. We obtain:

• •

$t_{i\in\{1,2,3,4\}}=x_{i}[x_{1}]$;

• •

$t_{2\in\{1,2,3\}}$ is $x_{2}[x_{3}][x_{4}[x_{1}]]$ and $t_{3\in\{1,2,3\}}$ is $x_{3}[x_{3}][x_{4}[x_{1}]]$;

• •

$t_{2\in\{1,2,4\}}$ is $x_{2}[x_{2}][x_{3}[x_{1}]]$ and $t_{4\in\{1,2,4\}}$ is $x_{4}[x_{2}][x_{3}[x_{1}]]$;

• •

$t_{3\in\{1,3,4\}}$ is $x_{3}[x_{4}][x_{2}[x_{1}]]$ and $t_{4\in\{1,3,4\}}$ is $x_{4}[x_{4}][x_{2}[x_{1}]]$;

• •

$t_{2\in\{1,2\}}$ is $x_{2}[x_{2}][t_{3\in\{1,2,3\}}][t_{4\in\{1,2,4\}}]=x_{2}[x_{2}][x_{3}[x_{3}][x_{4}[x_{1}]]][x_{4}[x_{2}][x_{3}[x_{1}]]]$;

• •

$t_{3\in\{1,3\}}$ is $x_{3}[x_{1}][t_{2\in\{1,2,3\}}][t_{4\in\{1,3,4\}}]=x_{3}[x_{1}][x_{2}[x_{3}][x_{4}[x_{1}]]][x_{4}[x_{4}][x_{2}[x_{1}]]]$;

• •

$t_{4\in\{1,4\}}$ is $x_{4}[x_{4}][t_{2\in\{1,2,4\}}][t_{3\in\{1,3,4\}}]=x_{4}[x_{4}][x_{2}[x_{2}][x_{3}[x_{1}]]][x_{3}[x_{4}][x_{2}[x_{1}]]]$;

• •

$t_{1\in\{1\}}$ is $x_{1}[x_{1}][t_{2\in\{1,2\}}][t_{3\in\{1,3\}}][t_{4\in\{1,4\}}]$,

which is

[TABLE]

There are clearly redundancies in this construction argument, as all instances of $x_{i}[x_{i}]$ can be replaced by $x_{i}$, and the $t_{3\in\{1,3\}}$ term updates all further subsets of $\{1,2,3,4\}$ containing both $1$ and $3$, and subsequently $t_{4\in\{1,4\}}$ updates all subsets containing both $1$ and $4$. Thus we need only the $x_{2}[x_{2}]=x_{2}$ part of $t_{2\in\{1,2\}}$ and the $x_{3}[x_{1}][t_{2\in\{1,2,3\}}]$ part of $t_{3\in\{1,3\}}$. Then $t_{1\in\{1\}}$ simplifies to

[TABLE]

The number of choice functions on the upset of a singleton is easily seen to be $\prod_{1\leq i\leq n}i^{\binom{n}{i}}$, so that the following result is an immediate corollary.

Corollary 6.2**.**

The $n$-generated free algebra in the variety generated by ${\bf 3}_{\{\underline{\phantom{a}}[\underline{\phantom{a}}]\}}$ has

[TABLE]

elements.

The power of expressibility of update terms easily extends to similar characterisations of the power of expressibility of other subsignatures of $\{\underline{\phantom{a}}[\underline{\phantom{a}}],\sqcup,@,-\}$ containing $\underline{\phantom{a}}[\underline{\phantom{a}}]$. For example, in the signature $\{@,\underline{\phantom{a}}[\underline{\phantom{a}}]\}$, we may use $@$ to form any desired intersection of domains, and then use update to pattern freely within these domains. It is very easy to see that the intersection of the domains of free generators in $F_{\tau}(S)$ (as a subalgebra of $\operatorname{Choice}(S)$) is precisely the set of principal upsets in the ordered set $\wp^{+}(S)$ of nonempty subsets of $S$. Thus, it follows from Theorem 6.1 that under the canonical representation into $\operatorname{Choice}(S)$, the free algebra $F_{\{@,\underline{\phantom{a}}[\underline{\phantom{a}}]\}}(S)$ is precisely the set of all choice functions in $\operatorname{Choice}(S)$ having a domain that is a principal upset in $\wp^{+}(S)$. Similarly, $\sqcup$ can be used to take unions of domains, so that $F_{\{\sqcup,@,\underline{\phantom{a}}[\underline{\phantom{a}}]\}}(S)$ consists of all choice functions on upsets in $\wp^{+}(S)$, while $F_{\{\sqcup,\underline{\phantom{a}}[\underline{\phantom{a}}]\}}(S)$ consists of all choice functions on unions of domains of the form $D_{s}$.

7. Conclusions, open problems and subsequent work

We have shown that the class $\operatorname{Rep}(\sqcup,\underline{\phantom{a}}[\underline{\phantom{a}}])$ of algebras that are isomorphic to systems of functions with override and update form a variety with a relatively simple finite axiomatisation. The class $\operatorname{Rep}(\sqcup)$ of override alone forms a nonfinitely axiomatisable quasivariety, but is not a variety, though its equational theory has a finite axiomatisation.

In future work we will develop a uniform approach to representability that will enable us to give complete axiomatisations for $\operatorname{Rep}(\tau)$ in all combinations of the other operations discussed in Section 2, provided that restriction is expressible. That approach does not extend to the critical case of override and update considered in the present work.

In Section 6 we have given a concrete description of the free algebras for the class $\operatorname{Rep}(\underline{\phantom{a}}[\underline{\phantom{a}}])$ which shows that update has surprisingly strong expressive power, and perhaps some extra prominence amongst the operations considered. Yet many properties of update remain elusive. The proof method described in Theorem 6.1 makes use of a kind of normal form for expressions in $\underline{\phantom{a}}[\underline{\phantom{a}}]$, and then also for subsignatures of $\{\underline{\phantom{a}}[\underline{\phantom{a}}],\sqcup,@,-\}$ containing it. Yet there remains the lack of any clear process for simplifying terms, for understanding equivalence of terms, for determining the minimum size of equivalent terms, and nor do we have a complete axiomatisation for $\operatorname{Rep}(\underline{\phantom{a}}[\underline{\phantom{a}}])$.

A further line of investigation is to incorporate composition of functions into the signature wherever possible. While all of these signatures can be expressed as term reducts of the signatures characterised by the authors in [8] and in [6], many of the combinations sit naturally with composition and remain unclassified. In future work on signatures that include $\mathbin{@}$, we expect it to be straightforward to add composition to the signatures considered.