* This is an extended version of [1].

# No-Go Theorems for Distributive Laws

Maaike Zwart  Department of Computer Science
University of Oxford<EMAIL_ADDRESS>and  Dan Marsden  Department
of Computer Science
University of Oxford<EMAIL_ADDRESS>
###### Abstract.

Monads are commonplace in computer science, and can be composed using Beck’s
distributive laws. Unfortunately, finding distributive laws can be extremely
difficult and error-prone. The literature contains some general principles for
constructing distributive laws. However, until now there have been no such
techniques for establishing when no distributive law exists.

We present three families of theorems for showing when there can be no
distributive law between two monads. The first widely generalizes a
counterexample attributed to Plotkin. It covers all the previous known no-go
results for specific pairs of monads, and includes many new results. The
second and third families are entirely novel, encompassing various new
practical situations. For example, they negatively resolve the open question
of whether the list monad distributes over itself, reveal a previously
unobserved error in the literature, and confirm a conjecture made by Beck
himself in his first paper on distributive laws. In addition, we establish
conditions under which there can be at most one possible distributive law
between two monads, proving various known distributive laws to be unique.

###### Key words and phrases:

monads, distributive laws, compositionality, no-go theorems

##  1\. Introduction

Monads have become a key tool in computer science. They are, amongst other
things, used to provide semantics for computational effects such as state,
exceptions, and I/O [2]. They are also used to structure functional programs
[3, 4], and even appear explicitly in the standard library of the Haskell
programming language [5]. As such, it is important to fully understand and
characterise their behaviour.

Monads are a categorical concept. A monad on a category $\mathcal{C}$ is a
triple $\langle T,\eta,\mu\rangle$ consisting of an endofunctor
$T:\mathcal{C}\rightarrow\mathcal{C}$ and two natural transformations
$\eta:1\Rightarrow T$ and $\mu:T\circ T\Rightarrow T$ satisfying axioms
described in Definition 2.1. Given two monads with underlying functors $S$ and
$T$, it is natural to ask if $T\circ S$ always carries the structure of a
monad. This would, for example, provide a way to combine simple monads
together to model more complex computational effects.

Unfortunately, composing the functor parts of two monads does not, in general,
result in a new monad. Beck has shown that the existence of a  _distributive
law_ provides sufficient (but not necessary) conditions for such a composition
to form a monad [6]. A distributive law between monads $S$ and $T$ is a
natural transformation of type:

$S\circ T\Rightarrow T\circ S,$

satisfying four equations described in Definition 2.1 below. This important
idea has since been generalised to notions of distributive laws for combining
monads with comonads, monads with pointed endofunctors, endofunctors with
endofunctors and various other combinations, see for example the work by
Lenisa _et al._ [7].

General-purpose techniques have been developed for constructing distributive
laws [8, 9, 10, 11, 12]. These methods are highly valuable, for, in the words
of Bonsangue _et al._ : _“It can be rather difficult to prove the defining
axioms of a distributive law.”_ [8]. In fact, it can be so difficult that on
occasion a distributive law has been published which later turned out to be
incorrect; Klin and Salamanca have made an overview of such cases involving
the powerset monad [13].

The literature has tended to focus on positive results, either demonstrating
specific distributive laws, or developing general-purpose techniques for
constructing them. By comparison, there is a relative paucity of negative
results, showing when no distributive law can exist. The most well-known
result of this type appears in the paper _Distributing probability over non-
determinism_ [14], where it is shown that there is no distributive law
combining the powerset and probability distribution monads, via a proof
credited to Plotkin. This result was strengthened by Dahlqvist and Neves to
show that the composite functor carries no monad structure at all [15].
Recently, the same proof technique was used by Klin and Salamanca to show that
composing the covariant powerset functor with itself yields an endofunctor
that does not carry any monad structure [13], correcting an earlier error in
the literature [11]. To the best our knowledge, these are currently the only
published impossibility results.

In this paper we present several theorems for proving the absence of
distributive laws for large classes of monads on the category $\mathbf{Set}$
of sets and functions. These theorems significantly extend the current
understanding of distributive laws. Our results can roughly be divided into
three classes:

  * •

Firstly, we generalize Plotkin’s method to general-purpose theorems covering
all the previously published no-go results about distributive laws, and
yielding new results as well.

  * •

Secondly, we develop a completely new family of no-go theorems, emphasising
unitality axioms rather than the idempotence central to Plotkin’s argument.

  * •

Finally, we prove two further no-go theorems, motivated by a question in
Beck’s original paper [6]. Here we introduce further novel techniques, based
on the ability to judiciously “make variables disappear” in terms.

As one application of our new methods, we show that the list monad cannot
distribute over itself, resolving an open question [11, 12] and previous error
[16] in the literature. Another open question we resolve is a conjecture made
by Beck in 1969 [6], stating that the Abelian group monad does not distribute
over the list monad. In addition to answering open questions, the no-go
theorems produced by these methods reveal yet another faulty distributive law
in the literature, involving the list and exception monads.

Apart from our negative results, we also prove a uniqueness result. Under
certain conditions, we prove that there is only one possible distributive law
facilitating monad compositions, namely the distributive law resembling the
times over plus distributivity. This proves that several known distributive
laws, such as the distributive law for the multiset monad over itself, are
unique.

Monads have deep connections with universal algebra. We fully embrace this
algebraic viewpoint on monads, basing our proofs on an explicit algebraic
equivalent of distributive laws formulated by Piróg and Staton [17], which was
inspired by the work of Cheng [18]. Formulating our results in algebraic form
is a key contribution of our work, simplifying and clarifying the essentials
of our proofs, which can be obscured by more direct calculations.

In physics, theorems proving the impossibility of certain things are called
_no-go theorems_ , because they clearly identify theoretical directions that
cannot succeed. We follow this example, and hope that by sharing our results,
we prevent others from wasting time on forlorn searches for distributive laws
that do not exist.

###  1.1. Contributions

We briefly outline our contribution. By taking an algebraic perspective, we
demonstrate the non-existence of distributive laws for large classes of
monads:

  * •

In Section 3 we widely generalize the essentials of a counterexample due to
Plotkin [14]:

    * –

We establish in Theorem 14 purely algebraic conditions under which a no-go
result holds. This theorem recovers all the known negative results we are
aware of, and many useful new results. The key ingredients for this theorem
are binary terms that are idempotent and commutative.

    * –

In Theorem 19 we generalize Theorem 14 further, showing there is nothing
essential about binary terms.

    * –

Theorem 21 eliminates commutativity assumptions, yielding more useful
insights.

    * –

Finally, in Section 3.2 we replace one of the idempotent terms from Theorem 14
with a unital one, still following the same general proof technique, yielding
Theorem 26.

  * •

In Section 4 we present three entirely new no-go theorems:

    * –

Theorem 30 states conditions under which algebraic theories with more than one
constant do not combine well with other theories. The usefulness of this
theorem is demonstrated by Example 1, which identifies a previously unnoticed
error in a theorem in the literature.

    * –

Theorem 37 is a general no-go theorem for monads that do not satisfy the so-
called _abides_ equation [19]. One of its applications is that it negatively
answers the open question of whether the list monad distributes over itself.

    * –

Theorem 41 is a general no-go theorem focussing on the combination of
idempotence and units. From this theorem it follows that there is no
distributive law for the powerset monad over the multiset monad: $P\circ
M\Rightarrow M\circ P$.

    * –

Section 4 also contains two characterization results, giving insights into how
a distributive law has to behave, if it exists at all. Proposition 28
identifies when the unit of one algebraic theory, presenting a monad, acts as
an annihilator when another monad is distributed over it. For example, this
characterizes the behaviour of empty lists and sets in certain composite
monads. Theorem 32 gives conditions under which at most one distributive law
can exist, and what form it must take. For example, the well-known
distributive law for the multiset monad over itself is unique.

  * •

In Section 5 a second new family of no-go theorems is presented, based on
another new approach to yielding no-go results within our algebraic framework:

    * –

Theorem 46 confirms a negative conjecture of Beck from the original paper on
distributive laws [6].

    * –

Theorem 48 provides further new results, showing there is no distributive law
$bL\circ P\Rightarrow P\circ bL$ between the powerset and bounded distributive
lattice monads.

  * •

In Section 6 we provide a detailed analysis of the availability of
distributive laws for some natural families of monads. This includes many
examples of applications of our theorems, as well as results from elsewhere in
the literature to provide a detailed picture.

    * –

We examine distributive laws between monads in the so-called Boom hierarchy, a
small family of monads representing data structures, which are studied in the
functional programming community.

    * –

To gain more examples of existing/non-existing distributive laws, we consider
an extension of the Boom hierarchy previously studied by Uustalu [20].

    * –

Finally, we consider possible iterations of compositions in the Boom
hierarchy.

  * •

In Section 7, we provide a summary of all axioms used for the various theorems
in this paper, together with an overview of which theorem uses which axioms.

Throughout this paper we restrict our attention to monads on the category
$\mathbf{Set}$ of sets and functions, as this is already an incredibly rich
setting. Our results are general-purpose in the sense that they are phrased in
terms of abstract properties of the algebraic theories corresponding to both
monads.

######  Remark 1.

To compose monads $\langle S,\eta,\mu\rangle$ and $\langle T,\eta,\mu\rangle$
one may ask if all we really want is some arbitrary monad structure on the
functor $TS$, rather than the specific structure given by a distributive law?
Generally, a monad structure arising from a distributive law is vastly
preferable to an arbitrary one, as it has many desirable properties. For
example, there are canonical monad morphisms $S\Rightarrow T\circ S$ and
$T\Rightarrow T\circ S$ inducing functors between both the Eilenberg-Moore and
Kleisli categories of the corresponding monads. Furthermore, $T$ lifts to a
monad on the Eilenberg-Moore category of $S$, and $S$ lifts to a monad on the
Kleisli category of $T$. More succinctly, a distributive law ensures that
there is a strong relationship between the parts and the whole.

###  1.2. Additional Material

This paper is an extended version of our LiCS2019 conference paper [1].
Besides providing detailed proofs and more discussion of the original results,
the following additions have been made:

  * •

Section 3.2 extends our Plotkin style counterexamples with a new theorem,
bringing more monads within the scope of our techniques.

  * •

Section 5 introduces a third family of theorems, not present in the original
conference paper. These theorems preclude the possibility of distributive laws
between additional naturally occurring monads.

  * •

Section 6 provides detailed analysis of when distributive laws are available
for many common monads. These concrete applications further illustrate the use
of our main theorems, and situate our results in the broader understanding of
distributive laws in the community.

  * •

Section 7 includes an overview of the axioms used in this paper, and which
theorem uses which axioms.

##  2\. Preliminaries

###  2.1. Monads and Distributive Laws

We introduce monads, distributive laws, and various examples that will recur
in later sections, primarily to fix notation. The material is standard, and
may be skipped by the expert reader. [Monad] For any category $\mathcal{C}$, a
monad $\langle T,\eta,\mu\rangle$ on $\mathcal{C}$ consists of an endofunctor
$T:\mathcal{C}\rightarrow\mathcal{C}$, and natural transformations
$\eta:1\Rightarrow T$ and $\mu:T\circ T\Rightarrow T$ referred to as the unit
and multiplication, satisfying the following axioms:

$\displaystyle\mu\cdot T\eta$ $\displaystyle=id$ (unit 1)
$\displaystyle\mu\cdot\eta T$ $\displaystyle=id$ (unit 2)
$\displaystyle\mu\cdot T\mu$ $\displaystyle=\mu\cdot\mu T$ (associativity)

Or, as commuting diagrams:

${T}$${TTT}$${TT}$${TT}$${T}$${TT}$${TT}$${T}$$\scriptstyle{\eta
T}$$\scriptstyle{T\eta}$$\scriptstyle{\mu
T}$$\scriptstyle{T\mu}$$\scriptstyle{\mu}$$\scriptstyle{\mu}$$\scriptstyle{\mu}$$\scriptstyle{\mu}$

We will restrict ourselves to monads on the category $\mathbf{Set}$ of sets
and functions. In addition, if there is a finitary version and a full version
of a monad, we mean the finitary one unless otherwise specified. We list a few
examples of monads on $\mathbf{Set}$, which we will use throughout this paper.
For any set $E$, the exception monad $(-+E)$ is given by:

  * •

$(-+E)$ maps a set $X$ to the disjoint union $X+E$.

  * •

$\eta^{E}_{X}$ is the left inclusion morphism.

  * •

$\mu^{E}_{X}$ is the identity on $X$, and collapses the two copies of $E$ down
to a single copy. That is, $\mu:(X+E)+E\Rightarrow X+E$.

When $E$ is a singleton set, this monad is also known as the maybe monad,
written as $(-)_{\bot}$. The list monad $L$ is given by:

  * •

$L(X)$ is the set of all finite lists of elements of $X$.

  * •

$\eta^{L}_{X}(x)$ is the singleton list $[x]$.

  * •

$\mu^{L}_{X}$ concatenates a list of lists.

This monad is also known as the free monoid monad, in acknowledgement of its
connection to the algebraic theory of monoids, see Example 4 below. The
multiset monad $M$ is given by:

  * •

$M(X)$ is the set of all finite multisets111by which we mean: multisets in
which only finitely many elements have a non-zero multiplicity. In other
words: multisets with finite support. We assume the multiplicities are in the
natural numbers. Multisets are also known as ‘bags’. of elements of $X$.

  * •

$\eta^{M}_{X}(x)$ is the singleton multiset $\Lbag x\Rbag$.

  * •

$\mu^{M}_{X}$ takes a union of multisets, adding multiplicities.

We can generalise the notion of multiset to take multiplicities in the
integers rather than the natural numbers. This results in the Abelian group
monad. This monad is again named after its algebraic presentation, see
Proposition 4. The finite powerset monad $P$ is given by:

  * •

$P(X)$ is the set of all finite subsets of $X$.

  * •

$\eta^{P}_{X}(x)$ is the singleton set $\\{x\\}$.

  * •

$\mu^{P}_{X}$ takes a union of sets.

[Binary Tree Monad] The binary tree monad $B$ is given by:

  * •

$B(X)$ is the set of all binary trees with leaves labelled by elements from
$X$.

  * •

$\eta^{B}_{X}(x)$ is the tree consisting of a single leaf labelled with $x$.

  * •

$\mu^{B}_{X}$ flattens a tree of trees.

The probability distribution monad $D$ is given by:

  * •

$D(X)$ is the set of all finitely supported probability distributions over
$X$.

  * •

$\eta^{D}_{X}(x)$ is the point distribution at $x$.

  * •

$\mu^{D}(e)(x)$ is the weighted average
$\sum_{d\in\operatorname{supp}(e)}e(d)d(x)$.

For any set of states $R$, the reader monad $(-)^{R}$ is given by:

  * •

$X^{R}$ is the set of functions from $R$ to $X$.

  * •

$\eta^{R}_{X}(x)$ is constantly $x$.

  * •

$\mu^{R}_{X}(f)(r)=f(r)(r)$.

Given a pair of monads, sufficient conditions for the composite functor to
form a monad are given by Beck’s distributive laws [6]: [Distributive Law]
Given monads $S$ and $T$, a distributive law for monad composition $T\circ S$
is a natural transformation $\lambda:S\circ T\Rightarrow T\circ S$ satisfying
the following axioms:

$\displaystyle\lambda\cdot\eta^{S}T$ $\displaystyle=T\eta^{S}$ (unit1)
$\displaystyle\lambda\cdot S\eta^{T}$ $\displaystyle=\eta^{T}S$ (unit2)
$\displaystyle\lambda\cdot\mu^{S}T$ $\displaystyle=T\mu^{S}\cdot\lambda S\cdot
S\lambda$ (multiplication1) $\displaystyle\lambda\cdot S\mu^{T}$
$\displaystyle=\mu^{T}S\cdot T\lambda\cdot\lambda T$ (multiplication2)

Or, as commuting diagrams:

${T}$${SST}$${STS}$${TSS}$${ST}$${TS}$${ST}$${TS}$${S}$${STT}$${TST}$${TTS}$${ST}$${TS}$${ST}$${TS}$$\scriptstyle{\eta^{S}T}$$\scriptstyle{T\eta^{S}}$$\scriptstyle{\mu^{S}T}$$\scriptstyle{S\lambda}$$\scriptstyle{\lambda
S}$$\scriptstyle{T\mu^{S}}$$\scriptstyle{\lambda}$$\scriptstyle{\lambda}$$\scriptstyle{S\eta^{T}}$$\scriptstyle{\eta^{T}S}$$\scriptstyle{S\mu^{T}}$$\scriptstyle{\lambda
T}$$\scriptstyle{T\lambda}$$\scriptstyle{\mu^{T}S}$$\scriptstyle{\lambda}$$\scriptstyle{\lambda}$

######  Remark 2.

For a pair of monads $S,T$ the expression “$S$ distributes over $T$” is often
used. This phrasing is somewhat ambiguous and prone to errors. We will
therefore explicitly state the type of the natural transformation, for example
“there is a distributive law of type $S\circ T\Rightarrow T\circ S$”.

######  Theorem 3 (Beck [6]).

Let $\mathcal{C}$ be a category, and $\langle S,\eta^{S},\mu^{S}\rangle$ and
$\langle T,\eta^{T},\mu^{T}\rangle$ two monads on $\mathcal{C}$. If
$\lambda:S\circ T\Rightarrow T\circ S$ is a distributive law, then $T\circ S$
carries a monad structure with unit $\eta^{T}\eta^{S}$ and multiplication
$\mu^{T}\mu^{S}\cdot T\lambda S$.

[Ring Monad [6]] The motivating example of a distributive law involves the
list monad and the Abelian group monad, and has type $\lambda:L\circ
A\Rightarrow A\circ L$. It captures exactly the distributivity of
multiplication over addition:

$\lambda\left(a\cdot(b+c)\right)=(a\cdot b)+(a\cdot c)$ (1)

The term ‘distributive law’ is derived from this example, and many other
distributive laws exploit similar algebraic properties. However, as we will
see in Section 4, caution is needed: the validity of an equation such as (1)
does not automatically imply the existence of a distributive law. [Multiset
Monad] The multiset monad distributes over itself in a manner analogous to
distributing multiplication over addition.

###  2.2. Algebraic Theories and Composite Theories

We now outline the connections between algebras, monads, and distributive laws
that we require in later sections. [Algebraic Theory] An algebraic signature
is a set of operation symbols $\Sigma$, each with an associated natural number
referred to as its arity. The set of $\Sigma$-terms over a set $X$ contains
$X$ as variables and is inductively closed under forming terms
$\sigma(t_{1},...,t_{n})$ for an $n$-ary operation symbol $\sigma$ and terms
$t_{1},...,t_{n}$.

An algebraic theory $\mathbb{T}$ consists of a signature
$\Sigma^{\mathbb{T}}$, and a set $E^{\mathbb{T}}$ of pairs of $\Sigma$-terms
referred to as equations or axioms. We will often write a pair $(s,t)\in
E^{\mathbb{T}}$ as $s=_{\mathbb{T}}t$ or simply $s=t$ when convenient. For a
subset $Y\subseteq X$ and a term $t$ we write $Y\vdash_{\mathbb{T}}t$ or
$Y\vdash t$ to indicate that the variables appearing in $t$ are contained in
the variable context $Y$. The precise set of variables appearing in $t$ will
be denoted $\operatorname{var}(t)$, and $\\#\operatorname{var}(t)$ denotes the
cardinality of this set. The following is well-known [21, 22, 23]:

######  Proposition 4.

Given a theory $(\Sigma^{\mathbb{T}},E^{\mathbb{T}})$, the free model monad
over that signature maps $X$ to the set of $\Sigma^{\mathbb{T}}$-terms over
$X$, quotiented by provable equality in equational logic from the axioms
$E^{\mathbb{T}}$. The unit maps a variable to its corresponding equivalence
class, and the multiplication flattens a term-of-terms to a term in the
obvious way. If a monad is isomorphic to a free model monad, it is said to be
presented by the corresponding theory.

[Monoids] The algebraic theory of monoids has a signature containing a
constant and a binary operation, satisfying left and right unitality and
associativity. The theory of commutative monoids extends this theory with the
commutativity equation. The theory of join semilattices further extends the
theory of commutative monoids with an additional idempotence axiom.

The corresponding free model monads are the list, multiset and finite powerset
monads respectively. In the paper _Notions of computation determine monads_ ,
Plotkin and Power show that many monads describing computational effects have
natural algebraic presentations [24]. An algebraic presentation of the reader
monad of Example 2.1, with state space $\\{0,1\\}$, has a signature containing
a single binary operation. Intuitively, $x*y$ is a process that proceeds as
$x$ if the state is $0$, and $y$ otherwise. This operation should satisfy:

$\displaystyle x*x=x\quad\text{and}\quad(w*x)*(y*z)=w*z$

These axioms generalize naturally to larger state spaces. The distribution
monad Example 2.1 can be presented by a family of binary operations $+^{p}$,
for $p\in(0,1)$, satisfying the following axioms [25, 26]:

$\displaystyle x+^{p}x$ $\displaystyle=x$ $\displaystyle x+^{p}y$
$\displaystyle=y+^{1-p}x$ $\displaystyle x+^{p}(y+^{r}z)$
$\displaystyle=(x+^{\frac{p}{p+(1-p)r}}y)+^{p+(1-p)r}z$

In addition to an algebraic equivalent of monads, we require an algebraic
version of distributive laws. This key notion is provided in the form of
_composite theories_ , which were introduced by Piróg and Staton [17].
[Composite Theory] Let $\mathbb{U}$ be an algebraic theory that contains two
theories $\mathbb{S}$ and $\mathbb{T}$.

  1. (1)

A term in $\mathbb{U}$ is separated if it is of the form $t[s_{x}/x]$, where
$X\vdash_{\mathbb{T}}t$ and $s_{x}$ is a family of $\mathbb{S}$-terms indexed
by $x\in X$.

  2. (2)

Two separated terms $t[s_{x}/x]$ and
$t^{\prime}[s^{\prime}_{x^{\prime}}/x^{\prime}]$ in $\mathbb{U}$ are equal
modulo $(\mathbb{T},\mathbb{S})$ if there are functions $h:X\rightarrow
Y,h^{\prime}:X^{\prime}\rightarrow Y$ and terms $\bar{s}_{y}$, such that:

    1. (a)

$t[h(x)/x]=_{\mathbb{T}}t^{\prime}[h^{\prime}(x^{\prime})/x^{\prime}]$

    2. (b)

$\forall x\in X:s_{x}=_{\mathbb{S}}\bar{s}_{h(x)}$

    3. (c)

$\forall x^{\prime}\in
X^{\prime}:s^{\prime}_{x^{\prime}}=_{\mathbb{S}}\bar{s}_{h^{\prime}(x^{\prime})}$

The theory $\mathbb{U}$ is said to be a composite of $\mathbb{T}$ after
$\mathbb{S}$, if every term $u$ in $\mathbb{U}$ is equal to a separated term,
and moreover this term is essentially unique in the sense that if
$v,v^{\prime}$ are separated and $v=_{\mathbb{U}}u=_{\mathbb{U}}v^{\prime}$
then $v$ and $v^{\prime}$ are equal modulo $(\mathbb{T},\mathbb{S})$. Note
that this is an oriented notion, a composite of $\mathbb{T}$ after
$\mathbb{S}$ is not equivalent to a composite of $\mathbb{S}$ after
$\mathbb{T}$. In this paper, we shall use an equivalent definition of equality
modulo $(\mathbb{T},\mathbb{S})$.

######  Theorem 5.

Let $\mathbb{S}$ and $\mathbb{T}$ be two algebraic theories, and let
$\mathbb{U}$ be an algebraic theory that contains both $\mathbb{S}$ and
$\mathbb{T}$. For terms $X\vdash_{\mathbb{T}}t$,
$X^{\prime}\vdash_{\mathbb{T}}t^{\prime}$ and families of $\mathbb{S}$-terms
$\\{s_{x}\;|\;x\in X\\}$ and $\\{s^{\prime}_{x^{\prime}}\;|\;x^{\prime}\in
X^{\prime}\\}$, the following are equivalent:

  1. (1)

The terms $t[s_{x}/x]$ and $t^{\prime}[s^{\prime}_{x^{\prime}}/x^{\prime}]$
are equal modulo $(\mathbb{T},\mathbb{S})$.

  2. (2)

There are functions $f:X\rightarrow Z$, $f^{\prime}:X^{\prime}\rightarrow Z$
satisfying:

    1. (a)

$t[f(x)/x]=_{\mathbb{T}}t^{\prime}[f^{\prime}(x^{\prime})/x^{\prime}]$.

    2. (b)

$f(x_{1})\;=f(x_{2})\;\,\Leftrightarrow\;s_{x_{1}}=_{\mathbb{S}}s_{x_{2}}$.

    3. (c)

$f^{\prime}(x^{\prime}_{1})=f^{\prime}(x^{\prime}_{2})\;\Leftrightarrow\;s^{\prime}_{x^{\prime}_{1}}=_{\mathbb{S}}s^{\prime}_{x^{\prime}_{2}}$.

    4. (d)

$\;\,f(x)\;=f^{\prime}(x^{\prime})\;\,\Leftrightarrow\;\;s_{x}\,=_{\mathbb{S}}s^{\prime}_{x^{\prime}}$.

######  Proof 2.1.

Showing that condition 2 implies condition 1 is straightforward. Taking $Y$ to
be the union of the ranges of $f$ and $f^{\prime}$, requirements 2b-2d ensure
that we can choose $\bar{s}_{y}$ such that:

$\bar{s}_{y}=\begin{cases}s_{x},&\mbox{if }f(x)=y\\\ s_{x^{\prime}},&\mbox{if
}f^{\prime}(x^{\prime})=y.\end{cases}$

To show that condition 1 implies condition 2, notice that by transitivity of
equality, $h$ and $h^{\prime}$ from Definition 4 already have the properties:

  1. (1)

$t[h(x)/x]=_{\mathbb{T}}t^{\prime}[h^{\prime}(x^{\prime})/x^{\prime}]$.

  2. (2)

$h(x_{1})\;=h(x_{2})\;\Rightarrow\;s_{x_{1}}=_{\mathbb{S}}s_{x_{2}}$.

  3. (3)

$h^{\prime}(x^{\prime}_{1})=h^{\prime}(x^{\prime}_{2})\Rightarrow\;s^{\prime}_{x^{\prime}_{1}}=_{\mathbb{S}}s^{\prime}_{x^{\prime}_{2}}$.

  4. (4)

$\;h(x)\;\,=h^{\prime}(x^{\prime})\,\Rightarrow\;\,s_{x}\,=_{\mathbb{S}}s^{\prime}_{x^{\prime}}$.

So all we need to show are the reverse implications of the latter three
points. To this end, pick a function $g:Y\rightarrow Z$ such that:

  * •

If $s_{x_{1}}=_{\mathbb{S}}s_{x_{2}}$, then $g(h(x_{1}))\;=g(h(x_{2}))$

  * •

If $s^{\prime}_{x^{\prime}_{1}}=_{\mathbb{S}}s^{\prime}_{x^{\prime}_{2}}$,
then $g(h^{\prime}(x^{\prime}_{1}))=g(h^{\prime}(x^{\prime}_{2}))$

  * •

If $\;s_{x}\,=_{\mathbb{S}}s^{\prime}_{x^{\prime}}$, then
$\;\,g(h(x))\,\,=g(h^{\prime}(x^{\prime}))$

The function $g$ effectively takes a quotient of $Y$, defined by the three
conditions above. Transitivity of equality ensures that the compositions
$f=g\circ h$ and $f^{\prime}=g\circ h^{\prime}$ preserve properties 1-4. By
definition, they also satisfy the reverse implications, and so they satisfy
condition 2.

We may assume that a composite theory is never inconsistent:

######  Proposition 6.

If $\mathbb{U}$ is a composite theory of theories $\mathbb{T}$ after
$\mathbb{S}$, and both $\mathbb{S}$ and $\mathbb{T}$ are consistent, then
$\mathbb{U}$ is consistent.

######  Proof 2.2.

Suppose for contradiction that $\mathbb{U}$ is an inconsistent theory. Then
for each pair of variables $x,y$ we have $x=_{\mathbb{U}}y$. Since both $x$
and $y$ are separated terms, essential uniqueness gives us two substitutions
$f:\\{x\\}\rightarrow Z$ and $g:\\{y\\}\rightarrow Z$ such that:

$\displaystyle x[f]=_{\mathbb{T}}y[g]$ $\displaystyle f(x)=g(y)$
$\displaystyle\;\;\Leftrightarrow\;\;x=_{\mathbb{S}}y$

For the first equation to be satisfied without violating the consistency of
$\mathbb{T}$, we must have that $f(x)=g(y)$. This implies, however, that
$x=_{\mathbb{S}}y$, which contradicts the consistency of $\mathbb{S}$. We
hence conclude that if $\mathbb{U}$ is a composite theory of $\mathbb{T}$
after $\mathbb{S}$, $\mathbb{U}$ must be consistent.

The following theorem shows that composite theories are indeed the algebraic
equivalent of distributive laws.

######  Theorem 7 (Piróg & Staton [17]).

Let $S$ and $T$ be $\mathbf{Set}$-monads presented by theories $\mathbb{S}$
and $\mathbb{T}$. There is a distributive law of type $S\circ T\Rightarrow
T\circ S$ if and only if there is a composite theory of $\mathbb{T}$ after
$\mathbb{S}$.

We will frequently exploit Theorem 7 by showing that no composite theory
exists, and therefore no distributive law.

For positive results it will be useful to know the actual action of the
distributive law promised by Theorem 7, if we know the composite theory.
Conversely, when a distributive law is known to exist, it is useful to have an
algebraic presentation for the resulting composite monad. The following
theorems provide us with just that. Similar observations have been made by
Lack [27, Proposition 4.7], written up more explicitly by Zanasi in his thesis
[28, Proposition 2.27]. Their results hold for symmetric monoidal theories.

######  Proposition 8.

Let $\mathbb{S}$ and $\mathbb{T}$ be algebraic theories presenting monads $S$
and $T$, and let $\mathbb{U}$ be a composite theory of $\mathbb{T}$ after
$\mathbb{S}$. Then the free model monad $U$ is isomorphic to the composition
of $T\circ S$ via the distributive law mapping the equivalence class of
representative $s[t_{x}/x]$ to the suitable equivalence class of a separated
term in $\mathbb{U}$ equal to $s[t_{x}/x]$.

The proof of this proposition is straightforward but tedious. We give a sketch
of the main ideas below, but for full details we refer to [29].

######  Proof 2.3 (Proof sketch).

We first establish that the functor $U$ is isomorphic to the functor $T\circ
S$ by finding an explicit natural isomorphism $\phi:U\Rightarrow T\circ S$. We
conclude that the functor $T\circ S$ has a monad structure, which is given by
the monad structure of the free model monad $U$ of theory $\mathbb{U}$. To
prove that this structure comes from a distributive law, we prove the
following three statements. Together, these statements are equivalent to
having a distributive law [6]:

  * •

$\langle TS,\eta^{T}\eta^{S},\mu^{TS}\rangle$ is a monad, with multiplication
$\mu^{TS}=\phi\cdot\mu^{U}\cdot(\phi^{-1})TS(\phi^{-1})$.

  * •

The natural transformations $\eta^{T}S$ and $T\eta^{S}$ are monad maps.

  * •

The middle unitary law holds: $\mu^{TS}\cdot T\eta^{S}\eta^{T}S=id_{TS}$.

The distributive law is then given by:
$\lambda=\mu^{TS}\cdot\eta^{T}ST\eta^{S}$

Knowing how to construct a distributive law from a composite theory, we will
now do the reverse: constructing a composite theory from a known distributive
law. To do this, we first define a set of equations derived from the
distributive law.

Let $S$ and $T$ be the free model monads of algebraic theories $\mathbb{S}$
and $\mathbb{T}$. If there is a distributive law $\lambda:S\circ T\Rightarrow
T\circ S$, then we define the set of $\lambda$-equations $E^{\lambda}$ as
follows: Let $s[t_{x}/x]$ be a representative of an element in $STX$, and
$t[s_{y}/y]$ a representative of an element in $TSX$. Then
$s[t_{x}/x]=t[s_{y}/y]\in E^{\lambda}$ iff $\lambda$ maps the equivalence
class of $s[t_{x}/x]$ to the equivalence class of $t[s_{y}/y]$.

######  Proposition 9.

Let $S$ and $T$ be the free model monads of algebraic theories $\mathbb{S}$
and $\mathbb{T}$. If there is a distributive law $\lambda:S\circ T\Rightarrow
T\circ S$, then the following theory is a composite of $\mathbb{T}$ after
$\mathbb{S}$, and the monad $\langle TS,\eta^{T}\eta^{S},\mu^{T}\mu^{S}\cdot
T\lambda S\rangle$ is the free model monad of this theory:

$\displaystyle\Sigma^{\mathbb{TS}^{\lambda}}$
$\displaystyle=\Sigma^{\mathbb{S}}\uplus\Sigma^{\mathbb{T}}$ $\displaystyle
E^{\mathbb{TS}^{\lambda}}$ $\displaystyle=E^{S}\cup E^{T}\cup E^{\lambda}$

We call the composite theory hence constructed $\mathbb{TS}^{\lambda}$.

Again the proof is straightforward but tedious. We give a proof sketch below,
but for full details we refer to [29].

######  Proof 2.4 (Proof sketch).

From Piróg and Staton’s theorem [17, Theorem 5], we already know that
$\lambda$ induces a monad that is the free model monad of a composite of
$\mathbb{T}$ after $\mathbb{S}$. What is left to show is that
$\mathbb{TS}^{\lambda}$ is indeed this composite theory. We prove this by
establishing an isomorphism between the Eilenberg-Moore category of the monad
TS and the category of algebras for $\mathbb{TS}^{\lambda}$.

Propositions 8 and 9 together give us a concrete presentation for composite
theories:

######  Corollary 10.

Let $\mathbb{S}$ and $\mathbb{T}$ be algebraic theories presenting monads $S$
and $T$, and let $\mathbb{TS}$ be a composite theory of $\mathbb{T}$ after
$\mathbb{S}$. Then the following gives a presentation of $\mathbb{TS}$:

$\displaystyle\Sigma^{\mathbb{TS}}$
$\displaystyle=\Sigma^{\mathbb{S}}\uplus\Sigma^{\mathbb{T}}$ $\displaystyle
E^{\mathbb{TS}^{\lambda}}$ $\displaystyle=E^{\mathbb{S}}\cup
E^{\mathbb{T}}\cup E^{\mathbb{\lambda}}$

where $E^{\mathbb{\lambda}}$ consists of all provable equations in
$\mathbb{TS}$ of form $s[t_{x}/x]=t[s_{y}/y]$.

##  3\. General Plotkin Theorems

In this section we develop algebraic generalizations of the counterexample
attributed to Gordon Plotkin [14], which showed that there is no distributive
law of type $D\circ P\Rightarrow P\circ D$, where $D$ is the distribution
monad of Example 2.1 and $P$ is the finite powerset monad of Example 2.1. We
present a slight rephrasing of this counterexample, augmented with commentary
indicating the main proof ideas that will be used in the later
generalizations. Throughout this section we adopt the notational conventions
of [14, 17] whenever possible to ease comparison with those papers.

######  Counterexample 11 (Probability does not distribute over non-
determinism).

Assume, for contradiction, that there is a distributive law of type
$\lambda:D\circ P\Rightarrow P\circ D$. Fix the set $X=\\{a,b,c,d\\}$, and
consider the element $\Xi\in DP(X)$ defined by:

$\Xi=\\{a,b\\}+^{\frac{1}{2}}\\{c,d\\}.$

We define three functions $f_{1},f_{2},f_{3}:X\rightarrow X$:

$\displaystyle f_{1}(a)=a$ $\displaystyle\quad f_{2}(a)=a$ $\displaystyle\quad
f_{3}(a)=a$ $\displaystyle f_{1}(b)=b$ $\displaystyle\quad f_{2}(b)=b$
$\displaystyle\quad f_{3}(b)=a$ $\displaystyle f_{1}(c)=a$ $\displaystyle\quad
f_{2}(c)=b$ $\displaystyle\quad f_{3}(c)=c$ $\displaystyle f_{1}(d)=b$
$\displaystyle\quad f_{2}(d)=a$ $\displaystyle\quad f_{3}(d)=c$

The plan of the proof is to analyze how $\Xi$ travels around the naturality
square for $\lambda$, for each of the three functions. The element $\Xi$ and
the three functions have been carefully chosen so that the distributive law
unit axioms can be applied during the proof.

$\begin{gathered}\leavevmode\hbox to134.73pt{\vbox
to74.13pt{\pgfpicture\makeatletter\hbox{\hskip 38.91133pt\lower-58.4029pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-16.6066pt}{-2.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$DP(X)$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{{
{}{}{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-16.6066pt}{-45.17912pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$DP(X)$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{{
{}{}{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{40.29892pt}{-2.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$PD(X)$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{{
{}{}{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{40.29892pt}{-45.17912pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$PD(X)$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{ {\pgfsys@beginscope
\pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@roundjoin{} {}{}{} {}{}{}
\pgfsys@moveto{-2.07999pt}{2.39998pt}\pgfsys@curveto{-1.69998pt}{0.95998pt}{-0.85318pt}{0.28pt}{0.0pt}{0.0pt}\pgfsys@curveto{-0.85318pt}{-0.28pt}{-1.69998pt}{-0.95998pt}{-2.07999pt}{-2.39998pt}\pgfsys@stroke\pgfsys@endscope}}
}{}{}{{}}\pgfsys@moveto{20.1396pt}{0.0pt}\pgfsys@lineto{36.36592pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{36.56592pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{22.99664pt}{5.44633pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\lambda_{X}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{20.1396pt}{-42.67912pt}\pgfsys@lineto{36.36592pt}{-42.67912pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{36.56592pt}{-42.67912pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{22.99664pt}{-53.15656pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\lambda_{X}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{-8.533pt}\pgfsys@lineto{0.0pt}{-33.74612pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{0.0pt}{-33.94612pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-35.57832pt}{-23.83955pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$DP(f_{i})$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{56.90552pt}{-8.533pt}\pgfsys@lineto{56.90552pt}{-33.74612pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{56.90552pt}{-33.94612pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{60.43852pt}{-23.83955pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$PD(f_{i})$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\end{gathered}$ (2)

We proceed as follows:

  * •

Trace $\Xi$ around the naturality square (2) for both $f_{1}$ and $f_{2}$. We
note that as $\\{-,-\\}$ is commutative, and $+^{\frac{1}{2}}$ is idempotent:

$DP(f_{1})(\Xi)=\eta^{D}_{PX}\\{a,b\\}=DP(f_{2})(\Xi).$

Commutativity, and particularly idempotence, will be important ideas for our
subsequent generalizations. For both $f_{1}$ and $f_{2}$ we can apply the
first distributive law unit axiom to conclude that:

$\lambda_{X}\circ
DP(f_{1})(\Xi)=\\{\eta^{D}_{X}(a),\eta^{D}_{X}(b)\\}=\lambda_{X}\circ
DP(f_{2})(\Xi).$

Now a careful consideration of the actions $PD(f_{1})$ and $PD(f_{2})$ allows
us to deduce that $\lambda_{X}(\Xi)$ must be a subset of:

$\\{\eta^{D}_{X}(a),\eta^{D}_{X}(b),\eta^{D}_{X}(c),\eta^{D}_{X}(d)\\}.$

This part is less straightforward to generalize. In principle it involves
inverse images of equivalence classes of terms in one algebraic theory, with
variables labelled by equivalence classes of terms in a second algebraic
theory. This motivates our move to an explicitly algebraic formulation. We can
see this whole step as establishing an upper bound on the set of variables
appearing in $\lambda_{X}(\Xi)$.

  * •

We then trace $\Xi$ around the naturality square (2) for $f_{3}$. In this
case, we exploit the idempotence of the operation $\\{-,-\\}$ to conclude:

$DP(f_{3})(\Xi)=\\{a\\}+^{\frac{1}{2}}\\{c\\}.$ (3)

This indicates idempotence is actually an important aspect of both monads for
this argument to work. Equation (3) allows us to apply the second unit axiom
for $\lambda$ to conclude:

$\lambda_{X}\circ DP(f_{3})(\Xi)=\\{a+^{\frac{1}{2}}c\\}.$

By considering the action of $PD(f_{3})$ as before, we conclude that
$\lambda_{X}(\Xi)$ must contain an element mapped onto $a+^{\frac{1}{2}}c$ by
$PD(f_{3})$, placing a lower bound on the set of variables that appear in
$\lambda_{X}(\Xi)$.

  * •

The lower and upper bounds established in the previous two steps contradict
each other, and so no distributive law of type $D\circ P\Rightarrow P\circ D$
can exist.

In summary, the argument requires two components:

  1. [1]

Some operations satisfying certain algebraic equational properties such as
idempotence and commutativity.

  2. [2]

Some slightly more mysterious properties of our monads, making the “inverse
image” parts of the argument work correctly.

######  Remark 12.

The original counterexample is actually shown for what is known as the free
real cone or finite valuation monad, as this requires slightly weaker
assumptions. We state it here for the distribution monad simply to avoid the
distraction of introducing yet another monad. This is essentially a cosmetic
decision, and our later results are equally applicable to the original
counterexample for the free real cone monad.

Our aim in this section is to extract general methods for showing no-go
results for constructing distributive laws, derived from the essential steps
in this counterexample. In order to do this, we isolate sufficient conditions
on algebraic theories inducing two monads, such that there can be no
distributive law between them. Earlier generalizations of this counterexample
have appeared in [13, 15]. All the existing approaches involve direct
calculations with the distributive law axioms, leading to somewhat opaque
conditions. They also remain limited to the case where one of the two monads
is the powerset monad, restricting their scope of application.

We introduce terminology for some special sets of terms in an algebraic
theory. The theorems are stated in terms of these special sets, which in some
cases can restrict the scope for which certain “global” conditions need to
apply, broadening the range of applicability. [Universal Terms] For an
algebraic theory, we say that a set of terms $T$ is:

  * •

Universal if every term is provably equal to a term in $T$.

  * •

Stable if $T$ is closed under substitution of variables for variables.

Some examples of universal and stable sets:

  1. [1]

For any theory, the set of all terms is a stable universal set.

  2. [2]

For the theory of real vector spaces, every term is equal to a term in which
scaling by the zero element does not appear. Terms that do not contain the
scale by zero operation are clearly also stable under variable renaming.
Therefore the terms not containing the scale by zero operation are a stable
universal set.

  3. [3]

In the theory of groups, every term is equal to a term in which no subterm and
its inverse are “adjacent”. This set is therefore universal. It is not stable,
as variable renaming may introduce a subterm adjacent to its inverse.

######  Remark 13.

On first reading, it is probably easiest to take the universal stable sets
required in subsequent theorems to be the set of all terms in a theory. This
is by far the most common case.

Throughout this section, the variable labels for any algebraic theory will
range over the natural numbers. We will also write $n$ for the set
$\\{1,...,n\\}$, so for example, $2\vdash t$ means $t$ is a term containing at
most two variables.

We proceed in four steps. Theorem 14 is an algebraic generalization of
Plotkin’s counterexample, capturing the algebraic properties required of both
theories in order for a proof of this type to work. In Theorem 19 we
generalize further, removing the restriction to binary terms that was
sufficient for the original application. This generalization complicates the
proof slightly, and so to clarify the methods involved we present two separate
theorems. Finally, Theorems 21 and 26 address the need for commutativity-like
axioms and idempotency axioms respectively, and bring further combinations of
monads into scope.

######  Theorem 14.

Let $\mathbb{P}$ and $\mathbb{V}$ be two algebraic theories, $T_{\mathbb{P}}$
a stable universal set of $\mathbb{P}$-terms, and $T_{\mathbb{V}}$ a stable
universal set of $\mathbb{V}$-terms. If there are terms:

$2\vdash_{\mathbb{P}}p\qquad\text{ and }\qquad 2\vdash_{\mathbb{V}}v$

such that:

  1. (P1)

$p$ is commutative:

$2\vdash p(1,2)=_{\mathbb{P}}p(2,1)$

  2. (P2)

$p$ is idempotent:

$1\vdash p(1,1)=_{\mathbb{P}}1$

  3. (P3)

For all $p^{\prime}\in T_{\mathbb{P}}$:

$\Gamma\vdash p(1,2)=_{\mathbb{P}}p^{\prime}\quad\Rightarrow\quad 2\vdash
p^{\prime}$

  1. (V1)

$v$ is idempotent:

$1\vdash v(1,1)=_{\mathbb{V}}1$

  2. (V2)

For all $v^{\prime}\in T_{\mathbb{V}}$, and any variable $x$:

$\Gamma\vdash x=_{\mathbb{V}}v^{\prime}\quad\Rightarrow\quad\\{x\\}\vdash
v^{\prime}$

  3. (V3)

For all $v^{\prime}\in T_{\mathbb{V}}$:

$\Gamma\vdash
v(1,2)=_{\mathbb{V}}v^{\prime}\quad\Rightarrow\quad\neg(\\{1\\}\vdash
v^{\prime}\vee\\{2\\}\vdash v^{\prime})$

Then there is no composite theory of $\mathbb{P}$ after $\mathbb{V}$.

######  Remark 15.

Properties (P3), (V2), and (V3) are constraints on the variables appearing in
certain terms, which are needed for the “inverse image” part of Counterexample
11. Property (P3) states that any term equal to the special binary term $p$
can have at most two free variables. Property (V2) states that any term equal
to a variable can only contain that variable, and property (V3) states that
any term equal to the special binary term $v$ must have at least two free
variables. Notice that the upper/lower bound principle from the original
argument is reflected in these conditions.

######  Proof 3.1.

Assume by way of a contradiction that a composite theory $\mathbb{U}$ of
$\mathbb{P}$ after $\mathbb{V}$ exists. Consider the term $v(p(1,2),p(3,4))$.
Then as $\mathbb{U}$ is composite, there exist $X\vdash p^{\prime}$ and
$\Gamma\vdash v^{\prime}_{x}$ for each $x\in X$ such that:

$\Gamma\vdash v(p(1,2),p(3,4))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}/x].$ (4)

Without loss of generality, we may assume that $p^{\prime}\in T_{\mathbb{P}}$
and $v^{\prime}_{x}\in T_{\mathbb{S}}$ by universality. Define partial
function $f_{1}$ as follows:

$\displaystyle f_{1}(1)$ $\displaystyle=f_{1}(3)=1$ $\displaystyle f_{1}(2)$
$\displaystyle=f_{1}(4)=2$

Then, using this substitution of variables and assumption (V1):

$\displaystyle\Gamma\vdash
v(p(1,2),p(3,4))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}/x]$
$\displaystyle\Rightarrow\;$
$\displaystyle\;\;\left\\{\;\text{substitution}\;\right\\}$
$\displaystyle\Gamma\vdash
v(p(1,2),p(3,4))[f_{1}]=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{1}]/x]$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{applying the
substitution on the left hand side}\;\right\\}$ $\displaystyle\Gamma\vdash
v(p(1,2),p(1,2))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{1}]/x]$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{assumption
\ref{ax:videm}: }v\text{ is idempotent}\;\right\\}$ $\displaystyle\Gamma\vdash
p(1,2)=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{1}]/x].$

We now have two separated terms that are equal to each other, so we can apply
essential uniqueness. This gives us that there are functions
$g_{1}:2\rightarrow Z$ and $g_{2}:X\rightarrow Z$ such that:

$\displaystyle p[g_{1}]=_{\mathbb{P}}p^{\prime}[g_{2}]$ (Thm 5, 2a)
$\displaystyle g_{1}(1)\neq g_{1}(2)$ (Thm 5, 2b) $\displaystyle
g_{1}(1)=g_{2}(x)$ $\displaystyle\Leftrightarrow
1=_{\mathbb{V}}v^{\prime}_{x}[f_{1}]$ (Thm 5, 2d) $\displaystyle
g_{1}(2)=g_{2}(x)$ $\displaystyle\Leftrightarrow
2=_{\mathbb{V}}v^{\prime}_{x}[f_{1}].$ (Thm 5, 2d)

As $T_{\mathbb{P}}$ is stable, any variable renaming of $p^{\prime}$ is also
in $T_{\mathbb{P}}$. And so, by assumption (P3) we must have for all
$x\in\operatorname{var}(p^{\prime})$: $g_{2}(x)=g_{1}(1)$ or
$g_{2}(x)=g_{1}(2)$, which means for each $v^{\prime}_{x}$:

$\Gamma\vdash 1=_{\mathbb{V}}v^{\prime}_{x}[f_{1}]\quad\vee\quad\Gamma\vdash
2=_{\mathbb{V}}v^{\prime}_{x}[f_{1}].$

Then, using assumption (V2) and the preimage of $f_{1}$, we conclude that for
all $v^{\prime}_{x}$:

$\\{1,3\\}\vdash v^{\prime}_{x}\quad\vee\quad\\{2,4\\}\vdash v^{\prime}_{x}.$
(5)

We use the same strategy again, but with a different substitution. Define a
second partial function $f_{2}$ as follows:

$\displaystyle f_{2}(1)$ $\displaystyle=f_{2}(4)=1$ $\displaystyle f_{2}(2)$
$\displaystyle=f_{2}(3)=2$

Using this substitution and assumptions (P1) and (V1):

$\displaystyle\Gamma\vdash
v(p(1,2),p(3,4))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}/x]$
$\displaystyle\Rightarrow\;$
$\displaystyle\;\;\left\\{\;\text{substitution}\;\right\\}$
$\displaystyle\Gamma\vdash
v(p(1,2),p(3,4))[f_{2}]=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{2}]/x]$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{applying the
substitution on the left hand side}\;\right\\}$ $\displaystyle\Gamma\vdash
v(p(1,2),p(2,1))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{2}]/x]$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{assumption
\ref{ax:pcomm}: }p\text{ is commutative}\;\right\\}$
$\displaystyle\Gamma\vdash
v(p(1,2),p(1,2))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{2}]/x]$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{assumption
\ref{ax:videm}: }v\text{ is idempotent}\;\right\\}$ $\displaystyle\Gamma\vdash
p(1,2)=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{2}]/x].$

Again we have two separated terms that are equal, so we apply essential
uniqueness. This gives us that there are functions $g_{3}:2\rightarrow Z$ and
$g_{4}:X\rightarrow Z$ such that:

$\displaystyle p[g_{3}]=_{\mathbb{P}}p^{\prime}[g_{4}]$ (Thm 5, 2a)
$\displaystyle g_{3}(1)\neq g_{3}(2)$ (Thm 5, 2b) $\displaystyle
g_{3}(1)=g_{4}(x)$ $\displaystyle\Leftrightarrow
1=_{\mathbb{V}}v^{\prime}_{x}[f_{2}]$ (Thm 5, 2d) $\displaystyle
g_{3}(2)=g_{4}(x)$ $\displaystyle\Leftrightarrow
2=_{\mathbb{V}}v^{\prime}_{x}[f_{2}].$ (Thm 5, 2d)

As $T_{\mathbb{P}}$ is stable, any variable renaming of $p^{\prime}$ is also
in $T_{\mathbb{P}}$. Therefore, by assumption (P3) we must have for all
$x\in\operatorname{var}(p^{\prime})$: $g_{4}(x)=g_{3}(1)$ or
$g_{4}(x)=g_{3}(2)$, which means for each $v^{\prime}_{x}$:

$\Gamma\vdash 1=_{\mathbb{V}}v^{\prime}_{x}[f_{2}]\quad\vee\quad\Gamma\vdash
2=_{\mathbb{V}}v^{\prime}_{x}[f_{2}].$

So, using assumption (V2) and the preimage of $f_{2}$, we know that for all
$v^{\prime}_{x}$:

$\\{1,4\\}\vdash v^{\prime}_{x}\qquad\vee\qquad\\{2,3\\}\vdash
v^{\prime}_{x}.$ (6)

We combine the two conclusions (5) and (6), yielding that for all
$v^{\prime}_{x}$:

$\displaystyle(\\{1,3\\}\vdash v^{\prime}_{x}\;\vee\;\\{2,4\\}\vdash
v^{\prime}_{x})\;\wedge\;(\\{1,4\\}\vdash
v^{\prime}_{x}\;\vee\;\\{2,3\\}\vdash v^{\prime}_{x})$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{distributing
}\wedge\text{ over }\vee\;\right\\}$ $\displaystyle(\\{1,3\\}\vdash
v^{\prime}_{x}\;\wedge\;\\{1,4\\}\vdash
v^{\prime}_{x})\;\vee\;(\\{1,3\\}\vdash
v^{\prime}_{x}\;\wedge\;\\{2,3\\}\vdash v^{\prime}_{x})\;\vee$
$\displaystyle(\\{2,4\\}\vdash v^{\prime}_{x}\;\wedge\;\\{1,4\\}\vdash
v^{\prime}_{x})\;\vee\;(\\{2,4\\}\vdash
v^{\prime}_{x}\;\wedge\;\\{2,3\\}\vdash v^{\prime}_{x})$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{this is only
possible if}\;\right\\}$ $\displaystyle\\{1\\}\vdash
v^{\prime}_{x}\;\vee\;\\{3\\}\vdash v^{\prime}_{x}\;\vee\;\\{4\\}\vdash
v^{\prime}_{x}\;\vee\;\\{2\\}\vdash v^{\prime}_{x}.$

In other words:

$\bigvee_{n\in 4}\\{n\\}\vdash v^{\prime}_{x},$ (7)

that is, each $v^{\prime}_{x}$ can have at most one variable.

To get a contradiction, we will now find a $v^{\prime}_{x}$ that must have at
least two variables. This is where we need assumption (V3). We make one more
substitution. Define a third partial function $f_{3}$ as follows:

$\displaystyle f_{3}(1)$ $\displaystyle=f_{3}(2)=1$ $\displaystyle f_{3}(3)$
$\displaystyle=f_{3}(4)=2$

Using this final substitution and (P2):

$\displaystyle\Gamma\vdash
v(p(1,2),p(3,4))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}/x]$
$\displaystyle\Rightarrow\;$
$\displaystyle\;\;\left\\{\;\text{substitution}\;\right\\}$
$\displaystyle\Gamma\vdash
v(p(1,2),p(3,4))[f_{3}]=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{3}]/x]$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{applying the
substitution on the left hand side}\;\right\\}$ $\displaystyle\Gamma\vdash
v(p(1,1),p(2,2))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{3}]/x]$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{assumption
\ref{ax:pidem}: }p\text{ is idempotent}\;\right\\}$ $\displaystyle\Gamma\vdash
v(1,2)=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{3}]/x]$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{making it more
obvious that }v\text{ is a separated term}\;\right\\}$
$\displaystyle\Gamma\vdash
5[v(1,2)/5]=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{3}]/x].$

Again, we arrive at an equality between two separated terms, allowing us to
apply essential uniqueness. This gives us that there are functions
$g_{5}:\\{5\\}\rightarrow Z$ and $g_{6}:X\rightarrow Z$ such that:

$\displaystyle 5[g_{5}]=_{\mathbb{P}}p^{\prime}[g_{6}]$ (Thm 5, 2a)
$\displaystyle g_{5}(5)=g_{6}(x)$ $\displaystyle\Leftrightarrow
v(1,2)=_{\mathbb{V}}v^{\prime}_{x}[f_{3}].$ (Thm 5, 2d)

As $\mathbb{P}$ is consistent, the variable $5[g_{5}]$ must appear in
$p^{\prime}[g_{6}]$. If it did not, we could define a substitution $h$ mapping
$5[g_{5}]$ to any other variable $y$, and then conclude
$y=_{\mathbb{P}}5[g_{5}][h]=_{\mathbb{P}}p^{\prime}[g_{6}][h]=_{\mathbb{P}}p^{\prime}[g_{6}]=_{\mathbb{P}}5[g_{5}]$,
which proves all variables are equal to each other in $\mathbb{P}$, which
means $\mathbb{P}$ is inconsistent. So by consistency of $\mathbb{P}$, the
variable $5[g_{5}]$ must appear in $p^{\prime}[g_{6}]$. Hence, there is an
$x_{0}$ such that $g_{5}(5)=g_{6}(x_{0})$. And so:

$\Gamma\vdash v(1,2)=_{\mathbb{V}}v^{\prime}_{x_{0}}[f_{3}].$

As $T_{\mathbb{S}}$ is stable, this $v^{\prime}_{x_{0}}[f_{3}]$ is an element
of $T_{\mathbb{V}}$, and so by (V3), $v^{\prime}_{x_{0}}[f_{3}]$ must have at
least two variables. Which means $v^{\prime}_{x_{0}}$ must have at least two
variables. This contradicts Equation (7), which claims that each
$v^{\prime}_{x}$ can have at most one variable. Therefore the assumed
composite theory cannot exist.

The following corollary reflects our real interest in monads:

######  Corollary 16.

If monads $P$ and $V$ have presentations $\mathbb{P}$ and $\mathbb{V}$ such
that the conditions of Theorem 14 can be satisfied, then there is no
distributive law of type $V\circ P\Rightarrow P\circ V$.

The subsequent theorems have similar corollaries, which we will not state
explicitly. [Powerset and Distribution Monad] Consider the terms $1\vee 2$ and
$1+^{\frac{1}{2}}2$ in the theories representing the powerset and distribution
monads of Examples 4 and 2.2. Since both of these terms are binary,
commutative, and idempotent, and the remaining axioms are satisfied, Theorem
14 captures the known results that there are no distributive laws of type
$D\circ P\Rightarrow P\circ D$ [14], $P\circ P\Rightarrow P\circ P$ [13], or
$P\circ D\Rightarrow D\circ P$ [30, stated without proof]. In addition,
Theorem 14 yields the new result that there is no distributive law of type
$D\circ D\Rightarrow D\circ D$, completing the picture for these monads.
[Powerset and Distribution Monad Again] We can also consider the distribution
monad to be presented by binary operations $+^{p}$ with $p$ in the  _closed_
interval $[0,1]$, and in fact this is the more common formulation. In this
case, Theorem 14 can still be directly applied, without having to move to the
more parsimonious presentation. We simply note that the terms not involving
the operations $+^{1}$ and $+^{0}$ form a stable universal set satisfying the
required axioms. The results discussed in the previous example can then be
recovered using the conventional presentation of the distribution monad.

######  Non-Example 17 (Reader Monad).

It is well known that the reader monad distributes over itself. Looking at the
presentation of the reader monad given in Example 4, we see that although it
has idempotent terms, there is no commutative term and hence Theorem 14 does
not apply.

A natural question to ask with regard to Theorem 14 is whether the choice of
_binary_ terms for both $p$ and $v$ is necessary. We thank Prakash Panangaden
for posing this question during an informal presentation of an earlier version
of this work [31]. The answer is that we can generalize to terms with any
arities strictly greater than one. Before we prove this more general
statement, we introduce a lemma that is central to establishing the upper
bound part of the argument.

######  Lemma 18.

Let $n,m$ be strictly positive natural numbers, and $\sigma$ a fixed-point
free permutation of $\\{1,...,m\\}$. For distinct variables $a^{j}_{i}$,
$1\leq i\leq m$, $1\leq j\leq n$, the sets:

$\displaystyle\\{a_{i_{1}}^{1},a_{i_{1}}^{2},a_{i_{1}}^{3},\ldots,a_{i_{1}}^{n}\\}$
$\displaystyle\\{a_{i_{2}}^{1},a_{\sigma(i_{2})}^{2},a_{i_{2}}^{3},\ldots,a_{i_{2}}^{n}\\}$
$\displaystyle\qquad\quad\;\;\vdots$
$\displaystyle\\{a_{i_{n}}^{1},a_{i_{n}}^{2},a_{i_{n}}^{3},\ldots,a_{\sigma(i_{n})}^{n}\\}$

have at most one common element. Here, each $i_{k}$ is an element of $\\{i\mid
1\leq i\leq m\\}$, not necessarily unique.

######  Proof 3.2.

We proceed by induction on $n$. The base case $n=1$ is trivially true. For
$n=n^{\prime}+1$, we consider the first two rows of our table of sets. There
are two cases.

  1. (1)

If $i_{1}=\sigma(i_{2})$, then the first two rows can only agree at their
second element, because each $a_{i}^{j}$ is distinct, and from the assumption
that $\sigma$ is fixed-point free we know that $i_{1}$ is different from
$i_{2}$ if $\sigma(i_{2})=i_{1}$. The claim follows directly from this
observation.

  2. (2)

If $i_{1}\neq\sigma(i_{2})$ then the first two rows disagree in the second
column. Therefore the elements common to all the sets cannot appear in the
second column. We then remove both row and column 2, and invoke the induction
hypothesis for $n=n^{\prime}$.

We then get a more general variant of Theorem 14.

######  Theorem 19.

Let $\mathbb{P}$ and $\mathbb{V}$ be two algebraic theories, $T_{\mathbb{P}}$
a stable universal set of $\mathbb{P}$-terms, and $T_{\mathbb{V}}$ a stable
universal set of $\mathbb{V}$-terms. If there are terms:

$m\vdash_{\mathbb{P}}p\qquad\text{ and }\qquad n\vdash_{\mathbb{V}}v$

such that:

  1. (P4)

$p$ is stable under a fixed-point free permutation $\sigma$:

$m\vdash p=_{\mathbb{P}}p[\sigma]$

  2. (P5)

$p$ is idempotent:

$1\vdash p[1/i]=_{\mathbb{P}}1$

  3. (P6)

For all $p^{\prime}\in T_{\mathbb{P}}$:

$\Gamma\vdash p=_{\mathbb{P}}p^{\prime}\quad\Rightarrow\quad m\vdash
p^{\prime}$

  1. (V4)

$v$ is idempotent:

$1\vdash v[1/i]=_{\mathbb{V}}1$

  2. (V5)

For all $v^{\prime}\in T_{\mathbb{V}}$, and any variable $i$:

$\Gamma\vdash i=_{\mathbb{V}}v^{\prime}\quad\Rightarrow\quad\\{i\\}\vdash
v^{\prime}$

  3. (V6)

For all $v^{\prime}\in T_{\mathbb{V}}$:

$\Gamma\vdash
v=_{\mathbb{V}}v^{\prime}\quad\Rightarrow\quad\neg\left(\bigvee_{i\in\Gamma}\\{i\\}\vdash
v^{\prime}\right)$

Then there is no composite theory of $\mathbb{P}$ after $\mathbb{V}$.

######  Remark 20.

The required properties are generalizations of the binary conditions in
Theorem 14. Most are straightforward, but axiom (P4), the analogue of binary
commutativity, is perhaps slightly surprising. Here we only require stability
under a single fixed-point free permutation.

######  Proof 3.3.

Assume by way of a contradiction that a composite theory $\mathbb{U}$ of
$\mathbb{P}$ after $\mathbb{V}$ exists. Let

$a_{i}^{j},1\leq i\leq m,1\leq j\leq n$

denote distinct variables. We consider the term

$v(p(a_{1}^{1},\ldots,a_{m}^{1}),\ldots,p(a_{1}^{n},\ldots,a_{m}^{n})).$

Then as $\mathbb{U}$ is composite, the separation axiom of composite theories
tells us that there exist $X\vdash p^{\prime}$ and $\Gamma\vdash
v^{\prime}_{x}$ for each $x\in X$ such that:

$\Gamma\vdash
v(p(a_{1}^{1},\ldots,a_{m}^{1}),\ldots,p(a_{1}^{n},\ldots,a_{m}^{n}))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}/x].$

Without loss of generality, we may assume $p^{\prime}\in T_{\mathbb{P}}$ and
$v^{\prime}_{x}\in T_{\mathbb{V}}$ by universality.

We use the same approach as in the proof of Theorem 14, using substitutions to
bound the variables that can appear in each of the $v^{\prime}_{x}$. Define
substitution $f_{1}$ as follows:

$f_{1}(a_{i}^{j})=a_{i}^{1}.$

We then have:

$\Gamma\vdash
v(p(a_{1}^{1},\ldots,a_{m}^{1}),\ldots,p(a_{1}^{1},\ldots,a_{m}^{1}))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{1}]/x].$

By assumption (V4), idempotence of $v$:

$\Gamma\vdash
p(a_{1}^{1},\ldots,a_{m}^{1})=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{1}]/x].$

As $T_{\mathbb{P}}$ is stable, any variable renaming of $p^{\prime}$ is also
in $T_{\mathbb{P}}$. Therefore, essential uniqueness tells us that there are
substitutions $g_{1}$ and $g_{2}$ such that:

$\displaystyle p[g_{1}]$ $\displaystyle=_{\mathbb{P}}p^{\prime}[g_{2}]$ (Thm
5, 2a) $\displaystyle g_{1}(a_{i}^{1})$ $\displaystyle\neq
g_{1}(a_{j}^{1})(i\neq j)$ (Thm 5, 2b) $\displaystyle g_{1}(a_{i}^{1})$
$\displaystyle=g_{2}(x)\Leftrightarrow
a_{i}^{1}=_{\mathbb{V}}v^{\prime}_{x}[f_{1}],$ (Thm 5, 2d)

and (P6) gives us that:

$\forall x\;\exists i:\;\Gamma\vdash
a_{i}^{1}=_{\mathbb{V}}v^{\prime}_{x}[f_{1}].$

Then by assumption (V5):

$\forall x\;\exists i:\;\\{a_{i}^{1}\\}\vdash v^{\prime}_{x}[f_{1}].$

So our first approximation of the variables appearing in $v^{\prime}_{x}$ is:

$\forall x\;\exists i:\;\\{a_{i}^{1},\ldots,a_{i}^{n}\\}\vdash
v^{\prime}_{x}.$ (8)

Now we define a family of substitutions for $2\leq k\leq n$ as follows:

$f_{k}(a_{i}^{j})=\begin{cases}a_{\sigma(i)}^{k}\text{ if }j=k\\\
a_{i}^{k}\text{ otherwise }.\end{cases}$

If we follow a similar argument as before, using essential uniqueness, (P6),
(V5), and also exploiting assumption (P4), we conclude that:

$\forall x,k\;\exists i_{k}:\\{a^{k}_{i_{k}}\\}\vdash v^{\prime}_{x}[f_{k}].$

And so:

$\forall x,k\;\exists i_{k}:\;\\{a_{\sigma^{-1}(i_{k})}^{j}\mid
j=k\\}\cup\\{a_{i_{k}}^{j}\mid j\neq k\\}\vdash v^{\prime}_{x}.$ (9)

Then we note that by Lemma 18, conditions (8) and (9):

$\forall x\;\exists i,j:\;\\{a_{i}^{j}\\}\vdash v^{\prime}_{x}.$ (10)

This provides an upper bound on the number of variables appearing in the
$v^{\prime}_{x}$, just like the first two substitutions did in the proof of
Theorem 14. To finish the argument, we define another substitution:

$f_{n+1}(a_{i}^{j})=a_{1}^{j}$

Applying this substitution:

$\Gamma\vdash
v(p(a_{1}^{1},\ldots,a_{1}^{1}),\ldots,p(a_{1}^{n},\ldots,a_{1}^{n}))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{n+1}]/x].$

Using assumption (P5):

$\Gamma\vdash
v(a_{1}^{1},\ldots,a_{1}^{n})=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{n+1}]/x].$

By essential uniqueness and consistency:

$\exists x_{0}:\;\Gamma\vdash
v(a_{1}^{1},\ldots,a_{1}^{n})=_{\mathbb{V}}v^{\prime}_{x_{0}}[f_{n+1}].$

As $T_{\mathbb{V}}$ is stable, this $v^{\prime}_{x}[f_{n+1}]$ is an element of
$T_{\mathbb{V}}$. And so, by assumption (V6), $v^{\prime}_{x_{0}}$ must
contain at least two variables, but this contradicts conclusion (10), and so
the assumed composite theory cannot exist.

It is clear that the simpler Theorem 14 is a special case of Theorem 19.
Besides providing greater generality, the main point of Theorem 19 is that it
clearly demonstrates that there is nothing special about binary terms. This
further clarifies our understanding of what abstract properties make the
original counterexample of Plotkin work. By moving to such a high level of
abstraction it is also easier to see that our other methods, described in
Sections 4 and 5, are not simply a further generalization of Plotkin’s
counterexample, as they make fundamentally different assumptions of the
underlying algebraic theories.

###  3.1. Concerning Commutativity

In Theorem 14 we require the special term $p$ to be commutative in order to
establish that no composite theory exists. In Theorem 19 this commutativity
was generalized to stability under the action of a fixed-point free
permutation. This raises the question of whether commutativity-like axioms are
essential to this type of proof. In fact, this is not the case, and a similar
no-go theorem can be established under modified assumptions that make no use
of commutativity.

######  Theorem 21.

Let $\mathbb{P}$ and $\mathbb{V}$ be two algebraic theories, $T_{\mathbb{P}}$
a stable universal set of $\mathbb{P}$-terms, and $T_{\mathbb{V}}$ a stable
universal set of $\mathbb{V}$-terms. If there are terms:

$2\vdash_{\mathbb{P}}p\qquad\text{ and }\qquad 2\vdash_{\mathbb{V}}v$

such that axioms (P2), (P3), (V1), (V2) and (V3) hold, and:

  1. (P7)

For all $p^{\prime}\in T_{\mathbb{P}}$, and any variable $x$:

$\Gamma\vdash x=_{\mathbb{P}}p^{\prime}\quad\Rightarrow\quad\\{x\\}\vdash
p^{\prime}$

  2. (P8)

For all $p^{\prime}\in T_{\mathbb{P}}$:

$\Gamma\vdash
p(1,2)=_{\mathbb{P}}p^{\prime}\quad\Rightarrow\quad\neg(\emptyset\vdash
p^{\prime})$

Then there is no composite theory of $\mathbb{P}$ after $\mathbb{V}$.

######  Remark 22.

Axiom (P7) is the same as axiom (V2), but now we require it to hold for
$\mathbb{P}$ as well as $\mathbb{V}$. Axiom (P8) states that the term $p(1,2)$
is not equal to a constant in $\mathbb{P}$.

######  Proof 3.4.

Assume by way of a contradiction that a composite theory $\mathbb{U}$ of
$\mathbb{P}$ after $\mathbb{V}$ exists. Then as $\mathbb{U}$ is composite,
there exist $X\vdash p^{\prime}$ and $\Gamma\vdash v^{\prime}_{x}$ for each
variable $x\in\operatorname{var}(p^{\prime})$ such that:

$\Gamma\vdash v(p(1,2),p(3,4))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}/x].$
(11)

Without loss of generality, we may assume $p^{\prime}\in T_{\mathbb{P}}$ and
all $v^{\prime}_{x}\in T_{\mathbb{V}}$ by universality.

As in previous proofs, we use various substitutions to learn more about the
terms $p^{\prime}$ and all $v^{\prime}_{x}$. The first substitution reduces
the left hand side of Equation (11) to a term involving just $p(1,2)$. This
allows us to use essential uniqueness to get information about
$v^{\prime}_{x}$. Define substitution $f_{1}$ as follows:

$\displaystyle f_{1}(1)$ $\displaystyle=f_{1}(3)=1$ $\displaystyle f_{1}(2)$
$\displaystyle=f_{1}(4)=2$

Then from Equation (11) we conclude:

$\displaystyle v(p(1,2),p(3,4))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}/x]$
$\displaystyle\Rightarrow\;$
$\displaystyle\;\;\left\\{\;\text{Substitution}\;\right\\}$ $\displaystyle
v(p(1,2)[f_{1}],p(3,4)[f_{1}])=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{1}]/x]$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{applying the
substitution on the left hand side}\;\right\\}$ $\displaystyle
v(p(1,2),p(1,2))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{1}]/x]$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{Assumption
}\ref{ax:videm}:v\text{ is idempotent }\;\right\\}$ $\displaystyle
p(1,2)=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{1}]/x].$

We now have two separated terms that are equal to each other, so by essential
uniqueness, there are functions $g_{1}:2\rightarrow Z$ and $g_{2}:X\rightarrow
Z$ such that:

$p[g_{1}]=_{\mathbb{P}}p^{\prime}[g_{2}],$ (12)

and, for all $x\in\operatorname{var}(p^{\prime})$:

$\displaystyle g_{1}(1)=g_{2}(x)$ $\displaystyle\Leftrightarrow
1=_{\mathbb{V}}v^{\prime}_{x}[f_{1}]$ $\displaystyle g_{1}(2)=g_{2}(x)$
$\displaystyle\Leftrightarrow 2=_{\mathbb{V}}v^{\prime}_{x}[f_{1}].$

As $T_{\mathbb{P}}$ is stable, any variable renaming of $p^{\prime}$ is also
in $T_{\mathbb{P}}$. And so, by assumption (P3), we must have
$g_{2}(x)=g_{1}(1)$ or $g_{2}(x)=g_{1}(2)$, which means:

$\Gamma\vdash 1=_{\mathbb{V}}v^{\prime}_{x}[f_{1}]\quad\vee\quad\Gamma\vdash
2=_{\mathbb{V}}v^{\prime}_{x}[f_{1}].$

Then using assumption (V2), for all $v^{\prime}_{x}$:

$\\{1,3\\}\vdash v^{\prime}_{x}\quad\vee\quad\\{2,4\\}\vdash v^{\prime}_{x}.$
(13)

We can now split the set of variables $\operatorname{var}(p^{\prime})$ into
two disjoint subsets:

$\displaystyle X_{1}$ $\displaystyle=\\{x\;|\;\\{1,3\\}\vdash
v^{\prime}_{x}\\}$ (14) $\displaystyle X_{2}$
$\displaystyle=\\{x\;|\;\\{2,4\\}\vdash v^{\prime}_{x}\\}.$ (15)

The aim of the rest of the proof will be to show that
$\operatorname{var}(p^{\prime})=\emptyset$, which will give a contradiction
with assumption (P8). For this, we will need some more substitutions. Define a
second partial function $f_{2}$ as follows:

$\displaystyle f_{2}(1)$ $\displaystyle=f_{2}(2)=1$ $\displaystyle f_{2}(3)$
$\displaystyle=f_{2}(4)=2$

Applying this substitution to Equation (11):

$\displaystyle v(p(1,2),p(3,4))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}/x]$
$\displaystyle\Rightarrow\;$
$\displaystyle\;\;\left\\{\;\text{Substitution}\;\right\\}$ $\displaystyle
v(p(1,2)[f_{2}],p(3,4)[f_{2}])=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{2}]/x]$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{applying the
substitution on the left hand side}\;\right\\}$ $\displaystyle
v(p(1,1),p(2,2))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{2}]/x]$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{Assumption
}\ref{ax:pidem}:p\text{ is idempotent }\;\right\\}$ $\displaystyle
v(1,2)=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{2}]/x],$

which is the same as:

$5[v(1,2)/5]=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{2}]/x].$

Again we have two separated terms that are equal, allowing us to use essential
uniqueness. We conclude that there are functions $g_{3}:\\{5\\}\rightarrow Z$
and $g_{4}:X\rightarrow Z$ such that:

$5[g_{3}]=_{\mathbb{P}}p^{\prime}[g_{4}],$

and, whenever $g_{3}(5)=g_{4}(x)$,
$v(1,2)=_{\mathbb{V}}v^{\prime}_{x}[f_{2}]$. By assumption (P7):

$\\{g_{3}(5)\\}\vdash p^{\prime}[g_{4}].$

And so for all $x\in\operatorname{var}(p^{\prime})$:

$v^{\prime}_{x}[f_{2}]=_{\mathbb{V}}v(1,2).$ (16)

That is, under substitution $f_{2}$, all the $v^{\prime}_{x}$ are equal to
$v(1,2)$. The next step is designed to get rid of substitution $f_{2}$, and
hence fully understand each $v^{\prime}_{x}$. Since we already know from
Equation (13) that the variables appearing in $v^{\prime}_{x}$ are different
depending on whether $x\in X_{1}$ or $x\in X_{2}$, we need to treat those
cases separately. Starting with $x\in X_{1}$, consider the partial functions
$f_{3}$:

$\displaystyle f_{3}(1)$ $\displaystyle=1$ $\displaystyle f_{3}(3)$
$\displaystyle=3$ $\displaystyle f_{3}(2)$ $\displaystyle=3$ $\displaystyle
f_{3}(4)$ $\displaystyle=4$

This substitution will act as an ‘inverse’ for $f_{2}$, as will become clear
in the following argument. Combining Equations (13) and (16):

$\displaystyle v^{\prime}_{x}[f_{2}][f_{3}]$ $\displaystyle=\;$
$\displaystyle\;\;\left\\{\;\text{writing out the substitutions}\;\right\\}$
$\displaystyle v^{\prime}_{x}[1/1,1/2,2/3,2/4][1/1,3/2,3/3,4/4]$
$\displaystyle=\;$ $\displaystyle\;\;\left\\{\;\text{ignoring the identity
substitutions}\;\right\\}$ $\displaystyle v^{\prime}_{x}[1/2,2/3,2/4][3/2]$
$\displaystyle=\;$ $\displaystyle\;\;\left\\{\;x\in X_{1}\text{ so
}\\{1,3\\}\vdash v^{\prime}_{x}\;\right\\}$ $\displaystyle
v^{\prime}_{x}[2/3][3/2]$ $\displaystyle=\;$
$\displaystyle\;\;\left\\{\;\text{the second substitution is the inverse of
the first}\;\right\\}$ $\displaystyle v^{\prime}_{x}.$

Since $v^{\prime}_{x}[f_{2}]=_{\mathbb{V}}v(1,2)$ by Equation (16), we
conclude for all $x\in X_{1}$:

$\displaystyle v^{\prime}_{x}[f_{2}]=_{\mathbb{V}}v(1,2)$
$\displaystyle\Rightarrow\;$
$\displaystyle\;\;\left\\{\;\text{substitution}\;\right\\}$ $\displaystyle
v^{\prime}_{x}[f_{2}][f_{3}]=_{\mathbb{V}}v(1,2)[f_{3}]$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{by the above:
}v^{\prime}_{x}[f_{2}][f_{3}]=v^{\prime}_{x}\;\right\\}$ $\displaystyle
v^{\prime}_{x}=_{\mathbb{V}}v(1,2)[f_{3}]$ $\displaystyle\Rightarrow\;$
$\displaystyle\;\;\left\\{\;\text{applying }f_{3}\;\right\\}$ $\displaystyle
v^{\prime}_{x}=_{\mathbb{V}}v(1,3).$ (17)

So for $x\in X_{1}$, we know that $v^{\prime}_{x}=_{\mathbb{V}}v(1,3)$. A
similar line of reasoning can be followed for $x\in X_{2}$. To negate
substitution $f_{2}$ for these $v^{\prime}_{x}$, we need the following
substitution:

$\displaystyle f_{4}(1)$ $\displaystyle=2$ $\displaystyle f_{4}(3)$
$\displaystyle=3$ $\displaystyle f_{4}(2)$ $\displaystyle=4$ $\displaystyle
f_{4}(4)$ $\displaystyle=4$

The rest of the argument is the same, leading to the conclusion that for all
$x\in X_{2}$, $v^{\prime}_{x}=_{\mathbb{V}}v(2,4)$. We now have all the
information about the $v^{\prime}_{x}$ that we need. We start working towards
a contradiction with yet another substitution. This time, it is a substitution
of _terms_ for variables:

$\displaystyle f_{5}(1)$ $\displaystyle=p(1,2)$ $\displaystyle f_{5}(2)$
$\displaystyle=p(1,2)$ $\displaystyle f_{5}(3)$ $\displaystyle=p(1,1)$
$\displaystyle f_{5}(4)$ $\displaystyle=p(2,2)$

These terms are chosen in such a way that the left hand side of Equation (11)
reduces to $p(1,2)$ after substitution with $f_{5}$, so that we can use
essential uniqueness again. On the right hand side, the substitution creates
$\mathbb{V}$-terms with $\mathbb{P}$-terms in them. Separating these terms
into $\mathbb{P}$-terms built out of $\mathbb{V}$-terms will yield new
information, and eventually the contradiction. So, starting from Equation
(11):

$\displaystyle v(p(1,2),p(3,4))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}/x]$
$\displaystyle\Rightarrow\;$
$\displaystyle\;\;\left\\{\;\text{Substitution}\;\right\\}$ $\displaystyle
v(p(1,2)[f_{5}],p(3,4)[f_{5}])=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{5}]/x]$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{applying the
substitution on the left hand side}\;\right\\}$ $\displaystyle
v(p(p(1,2),p(1,2)),p(p(1,1),p(2,2))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{5}]/x]$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;p\text{ is
idempotent}\;\right\\}$ $\displaystyle
v(p(1,2),p(1,2))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{5}]/x]$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;v\text{ is
idempotent}\;\right\\}$ $\displaystyle
p(1,2)=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{5}]/x].$ (18)

Before applying essential uniqueness to Equation (18), we need to separate the
right hand side of this equation. Remember from Equation (17) that
$v^{\prime}_{x}=_{\mathbb{V}}v(1,3)$ or $v^{\prime}_{x}=_{\mathbb{V}}v(2,4)$
depending on whether $x\in X_{1}$ or $x\in X_{2}$. And so, for $x\in X_{1}$:

$\displaystyle v^{\prime}_{x}=_{\mathbb{V}}v(1,3)$
$\displaystyle\Rightarrow\;$
$\displaystyle\;\;\left\\{\;\text{substitution}\;\right\\}$ $\displaystyle
v^{\prime}_{x}[f_{5}]=_{\mathbb{U}}v(1,3)[f_{5}]$ $\displaystyle\Rightarrow\;$
$\displaystyle\;\;\left\\{\;\text{applying the substitution on the right hand
side}\;\right\\}$ $\displaystyle
v^{\prime}_{x}[f_{5}]=_{\mathbb{U}}v(p(1,2),p(1,1))$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{Substitution:
}1/3,1/4\;\right\\}$ $\displaystyle
v^{\prime}_{x}[f_{5}]=_{\mathbb{U}}v(p(1,2),p(3,4)[1/3,1/4])$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{Equation
\eqref{eq:separation}}\;\right\\}$ $\displaystyle
v^{\prime}_{x}[f_{5}]=_{\mathbb{U}}p^{\prime}[v^{\prime}_{y}[1/3,1/4]/y],$

where we know from Equation (17) that for $y\in X_{1}$,
$v^{\prime}_{y}=_{\mathbb{V}}v(1,3)$ and for $y\in X_{2}$,
$v^{\prime}_{y}=_{\mathbb{V}}v(2,4)$. Similarly, for $x\in X_{2}$:

$\displaystyle v^{\prime}_{x}=_{\mathbb{V}}v(2,4)$
$\displaystyle\Rightarrow\;$
$\displaystyle\;\;\left\\{\;\text{substitution}\;\right\\}$ $\displaystyle
v^{\prime}_{x}[f_{5}]=_{\mathbb{U}}v(2,4)[f_{5}]$ $\displaystyle\Rightarrow\;$
$\displaystyle\;\;\left\\{\;\text{applying the substitution on the right hand
side}\;\right\\}$ $\displaystyle
v^{\prime}_{x}[f_{5}]=_{\mathbb{U}}v(p(1,2),p(2,2))$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{Substitution:
}2/3,2/4\;\right\\}$ $\displaystyle
v^{\prime}_{x}[f_{5}]=_{\mathbb{U}}v(p(1,2),p(3,4)[2/3,2/4])$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{Equation
\eqref{eq:separation}}\;\right\\}$ $\displaystyle
v^{\prime}_{x}[f_{5}]=_{\mathbb{U}}p^{\prime}[v^{\prime}_{y}[2/3,2/4]/y],$

where we know from Equation (17) that for $y\in X_{1}$,
$v^{\prime}_{y}=_{\mathbb{V}}v(1,3)$ and for $y\in X_{2}$,
$v^{\prime}_{y}=_{\mathbb{V}}v(2,4)$. And so, continuing from Equation (18):

$\displaystyle p(1,2)=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{5}]/x]$
$\displaystyle\Rightarrow\;$ $\displaystyle
p(1,2)=_{\mathbb{U}}p^{\prime}[p^{\prime}[v^{\prime}_{y}[1/3,1/4]/y]/x\in
X_{1}),$
$\displaystyle\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\,p^{\prime}[v^{\prime}_{y}[2/3,2/4]/y]/x\in
X_{2})],$

where $v^{\prime}_{y}=_{\mathbb{V}}v(1,3)$ for $y\in X_{1}$ and
$v^{\prime}_{y}=_{\mathbb{V}}v(2,4)$ for $y\in X_{2}$. We can now apply
essential uniqueness, and use property (P3) to conclude that both:

$\displaystyle 1=_{\mathbb{V}}v^{\prime}_{y}[1/3,1/4]\quad\vee\quad$
$\displaystyle 2=_{\mathbb{V}}v^{\prime}_{y}[1/3,1/4]$ (19) $\displaystyle
1=_{\mathbb{V}}v^{\prime}_{y}[2/3,2/4]\quad\vee\quad$ $\displaystyle
2=_{\mathbb{V}}v^{\prime}_{y}[2/3,2/4].$ (20)

For $y\in X_{1}$, however:

$\displaystyle v^{\prime}_{y}[2/3,2/4]$
$\displaystyle=_{\mathbb{V}}v(1,3)[2/3,2/4]$ $\displaystyle=v(1,2).$

So, to satisfy equation (20), we conclude that $v(1,2)=_{\mathbb{V}}1$ or
$v(1,2)=_{\mathbb{V}}2$. By property (V2), this means that $\\{1\\}\vdash
v(1,2)$ or $\\{2\\}\vdash v(1,2)$. This contradicts property (V3). And so we
must conclude that $X_{1}=\emptyset$. Similarly, for $y\in X_{2}$:

$\displaystyle v^{\prime}_{y}[1/3,1/4]$
$\displaystyle=_{\mathbb{V}}v(2,4)[1/3,1/4]$ $\displaystyle=v(2,1).$

In order to satisfy equation 19, we must have $v(2,1)=_{\mathbb{V}}1$ or
$v(2,1)=_{\mathbb{V}}2$. By property (V2), this means that $\\{1\\}\vdash
v(2,1)$ or $\\{2\\}\vdash v(2,1)$, which contradicts property (V3). And so we
must also conclude that $X_{2}=\emptyset$. Therefore:

$\displaystyle\operatorname{var}(p^{\prime})$ $\displaystyle=X_{1}\cup X_{2}$
$\displaystyle=\emptyset\cup\emptyset$ $\displaystyle=\emptyset.$

However, from Equation (12) we know:
$p[g_{1}]=_{\mathbb{P}}p^{\prime}[g_{2}]$, and from property (P8) we know
that:

$\neg(\emptyset\vdash p^{\prime}[g_{2}]).$

And so, $\operatorname{var}(p^{\prime})$ cannot be empty. Contradiction! Hence
no composite theory of $\mathbb{P}$ after $\mathbb{V}$ can exist.

######  Remark 23.

The proofs in this section require different types of substitutions, and this
difference impacts their scope of application. The proofs of Theorems 14 and
19 only require variable-for-variable substitutions, and actually preclude the
existence of distributive laws for pointed endofunctors, generalizing [13,
Theorem 2.4]. The proof of Theorem 21 requires more complex substitutions,
implicitly assuming the multiplication axioms. Therefore, Theorem 21 only
applies to distributive laws between monads.

If we consider the algebraic theory of an idempotent binary operation, Theorem
21 shows that the induced monad cannot distribute over itself. This remains
true if we add either units or associativity, showing various non-commutative
variants of non-determinism cannot be distributed over themselves.

Similarly, if we denote any of these monads by $T$, there is no distributive
law $D\circ T\Rightarrow T\circ D$, where $D$ is the distribution monad.

######  Non-Example 24 (Reader Monad).

The presentation of the binary reader monad given in Example 4 satisfies:

$x=(x*y)*(z*x)$

However, this theory has no term $p$ satisfying both axioms (P2) and (P3). So
as expected, we cannot apply Theorem 21 to the binary reader monad.

###  3.2. Regarding Idempotence

All theorems so far rely heavily on idempotent terms in both theories. The
main advantage idempotent terms provide for our proofs is that they can be
reduced to a variable in a controlled way. Idempotence is, however, not the
only algebraic property with this effect. Compare idempotence:

$x*x=x$

to unitality:

$x*1=x$

Both idempotence and unitality have $x$ as the only variable appearing on
either side of the equation, and both equations reduce a more complicated term
to a single variable. We can capture this behaviour in slightly more general
terms, namely: _“There is a term $t$ and a substitution $f$ such that for any
variable $x\in\operatorname{var}(t)$, $t[f(x^{\prime})/x^{\prime}\neq x]=x$”._
For the idempotence and unitality equations, the term $t$ would be $x*y$, and
the substitution would be $f(y)=x$ for idempotence and $f(y)=1$ for unitality.

This generalisation of the idempotence equation leads us to Theorem 26. The
proof technique used for Theorem 14 still works with this more general
assumption, although extra care needs to be taken when substituting a
$\mathbb{T}$-term into an $\mathbb{S}$-term, as this could turn a previously
separated term into a term that is no longer separated. As in the previous
proofs, we need extra assumptions such as commutativity to make the proof go
through. Notice that we only generalise one of the two idempotent terms. For
the other term, the current proof method requires the more specific properties
of the idempotence equation.

######  Remark 25.

In Theorem 26 below we state and prove the theorem for _binary_ terms. This is
to make it easier to see where and how the more general assumption replaces
the assumption of idempotency in the proof. By copying the strategy from
Theorem 19, however, it is straightforward to generalise Theorem 26 to the
case where $p$ is an $m$-ary term and $v$ and $n$-ary term.

######  Theorem 26.

Let $\mathbb{P}$ and $\mathbb{V}$ be two algebraic theories, $T_{\mathbb{P}}$
a stable universal set of $\mathbb{P}$-terms, and $T_{\mathbb{V}}$ a stable
universal set of $\mathbb{V}$-terms. If there are terms:

$2\vdash_{\mathbb{P}}p\qquad\text{ and }\qquad 2\vdash_{\mathbb{V}}v$

such that:

  1. (P1)

$p$ is commutative:

$2\vdash p(1,2)=_{\mathbb{P}}p(2,1)$

  2. (P2)

There is a substitution $f_{p}:\operatorname{var}(p)\rightarrow
T_{\mathbb{P}}$, such that:

$\Gamma\vdash p(1,f_{p}(2))=_{\mathbb{P}}1.$

  3. (P3)

For all $n\vdash p^{\prime}\in T_{\mathbb{P}}$:

$n\vdash p(1,2)=_{\mathbb{P}}p^{\prime}\quad\Rightarrow\quad 2\vdash
p^{\prime}$

  1. (V1)

$v$ is idempotent:

$1\vdash v(1,1)=_{\mathbb{V}}1$

  2. (V2)

For all $v^{\prime}\in T_{\mathbb{V}}$, and each variable $x$:

$\Gamma\vdash x=_{\mathbb{V}}v^{\prime}\quad\Rightarrow\quad\\{x\\}\vdash
v^{\prime}$

  3. (V3)

For all $v^{\prime}\in T_{\mathbb{V}}$:

$\Gamma\vdash
v(1,2)=_{\mathbb{V}}v^{\prime}\quad\Rightarrow\quad\neg(\\{1\\}\vdash
v^{\prime}\vee\\{2\\}\vdash v^{\prime})$

Then there is no composite theory of $\mathbb{P}$ after $\mathbb{V}$.

######  Proof 3.5.

Assume by way of contradiction that a composite theory $\mathbb{U}$ of
$\mathbb{P}$ after $\mathbb{V}$ exists. Then as $\mathbb{U}$ is composite, the
separation axiom tells us that there exist $X\vdash p^{\prime}$ and
$\Gamma\vdash v^{\prime}_{x}$ for each $x\in X$ such that:

$\Gamma\vdash v(p(1,2),p(3,4))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}/x].$
(21)

We make the following substitution of variables:

$\displaystyle f_{1}(1)$ $\displaystyle=1$ $\displaystyle f_{1}(3)$
$\displaystyle=1$ $\displaystyle f_{1}(2)$ $\displaystyle=2$ $\displaystyle
f_{1}(4)$ $\displaystyle=2$

This yields:

$\displaystyle
v(p(1,2),p(1,2))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{1}]/x]$
$\displaystyle\Leftrightarrow\;\;$ $\displaystyle\;\;\left\\{\;v\text{ is
idempotent}\;\right\\}$ $\displaystyle
p(1,2)=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{1}]/x].$

By essential uniqueness and assumption (P3), we conclude that for all $x$:

$v^{\prime}_{x}[f_{1}]=_{\mathbb{V}}1\quad\vee\quad
v^{\prime}_{x}[f_{1}]=_{\mathbb{V}}2.$ (22)

So, using assumption (V2):

$\\{1,3\\}\vdash v^{\prime}_{x}\quad\vee\quad\\{2,4\\}\vdash v^{\prime}_{x}.$
(23)

We make a second substitution:

$\displaystyle f_{2}(1)$ $\displaystyle=1$ $\displaystyle f_{2}(3)$
$\displaystyle=2$ $\displaystyle f_{2}(2)$ $\displaystyle=2$ $\displaystyle
f_{2}(4)$ $\displaystyle=1$

This yields:

$\displaystyle
v(p(1,2),p(2,1))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{2}]/x]$
$\displaystyle\Leftrightarrow\;\;$ $\displaystyle\;\;\left\\{\;p\text{ is
commutative}\;\right\\}$ $\displaystyle
v(p(1,2),p(1,2))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{2}]/x]$
$\displaystyle\Leftrightarrow\;\;$ $\displaystyle\;\;\left\\{\;v\text{ is
idempotent}\;\right\\}$ $\displaystyle
p(1,2)=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{2}]/x].$

By essential uniqueness and assumption (P3), we conclude that for all $x$:

$v^{\prime}_{x}[f_{2}]=_{\mathbb{V}}1\quad\vee\quad
v^{\prime}_{x}[f_{2}]=_{\mathbb{V}}2.$

So, using assumption (V2):

$\\{1,4\\}\vdash v^{\prime}_{x}\quad\vee\quad\\{2,3\\}\vdash v^{\prime}_{x}.$
(24)

Taking Equations (23) and (23) together, we conclude for all x:

$\bigvee_{i\in 4}\\{i\\}\vdash v^{\prime}_{x}.$ (25)

This implies that for each $x$, $v^{\prime}_{x}$ is equal to a variable:

  * •

If $\\{1\\}\vdash v^{\prime}_{x}$, then
$v^{\prime}_{x}[f_{1}]=v^{\prime}_{x}$. From Equation 22 we know that
$v^{\prime}_{x}[f_{1}]=_{\mathbb{V}}1$ or
$v^{\prime}_{x}[f_{1}]=_{\mathbb{V}}2$. And so also
$v^{\prime}_{x}=_{\mathbb{V}}1$ or $v^{\prime}_{x}=_{\mathbb{V}}2$.

  * •

If $\\{2\\}\vdash v^{\prime}_{x}$, then also
$v^{\prime}_{x}[f_{1}]=v^{\prime}_{x}$, and so again
$v^{\prime}_{x}=_{\mathbb{V}}1$ or $v^{\prime}_{x}=_{\mathbb{V}}2$.

  * •

If $\\{3\\}\vdash v^{\prime}_{x}$, then
$v^{\prime}_{x}[f_{1}][3/1,4/2]=v^{\prime}_{x}$. From Equation 22 we know that
$v^{\prime}_{x}[f_{1}][3/1,4/2]=_{\mathbb{V}}~{}3$ or
$v^{\prime}_{x}[f_{1}][3/1,4/2]=_{\mathbb{V}}4$. And so also
$v^{\prime}_{x}=_{\mathbb{V}}3$ or $v^{\prime}_{x}=_{\mathbb{V}}4$.

  * •

If $\\{4\\}\vdash v^{\prime}_{x}$, then also
$v^{\prime}_{x}[f_{1}][3/1,4/2]=v^{\prime}_{x}$, and so again
$v^{\prime}_{x}=_{\mathbb{V}}3$ or $v^{\prime}_{x}=_{\mathbb{V}}4$.

We make a final substitution, using the substitution $f_{p}$ from property
(P2)::

$\displaystyle f_{3}(1)$ $\displaystyle=1$ $\displaystyle f_{3}(3)$
$\displaystyle=2$ $\displaystyle f_{3}(2)$ $\displaystyle=f_{p}(2)$
$\displaystyle f_{3}(4)$ $\displaystyle=f_{p}(4)$

This yields:

$\displaystyle
v(p(1,f_{p}(2)),p(3,f_{p}(4)))=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{3}]/x]$
$\displaystyle\Leftrightarrow\;\;$ $\displaystyle\;\;\left\\{\;\text{property
\ref{ax:punit}}\;\right\\}$ $\displaystyle
v(1,3)=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{3}]/x]$
$\displaystyle\Rightarrow\;\;$ $\displaystyle\;\;\left\\{\;\text{ clarifying
that }v(1,3)\text{ is a separated term}\;\right\\}$ $\displaystyle
5[v(1,3)/5]=_{\mathbb{U}}p^{\prime}[v^{\prime}_{x}[f_{3}]/x].$

Notice that the term $p^{\prime}[v^{\prime}_{x}[f_{3}]/x]$ is separated: since
every $v^{\prime}_{x}$ is just a variable, the substitution $f_{3}$ does not
break separation, even though it might insert a $\mathbb{P}$ term. We apply
essential uniqueness: there are substitutions $g_{1}:\\{5\\}\rightarrow
Z,g_{2}:X\rightarrow Z$ such that:

$\displaystyle 5[g_{1}]$ $\displaystyle=_{\mathbb{P}}p^{\prime}[g_{2}]$
$\displaystyle g_{1}(5)=g_{2}(x)$ $\displaystyle\Leftrightarrow
v(1,3)=_{\mathbb{V}}v^{\prime}_{x}.$

By consistency of $\mathbb{P}$, we know that there is at least one $x$ such
that $g_{1}(5)=g_{2}(x)$. And hence there is at least one $v^{\prime}_{x}$
such that $v^{\prime}_{x}=_{\mathbb{V}}v(1,3)$. But this contradicts
assumption (V3), since for all $x$, $v^{\prime}_{x}$ is equal to a variable.
We conclude that no composite theory of $\mathbb{P}$ after $\mathbb{V}$ can
exist.

Theorem 26 precludes even more distributive laws:

[Multiset and Powerset Monad: Filling in the Gap] The theory of commutative
monoids, presenting the multiset monad, does not have an idempotent term.
Therefore, it has so far been unaffected by our no-go theorems. It does,
however, have a unital term, bringing it in scope of Theorem 26. From Manes
and Mulry [11, Theorem 4.3.4] we know that there are distributive laws $M\circ
M\Rightarrow M\circ M$ and $M\circ P\Rightarrow P\circ M$, where $M$ is the
multiset monad and $P$ the powerset monad. We already know that the powerset
monad does not distribute over itself, which leaves the combination $P\circ
M\Rightarrow M\circ P$. Theorem 26 fills this gap, showing there is no
distributive law of that type.

##  4\. No-Go Theorems Beyond Plotkin

So far, all our impossibility results involve at least one monad with an
idempotent term in its corresponding algebraic theory. But the absence of an
idempotent term does not guarantee the existence of a distributive law.
Consider the list monad for example. This monad is quite similar to the
multiset monad, and we observed in Example 1 that the “times over plus” law of
Equation (1) induces a distributive law for the multiset monad over itself. If
we assume this also yields a distributive law for the list monad over itself,
then from one of the multiplication axioms:

$\lambda([[a,b],[c,d]])=[[a,c],[a,d],[b,c],[b,d]],$

whilst from the other:

$\lambda([[a,b],[c,d]])=[[a,c],[b,c],[a,d],[b,d]].$

These two statements are incompatible, so the list monad cannot distribute
over itself in this way. However, not all distributive laws resemble the
distributivity of times over plus, so from this observation alone we cannot
yet rule out the possibility of a distributive law for the list monad over
itself. In fact, Manes and Mulry found three other distributive laws for the
_non-empty_ list monad over itself [11, Example 5.1.9], [12, Example 4.10].
But despite these distributive laws being good candidates, they fail to extend
to distributive laws for the full list monad over itself.

The results in this section build up towards a proof that shows the search for
a distributive law for the list monad over itself is futile; no such law
exists. As in the previous section, we state our results in general terms, so
that they do not only apply to the list monad, but to any monad satisfying the
conditions of the theorems.

Firstly, we show in Proposition 28 that under certain circumstances, constants
of one algebraic theory act as ‘multiplicative zeroes’ for terms of the other
theory. One application is that any putative distributive law of the list
monad over itself must satisfy:

$\lambda[L_{1},\ldots,L_{n}]=[]\text{ if there is an }i\text{ s.t. }L_{i}=[].$

When the theory has multiple constants, this observation immediately leads to
a contradiction, and hence give us no-go Theorem 30.

Building on Proposition 28, we then derive conditions under which a
distributive law has to behave like the distributivity of times over plus (1),
resulting in Theorem 32. As a consequence, monads satisfying the conditions of
this theorem compose via a unique distributive law, if they compose at all.
Again this theorem applies to the list monad, meaning there can be at most one
distributive law for the list monad over itself.

Finally, in Theorems 37 and 41 we identify properties that together with
Theorem 32 provide two more no-go theorems: Theorem 37 and Theorem 41. Whereas
idempotence was the main property of interest for the no-go theorems in
Section 3, the focus now becomes unitality equations. In addition, the abides
equation (above-besides, [19]) will be important for Theorem 37:

$(a*b)*(c*d)=(a*c)*(b*d).$ (26)

We will require that this equation does _not_ hold. This is made precise in
property (T5)b below. From this theorem we can conclude that there is no
distributive law for the list monad over itself: the lacking of the abides
property is exactly what causes the problem identified at the beginning of
this section.

Throughout this section, we will consider two algebraic theories $\mathbb{S}$
and $\mathbb{T}$. For $\mathbb{S}$ we identify the following properties:

  1. (S1)

For any two terms $s^{\prime},s^{\prime\prime}$:

$\emptyset\vdash s^{\prime}\;\wedge\;\Gamma\vdash
s^{\prime}=_{\mathbb{S}}s^{\prime\prime}\quad\Rightarrow\quad\emptyset\vdash
s^{\prime\prime}.$

  2. (S2)

For any term $s^{\prime}$ and variable $x$:

$\Gamma\vdash s^{\prime}=_{\mathbb{S}}x\quad\Rightarrow\quad\\{x\\}\vdash
s^{\prime}.$

  3. (S3)

$\mathbb{S}$ has an $n$-ary term $s$ ($n\geq 1$), for which there is a
substitution $f:\operatorname{var}(s)\rightarrow\mathbb{S}$ such that for any
$x\in\operatorname{var}(s)$:

$\Gamma\vdash s[f(y)/y\neq x]=_{\mathbb{S}}x.$

  4. (S4)

For any n-ary term $s^{\prime}$ ($n\geq 1$), there is a substitution
$f:\operatorname{var}(s^{\prime})\rightarrow\mathbb{S}$ such that for any
$x\in\operatorname{var}(s^{\prime})$:

$\Gamma\vdash s^{\prime}[f(y)/y\neq x]=_{\mathbb{S}}x.$

  5. (S5)

$\mathbb{S}$ has a binary term $s$ such that:

    1. (a)

$e_{s}$ is a unit for $s$:

$\\{x\\}\vdash s(x,e_{s})=_{\mathbb{S}}x=_{\mathbb{S}}s(e_{s},x).$

    2. (b)

$s$ is idempotent:

$\\{x\\}\vdash s(x,x)=_{\mathbb{S}}x.$

And for $\mathbb{T}$:

  1. (T1)

For all terms $X\vdash t^{\prime}$, constant $e_{\mathbb{T}}$, and any
variable substitution $f:X\rightarrow Y$:

$Y\vdash t^{\prime}[f]=_{\mathbb{T}}e_{\mathbb{T}}\quad\Rightarrow\quad
X\vdash t^{\prime}=_{\mathbb{T}}e_{\mathbb{T}}.$

  2. (T2)

For any two terms $t^{\prime},t^{\prime\prime}$:

$\emptyset\vdash t^{\prime}\;\wedge\;\Gamma\vdash
t^{\prime}=_{\mathbb{T}}t^{\prime\prime}\quad\Rightarrow\quad\emptyset\vdash
t^{\prime\prime}.$

  3. (T3)

For any term $t^{\prime}$ and variable $x$:

$\Gamma\vdash t^{\prime}=_{\mathbb{T}}x\quad\Rightarrow\quad\\{x\\}\vdash
t^{\prime}.$

  4. (T4)

$\mathbb{T}$ has a constant $e_{\mathbb{T}}$.

  5. (T5)

$\mathbb{T}$ has a binary term $t$ such that:

    1. (a)

$e_{t}$ is a unit for $t$:

$\\{x\\}\vdash t(x,e_{t})=_{\mathbb{T}}x=_{\mathbb{T}}t(e_{t},x).$

    2. (b)

The abides equation does not hold in $\mathbb{T}$:

$\displaystyle\Gamma\vdash t(t(x,y),t(z,w))=_{\mathbb{T}}t(t(x,z),t(y,w))$
$\displaystyle\Rightarrow\;3\vdash t(t(x,y),t(z,w)).$

######  Remark 27 (Interpretation of Axioms).

The properties (S1), (S2), (T2), (T3) are all constraints on the variables
appearing in terms. (S1) and (T2) read: “Any term provably equal to a constant
cannot have any variables itself”. This is, for example, not the case for any
theory involving multiplicative zeroes. In the theory of rings, $0*x=0$, and
since the term $0*x$ has a variable, it does not satisfy (S1)/(T2).

(S2) and (T3) read: “Any term provably equal to a variable only contains that
single variable”. Idempotent terms are examples of terms that equal a
variable, satisfying this condition. In theories with absorption axioms, such
as the equation $x\vee(x\wedge y)=x$ from bounded lattices, properties
(S2)/(T3) do not hold.

Properties (S3) and (S4) are generalizations of idempotence and unital
equations. They require that terms can be reduced to variables via a suitable
substitution. Idempotence and unitality are both instances of this.
Idempotence requires the substitution to change all variables to $x$:
$s(x,y)[x/x,x/y]=s(x,x)=x$, while unitality uses a substitution of a constant
for all but one variable: $s(x,y)[e_{s}/y]=s(x,e_{s})=x$. The difference
between (S3) and (S4) is the quantifier.

Property (T1) is a weaker version of (T2), focussing on the provability of an
equality between a term and a constant, rather than restricting the variables
appearing in that term. It reads: “If a variable substitution of term
$t^{\prime}$ is provably equal to a constant, then $t^{\prime}$ is already
provably equal to that constant.” The usefulness of this property compared to
(T2) is that is allows for equations such as $0*x=0$, which were forbidden by
(T2).

Notice that property (T2) implies (T1): if $t^{\prime}[f]=e_{\mathbb{T}}$ then
(T2) requires $t^{\prime}[f]$ to contain no variables. Since $f$ is a variable
substitution, this means $t^{\prime}$ already had no variables, and hence
$t^{\prime}=t^{\prime}[f]=e_{\mathbb{T}}$, so (T1) is satisfied. This
justifies our claim that one is a weaker version of the other.

Also notice that (S5)a and (S5)b both imply (S3).

If a theory $\mathbb{S}$ has a presentation in which all operations are either
idempotent or have a unit, then an easy induction shows that $\mathbb{S}$ will
satisfy (S4). More precisely, if for every $s^{\prime}\in\Sigma^{\mathbb{S}}$,
either:

  * •

$s^{\prime}$ is idempotent, that is: $s^{\prime}[x/y\neq x]=_{\mathbb{S}}x$,
or:

  * •

$s^{\prime}$ has a unit $e_{s^{\prime}}$: $s^{\prime}[e_{s^{\prime}}/y\neq
x]=_{\mathbb{S}}x$,

then $\mathbb{S}$ satisfies (S4).

[Algebraic Properties of Key Monads]

  * •

The list monad, presented by the theory of monoids, satisfies (S1) and (S2).
The monoid multiplication satisfies (S5)a and hence also (S3) and even (S4),
but the theory of monoids does not satisfy (S5)b. The equation
$(x*y)*(z*w)=(x*z)*(y*w)$ holds in the theory of monoids if and only if $y=z$,
and so it satisfies all of (T1), (T2), (T3), (T4), (T5)a, and (T5)b.

  * •

The powerset monad is presented by the theory of join semilattices, which
satisfies (S5)b in addition to (S1), (S2), (S3), (S4), and (S5)a. However,
this theory does not have property (T5)b as the join is commutative and
associative and so satisfies the abides equation (26). Properties (T1), (T2),
(T3), (T4), and (T5)a still hold.

  * •

The exception monad corresponds to an algebraic theory with a signature
containing constants for each exception, and no axioms. It satisfies (S1),
(S2), and (S4). It does not satisfy (S3), (S5)a, and (S5)b as there are no
binary terms. Similarly, it satisfies (T1), (T2), (T3), and (T4), but not
(T5)a or (T5)b.

###  4.1. Multiplicative Zeroes

Our first focus is on properties (S3) and (T4). The goal is to prove that in a
composite of theories $\mathbb{S}$ and $\mathbb{T}$, the constant
$e_{\mathbb{T}}$ behaves like a multiplicative zero, consuming any
$\mathbb{S}$-term it appears in.

######  Proposition 28.

Let $\mathbb{S}$ be an algebraic theory satisfying property (S3) for term $s$
in $\mathbb{S}$, and $\mathbb{T}$ a theory satisfying properties (T1) and
(T4), giving constant $e_{\mathbb{T}}$. If $\mathbb{U}$ is a composite theory
of $\mathbb{T}$ after $\mathbb{S}$, then we must have that, for any
$x_{i}\in\operatorname{var}(s)$,
$s[e_{\mathbb{T}}/x_{i}]=_{\mathbb{U}}e_{\mathbb{T}}$.

######  Proof 4.1.

The statement is trivial in the case that $s$ has only one free variable,
because property (S3) implies that we must have $s(x)=_{\mathbb{S}}x$. We may
therefore assume that $s$ has at least two free variables.

In a composite theory, every term is equal to a separated term. So there is a
$t^{\prime}$ and there are $s^{\prime}_{x}$ such that:

$s[e_{\mathbb{T}}/x_{i}]=_{\mathbb{U}}t^{\prime}[s^{\prime}_{x}/x].$

Using the substitution $f$ given by property (S3):

$\displaystyle s[e_{\mathbb{T}}/x_{i}][f(y)/y\neq
x_{i}]=_{\mathbb{U}}t^{\prime}[s^{\prime}_{x}[f(y)/y\neq x_{i}]/x]$
$\displaystyle\Rightarrow\;\;$ $\displaystyle\;\;\left\\{\;\text{axiom
\ref{ax:newsnary}}\;\right\\}$ $\displaystyle
e_{\mathbb{T}}=_{\mathbb{U}}t^{\prime}[s^{\prime}_{x}[f(y)/y\neq x_{i}]/x].$

We now have two separated terms equal to each other, so we can use essential
uniqueness to conclude that there are variable substitutions $g_{1},g_{2}$
such that:

$e_{\mathbb{T}}[g_{1}]=_{\mathbb{T}}t^{\prime}[g_{2}].$

Since $g_{2}$ is a variable substitution, we can apply assumption (T1), and
conclude that $t^{\prime}=_{\mathbb{T}}e_{\mathbb{T}}$. Going back to our
original equation:

$\displaystyle
s[e_{\mathbb{T}}/x_{i}]=_{\mathbb{U}}t^{\prime}[s^{\prime}_{x}/x]$
$\displaystyle\Rightarrow\;\;$
$\displaystyle\;\;\left\\{\;t^{\prime}=_{\mathbb{T}}e_{\mathbb{T}}\;\right\\}$
$\displaystyle
s[e_{\mathbb{T}}/x_{i}]=_{\mathbb{U}}e_{\mathbb{T}}[s^{\prime}_{x}/x]$
$\displaystyle\Rightarrow\;\;$
$\displaystyle\;\;\left\\{\;e_{\mathbb{T}}\text{ has no variables}\;\right\\}$
$\displaystyle s[e_{\mathbb{T}}/x_{i}]=_{\mathbb{U}}e_{\mathbb{T}},$

which is what we needed to show.

######  Remark 29.

If $\mathbb{S}$ satisfies property (S4), that is, all terms in $\mathbb{S}$
with $\geq 1$ variables satisfy (S3), then the constant $e_{\mathbb{T}}$ in
$\mathbb{T}$ annihilates any $\mathbb{S}$-term it appears in. We say that
$e_{\mathbb{T}}$ acts as a multiplicative zero.

If $\mathbb{T}$ has more than one constant, this could lead to
inconsistencies. Our next no-go theorem makes this precise:

######  Theorem 30 (No-Go Theorem: Too Many Constants).

Let $\mathbb{S}$ and $\mathbb{T}$ be algebraic theories with properties (S3)
and (T1) respectively. Further assume that the term $s$ satisfying (S3) has at
least two free variables. Then there exists no composite theory of
$\mathbb{T}$ after $\mathbb{S}$ if $\mathbb{T}$ has two or more constants.

######  Proof 4.2.

Suppose that $\mathbb{U}$ is a composite theory of $\mathbb{T}$ after
$\mathbb{S}$ and let $e_{1}$ and $e_{2}$ be distinct constants in
$\mathbb{T}$. Suppose that $\\{x,y\\}\subseteq\operatorname{var}(s)$. Then by
Proposition 28 we have:

$e_{1}=_{\mathbb{U}}s[e_{1}/x,e_{2}/y]=_{\mathbb{U}}e_{2}.$

By essential uniqueness, we may conclude that $e_{1}=_{\mathbb{T}}e_{2}$.
Contradiction. So $\mathbb{U}$ cannot be a composite of $\mathbb{T}$ after
$\mathbb{S}$.

[Iterated Distributive Laws] Theorem 30 is remarkably useful for determining
whether iterated distributive laws are possible. Cheng shows in her paper
_Iterated distributive laws_ [32] that three or more monads can be composed if
there are distributive laws for the pairwise compositions of the monads, and
these distributive laws additionally satisfy the Yang-Baxter equation. Theorem
30 approaches the question of iterated distributive laws from the other end,
by severely limiting the possibilities. If in a proposed composition of monads
$C\circ B\circ A$, the monads $B$ and $C$ each have a constant (and the other
mild requirements of Theorem 30 are satisfied), then there is no distributive
law $A\circ(C\circ B)\Rightarrow(C\circ B)\Rightarrow A$, and hence any
possible pairwise distributive laws will not satisfy Yang-Baxter.

We give a few concrete examples involving the list, multiset and powerset
monads $L,M,P$, whose algebraic theories are monoids, commutative monoids, and
join semilattices respectively. We know from Manes and Mulry [11, Theorem
4.3.4] that we can form the monads $M\circ L$, $M\circ M$, and $M\circ P$ via
distributive laws. All of these monads have two constants, which satisfy the
condition for $\mathbb{T}$ in Theorem 30. By picking the term $x*y$ in each of
the theories for $L$, $M$, and $P$, we see that these monads satisfy the
condition for $\mathbb{S}$. We can therefore exclude all of the following
compositions via distributive laws:

Table 1. Overview of possible distributive laws of type:

row $\circ$ column $\Rightarrow$ column $\circ$ row, involving the monads
list $(L)$, multiset $(M)$, and powerset $(P)$.
$M\circ L$ $M\circ M$ $M\circ P$ $L$ $\times$ $\times$ $\times$ $M$ $\times$
$\times$ $\times$ $P$ $\times$ $\times$ $\times$

[An Error in the Literature] We saw in the previous example that the term
$x*y$ from monoids (the list monad) satisfies the conditions for $\mathbb{S}$
in Theorem 30. The exception monad satisfies (T1), so when the exception monad
has more than one exception, Theorem 30 states that there is no distributive
law $L\circ(-+E)\Rightarrow(-+E)\circ L$.

However, Manes and Mulry claim to have a distributive law of this type for the
case where $E=\\{a,b\\}$ [12, Example 4.12], given by:

$\displaystyle\lambda[]$ $\displaystyle=[]$ $\displaystyle\lambda[e]$
$\displaystyle=e\text{ for any exception }e\in E$ $\displaystyle\lambda L$
$\displaystyle=L\text{ if no element of $L$ is in }E$ $\displaystyle\lambda L$
$\displaystyle=a\text{ otherwise.}$

We check more concretely that this cannot be a distributive law by showing
that it fails the first multiplication axiom from Definition 2.1:

${{[[b],[]]}}$${{[b,[]]}}$${a}$${{[b]}}$${b}$${a}$$\scriptstyle{\mu^{L}_{EX}}$$\scriptstyle{L(\lambda_{X})}$$\scriptstyle{\lambda_{LX}}$$\scriptstyle{E(\mu^{L}_{X})}$$\scriptstyle{\lambda_{X}}$${\neq}$

The given distributive law follows directly from Manes and Mulry’s Theorem 4.6
[12]. We suspect that the problem originates in Lemma 4.5 of this paper. Louis
Parlant found that the proof of this lemma might use the isomorphism
$(A\otimes I)\cong A$ implicitly if the signature of the theory has constants,
while the lemma explicitly does not assume any monoidal properties of its
functors. So the lemma, and hence also Theorem 4.6, may not be valid in the
case that the theory has constants. In addition, the induction in the proof of
Lemma 4.5 starts at $n=1$, where $n$ is the number of variables appearing in a
term. This induction therefore excludes constants, which should be considered
separately but are absent from the proof.

It is important to notice that Theorem 30 does not contradict the well-known
result that the exception monad distributes over every set monad $T$; that
result is for the other direction $(-+E)\circ T\Rightarrow T\circ(-+E)$.

######  Non-Example 31 (Exception Monad).

It is well known that the exception monad distributes over itself. Even though
the corresponding theory satisfies properties (S3) and (T1), there are no
terms with more than one free variable, and hence Theorem 30 does not apply.

###  4.2. The One Distributive Law, If It Exists

Needing just the properties (S3), (T1), and (T4), Proposition 28 already
greatly restricts the possibilities for a distributive law between monads $S$
and $T$. We will now see that if both $\mathbb{S}$ and $\mathbb{T}$ have
binary terms with units, then in a composite theory, the binary of
$\mathbb{S}$ distributes over the binary of $\mathbb{T}$ like times over plus
in Equation (1). For the monads corresponding to these theories, this means
that there is only one candidate distributive law to consider.

######  Theorem 32 (Times over Plus Theorem).

Let $\mathbb{S}$ and $\mathbb{T}$ be two algebraic theories, satisfying (S1),
(S2), (S4) and (T2), (T3), (T4) respectively. Assume furthermore that there
are terms:

$2\vdash_{\mathbb{S}}s\qquad\text{ and }\qquad 2\vdash_{\mathbb{T}}t,$

satisfying (S5)a and (T5)a respectively. Finally, let $\mathbb{U}$ be a
composite theory of $\mathbb{T}$ after $\mathbb{S}$. Then $s$ distributes over
$t$:

$\displaystyle s(t(y_{1},y_{2}),x_{0})$
$\displaystyle=_{\mathbb{U}}t(s(y_{1},x_{0}),s(y_{2},x_{0}))$ (27)
$\displaystyle s(x_{0},t(y_{1},y_{2}))$
$\displaystyle=_{\mathbb{U}}t(s(x_{0},y_{1}),s(x_{0},y_{2})).$ (28)

We derive the distributional behaviour in three stages, relying as always on
separation and essential uniqueness in a composite theory. Suppose that
$t^{\prime}[s^{\prime}_{x}/x]$ is a separated term such that
$s(t(y_{1},y_{2}),x_{0})=_{\mathbb{U}}t^{\prime}[s^{\prime}_{x}/x]$, then we
derive the following about $t^{\prime}[s^{\prime}_{x}/x]$:

  1. (1)

First we prove which variables appear in the terms $s^{\prime}_{x}$ of the
separated term: $\operatorname{var}(s^{\prime}_{x})=\\{y_{1},x_{0}\\}$ or
$\operatorname{var}(s^{\prime}_{x})=\\{y_{2},x_{0}\\}$.

  2. (2)

Then, we prove that each of the $s^{\prime}_{x}$ is either equal to
$s(y_{1},x_{0})$ or to $s(y_{2},x_{0})$.

  3. (3)

Finally, we derive that the separated term $t^{\prime}[s^{\prime}_{x}/x]$ has
to be equal to $t(s(y_{1},x_{0}),s(y_{2},x_{0}))$.

The proofs of these three stages are quite long. They are separated into
different lemmas to make it easier to keep track of the main line of
reasoning.

######  Lemma 33.

Let $\mathbb{S}$ and $\mathbb{T}$ be two algebraic theories satisfying (S1),
(S2), (S4), and (T2), (T4) respectively. Assume furthermore that there are
terms:

$2\vdash_{\mathbb{S}}s\qquad\text{ and }\qquad 2\vdash_{\mathbb{T}}t,$

satisfying (S5)a and (T5)a respectively. Finally, let $\mathbb{U}$ be a
composite theory of $\mathbb{T}$ after $\mathbb{S}$. Then there is a
$\mathbb{T}$-term $X\vdash t^{\prime}$ and there is a family of
$\mathbb{S}$-terms $s^{\prime}_{x},x\in X$ such that:

$s(t(y_{1},y_{2}),x_{0})=_{\mathbb{U}}t^{\prime}[s^{\prime}_{x}/x],$

and for each $x\in\operatorname{var}(t^{\prime})$:

$\operatorname{var}(s^{\prime}_{x})=\\{y_{1},x_{0}\\}\qquad\text{or}\qquad\operatorname{var}(s^{\prime}_{x})=\\{y_{2},x_{0}\\}.$

Moreover, there is an $x$ such that
$\operatorname{var}(s^{\prime}_{x})=\\{y_{1},x_{0}\\}$ and an $x$ such that
$\operatorname{var}(s^{\prime}_{x})=\\{y_{2},x_{0}\\}$.

Similarly, there is a $\mathbb{T}$-term $X^{\prime}\vdash t^{\prime\prime}$
and there is a family of $\mathbb{S}$-terms
$s^{\prime\prime}_{x^{\prime}},x^{\prime}\in X^{\prime}$ such that:

$s(x_{0},t(y_{1},y_{2}))=_{\mathbb{U}}t^{\prime\prime}[s^{\prime\prime}_{x^{\prime}}/x^{\prime}],$

and for each $x^{\prime}\in\operatorname{var}(t^{\prime\prime})$:

$\operatorname{var}(s^{\prime\prime}_{x^{\prime}})=\\{y_{1},x_{0}\\}\qquad\text{or}\qquad\operatorname{var}(s^{\prime\prime}_{x^{\prime}})=\\{y_{2},x_{0}\\}.$

Moreover, there is an $x^{\prime}$ such that
$\operatorname{var}(s^{\prime\prime}_{x^{\prime}})=\\{y_{1},x_{0}\\}$ and an
$x^{\prime}$ such that
$\operatorname{var}(s^{\prime\prime}_{x^{\prime}})=\\{y_{2},x_{0}\\}$.

######  Proof 4.3.

We only explicitly prove the statements for $s(t(y_{1},y_{2}),x_{0})$. The
proof for $s(x_{0},t(y_{1},y_{2}))$ is similar.

From the fact that $\mathbb{U}$ is a composite of the theories $\mathbb{S}$
and $\mathbb{T}$, we know that every term in $\mathbb{U}$ is equal to a
separated term. And so, there is a $X\vdash t^{\prime}$ and there is a family
$s^{\prime}_{x},x\in X$ such that:

$\displaystyle
s(t(y_{1},y_{2}),x_{0})=_{\mathbb{U}}t^{\prime}[s^{\prime}_{x}/x].$ (29)

We substitute $x_{0}\mapsto e_{s}$ in Equation (29). This yields:

$\displaystyle
s(t(y_{1},y_{2}),e_{s})=_{\mathbb{U}}t^{\prime}[s^{\prime}_{x}[e_{s}/x_{0}]/x]$
$\displaystyle\Rightarrow\;\;$ $\displaystyle\;\;\left\\{\;e_{s}\text{ is the
unit of }s\;\right\\}$ $\displaystyle
t(y_{1},y_{2})=_{\mathbb{U}}t^{\prime}[s^{\prime}_{x}[e_{s}/x_{0}]/x].$ (30)

By the essential uniqueness property, we conclude that there are functions:

$f:\\{y_{1},y_{2}\\}\rightarrow Z,\quad f^{\prime}:X\rightarrow Z,$

such that:

$\displaystyle t(y_{1},y_{2})[f]=_{\mathbb{T}}t^{\prime}[f^{\prime}].$ (31)

Furthermore, whenever $f(y_{1})=f^{\prime}(x)$ or $f(y_{2})=f^{\prime}(x)$, we
have respectively:

$\displaystyle y_{1}$ $\displaystyle=_{\mathbb{S}}s^{\prime}_{x}[e_{s}/x_{0}]$
(32) $\displaystyle y_{2}$
$\displaystyle=_{\mathbb{S}}s^{\prime}_{x}[e_{s}/x_{0}].$ (33)

Since we assume variables $y_{1}$ and $y_{2}$ to be distinct, essential
uniqueness also gives us $f(y_{1})\neq f(y_{2})$.

We analyse Equation (31) more closely, comparing the variables appearing in
both $t(y_{1},y_{2})[f]$ and $t^{\prime}[f^{\prime}]$. First, we show that
$\\{f^{\prime}(x)\,|\,x\in\operatorname{var}(t^{\prime})\\}\subseteq\\{f(y_{1}),f(y_{2})\\}$.
This follows from the following equalities:

$\displaystyle e_{t}$ $\displaystyle=_{\mathbb{T}}\;$
$\displaystyle\;\;\left\\{\;e_{t}\text{ is the unit for }t\;\right\\}$
$\displaystyle t(e_{t},e_{t})$ $\displaystyle=_{\mathbb{T}}\;$
$\displaystyle\;\;\left\\{\;\text{Substitution}\;\right\\}$ $\displaystyle
t(f(y_{1}),f(y_{2}))[e_{t}/f(y_{1}),e_{t}/f(y_{2})]$
$\displaystyle=_{\mathbb{T}}\;$ $\displaystyle\;\;\left\\{\;\text{Equation
}\eqref{t-knowledge1}\;\right\\}$ $\displaystyle
t^{\prime}[f^{\prime}][e_{t}/f(y_{1}),e_{t}/f(y_{2})].$

So:
$e_{t}=_{\mathbb{T}}t^{\prime}[f^{\prime}][e_{t}/f(y_{1}),e_{t}/f(y_{2})]$.
Then by assumption (T2):

$\operatorname{var}(t^{\prime}[f^{\prime}][e_{t}/f(y_{1}),e_{t}/f(y_{2})])=\emptyset.$

Therefore, $t^{\prime}[f^{\prime}]$ can contain no other variables than
$f(y_{1})$ and $f(y_{2})$. That is:

$\\{f^{\prime}(x)\,|\,x\in\operatorname{var}(t^{\prime})\\}\subseteq\\{f(y_{1}),f(y_{2})\\}.$
(34)

Next, we show that both $f(y_{1})$ and $f(y_{2})$ need to appear in
$t^{\prime}[f^{\prime}]$. Suppose that $f(y_{1})$ does not appear in
$t^{\prime}[f^{\prime}]$. Then from Equation (34) we know that for all
$x\in\operatorname{var}(t^{\prime})$, $f^{\prime}(x)=f(y_{2})$. Then:

$\displaystyle f(y_{1})$ $\displaystyle=_{\mathbb{T}}\;$
$\displaystyle\;\;\left\\{\;e_{t}\text{ is the unit for }t\;\right\\}$
$\displaystyle t(f(y_{1}),e_{t})$ $\displaystyle=_{\mathbb{T}}\;$
$\displaystyle\;\;\left\\{\;\text{Substitution}\;\right\\}$ $\displaystyle
t(f(y_{1}),f(y_{2}))[e_{t}/f(y_{2})]$ $\displaystyle=_{\mathbb{T}}\;$
$\displaystyle\;\;\left\\{\;\text{Equation \eqref{t-knowledge1}}\;\right\\}$
$\displaystyle t^{\prime}[f^{\prime}][e_{t}/f(y_{2})]$
$\displaystyle=_{\mathbb{T}}\;$ $\displaystyle\;\;\left\\{\;\text{For all
}x,f^{\prime}(x)=f(y_{2})\;\right\\}$ $\displaystyle t^{\prime}[e_{t}/x].$

So: $f(y_{1})=_{\mathbb{T}}t^{\prime}[e_{t}/x]$, but this contradicts
assumption (T2), because $\operatorname{var}(t^{\prime}[e_{t}/x])=\emptyset$,
since every free variable in $t^{\prime}$ has been substituted with the
constant $e_{t}$, and
$\operatorname{var}(f(y_{1}))=\\{f(y_{1})\\}\neq\emptyset$.

So $f(y_{1})$ has to appear in $t^{\prime}[f^{\prime}]$. A similar line of
reasoning yields the same conclusion for $f(y_{2})$. Therefore, there is an
$x$ such that $f^{\prime}(x)=f(y_{1})$ and there is an $x$ such that
$f^{\prime}(x)=f(y_{2})$. In summary, if we define:

$\displaystyle X_{1}$
$\displaystyle=\\{x\in\operatorname{var}(t^{\prime})\,|\,f^{\prime}(x)=f(y_{1})\\}$
$\displaystyle X_{2}$
$\displaystyle=\\{x\in\operatorname{var}(t^{\prime})\,|\,f^{\prime}(x)=f(y_{2})\\},$

then we know that neither $X_{1}$ nor $X_{2}$ is empty and that $X_{1}\cup
X_{2}=\operatorname{var}(t^{\prime})$.

We finally consider Equations (32) and (33) to reach a conclusion about the
variables appearing in the terms $s^{\prime}_{x}$. Since for all $x\in
X_{1}:f^{\prime}(x)=f(y_{1})$, we have by Equation (32) that
$s^{\prime}_{x}[e_{s}/x_{0}]=_{\mathbb{S}}y_{1}$. Similarly, for all $x\in
X_{2}$, $s^{\prime}_{x}[e_{s}/x_{0}]=_{\mathbb{S}}y_{2}$. By assumption (S2),
we conclude that:

$\displaystyle\forall x\in X_{1}:\;$ $\displaystyle\\{x_{0},y_{1}\\}\vdash
s^{\prime}_{x}$ (35) $\displaystyle\forall x\in X_{2}:\;$
$\displaystyle\\{x_{0},y_{2}\\}\vdash s^{\prime}_{x}.$ (36)

In addition, since for any $x\in X_{1}$,
$y_{1}=_{\mathbb{S}}s^{\prime}_{x}[e_{s}/x_{0}]$, we would have $y_{1}$ equal
to a constant if $y_{1}$ would not appear in $s^{\prime}_{x}$, contradicting
assumption (S1). Similarly for $y_{2}$ and $s^{\prime}_{x},x\in X_{2}$. And
so:

$\displaystyle\forall x\in X_{1}:\;$ $\displaystyle
y_{1}\in\operatorname{var}(s^{\prime}_{x})$ (37) $\displaystyle\forall x\in
X_{2}:\;$ $\displaystyle y_{2}\in\operatorname{var}(s^{\prime}_{x}).$ (38)

To prove that $x_{0}\in\operatorname{var}(s^{\prime}_{x})$ for all
$x\in\operatorname{var}(t^{\prime})$, we substitute $x_{0}\mapsto e_{t}$ in
Equation (29):

$s(t(y_{1},y_{2}),e_{t})=_{\mathbb{U}}t^{\prime}[s^{\prime}_{x}[e_{t}/x_{0}]/x].$

By Proposition 28, $s(t(y_{1},y_{2}),e_{t})=_{\mathbb{U}}e_{t}$. Therefore we
must have that also:

$t^{\prime}[s^{\prime}_{x}[e_{t}/x_{0}]/x]=_{\mathbb{U}}e_{t}.$ (39)

The left hand side of this equation might not be separated, since we
substitute a $\mathbb{T}$-term inside $\mathbb{S}$-terms. We analyse the terms
$s^{\prime}_{x}[e_{t}/x_{0}]$ further to separate them into $\mathbb{T}$-terms
of $\mathbb{S}$-terms. There are two cases: either
$x_{0}\in\operatorname{var}(s^{\prime}_{x})$ or not.

  * •

If $x_{0}\in\operatorname{var}(s^{\prime}_{x})$, then by property (S4):
$s^{\prime}_{x}[e_{t}/x_{0}]=e_{t}$, which is a separated term.

  * •

If $x_{0}\notin\operatorname{var}(s^{\prime}_{x})$, then
$s^{\prime}_{x}[e_{t}/x_{0}]=s^{\prime}_{x}$, which is also a separated term.

We conclude that $t^{\prime}[s^{\prime}_{x}[e_{t}/x_{0}]/x]$ is separated. It
is our goal to show that we must have $x_{0}$ appearing in each
$s^{\prime}_{x}$. To this end, define:

$X_{3}=\\{x\in\operatorname{var}(t^{\prime})\;|\;x_{0}\in s^{\prime}_{x}\\}.$

We will show that we must have $X_{3}=\operatorname{var}(t^{\prime})$. We
define:

$t^{\prime\prime}=t^{\prime}[e_{t}/x\in X_{3}].$

Then:

$\displaystyle t^{\prime\prime}[s^{\prime}_{x}/x]$
$\displaystyle=_{\mathbb{U}}\;\;$ $\displaystyle\;\;\left\\{\;\text{definition
of }t^{\prime\prime}\;\right\\}$ $\displaystyle t^{\prime}[e_{t}/x\in
X_{3},s^{\prime}_{x}/x\notin X_{3}]$ $\displaystyle=_{\mathbb{U}}\;\;$
$\displaystyle\;\;\left\\{\;\text{for }x\in
X_{3}:s^{\prime}_{x}[e_{t}/x_{0}]=e_{t}\right.$
$\displaystyle\left.\;\;\;\;\,\text{and for }x\notin
X_{3}:s^{\prime}_{x}[e_{t}/x_{0}]=s^{\prime}_{x}\;\right\\}$ $\displaystyle
t^{\prime}[s^{\prime}_{x}[e_{t}/x_{0}]/x]$ $\displaystyle=_{\mathbb{U}}\;\;$
$\displaystyle\;\;\left\\{\;\text{Equation~{}\eqref{eq:t'=et}}\;\right\\}$
$\displaystyle e_{t}.$

So we can apply essential uniqueness to the equation
$t^{\prime\prime}[s^{\prime}_{x}/x]=_{\mathbb{U}}e_{t}$. We conclude that
there must be a variable substitution $g$ such that
$t^{\prime\prime}[g]=_{\mathbb{T}}e_{t}$. By property (T2) we conclude that
$\operatorname{var}(t^{\prime\prime}[g])=\emptyset$ and hence also
$\operatorname{var}(t^{\prime\prime})=\emptyset$. Since
$t^{\prime\prime}=t^{\prime}[e_{t}/x\in X_{3}]$, we conclude that $t^{\prime}$
has no variables that are not in $X_{3}$. In other words:
$X_{3}=\operatorname{var}(t^{\prime})$, and hence for all
$x\in\operatorname{var}(t^{\prime})$,
$x_{0}\in\operatorname{var}(s^{\prime}_{x})$.

This, together with Equations (35), (36), (37) and (38), proves that for all
$x\in\operatorname{var}(t^{\prime})$:

$\operatorname{var}(s^{\prime}_{x})=\\{y_{1},x_{0}\\}\qquad\text{or}\qquad\operatorname{var}(s^{\prime}_{x})=\\{y_{2},x_{0}\\}.$

The fact that neither $X_{1}$ nor $X_{2}$ are empty means that this proves the
lemma.

With the first step done, we move on to the second step:

######  Lemma 34.

Let $\mathbb{S}$ and $\mathbb{T}$ be two algebraic theories satisfying (S1),
(S2), (S4) and (T2), (T3), (T4) respectively. Assume furthermore that there
are terms:

$2\vdash_{\mathbb{S}}s\qquad\text{ and }\qquad 2\vdash_{\mathbb{T}}t,$

satisfying (S5)a and (T5)a respectively. Finally, let $\mathbb{U}$ be a
composite theory of $\mathbb{T}$ after $\mathbb{S}$. Then there is a
$\mathbb{T}$-term $X\vdash t^{\prime}$ and there is a family of
$\mathbb{S}$-terms $s^{\prime}_{x},x\in X$ such that:

$s(t(y_{1},y_{2}),x_{0})=_{\mathbb{U}}t^{\prime}[s^{\prime}_{x}/x],$

and for each $x\in\operatorname{var}(t^{\prime})$:

$s^{\prime}_{x}=_{\mathbb{S}}s(y_{1},x_{0})\qquad\text{or}\qquad
s^{\prime}_{x}=_{\mathbb{S}}s(y_{2},x_{0}).$

Moreover, there is an $x$ such that
$s^{\prime}_{x}=_{\mathbb{S}}s(y_{1},x_{0})$ and an $x$ such that
$s^{\prime}_{x}=_{\mathbb{S}}s(y_{2},x_{0})$.

Similarly, there is a $\mathbb{T}$-term $X^{\prime}\vdash t^{\prime\prime}$
and there is a family of $\mathbb{S}$-terms
$s^{\prime\prime}_{x^{\prime}},x^{\prime}\in X^{\prime}$ such that:

$s(x_{0},t(y_{1},y_{2}))=_{\mathbb{U}}t^{\prime\prime}[s^{\prime\prime}_{x^{\prime}}/x^{\prime}],$

and for each $x^{\prime}\in\operatorname{var}(t^{\prime\prime})$:

$s^{\prime\prime}_{x^{\prime}}=_{\mathbb{S}}s(x_{0},y_{1})\qquad\text{or}\qquad
s^{\prime\prime}_{x^{\prime}}=_{\mathbb{S}}s(x_{0},y_{2}).$

Moreover, there is an $x^{\prime}$ such that
$s^{\prime\prime}_{x^{\prime}}=_{\mathbb{S}}s(y_{1},x_{0})$ and an
$x^{\prime}$ such that
$s^{\prime\prime}_{x^{\prime}}=_{\mathbb{S}}s(y_{2},x_{0})$.

######  Proof 4.4.

Again, we only explicitly prove the statements for $s(t(y_{1},y_{2}),x_{0})$.
The second half of the claim follows similarly.

As $\mathbb{U}$ is a composite theory, we know from the separation axiom that
there is a $\mathbb{T}$-term $X\vdash t^{\prime}$ and a family of
$\mathbb{S}$-terms $s^{\prime}_{x},\,x\in X$ such that:

$s(t(y_{1},y_{2}),x_{0})=_{\mathbb{U}}t^{\prime}[s^{\prime}_{x}/x].$

We substitute $y_{1}\mapsto e_{t}$:

$\displaystyle
s(t(e_{t},y_{2}),x_{0})=_{\mathbb{U}}t^{\prime}[s^{\prime}_{x}[e_{t}/y_{1}]/x]$
$\displaystyle\Rightarrow\;\;$ $\displaystyle\;\;\left\\{\;e_{t}\text{ is the
unit of }t\;\right\\}$ $\displaystyle
s(y_{2},x_{0})=_{\mathbb{U}}t^{\prime}[s^{\prime}_{x}[e_{t}/y_{1}]/x]$
$\displaystyle\Rightarrow\;\;$ $\displaystyle\;\;\left\\{\;\text{showing that
$s(y_{2},x_{0})$ is a separated term}\;\right\\}$ $\displaystyle
z[s(y_{2},x_{0})/z]=_{\mathbb{U}}t^{\prime}[s^{\prime}_{x}[e_{t}/y_{1}]/x].$
(40)

To use essential uniqueness, we need two separated terms. However,
$t^{\prime}[s^{\prime}_{x}[e_{t}/y_{1}]/x]$ is a $\mathbb{T}$-term built out
of $\mathbb{S}$-terms with possibly a $\mathbb{T}$-constant in them. So we
need to separate this term. We use Proposition 28 in combination with our
knowledge from Lemma 33 about the variables appearing in each $s^{\prime}_{x}$
to do this. Define:

$\displaystyle X_{1}$
$\displaystyle=\\{x\in\operatorname{var}(t^{\prime})\,|\,\operatorname{var}(s^{\prime}_{x})=\\{y_{1},x_{0}\\}\\}$
$\displaystyle X_{2}$
$\displaystyle=\\{x\in\operatorname{var}(t^{\prime})\,|\,\operatorname{var}(s^{\prime}_{x})=\\{y_{2},x_{0}\\}\\}.$

From Lemma 33 we know that neither $X_{1}$ nor $X_{2}$ is empty and their
union contains all variables in $t^{\prime}$. For each $x\in X_{1}$, we use
property (S4) to apply Proposition 28, which tells us
$s^{\prime}_{x}[e_{t}/y_{1}]=_{\mathbb{U}}e_{t}$. For each $x\in X_{2}$, we
know that since $y_{1}$ does not appear in $s^{\prime}_{x}$,
$s^{\prime}_{x}[e_{t}/y_{1}]=_{\mathbb{U}}s^{\prime}_{x}$. Therefore:

$t^{\prime}[s^{\prime}_{x}[e_{t}/y_{1}]/x]=_{\mathbb{T}}t^{\prime}[e_{t}/x\in
X_{1},s^{\prime}_{x}/x\in X_{2})].$ (41)

Next, define:

$t^{\prime\prime}=t^{\prime}[e_{t}/x\in X_{1}].$

Then $X_{2}\vdash_{\mathbb{T}}t^{\prime\prime}$. We have:

$\displaystyle t^{\prime\prime}[s^{\prime}_{x}/x]$
$\displaystyle=_{\mathbb{U}}\;$ $\displaystyle\;\;\left\\{\;\text{Definition
of }t^{\prime\prime}\;\right\\}$ $\displaystyle t^{\prime}[e_{t}/x\in
X_{1},s^{\prime}_{x}/x\in X_{2}]$ $\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;\text{Equation \eqref{eq:t'}}\;\right\\}$
$\displaystyle t^{\prime}[s^{\prime}_{x}[e_{t}/y_{1}]/x]$
$\displaystyle=_{\mathbb{U}}\;$ $\displaystyle\;\;\left\\{\;\text{Equation
\eqref{eq:z-t0}}\;\right\\}$ $\displaystyle z[s(y_{2},x_{0})/z].$

Now we can use the essential uniqueness property, and conclude that there are
functions $f:\\{z\\}\rightarrow Z,f^{\prime}:X_{2}\rightarrow Z$ such that:

$\displaystyle z[f(z)/z]=_{\mathbb{T}}t^{\prime\prime}[f^{\prime}(x)/x].$ (42)

Furthermore, we have:

$\displaystyle f^{\prime}(x)=f(z)\Leftrightarrow s^{\prime}_{x}$
$\displaystyle=_{\mathbb{S}}s(y_{2},x_{0}).$ (43)

From Equation (42) and assumption (T3) we conclude that $\\{f(z)\\}\vdash
t^{\prime\prime}[f^{\prime}(x)/x]$. And hence for all $x\in X_{2}$,
$f^{\prime}(x)=f(z)$. So by Equation (43), for each $x\in X_{2}$:
$s^{\prime}_{x}=_{\mathbb{S}}s(y_{2},x_{0})$, which gives us half of the
desired conclusion about each
$s^{\prime}_{x},x\in\operatorname{var}(t^{\prime})$.

A similar argument using the substitution $y_{2}\mapsto e_{t}$ instead of
$y_{1}\mapsto e_{t}$ leads to the conclusion that for each $x\in X_{1}$,
$s^{\prime}_{x}=_{\mathbb{S}}s(y_{1},x_{0})$.

And finally, we prove the last step, in which we show that $s$ distributes
over $t$. This yields a proof of Theorem 32. We restate the theorem for
convenience:

######  Theorem 35 (Times over Plus Theorem).

Let $\mathbb{S}$ and $\mathbb{T}$ be two algebraic theories, satisfying (S1),
(S2), (S4) and (T2), (T3), (T4) respectively. Assume furthermore that there
are terms:

$2\vdash_{\mathbb{S}}s\qquad\text{ and }\qquad 2\vdash_{\mathbb{T}}t,$

satisfying (S5)a and (T5)a respectively. Finally, let $\mathbb{U}$ be a
composite theory of $\mathbb{T}$ after $\mathbb{S}$. Then $s$ distributes over
$t$:

$\displaystyle s(t(y_{1},y_{2}),x_{0})$
$\displaystyle=_{\mathbb{U}}t(s(y_{1},x_{0}),s(y_{2},x_{0}))$ (44)
$\displaystyle s(x_{0},t(y_{1},y_{2}))$
$\displaystyle=_{\mathbb{U}}t(s(x_{0},y_{1}),s(x_{0},y_{2})).$ (45)

######  Proof 4.5.

Again, we only explicitly prove the first statement, as the proof of the
second statement is similar, using the appropriate parts of Lemmas 33 and 34.

From the separation axiom of composite theories and Lemma 34 we know that
there is a $\mathbb{T}$-term $X\vdash t^{\prime}$ and a family of
$\mathbb{S}$-terms $s^{\prime}_{x},\,x\in X$ such that either
$s^{\prime}_{x}=s(y_{1},x_{0})$ or $s^{\prime}_{x}=s(y_{2},x_{0})$ and: