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

Define:

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

Then, using the substitution $x_{0}\mapsto e_{s}$, we get:

$\displaystyle t(y_{1},y_{2})$ $\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;e_{s}\text{ is the unit of }s\;\right\\}$
$\displaystyle s(t(y_{1},y_{2}),e_{s})$ $\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;\text{Substitution}\;\right\\}$ $\displaystyle
s(t(y_{1},y_{2}),x_{0})[e_{s}/x_{0}]$ $\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;\text{Lemma~{}\ref{t_0-diamond}}\;\right\\}$
$\displaystyle t^{\prime}[s^{\prime}_{x}[e_{s}/x_{0}]/x]$
$\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;s^{\prime}_{x}=s(y_{1},x_{0})\text{ or
}s^{\prime}_{x}=s(y_{2},x_{0})\right.$ $\displaystyle\left.\;\;\;\text{ and
}e_{s}\text{ is the unit of }s\;\right\\}$ $\displaystyle
t^{\prime}[y_{1}/x\in X_{1},y_{2}/x\in X_{2}].$

So:

$t(y_{1},y_{2})=_{\mathbb{U}}t^{\prime}[y_{1}/x\in X_{1},y_{2}/x\in X_{2}].$
(46)

We also have:

$\displaystyle t^{\prime}[s^{\prime}_{x}/x]$ $\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;\text{Lemma~{}\ref{t_0-diamond}}\;\right\\}$
$\displaystyle t^{\prime}[s(y_{1},x_{0})/x\in X_{1},s(y_{2},x_{0})/x\in
X_{2}]$ $\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;\text{Substitution:
}\text{term}=\text{variable}[\text{term}/\text{variable}]\;\right\\}$
$\displaystyle t^{\prime}[y_{1}[s(y_{1},x_{0})/y_{1}]/x\in
X_{1},y_{2}[s(y_{2},x_{0})/y_{2}]/x\in X_{2}].$

So we conclude:

$\displaystyle t^{\prime}[s^{\prime}_{x}/x]$ $\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;\text{by the reasoning above}\;\right\\}$
$\displaystyle t^{\prime}[y_{1}[s(y_{1},x_{0})/y_{1}]/x\in
X_{1},y_{2}[s(y_{2},x_{0})/y_{2}]/x\in X_{2}]$ $\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;\text{Equation \eqref{eq:theorem1}}\;\right\\}$
$\displaystyle t(y_{1},y_{2})[s(y_{1},x_{0})/y_{1},s(y_{2},x_{0})/y_{2}]$
$\displaystyle=_{\mathbb{U}}\;$ $\displaystyle
t(s(y_{1},x_{0}),s(y_{2},x_{0})),$

which proves the theorem.

In suitable cases, Theorem 32 reduces the search space for distributive laws
to a single possibility. From Proposition 8 we know that the action of
distributive laws is determined by the separated terms in the composite
theory. And so:

######  Corollary 36.

Let $S$ and $T$ be two monads presented by algebraic theories $\mathbb{S}$ and
$\mathbb{T}$, having signatures with at least one constant and one binary
operation. If for both theories the constant acts as a unit for the binary
operation and the theories further satisfy (S1), (S2), (S4), and (T2) and (T3)
respectively, then any distributive law $S\circ T\Rightarrow T\circ S$
distributes the binary from $\mathbb{S}$ over the binary from $\mathbb{T}$ as
in Equation (1).

[Unique Distributive Laws] Let $S$ be any of the monads tree222respresented by
the theory of a single binary operation and a constant, satisfying only left
and right unitality., list, or multiset. Then the corresponding algebraic
theory $\mathbb{S}$ contains only linear equations. Let $T$ be either the
multiset or powerset monad. Since the multiset and powerset monads are
commutative monads, we know that there is a distributive law $S\circ
T\Rightarrow T\circ S$ [11, Theorem 4.3.4]. Corollary 36 states that this
distributive law is unique. In particular, the distributive law for the
multiset monad over itself mentioned in Example 1 is unique.

###  4.3. Lacking the Abides Property: a No-Go Theorem

With Theorem 32 narrowing down the possible distributive laws for two monads,
it is easier to find cases in which no distributive law can exist at all. We
identify two properties that clash with Theorem 32, one for $\mathbb{T}$ and
one for $\mathbb{S}$. In this section we show that not satisfying the abides
equation, property (T5)b, in combination with Theorem 32 prevents the
existence of a distributive law. In the next section we do the same for
idempotence, property (S5)b. Both properties are sufficiently common to cover
a broad class of monads.

######  Theorem 37 (No-Go Theorem: Lacking Abides).

Let $\mathbb{S}$ and $\mathbb{T}$ be algebraic theories satisfying the
conditions of Theorem 32, and assume that the binary $t$ in $\mathbb{T}$
promised by (T5)a additionally satisfies (T5)b, then there does not exist a
composite theory of $\mathbb{T}$ after $\mathbb{S}$.

######  Proof 4.6.

Suppose there exists a composite theory $\mathbb{U}$. Given Theorem 32, we
compute a separated term equal in $\mathbb{U}$ to
$s(t(y_{1},y_{2}),t(y_{3},y_{4}))$:

$\displaystyle s(t(y_{1},y_{2}),t(y_{3},y_{4}))$
$\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;\text{Substitution}\;\right\\}$ $\displaystyle
s(t(y_{1},y_{2}),x_{0})[t(y_{3},y_{4})/x_{0}]$ $\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;\text{Equation \eqref{theoremeq1} from
Theorem~{}\ref{thm:times-over-plus}}\;\right\\}$ $\displaystyle
t(s(y_{1},x_{0}),s(y_{2},x_{0}))[t(y_{3},y_{4})/x_{0}]$
$\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;\text{Substitution}\;\right\\}$ $\displaystyle
t(s(y_{1},t(y_{3},y_{4})),s(y_{2},t(y_{3},y_{4})))$
$\displaystyle=_{\mathbb{U}}\;$ $\displaystyle\;\;\left\\{\;\text{Equation
\eqref{theoremeq2} from Theorem~{}\ref{thm:times-over-plus}}\;\right\\}$
$\displaystyle
t(t(s(y_{1},y_{3}),s(y_{1},y_{4})),t(s(y_{2},y_{3}),s(y_{2},y_{4}))).$ (47)

Notice that we made a choice, taking out the right $t$ term in

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

rather than the left:

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

The latter option yields:

$\displaystyle s(t(y_{1},y_{2}),t(y_{3},y_{4}))$
$\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;\text{Substitution}\;\right\\}$ $\displaystyle
s(x_{0},t(y_{3},y_{4}))[t(y_{1},y_{2})/x_{0}]$ $\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;\text{Equation \eqref{theoremeq2} from
Theorem~{}\ref{thm:times-over-plus}}\;\right\\}$ $\displaystyle
t(s(x_{0},y_{3}),s(x_{0},y_{4}))[t(y_{1},y_{2})/x_{0}]$
$\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;\text{Substitution}\;\right\\}$ $\displaystyle
t(s(t(y_{1},y_{2}),y_{3}),s(t(y_{1},y_{2}),y_{4}))$
$\displaystyle=_{\mathbb{U}}\;$ $\displaystyle\;\;\left\\{\;\text{Equation
\eqref{theoremeq1} from Theorem~{}\ref{thm:times-over-plus}}\;\right\\}$
$\displaystyle
t(t(s(y_{1},y_{3}),s(y_{2},y_{3})),t(s(y_{1},y_{4}),s(y_{2},y_{4})).$ (48)

Of course, both computations are equally valid, so the terms in Equations (47)
and (48) must be equal:

$\displaystyle
t(t(s(y_{1},y_{3}),s(y_{1},y_{4})),t(s(y_{2},y_{3}),s(y_{2},y_{4})))$
$\displaystyle=_{\mathbb{U}}\;$ $\displaystyle
t(t(s(y_{1},y_{3}),s(y_{2},y_{3})),t(s(y_{1},y_{4}),s(y_{2},y_{4}))).$

Since these are two separated terms that are equal, we can apply the essential
uniqueness property, stating that there exist functions:

$\displaystyle f:$ $\displaystyle\>\\{x_{1},x_{2},x_{3},x_{4}\\}\rightarrow Z$
$\displaystyle f^{\prime}:$
$\displaystyle\>\\{x_{5},x_{6},x_{7},x_{8}\\}\rightarrow Z,$

such that:

  * •

Equality in $\mathbb{T}$:

$\displaystyle t(t(f(x_{1}),f(x_{2})),t(f(x_{3}),f(x_{4})))$
$\displaystyle=_{\mathbb{T}}\;$ $\displaystyle
t(t(f^{\prime}(x_{5}),f^{\prime}(x_{6})),t(f^{\prime}(x_{7}),f^{\prime}(x_{8}))).$

  * •

$f(x_{i})=f^{\prime}(x_{j})$ iff the $\mathbb{S}$-terms substituted for
$x_{i}$ and $x_{j}$ in Equations (47) and (48) are equal in $\mathbb{S}$.

From the second part of essential uniqueness we get that:

$\displaystyle f(x_{1})$ $\displaystyle=f^{\prime}(x_{5})$ $\displaystyle
f(x_{3})$ $\displaystyle=f^{\prime}(x_{6})$ $\displaystyle f(x_{2})$
$\displaystyle=f^{\prime}(x_{7})$ $\displaystyle f(x_{4})$
$\displaystyle=f^{\prime}(x_{8}).$

For readability of the next argument, set:

$\displaystyle z_{1}=f(x_{1})$ $\displaystyle=f^{\prime}(x_{5})$
$\displaystyle z_{3}=f(x_{3})$ $\displaystyle=f^{\prime}(x_{6})$
$\displaystyle z_{2}=f(x_{2})$ $\displaystyle=f^{\prime}(x_{7})$
$\displaystyle z_{4}=f(x_{4})$ $\displaystyle=f^{\prime}(x_{8}).$

Putting this in the equality in $\mathbb{T}$ we found under the first bullet
point yields:

$\displaystyle t(t(z_{1},z_{2}),t(z_{3},z_{4}))$
$\displaystyle=_{\mathbb{T}}t(t(z_{1},z_{3}),t(z_{2},z_{4})).$

And so by property (T5)b:

$\\#\operatorname{var}(t(t(z_{1},z_{2}),t(z_{3},z_{4})))\leq 3.$

So there must be $i,j$ such that $i\neq j$ and $z_{i}=z_{j}$. Suppose without
loss of generality that $z_{1}=z_{2}$. Then by essential uniqueness we must
have that $s(y_{1},y_{3})=_{\mathbb{S}}s(y_{1},y_{4})$. But then we can
reason:

$\displaystyle y_{1}$ $\displaystyle=_{\mathbb{S}}\;$
$\displaystyle\;\;\left\\{\;e_{s}\text{ is a unit for }s\;\right\\}$
$\displaystyle s(y_{1},e_{s})$ $\displaystyle=_{\mathbb{S}}\;$
$\displaystyle\;\;\left\\{\;\text{Substitution}\;\right\\}$ $\displaystyle
s(y_{1},y_{3})[e_{s}/y_{3}]$ $\displaystyle=_{\mathbb{S}}\;$
$\displaystyle\;\;\left\\{\;s(y_{1},y_{3})=s(y_{1},y_{4})\;\right\\}$
$\displaystyle s(y_{1},y_{4})[e_{s}/y_{3}]$ $\displaystyle=_{\mathbb{S}}\;$
$\displaystyle\;\;\left\\{\;\text{Substitution: no }y_{3}\text{ in
}s(y_{1},y_{4})\;\right\\}$ $\displaystyle s(y_{1},y_{4}).$

We conclude that, by property (S2): $\\{y_{1}\\}\vdash s(y_{1},y_{4})$, and so
we must have $y_{4}=y_{1}$. Since these variables are assumed to be distinct,
we have a contradiction. The same argument holds for any other $i,j$ pair.
Therefore, the existence of a composite theory leads to a contradiction. In
other words, no such composite theory exists.

######  Corollary 38.

If monads $S$ and $T$ are presented by algebraic theories $\mathbb{S}$ and
$\mathbb{T}$, satisfying the axioms of Theorem 37, then there does not exist a
distributive law $S\circ T\Rightarrow T\circ S$.

[Resolving an Open Question] This finally settles the question of whether the
list monad distributes over itself, posed repeatedly by Manes and Mulry [11,
12]. The theory of monoids satisfies all the conditions required of both
theories in Theorem 37, and hence there is no distributive law for the list
monad over itself.

Note that a distributive law for lists was claimed by King and Wadler [16],
although it was subsequently shown to be incorrect by Jones and Duponcheel
[33].

######  Remark 39.

Although there is no distributive law for the list monad over itself, the
functor $LL$ does still carry a monad structure. We are very grateful to
Bartek Klin for pointing this out to us. The monad structure on $LL$ can be
described as follows:

  * •

There is a distributive law for the list monad over the non-empty list monad
$L\circ L^{+}\Rightarrow L^{+}\circ L$ [11].

  * •

There is a distributive law for the resulting monad over the maybe monad
$(L^{+}L)\circ(-)_{\bot}\Rightarrow(-)_{\bot}\circ(L^{+}L)$, derived from
general principles [11].

  * •

The resulting functor $(-)_{\bot}\circ(L^{+}\circ L)$ is isomorphic to $L\circ
L$, and carries a monad structure. Hence $L\circ L$ carries a monad structure,
but not one that can be derived from a distributive law $L\circ L\Rightarrow
L\circ L$.

######  Non-Example 40 (Multiset Monad).

The multiset monad is closely related to the list monad, with an algebraic
theory having just one extra equation compared to the list monad:
commutativity. Because of this equation, the theory does not have property
(T5)b. As we have seen in Example 36, there is a unique distributive law for
the multiset monad over itself.

###  4.4. Yet Another No-Go Theorem Caused by Idempotence

In Section 3 we saw a no-go theorem that required an idempotent term on one
side, and a unital one on the other: Theorem 26. We will now see a second
theorem of this type. Adding idempotence of the binary to the assumptions for
$\mathbb{S}$ yields yet another no-go theorem, which partly overlaps with
Theorem 26, but neither theorem is a consequence of the other.

######  Theorem 41 (No-Go Theorem: Idempotence and Units).

Let $\mathbb{S}$ and $\mathbb{T}$ be 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, (S5)b and (T5)a respectively. Then there exists no composite
theory of $\mathbb{T}$ after $\mathbb{S}$.

######  Proof 4.7.

Suppose such a composite theory $\mathbb{U}$ exists. Then we have:

$\displaystyle t(y_{1},y_{2})$ $\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;\text{\ref{ax:sidem}: }s\text{ is
idempotent}\;\right\\}$ $\displaystyle s(t(y_{1},y_{2}),t(y_{1},y_{2}))$
$\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;\text{Substitution}\;\right\\}$ $\displaystyle
s(t(y_{1},y_{2}),x_{0})[t(y_{1},y_{2})/x_{0}]$ $\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;\text{Equation \eqref{theoremeq1} from
Theorem~{}\ref{thm:times-over-plus}}\;\right\\}$ $\displaystyle
t(s(y_{1},x_{0}),s(y_{2},x_{0}))[t(y_{1},y_{2})/x_{0}]$
$\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;\text{Substitution}\;\right\\}$ $\displaystyle
t(s(y_{1},t(y_{1},y_{2})),s(y_{2},t(y_{1},y_{2})))$
$\displaystyle=_{\mathbb{U}}\;$ $\displaystyle\;\;\left\\{\;\text{Equation
\eqref{theoremeq2} from Theorem~{}\ref{thm:times-over-plus}}\;\right\\}$
$\displaystyle
t(t(s(y_{1},y_{1}),s(y_{1},y_{2})),t(s(y_{2},y_{1}),s(y_{2},y_{2})))$
$\displaystyle=_{\mathbb{U}}\;$
$\displaystyle\;\;\left\\{\;\text{\ref{ax:sidem}: }s\text{ is
idempotent}\;\right\\}$ $\displaystyle
t(t(y_{1},s(y_{1},y_{2})),t(s(y_{2},y_{1}),y_{2})).$

From the essential uniqueness property, we may conclude that there are
functions $f:\\{y_{1},y_{2}\\}\mapsto
Z,f^{\prime}:\\{y^{\prime}_{1},y^{\prime}_{2},y^{\prime}_{3},y^{\prime}_{4}\\}\mapsto
Z$ such that:

$\displaystyle t(f(y_{1}),f(y_{2}))$
$\displaystyle=_{\mathbb{T}}t(t(f^{\prime}(y^{\prime}_{1}),f^{\prime}(y^{\prime}_{2})),t(f^{\prime}(y^{\prime}_{3}),f^{\prime}(y^{\prime}_{4}))),$

and $f(y_{i})=f^{\prime}(y^{\prime}_{j})$ if and only if the
$\mathbb{S}$-terms substituted for $y_{i}$ and $y^{\prime}_{j}$ in
$t(y_{1},y_{2})$ and $t(t(y_{1},s(y_{1},y_{2})),t(s(y_{2},y_{1}),y_{2}))$ are
equal. From this we immediately get:

$\displaystyle f(y_{1})$ $\displaystyle=f^{\prime}(y^{\prime}_{1})$
$\displaystyle f(y_{2})$ $\displaystyle=f^{\prime}(y^{\prime}_{4}).$

We know from essential uniqueness that $f(y_{1})\neq f(y_{2})$. We show that
$\\{f^{\prime}(y^{\prime}_{2}),f^{\prime}(y^{\prime}_{3})\\}\subseteq\\{f(y_{1}),f(y_{2})\\}$.
Since we have:

$t(f(y_{1}),f(y_{2}))=_{\mathbb{T}}t(t(f^{\prime}(y^{\prime}_{1}),f^{\prime}(y^{\prime}_{2})),t(f^{\prime}(y^{\prime}_{3}),f^{\prime}(y^{\prime}_{4}))),$

we also have:

$\displaystyle t(f(y_{1}),f(y_{2}))[e_{t}/f(y_{1}),e_{t}/f(y_{2})]$
$\displaystyle=_{\mathbb{T}}t(t(f^{\prime}(y^{\prime}_{1}),f^{\prime}(y^{\prime}_{2})),t(f^{\prime}(y^{\prime}_{3}),f^{\prime}(y^{\prime}_{4})))[e_{t}/f(y_{1}),e_{t}/f(y_{2})]$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{Substitution,
and
}f(y_{1})=f^{\prime}(y^{\prime}_{1}),f(y_{2})=f^{\prime}(y^{\prime}_{4})\;\right\\}$
$\displaystyle
t(e_{t},e_{t})=_{\mathbb{T}}t(t(e_{t},f^{\prime}(y^{\prime}_{2})),t(f^{\prime}(y^{\prime}_{3}),e_{t}))[e_{t}/f(y_{1}),e_{t}/f(y_{2})]$
$\displaystyle\Rightarrow\;$ $\displaystyle\;\;\left\\{\;\text{\ref{ax:tunit}:
}e_{t}\text{ is the unit of }t\;\right\\}$ $\displaystyle
e_{t}=_{\mathbb{T}}t(f^{\prime}(y^{\prime}_{2}),f^{\prime}(y^{\prime}_{3}))[e_{t}/f(y_{1}),e_{t}/f(y_{2})].$

So by (T2),
$\operatorname{var}(t(f^{\prime}(y^{\prime}_{2}),f^{\prime}(y^{\prime}_{3}))[e_{t}/f(y_{1}),e_{t}/f(y_{2})])=\emptyset$.
So we must have:

$\\{f^{\prime}(y^{\prime}_{2}),f^{\prime}(y^{\prime}_{3})\\}\subseteq\\{f(y_{1}),f(y_{2})\\}.$

But then, by the second part of the essential uniqueness property:

$s(y_{1},y_{2})=_{\mathbb{S}}y_{1}\quad\text{or}\quad
s(y_{1},y_{2})=_{\mathbb{S}}y_{2}.$

Both contradict (S2). Therefore, the composite theory $\mathbb{U}$ cannot
exist.

######  Corollary 42.

If monads $S$ and $T$ are presented by algebraic theories $\mathbb{S}$ and
$\mathbb{T}$, satisfying the axioms of Theorem 41, then there does not exist a
distributive law $S\circ T\Rightarrow T\circ S$.

[Powerset Monad Again] The theory of join semilattices satisfies all the
axioms required of both theories in theorem 41. Therefore, there is no
distributive law for the powerset monad over itself. This was already shown by
Klin and Salamanca [13] using similar methods as in Section 3. Theorem 41
gives a second, independent proof of this fact.

######  Remark 43.

Theorems 41 and 26 both require an idempotent term in theory $\mathbb{S}$, and
a unital term in theory $\mathbb{T}$, to preclude a composite theory of
$\mathbb{T}$ after $\mathbb{S}$. However, these theorems are neither
equivalent, nor does one imply the other. The most obvious difference is that
Theorem 26 is stated slightly more general, where instead of a unital term a
generalisation of both unitality and idempotence is required. When restricting
this requirement to just a unital term, there are still differences between
the two theorems: Theorem 26 applies only if the unital term in $\mathbb{T}$
is commutative, whereas Theorem 41 allows this term to be non-commutative.
Conversely, Theorem 41 requires the idempotent term in $\mathbb{S}$ to be
unital, where Theorem 26 does not have this restriction.

######  Non-Example 44 (Multiset Monad: The Sweet Spot).

We come back to the multiset monad. In Non-Example 40 we saw that the
algebraic theory presenting the multiset monad had one extra equation compared
to the theory for the list monad: commutativity. Because of this equation,
property (T5)b did not hold, and therefore Theorem 37 did not apply.

There is a similar relation between the multiset monad and the powerset monad.
Compared to the powerset monad, the theory presenting the multiset monad
_lacks_ just one equation: idempotence, which is exactly what property (S5)b
requires. The lack of this equation in the theory for the multiset monad
therefore means that Theorem 41 does not apply to multiset either. So multiset
holds a sort of ‘sweet spot’ in between the two no-go theorems, where a
distributive law $M\circ M\Rightarrow M\circ M$ still can and does exist.

##  5\. A Conjecture of Beck Yielding More No-Go Theorems

###  5.1. Motivation

The classical example of a distributive law constructs the ring monad from the
list monad $L$, and the Abelian group monad $A$, via a distributive law
$L\circ A\Rightarrow A\circ L$. We encountered this distributive law in
Example 3. It dates back to Beck’s original paper [6], and exploits the
arithmetic distribution of multiplication over addition. A natural question,
briefly considered by Beck, is whether there can be a distributive law $A\circ
L\Rightarrow L\circ A$ with these monads reversed. Beck gives the intuition
that such a distributive law “would have the air of a universal solution to
the problem of factoring polynomials into linear factors”. As such, he
suggests $L\circ A$ “has little chance of being a triple”. Addressing the
question of whether “plus distributes over times” is the motivating example
for the work in this section. Unsurprisingly, Beck’s intuition is correct, and
no such distributive law exists. It turns out that Proposition 28 is key to
the proof.

######  Counterexample 45.

There is no distributive law $A\circ L\Rightarrow L\circ A$ for the Abelian
group monad over the list monad.

######  Proof 5.1.

The theory of Abelian groups $\mathbb{A}$, yielding the Abelian group monad
$A$, has presentation:

  * •

Signature: $\Sigma^{\mathbb{A}}=\\{0^{(0)},-(.)^{(1)},+^{(2)}\\}$.

  * •

Equations: $E^{\mathbb{A}}$ contains the equations stating that $0$ is the
unit of $+$, $+$ is associative and commutative, and $-x$ is the additive
inverse of $x$: $x+(-x)=0$.

The theory of monoids $\mathbb{M}$, yielding the list monad $L$, has
presentation:

  * •

Signature: $\Sigma^{\mathbb{M}}=\\{1^{(0)},*^{(2)}\\}$.

  * •

Equations: $E^{\mathbb{M}}$ contains the equations stating that $1$ is unit of
$*$, and $*$ is associative.

The term $x+y$ in $\mathbb{A}$ satisfies the conditions for $\mathbb{S}$ in
Proposition 28, and $\mathbb{M}$ satisfies the conditions for $\mathbb{T}$. We
conclude that in any composite theory $\mathbb{U}$ of $\mathbb{M}$ after
$\mathbb{A}$, the following equation must hold:

$x+1=_{\mathbb{U}}1.$

We prove that this implies that $x=_{\mathbb{U}}0$:

$\displaystyle x$ $\displaystyle=_{\mathbb{U}}\;\;$
$\displaystyle\;\;\left\\{\;\text{unit}\;\right\\}$ $\displaystyle x+0$
$\displaystyle=_{\mathbb{U}}\;\;$
$\displaystyle\;\;\left\\{\;\text{inverse}\;\right\\}$ $\displaystyle
x+(1+(-1))$ $\displaystyle=_{\mathbb{U}}\;\;$
$\displaystyle\;\;\left\\{\;\text{associativity}\;\right\\}$
$\displaystyle(x+1)+(-1)$ $\displaystyle=_{\mathbb{U}}\;\;$
$\displaystyle\;\;\left\\{\;x+1=_{\mathbb{U}}1\;\right\\}$ $\displaystyle
1+(-1)$ $\displaystyle=_{\mathbb{U}}\;\;$
$\displaystyle\;\;\left\\{\;\text{inverse}\;\right\\}$ $\displaystyle 0.$

Hence for any two variables: $x=_{\mathbb{U}}0=_{\mathbb{U}}y$, which means
any composite theory $U$ is inconsistent. Since the component theories
$\mathbb{M}$ and $\mathbb{A}$ are consistent, Proposition 6 tells us that
there is no such composite theory.

As for the previous proof ideas, this specific negative result can be
abstracted to yield general theorems. We shall address this in the following
section.

###  5.2. Generalization

The well-known _positive_ result of Manes and Mulry [11] about distributive
laws requires monads presented by theories with only linear equations. That
is, with variables appearing exactly once on each side of the equation. These
monads distribute over commutative monads: $linear\circ commutative\Rightarrow
commutative\circ linear$. The careful management of variables has also been
important to the proofs of the _negative_ theorems in Section 3 and Section 4.
Generally these theorems do not apply to theories with inverses such as
groups, as $x-x=0$ means we can make variables appear and disappear almost at
will, leading to behaviour too wild to analyze. The concrete Counterexample 45
_did_ apply to an algebraic theory involving inverses. In fact, it made
essential use of the ability to make variables appear and disappear, turning
this behaviour from a liability into an asset.

We now abstract from Counterexample 45, deducing two general theorems that
require ‘variables to go missing’ in different ways. The first theorem
requires an equation of form $s^{\prime}=e_{\mathbb{S}}$, where
$e_{\mathbb{S}}$ is a constant and $s^{\prime}$ has at least one variable. The
second theorem asks for an equation of form $s^{\prime}=s$, where the term $s$
has a variable that does not appear in $s^{\prime}$, and neither $s$ nor
$s^{\prime}$ are constants.

We begin with the case of a theory with an equation
$s^{\prime}=e_{\mathbb{S}}$. Here, the example to keep in mind is an inverse
axiom such as $x-x=0$, typical of group-like structures, such as groups and
rings. This is the most direct abstraction of the motivating counterexample.

Notice that the proof of Counterexample 45 used associativity. We could have
avoided this by using the following alternative, but less intuitive, reasoning
that applies Proposition 28 twice:

$\displaystyle x$ $\displaystyle=_{\mathbb{U}}\;\;$
$\displaystyle\;\;\left\\{\;\text{unit}\;\right\\}$ $\displaystyle x+0$
$\displaystyle=_{\mathbb{U}}\;\;$
$\displaystyle\;\;\left\\{\;\text{inverse}\;\right\\}$ $\displaystyle
x+(1+(-1))$ $\displaystyle=_{\mathbb{U}}\;\;$
$\displaystyle\;\;\left\\{\;\text{substitution}\;\right\\}$ $\displaystyle
x+(1+y)[-1/y]$ $\displaystyle=_{\mathbb{U}}\;\;$
$\displaystyle\;\;\left\\{\;\text{Proposition~{}\ref{propnary}:
}1+y=_{\mathbb{U}}1\;\right\\}$ $\displaystyle x+1[-1/y]$
$\displaystyle=_{\mathbb{U}}\;\;$ $\displaystyle\;\;\left\\{\;\text{no
variable }y\;\right\\}$ $\displaystyle x+1$ $\displaystyle=_{\mathbb{U}}\;\;$
$\displaystyle\;\;\left\\{\;\text{Proposition~{}\ref{propnary}:
}x+1=_{\mathbb{U}}1\;\right\\}$ $\displaystyle 1.$

This argumentation uses fewer assumptions, so this is the proof we generalize
below.

######  Theorem 46 (No-Go Theorem: Inverse Trouble).

Let $\mathbb{S}$ be an algebraic theory such that:

  1. (S1)

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

  2. (S2)

$\mathbb{S}$ has a term $s$ of arity $\geq 2$ such that $e_{\mathbb{S}}$ is a
unit of $s$, that is, for any variable $x\in\operatorname{var}(s)$:

$s[e_{\mathbb{S}}/y\neq x]=_{\mathbb{S}}x.$

  3. (S3)

$\mathbb{S}$ satisfies an equation of form

$X\vdash s^{\prime}=_{\mathbb{S}}e_{\mathbb{S}},$

with $\operatorname{var}(s^{\prime})\neq\emptyset$, and $s^{\prime}$ can be
written as $s^{\prime\prime}[s_{i}/x_{i}]$, such that
$\operatorname{var}(s^{\prime\prime})\cap\operatorname{var}(s^{\prime})\neq\emptyset$,
and there is a substitution
$f:\operatorname{var}(s^{\prime\prime})\rightarrow\mathbb{S}$ such that for
any $x\in\operatorname{var}(s^{\prime\prime})$:

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

Let $\mathbb{T}$ be an algebraic theory such that:

  1. (T1)

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

  2. (T2)

For all terms $t^{\prime}$ and any 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}}.$

Then there does not exist a composite theory of $\mathbb{T}$ after
$\mathbb{S}$.

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

(S3) is designed to generalize the proof technique illustrated above. We used
the equation $x+(-x)=0$, and the fact that $x+(-x)$ could be written as
$x+y[(-x)/y]$. We then used Proposition 28 on $x+y$. In order for this
argument to work in general, we hence require:

  * •

A term $s^{\prime}$ which is equal to a constant, $x+(-x)$ in the example
above.

  * •

A term $s^{\prime\prime}$ such that $s^{\prime}$ is equal to
$s^{\prime\prime}$ under a certain substitution, $x+y$ in the example.

  * •

Since we want to apply Proposition 28, $s^{\prime\prime}$ needs to satisfy the
conditions for this proposition.

  * •

And lastly we require that $s^{\prime}$ and $s^{\prime\prime}$ share at least
one variable, which is a technicality needed to make the proof go through.

We need axiom (T2) to be able to apply Propositionpropnary. As a reminder, it
reads: “If a variable substitution of term $t$ is provably equal to a
constant, then $t$ is already provably equal to that constant.”

######  Proof 5.2.

Let $\mathbb{U}$ be any (candidate) composite theory of $\mathbb{T}$ after
$\mathbb{S}$. Consider the equation $s^{\prime}=e_{\mathbb{S}}$. We know that
$\mathbb{S}$ has a term $s$ such that $e_{\mathbb{S}}$ is a unit of $s$.
Choose variable $x$ such that $x\notin\operatorname{var}(s^{\prime})$. Then we
use both the unit equation for $s$ and the fact that
$s^{\prime}=e_{\mathbb{S}}$:

$\displaystyle x=_{\mathbb{U}}s[e_{\mathbb{S}}/y\neq x]$
$\displaystyle\Rightarrow\;\;$
$\displaystyle\;\;\left\\{\;e_{\mathbb{S}}=_{\mathbb{S}}s^{\prime}\;\right\\}$
$\displaystyle x=_{\mathbb{U}}s[s^{\prime}/y\neq x].$

Next, we substitute $e_{\mathbb{T}}$ into all variables in $s^{\prime}$. Since
we chose $x$ such that $x\notin\operatorname{var}(s^{\prime})$, this
substitution has no effect on the left hand side of our equation.

$\displaystyle x=_{\mathbb{U}}s[s^{\prime}/y\neq x]$
$\displaystyle\Rightarrow\;\;$
$\displaystyle\;\;\left\\{\;\text{Substitution}\;\right\\}$ $\displaystyle
x[e_{\mathbb{T}}/z\in\operatorname{var}(s^{\prime})]=_{\mathbb{U}}s[s^{\prime}[e_{\mathbb{T}}/z\in\operatorname{var}(s^{\prime})]/y\neq
x]$ $\displaystyle\Rightarrow\;\;$
$\displaystyle\;\;\left\\{\;x\notin\operatorname{var}(s^{\prime})\;\right\\}$
$\displaystyle
x=_{\mathbb{U}}s[s^{\prime}[e_{\mathbb{T}}/z\in\operatorname{var}(s^{\prime})]/y\neq
x].$

We will now work on the term
$s[s^{\prime}[e_{\mathbb{T}}/z\in\operatorname{var}(s^{\prime})]/y\neq x]$.
Recall that $s^{\prime}$ can be written as $s^{\prime\prime}[s_{i}/x_{i}]$ and
$s^{\prime\prime}$ satisfies the conditions for Proposition 28. Also, since
$\operatorname{var}(s^{\prime\prime})\cap\operatorname{var}(s^{\prime})\neq\emptyset$,
we know that the substitution
$s^{\prime}[e_{\mathbb{T}}/z\in\operatorname{var}(s^{\prime})]=_{\mathbb{U}}s^{\prime\prime}[s_{i}/x_{i}][e_{\mathbb{T}}/z\in\operatorname{var}(s^{\prime})]$
yields a term where at least one of the variables of $s^{\prime\prime}$ gets
substituted with $e_{\mathbb{T}}$. Hence by Proposition 28, this resulting
term is equal to $e_{\mathbb{T}}$. Therefore:

$\displaystyle
x=_{\mathbb{U}}s[s^{\prime}[e_{\mathbb{T}}/z\in\operatorname{var}(s^{\prime})]/y\neq
x]$ $\displaystyle\Rightarrow\;\;$ $\displaystyle\;\;\left\\{\;\text{writing
}s^{\prime}\text{ as }s^{\prime\prime}[s_{i}/x_{i}]\;\right\\}$ $\displaystyle
x=_{\mathbb{U}}s[s^{\prime\prime}[s_{i}/x_{i}][e_{\mathbb{T}}/z\in\operatorname{var}(s^{\prime})]/y\neq
x]$ $\displaystyle\Rightarrow\;\;$
$\displaystyle\;\;\left\\{\;\text{Proposition~{}\ref{propnary}:
}s^{\prime\prime}[s_{i}/x_{i}][e_{\mathbb{T}}/z\in\operatorname{var}(s^{\prime})]=_{\mathbb{U}}e_{\mathbb{T}}\;\right\\}$
$\displaystyle x=_{\mathbb{U}}s[e_{\mathbb{T}}/y\neq x]$
$\displaystyle\Rightarrow\;\;$
$\displaystyle\;\;\left\\{\;\text{Proposition~{}\ref{propnary}
again}\;\right\\}$ $\displaystyle x=_{\mathbb{U}}e_{\mathbb{T}}.$

Notice that in the last step, we applied Proposition 28 to $s$ instead of
$s^{\prime\prime}$. We are allowed to do this because $s$ is unital by
assumption (S2), and hence also satisfies Proposition 28.

From the equation $x=_{\mathbb{U}}e_{\mathbb{T}}$, we get by simple variable
substitution that $y=_{\mathbb{U}}e_{\mathbb{T}}$ for any variable $y$, and so
specifically: $x=_{\mathbb{U}}e_{\mathbb{T}}=_{\mathbb{U}}y$. We conclude that
$\mathbb{U}$ is inconsistent. As the original theories are assumed to be
consistent, there is no such composite theory.

In case of Abelian groups and monoids, the equation
$s^{\prime}=e_{\mathbb{S}}$ required from Abelian groups is the inverse
equation $x+(-x)=0$. This equation can be written as $(x+y)[(-x)/y]$. Since
the terms $x+y$ and $x+(-x)$ share the variable $x$, condition (S3) is
satisfied.

There are countless monads satisfying the criteria for $\mathbb{T}$. A few
natural examples are the list, multiset, powerset, and the exception monads.

We have already seen that Abelian groups satisfy the criteria for
$\mathbb{S}$. In addition, any theory with a multiplicative zero $x*0=0$ can
be a good candidate, if the binary operation $*$ is either idempotent or
unital. Rings are an obvious example, but Proposition 28 gives us many more.
The multiset monad satisfies all the criteria for $\mathbb{S}$ and
$\mathbb{T}$ in Proposition 28. We know that there is a distributive law for
the multiset monad over itself, see Example 1, so the unit of one of the
binary operations in the composite theory corresponding to the monad $M\circ
M$ must act as a multiplicative zero for the other.

We can hence make the following table of example compositions Theorem 46
proves impossible via a distributive law:

Table 2. Overview of some distributive laws of type:

row $\circ$ column $\Rightarrow$ column $\circ$ row, which are excluded by
Theorem 46.
List Multiset Powerset Exception Abelian groups $\times$ $\times$ $\times$
$\times$ Rings $\times$ $\times$ $\times$ $\times$ (Multiset)2 $\times$
$\times$ $\times$ $\times$

More examples illustrating the scope of Theorem 46 will be given in Section 6.

The second theorem we find as a generalization of Counterexample 45 focusses
on the equation $s=s^{\prime}$, where $s$ has a variable that does not appear
in $s^{\prime}$. Here the motivating example axioms are absorption laws
$a\wedge(a\vee b)=a$, seen in lattices and similar structures. This is a
slightly less direct abstraction of Counterexample 45, exploiting the
observation that the key requirement is controlled introduction and
elimination of variables.

######  Theorem 48 (No-Go Theorem: Absorption Trouble).

Let $\mathbb{S}$ be an algebraic theory such that:

  1. (S1)

$\mathbb{S}$ satisfies an equation of form $X\vdash
s=_{\mathbb{S}}s^{\prime}$, where
$\operatorname{var}(s)\setminus\operatorname{var}(s^{\prime})\neq\emptyset$
(that is, $s$ has a variable that does not appear in $s^{\prime}$).

  2. (S2)

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.$

  3. (S3)

There is a substitution
$f^{\prime}:\operatorname{var}(s^{\prime})\rightarrow\mathbb{S}$ such that for
any $x\in\operatorname{var}(s^{\prime})$:

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

Let $\mathbb{T}$ be an algebraic theory such that:

  1. (T1)

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

  2. (T2)

For all terms $t^{\prime}$ and any 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}}.$

Then there does not exist a composite theory of $\mathbb{T}$ after
$\mathbb{S}$.

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

Apart from (S1), all the required properties are familiar from Section 4. (S2)
and (S3) are generalizations of idempotence/unitality equations, while (T2)
states that “If a variable substitution of term $t$ is provably equal to a
constant, then $t$ is already provably equal to that constant.”

######  Proof 5.3.

Let $\mathbb{U}$ be any (candidate) composite theory of $\mathbb{T}$ after
$\mathbb{S}$. Consider the equation $s=s^{\prime}$ from the assumptions. Let
$f^{\prime}$ be a substitution of the variables in $s^{\prime}$ such that
$s^{\prime}[f^{\prime}]=_{\mathbb{S}}x$, where
$x\in\operatorname{var}(s^{\prime})$. Then:

$\displaystyle s=_{\mathbb{S}}s^{\prime}$ $\displaystyle\Rightarrow\;\;$
$\displaystyle\;\;\left\\{\;\text{Substitution}\;\right\\}$ $\displaystyle
s[f^{\prime}]=_{\mathbb{S}}s^{\prime}[f^{\prime}]$
$\displaystyle\Rightarrow\;\;$
$\displaystyle\;\;\left\\{\;s^{\prime}[f^{\prime}]=_{\mathbb{S}}x\text{ by
construction of }f^{\prime}\;\right\\}$ $\displaystyle
s[f^{\prime}]=_{\mathbb{S}}x.$

Now let $g$ be the constant substitution
$g:\operatorname{var}(s)\setminus\operatorname{var}(s^{\prime})\rightarrow\\{e_{\mathbb{T}}\\}$,
mapping all the variables that appear in $s$ but not in $s^{\prime}$ to the
constant $e_{\mathbb{T}}$. Since
$\operatorname{var}(s)\setminus\operatorname{var}(s^{\prime})\neq\emptyset$,
at least one instance of $e_{\mathbb{T}}$ will be present in
$s[f^{\prime}][g]$. Then:

$\displaystyle s[f^{\prime}]=_{\mathbb{U}}x$ $\displaystyle\Rightarrow\;\;$
$\displaystyle\;\;\left\\{\;\text{Substitution}\;\right\\}$ $\displaystyle
s[f^{\prime}][g]=_{\mathbb{U}}x[g]$ $\displaystyle\Rightarrow\;\;$
$\displaystyle\;\;\left\\{\;x\in\operatorname{var}(s^{\prime})\text{ and
therefore untouched by }g\;\right\\}$ $\displaystyle
s[f^{\prime}][g]=_{\mathbb{U}}x$ $\displaystyle\Rightarrow\;\;$
$\displaystyle\;\;\left\\{\;\text{Proposition~{}\ref{propnary}, since
}s[f^{\prime}][g]\text{ contains at least one }e_{\mathbb{T}}\;\right\\}$
$\displaystyle e_{\mathbb{T}}=_{\mathbb{U}}x.$

Using substitution, we can hence show that
$x=_{\mathbb{U}}e_{\mathbb{T}}=_{\mathbb{U}}y$, from which it follows that
$\mathbb{U}$ is inconsistent. As the original theories are assumed to be
consistent, there is no such composite theory.

Theorem 48 solves a question Julian Salamanca posed in 2018 [34], asking
whether there is a distributive law $bL\circ P\Rightarrow P\circ bL$,
distributing the bounded lattice monad $bL$ over the powerset monad $P$. The
answer is no.

There is no distributive law for the (bounded) lattice monad over the powerset
monad. The presentation for the bounded lattice monad is given by:

  * •

Signature: $\\{\top^{(0)},\bot^{(0)},\vee^{(2)},\wedge^{(2)}\\}$.

  * •

Equations: $\top$ is the unit of $\wedge$, $\bot$ is the unit of $\vee$,
associativity of $\vee$ and $\wedge$, commutativity of $\vee$ and $\wedge$,
idempotence of $\vee$ and $\wedge$, absorption both ways: $x\vee(x\wedge y)=x$
and $x\wedge(x\vee y)=x$.

We see that the bounded lattice monad satisfies the criteria for $\mathbb{S}$
in Theorem 48:

  * •

The equation $s=s^{\prime}$ is $x\vee(x\wedge y)=x$.

  * •

The substitution $f$ such that $s[f]=x$ uses the unit of $\wedge$ and
idempotence of $\vee$:

$x\vee(x\wedge y)[\top/y]=x\vee(x\wedge\top)=x\vee x=x.$

  * •

The substitution $f^{\prime}$ such that $s^{\prime}[f^{\prime}]=x$ is the
identity, since the term $s^{\prime}$ is just the variable $x$.

The presentation of the powerset monad is given by:

  * •

Signature: $\\{0^{(0)},+^{(2)}\\}$.

  * •

Equations: $0$ is unit of $+$, $+$ is associative, commutative, and
idempotent.

The powerset monad satisfies the criteria for $\mathbb{T}$ in Theorem 48, and
so we conclude that there is no distributive law $bL\circ P\Rightarrow P\circ
bL$.

##  6\. The Boom Hierarchy: a case study for distributive laws

We now pursue a detailed investigation of when distributive laws exist between
some natural families of monads. To do so, we shall combine the techniques
developed in earlier sections with results from the wider literature. Our
objectives are to illustrate that the absence of distributive laws is not at
all unusual, to document many useful examples, and to develop some intuitions
via concrete applications.

We shall begin with the so-called Boom hierarchy, a small family of monads
considered in the functional programming literature [35]. Later, to increase
our available data points, we will expand the original Boom hierarchy to
include more exotic, if slightly less natural, data structures. Similar
expansions of the Boom hierarchy have been studied by Uustalu [20].

The Boom hierarchy is a simple family of four monads, providing a pleasing
connection between commonly used data structures and natural algebraic axioms.
The hierarchy consists of the tree, list, multiset, and powerset monads. Each
of these monads has the same signature, consisting of a constant and a binary
operation. If the only axiom is the unitality axiom, the resulting monad is
the binary tree monad. Adding associativity yields the list monad. Further
adding commutativity yields the multiset monad, and finally adding idempotence
results in the finite powerset monad, as shown in Table 3.

######  Remark 50.

The Boom hierarchy is named after the Dutch Computer Scientist Hendrik Boom.
The fact that ‘Boom’ also means ‘tree’ in Dutch is not entirely coincidental.
Allegedly, the name was coined by Peter Grogono in a meeting with Stephen
Spackman and Hendrik Boom. Spackman was a MSc student co-supervised by Grogono
and Boom, working on this hierarchy of data structures. When Grogono suggested
the name for the hierarchy, Boom’s response was “What, because it is about
trees?”. The name has stuck ever since [36]. Lambert Meertens is the first to
mention this hierarchy in the literature [35], citing an unpublished working
paper by Boom [37].

Table 3. The Boom hierarchy theory | unit | associative | commutative | idempotent
---|---|---|---|---
tree | $\checkmark$ | $\times$ | $\times$ | $\times$
list | $\checkmark$ | $\checkmark$ | $\times$ | $\times$
multiset | $\checkmark$ | $\checkmark$ | $\checkmark$ | $\times$
powerset | $\checkmark$ | $\checkmark$ | $\checkmark$ | $\checkmark$

Studying the patterns of distributive laws in the Boom hierarchy provided some
of the original inspiration for the abstract no-go theorems presented in
earlier sections. We now use the same hierarchy, and generalizations of it, to
demonstrate both their scope and limitations, and their relationship to the
existing positive results we are aware of in the literature.

###  6.1. The Original Boom Hierarchy

For the original Boom hierarchy we have complete knowledge of possible
compositions via distributive laws. An overview is presented in Table 4 below.

The negative result for $P\circ P\Rightarrow P\circ P$ was already shown by
Klin and Salamanca [13], and can also be recovered from both Theorems 14 and
41. The other negative results follow from either Theorem 37 or Theorem 41.
Sometimes both theorems can be applied, for example to preclude a distributive
law $P\circ L\Rightarrow L\circ P$.

The positive results are due to Manes and Mulry. They show that any monad with
only linear equations in its presentation distributes over any commutative
monad333A commutative monad is a strong monad for which the two possible
double strengths coincide [38]. Algebraically, this means that all operations
in the signature commute with one another. This is quite different from the
algebraic property of commutativity that we consider in the Boom hierarchy.
via the times over plus distributivity [11, Theorem 4.3.4]. The multiset and
powerset monad are both commutative, and the theories of the tree, list and
multiset monads all have solely linear equations. This yields the six
distributive laws indicated in the table. Theorem 32 proves that these
distributive laws are in fact the only possible distributive laws for these
monads.

Table 4. Possible compositions in the Boom hierarchy,

with distributive laws of type: row $\circ$ column $\Rightarrow$ column
$\circ$ row.

| tree | list | multiset | powerset
---|---|---|---|---
tree | $\times$ | $\times$ | $\checkmark$ | $\checkmark$
list | $\times$ | $\times$ | $\checkmark$ | $\checkmark$
multiset | $\times$ | $\times$ | $\checkmark$ | $\checkmark$
powerset | $\times$ | $\times$ | $\times$ | $\times$

In this small sample, Manes and Mulry’s theorem is powerful enough to yield
all the possible positive results. However, Table 4 is too small to draw
general conclusions. To extract more information, we expand our hierarchy of
monads in the next section.

###  6.2. The Extended Boom Hierarchy

The original Boom hierarchy discussed in Section 6.1 consisted of a small
number of well motivated data structures. Unfortunately, this small size means
that it provides limited scope for identifying patterns in distributive law
phenomena. To address this, we now consider an extended hierarchy in which all
possible combinations of the original algebraic axioms appear, rather than the
axioms being gradually added in a fixed order. This yields a total of eight
different monads: tree, idempotent tree, commutative tree (mobile),
associative tree (list), idempotent and commutative tree, idempotent and
associative tree (square-free list), associative and commutative tree
(multiset), idempotent commutative and associative tree (powerset). If we
additionally consider the non-empty versions of these monads, corresponding
algebraically to removing the constant from the signature, the number of
monads doubles to sixteen. Of course, some of these monads are less natural
from a functional programming perspective, but they provide a convenient range
of candidates for investigation.

An overview of these monads is given in Table 5 below. We have named the
monads according to the axioms their theories satisfy: $U$(unitality),
$A$(associativity), $C$(commutativity), $I$(idempotence). For example,
multisets are associative and commutative trees with units, so they are
denoted $UAC$ in the table, whereas their non-empty version, which has no
unit, is called $AC$. Note that this convention is unambiguous as we always
impose the unitality axiom when the unit constant is present.

Table 5. The extended Boom hierarchy theory | unital | associative | commutative | idempotent
---|---|---|---|---
non-empty tree | $\times$ | $\times$ | $\times$ | $\times$
I | $\times$ | $\times$ | $\times$ | $\checkmark$
C | $\times$ | $\times$ | $\checkmark$ | $\times$
CI | $\times$ | $\times$ | $\checkmark$ | $\checkmark$
A | $\times$ | $\checkmark$ | $\times$ | $\times$
AI | $\times$ | $\checkmark$ | $\times$ | $\checkmark$
AC | $\times$ | $\checkmark$ | $\checkmark$ | $\times$
ACI | $\times$ | $\checkmark$ | $\checkmark$ | $\checkmark$
U (tree) | $\checkmark$ | $\times$ | $\times$ | $\times$
UI | $\checkmark$ | $\times$ | $\times$ | $\checkmark$
UC (mobile) | $\checkmark$ | $\times$ | $\checkmark$ | $\times$
UCI | $\checkmark$ | $\times$ | $\checkmark$ | $\checkmark$
UA (list) | $\checkmark$ | $\checkmark$ | $\times$ | $\times$
UAI (square-free list) | $\checkmark$ | $\checkmark$ | $\times$ | $\checkmark$
UAC (multiset) | $\checkmark$ | $\checkmark$ | $\checkmark$ | $\times$
UACI (powerset) | $\checkmark$ | $\checkmark$ | $\checkmark$ | $\checkmark$

Within the extended Boom hierarchy, there are a total of 256 monad
compositions to consider. Some distributive laws arise via Manes and Mulry’s
positive general theorems [11, Theorem 4.3.4] and [12, Example 4.9]. Other
combinations are known to have a distributive law because an ad-hoc one has
been found, for example for the non-empty list monad over itself [11, 12]. A
large number of the combinations are proven impossible by theorems from this
paper. Our current knowledge about the existence of distributive laws for this
extended Boom hierarchy is given in Table 6.

Table 6. The extended Boom hierarchy, with laws of type: row $\circ$ column $\Rightarrow$ column $\circ$ row. | $\emptyset$ | I | C | CI | A | AI | AC | ACI | U | UI | UC | UCI | UA | UAI | UAC | UACI
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---
$\emptyset$ | $\checkmark$ | $?$ | $?$ | $?$ | $?$ | $?$ | $\checkmark$ | $\checkmark$ | $?$ | $?$ | $?$ | $?$ | $?$ | $?$ | $\checkmark$ | $\checkmark$
I | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $\times$ | $\times$ | $?$ | $\times$ | $\times$ | $\times$
C | $\checkmark$ | $?$ | $?$ | $?$ | $?$ | $?$ | $\checkmark$ | $\checkmark$ | $?$ | $?$ | $?$ | $?$ | $?$ | $?$ | $\checkmark$ | $\checkmark$
CI | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $\times$ | $\times$ | $?$ | $\times$ | $\times$ | $\times$
A | $\checkmark$ | $?$ | $?$ | $?$ | $\checkmark$ | $?$ | $\checkmark$ | $\checkmark$ | $?$ | $?$ | $?$ | $?$ | $?$ | $?$ | $\checkmark$ | $\checkmark$
AI | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $\times$ | $\times$ | $?$ | $\times$ | $\times$ | $\times$
AC | $\checkmark$ | $?$ | $?$ | $?$ | $?$ | $?$ | $\checkmark$ | $\checkmark$ | $?$ | $?$ | $?$ | $?$ | $?$ | $?$ | $\checkmark$ | $\checkmark$
ACI | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $\times$ | $\times$ | $?$ | $\times$ | $\times$ | $\times$
U | $\checkmark$ | $?$ | $?$ | $?$ | $?$ | $?$ | $\checkmark$ | $\checkmark$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\checkmark$ | $\checkmark$
UI | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$
UC | $\checkmark$ | $?$ | $?$ | $?$ | $?$ | $?$ | $\checkmark$ | $\checkmark$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\checkmark$ | $\checkmark$
UCI | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$
UA | $\checkmark$ | $?$ | $?$ | $?$ | $?$ | $?$ | $\checkmark$ | $\checkmark$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\checkmark$ | $\checkmark$
UAI | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$
UAC | $\checkmark$ | $?$ | $?$ | $?$ | $?$ | $?$ | $\checkmark$ | $\checkmark$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\checkmark$ | $\checkmark$
UACI | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $?$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$

Out of the 256 pairs of monads in Table 6:

  * •

The 41 labelled with $\checkmark$ have a distributive law between them.

  * •

The 122 labelled with $\times$ do not have a distributive law between them.

  * •

The remaining 93 pairs labelled with $?$ remain to be understood.

That is, almost half of the combinations of monads from the extended Boom
hierarchy do not have a distributive law between them. The bottom right corner
of Table 6 is especially striking. Every possible combination is understood,
and 56 out of 64 combinations do not have a distributive law. This provides
further evidence that we should not assume “most” monads will compose via
suitable distributive laws.

An unsurprising pattern that emerges from Table 6 is that the axioms of
idempotence and units are ‘bad’ properties for monad compositions. Since all
of our no-go theorems require at least one of these properties to hold, this
observation does not lead to any new insights.

In the positive results, the most apparent patterns are the columns
$\emptyset$, $AC$, $ACI$, $UAC$, and $UACI$. These are precisely the cases
captured by Manes and Mulry.

For the remaining open cases, we cannot make any meaningful predictions. Our
current techniques in no-go theorems require some way of bringing a term down
to a variable, either via idempotence or via units. Whether this is the key
property that prevents the existence of distributive laws remains an open
question. On the other hand, all general positive results rely on one of the
monads being commutative. The ad-hoc distributive law of the non-empty list
monad over itself clearly indicates that commutativity is not a necessary
condition for distributive laws to exist.

One thing is certain: to systematically fill in the gaps in Table 6 we will
need additional ideas, supporting either further positive, or negative,
theorems. As such, analyzing these hierarchies highlight directions which will
deepen our understanding of distributive laws.

###  6.3. Repeated Compositions

Another way to extend the original Boom hierarchy is to add the monads
resulting from the six distributive laws appearing in Table 4. In order to
study these additional monads, we first give concrete presentations for each
of them:

######  Lemma 51.

The presentations of the composite monads $MT$, $ML$, $MM$, $PT$, $PL$, $PM$
are as follows:

  * •

The composite monad $MT$ is presented by the following theory:

    * –

Signature: $\Sigma^{MT}=\\{0^{(0)},1^{(0)},+^{(2)},*^{(2)}\\}$.

    * –

Equations: $0$ is the unit of $+$, $+$ is associative and commutative, $1$ is
the unit of $*$, $0$ is a multiplicative zero:

$\displaystyle 0*x$ $\displaystyle=0$ (49) $\displaystyle x*0$
$\displaystyle=0,$ (50)

and $*$ distributes over $+$ from both left and right:

$\displaystyle x*(y+z)$ $\displaystyle=(x*y)+(x*z)$ (51)
$\displaystyle(x+y)*z$ $\displaystyle=(x*z)+(y*z).$ (52)

  * •

$ML$ has the same signature and equations as $MT$, with the additional
equation that $*$ is associative.

  * •

$MM$ also has the same signature and equations as $MT$, with $*$ additionally
being associative and commutative.

  * •

$PT$, $PL$, and $PM$ have the same signatures and equations as $MT$, $ML$, and
$MM$ respectively, with one additional equation: $+$ is idempotent.

######  Proof 6.1.

We prove only that the given presentation for the monad $MT$ is correct, the
others follow similarly. From Corollary 10, we know that the composite monad
$MT$ has presentation:

  * •

Signature:
$\Sigma^{MT}=\Sigma^{M}\uplus\Sigma^{T}=\\{0^{(0)},1^{(0)},+^{(2)},*^{(2)}\\}$.

  * •

Equations: $E^{MT}=E^{M}\cup E^{T}\cup E^{\lambda}$ = $\\{0$ is the unit of
$+$, $+$ is associative and commutative$\\}$ $\cup$ $\\{1$ is the unit of
$*\\}$ $\cup$ $\\{s[t_{x}/x]=_{\mathbb{MT}}t[s_{y}/y]\;|\;s,s_{y}$ terms in
$\mathbb{M}$, $t,t_{x}$ terms in $\mathbb{T}\\}$.

So all we need to show is that Equations (49), (50), (51), and (52) are enough
to prove all equations in $E^{\lambda}$, that is, of form
$s[t_{x}/x]=_{\mathbb{MT}}t[s_{y}/y]$.

To prove that all equations in $E^{\lambda}$ are provable from the four given
axioms, it is enough to show that each term of form $s[t_{x}/x]$ is separable
via the given axioms. Essential uniqueness then does the rest: Suppose that
both $s[t_{x}/x]=_{\mathbb{MT}}t[s_{y}/y]$ and
$s[t_{x}/x]=_{\mathbb{MT}}t^{\prime}[s^{\prime}_{y^{\prime}}/{y^{\prime}}]$
are in $E^{\lambda}$, and the first of these equations is provable using
Equations (49), (50), (51), and (52). Then by transitivity of
$=_{\mathbb{MT}}$ we know
$t^{\prime}[s^{\prime}_{y^{\prime}}/{y^{\prime}}]=_{\mathbb{MT}}t[s_{y}/y]$.
Since this is an equality between two separated terms, essential uniqueness
gives us that it is provable using just the axioms in $E^{M}$ and $E^{T}$. So
once we have derived one equation in $E^{\lambda}$ involving a particular term
$s[t_{x}/x]$, we automatically gain all equations in $E^{\lambda}$ involving
this term.

To prove that every term of form $s[t_{x}/x]$ is separable using just the
axioms Equations (49), (50), (51), and (52), we use induction on the term
complexity of $s$:

Base cases: $s$ is a constant or a variable. In these cases $s[t_{x}/x]$ is
already separated. Induction step: Suppose that $s=s_{1}*s_{2}$, and assume
that $s_{1}[t_{x}/x]$ and $s_{2}[t_{x}/x]$ are both separable using the four
equations described above. Then we need to show that $s[t_{x}/x]$ is
separable. Let $t^{\prime}_{1}[s^{\prime}_{y^{\prime}}/y^{\prime}]$ and
$t^{\prime}_{2}[s^{\prime}_{y^{\prime}}/y^{\prime}]$ be the terms resulting
from separating $s_{1}$ and $s_{2}$ respectively. We need induction on both
$t^{\prime}_{1}$ and $t^{\prime}_{2}$:

  * •

If $t^{\prime}_{1}$ is a constant, $t^{\prime}_{1}=0$, then by Equation (49):
$s[t_{x}/x]=0*s_{2}=0$, and hence $s[t_{x}/x]$ is separable.

  * •

If $t^{\prime}_{1}$ is a variable, $t^{\prime}_{1}=x_{1}$, we use induction
$t^{\prime}_{2}$:

    * –

If $t^{\prime}_{2}$ is a constant, then by Equation (50):
$s[t_{x}/x]=s_{1}*0=0$, and hence $s[t_{x}/x]$ is separable.

    * –

If $t^{\prime}_{2}$ is a variable, $t^{\prime}_{2}=x_{2}$, then
$s[t_{x}/x]=x_{1}*x_{2}$, which is a separated term.

    * –

If $t^{\prime}_{2}$ is term of form $t^{\prime}_{3}+t^{\prime}_{4}$, and we
assume (induction hypothesis) that $x_{1}*t^{\prime}_{3}$ is separable and
$x_{1}*t^{\prime}_{4}$ is separable, then
$s[t_{x}/x]=x_{1}*(t^{\prime}_{3}+t^{\prime}_{4})$. By Equation (51), we can
write:

$\displaystyle s[t_{x}/x]$ $\displaystyle=\;$ $\displaystyle
x_{1}*(t^{\prime}_{3}+t^{\prime}_{4})$ $\displaystyle=\;$
$\displaystyle(x_{1}*t^{\prime}_{3})+(x_{1}*t^{\prime}_{4}).$

Since both $(x_{1}*t^{\prime}_{3})$ and $(x_{1}*t^{\prime}_{4})$ are
separable, this shows that $s[t_{x}/x]$ is separable.

  * •

If $t^{\prime}_{1}$ is a term of form $t^{\prime}_{5}+t^{\prime}_{6}$, we may
assume (induction hypothesis) that $t^{\prime}_{5}*t^{\prime}_{2}$ and
$t^{\prime}_{6}*t^{\prime}_{2}$ are separable. By Equation (52), we know:

$\displaystyle s[t_{x}/x]$ $\displaystyle=\;$
$\displaystyle(t^{\prime}_{5}+t^{\prime}_{6})*t^{\prime}_{2}$
$\displaystyle=\;$
$\displaystyle(t^{\prime}_{5}*t^{\prime}_{2})+(t^{\prime}_{6}*t^{\prime}_{2}).$

Since both $(t^{\prime}_{5}*t^{\prime}_{2})$ and
$(t^{\prime}_{6}*t^{\prime}_{2})$ are separable, this shows that $s[t_{x}/x]$
is separable.

We conclude that the given presentation is indeed a presentation for the monad
$MT$.

Checking these presentations against the various no-go theorems presented in
this paper yields a new table of possible compositions, displayed in Table 7.
Other than the six combinations we already discovered in the original Boom
hierarchy, we find no new combinations of monads that compose via a
distributive law. The results shown in the columns of the composite monads
$MT,ML,MM,PT,PL,PM$ are covered by Theorem 30, while the rows with any of
these composite monads are covered by Theorem 46.

Table 7. Possible compositions in the Boom hierarchy,

with distributive laws of type: row $\circ$ column $\Rightarrow$ column
$\circ$ row.
tree list multiset powerset MT ML MM PT PL PM tree $\times$ $\times$
$\checkmark$ $\checkmark$ $\times$ $\times$ $\times$ $\times$ $\times$
$\times$ list $\times$ $\times$ $\checkmark$ $\checkmark$ $\times$ $\times$
$\times$ $\times$ $\times$ $\times$ multiset $\times$ $\times$ $\checkmark$
$\checkmark$ $\times$ $\times$ $\times$ $\times$ $\times$ $\times$ powerset
$\times$ $\times$ $\times$ $\times$ $\times$ $\times$ $\times$ $\times$
$\times$ $\times$ MT $\times$ $\times$ $\times$ $\times$ $\times$ $\times$
$\times$ $\times$ $\times$ $\times$ ML $\times$ $\times$ $\times$ $\times$
$\times$ $\times$ $\times$ $\times$ $\times$ $\times$ MM $\times$ $\times$
$\times$ $\times$ $\times$ $\times$ $\times$ $\times$ $\times$ $\times$ PT
$\times$ $\times$ $\times$ $\times$ $\times$ $\times$ $\times$ $\times$
$\times$ $\times$ PL $\times$ $\times$ $\times$ $\times$ $\times$ $\times$
$\times$ $\times$ $\times$ $\times$ PM $\times$ $\times$ $\times$ $\times$
$\times$ $\times$ $\times$ $\times$ $\times$ $\times$

##  7\. Conclusion

We have shown there can be no distributive law between large classes of
monads:

  * •

Section 3 developed general theorems for demonstrating when distributive laws
cannot exist, derived from a classical counterexample of Plotkin, making
essential use of idempotence axioms.

  * •

Section 4 introduced novel ideas, exploiting unitality axioms, yielding
counterexamples beyond those possible in Section 3.

  * •

Section 5 developed a third family of no-go theorems, motivated by a question
of Beck. Here the ability to “make variables disappear” in terms is central,
such as in inverse and absorption axioms.

Our results cover many naturally occurring combinations of monads, including
all previously known negative results. They also identify issues in the
existing literature, resolve the open question of whether the list monad
distributes over itself, and confirm a negative conjecture of Beck.

We strongly advocated the use of algebraic methods. These techniques were used
for all of our proofs. Taking this approach, rather than direct calculations
involving Beck’s axioms, enabled us to single out the essentials of each
proof, so that the resulting theorems could be stated in full generality.

Lastly, we would like to emphasize that the methods described in this paper
are of broader application, beyond our specific theorems. For example, Julian
Salamanca found that there is no distributive law of the group monad over the
powerset monad $G\circ P\Rightarrow P\circ G$ [34], before we formulated
Theorem 46. Although elements of his proof are very similar to those used in
section Section 3, the proof itself uses further ideas outside the scope of
our theorems.

###  7.1. Summary of Axioms and Theorems

Our theorems use a range of different properties of algebraic theories. To aid
navigation, we conclude with a summary of the properties that we exploit, and
which theorems exploit them.

Our theorems typically require the existence of a special term with multiple
properties, such as a binary term that is both idempotent and commutative.
Below we list all these properties separately. Table 8 then specifies which
theorems require which properties to hold simultaneously for a single term.
Note that some properties, such as Ax15, seem trivial on their own, but in
conjunction with other properties we require of the special term in our
theorems they are no longer trivial and must be stated as a requirement.

In addition, our theorems require certain properties to hold for the theories
in question, such as the existence of a constant in the theory, or conditions
that must hold for all terms in the theory, such as _“if a term is equal to a
constant, then it cannot have any variables”_. In the list below, we split the
properties into those that must hold for one special term, and those that must
hold for the theory.

  * Properties of terms:

    * $\bullet$

There is a binary term $\phi$ such that:

      1. Ax1

$\phi$ is idempotent:

$\\{x\\}\vdash\phi(x,x)=x$

      2. Ax2

$\phi$ has a unit:

$\\{x\\}\vdash\phi(x,e)=x=\phi(e,x)$

      3. Ax3

There is a substitution $f$ of terms for variables such that $\phi[f]$ is
equal to a variable:

$\exists f~{}s.t.~{}\Gamma\vdash\phi[f]=x$

      4. Ax4

$\phi$ is commutative:

$\\{x,y\\}\vdash\phi(x,y)=\phi(y,x)$

      5. Ax5

$\phi$ does not satisfy the abides equation:

$\left(\Gamma\vdash\phi(\phi(x,y),\phi(z,w))=\phi(\phi(x,z),\phi(y,w))\right)\;\;\Rightarrow\;\;\\#\\{x,y,z,w\\}\leq
3$

      6. Ax6

Any term provably equal to $\phi$ has at most two variables:

$\forall\phi^{\prime}:(\Gamma\vdash\phi(x,y)=\phi^{\prime})\;\;\Rightarrow\;\;\\{x,y\\}\vdash\phi^{\prime}$

      7. Ax7

Any term provably equal to $\phi$ has at least one variable:

$\forall\phi^{\prime}:(\Gamma\vdash\phi(x,y)=\phi^{\prime})\;\;\Rightarrow\;\;\neg(\emptyset\vdash\phi^{\prime})$

      8. Ax8

Any term provably equal to $\phi$ has at least two variables:

$\forall\phi^{\prime}:(\Gamma\vdash\phi(x,y)=\phi^{\prime})\;\;\Rightarrow\;\;\neg(\\{x\\}\vdash\phi^{\prime}\;\vee\;\\{y\\}\vdash\phi^{\prime})$

    * $\bullet$

There is an $n$-ary term $\phi$ ($n\geq 2$) such that:

      1. Ax9

$\phi$ is idempotent:

$\\{x\\}\vdash\phi[x/x_{i}]=x$

      2. Ax10

$\phi$ has a unit:

$\\{x_{i}\\}\vdash\phi[e/x_{j\neq i}]=x_{i}$

      3. Ax11

There is a substitution $f$ of terms for variables such that $\phi[f]$ is
equal to a variable:

$\exists f~{}s.t.~{}\Gamma\vdash\phi[f]=x$

      4. Ax12

$\phi$ is stable under a fixed-point free permutation $\sigma$ of its
variables:

$\Gamma\vdash\phi=\phi[\sigma]$

      5. Ax13

Any term provably equal to $\phi$ has at most $n$ variables:

$\forall\phi^{\prime}:(\Gamma\vdash\phi(x_{1},\ldots,x_{n})=\phi^{\prime})\;\;\Rightarrow\;\;\\{x_{1},\ldots,x_{n}\\}\vdash\phi^{\prime}$

      6. Ax14

Any term provably equal to $\phi$ has at least two variables:

$\forall\phi^{\prime}:(\Gamma\vdash\phi=\phi^{\prime})\;\;\Rightarrow\;\;\neg(\bigvee_{x\in\Gamma}\\{x\\}\vdash\phi^{\prime})$

    * $\bullet$

There is an $n$-ary term $\phi$ ($n\geq 1$) such that:

      1. Ax15

There is a substitution $f$ of terms for variables such that $\phi[f]$ is
equal to a variable:

$\exists f~{}s.t.~{}\Gamma\vdash\phi[f]=x$

      2. Ax16

$\phi$ can be written as $\phi^{\prime}[\phi^{\prime\prime}_{i}/x_{i}]$, such
that $\phi$ and $\phi^{\prime}$ share at least one variable, and Ax15 holds
for $\phi^{\prime}$.

      3. Ax17

$\phi$ is provably equal to a constant, but contains at least one variable:

$\exists e~{}s.t.~{}(\emptyset\vdash
e)\;\wedge\;(e=\phi)\;\wedge\;\neg(\emptyset\vdash\phi)$

      4. Ax18

There is a term $\phi^{\prime}$ that is provably equal to $\phi$, and $\phi$
contains a variable that $\phi^{\prime}$ does not have. Moreover,
$\phi^{\prime}$ satisfies Ax15.

$\exists\phi^{\prime}~{}s.t.~{}(\Gamma\vdash\phi=\phi^{\prime})\;\wedge\;\operatorname{var}(\phi)\setminus\operatorname{var}(\phi^{\prime})\neq\emptyset$

  * Properties of theories:

    * $\bullet$

The algebraic theory in question must satisfy:

      1. Ax19

For all terms $\phi$ of arity $\geq 1$ there is a substitution $f$ of terms
for variables such that $\phi[f]$ is equal to a variable:

$\forall\phi~{}\exists f~{}s.t.~{}\Gamma\vdash\phi[f]=x$

      2. Ax20

There exists a constant term in the theory. That is, there is a term that has
no variables.

$\exists e~{}s.t.~{}\emptyset\vdash e$

      3. Ax21

There are at least two constants.

      4. Ax22

If any variable substitution of a term is equal to a constant, then that term
itself is equal to a constant:

$\forall\phi,e:(\exists f~{}s.t.~{}\phi[f]=e)\;\;\Rightarrow\;\;\phi=e$

      5. Ax23

If a term is provably equal to a constant, then it does not have any
variables:

$\forall\phi,e:(\emptyset\vdash e\wedge
e=\phi)\;\;\Rightarrow\;\;\emptyset\vdash\phi$

      6. Ax24

If a term is provably equal to a variable, then that variable is the only
variable appearing in the term:

$\forall\phi,x:(\Gamma\vdash\phi=x)\;\;\Rightarrow\;\;\\{x\\}\vdash\phi$

An overview of our theorems and which axioms they use is presented in Table 8.
We advise to use this table only as a quick reference, and to always check the
precise statements of the theorems before drawing any conclusions about
specific monads.

Table 8. Theorems and axioms appearing in this paper. Theorem | Axioms for $S$ | Axioms for $T$
---|---|---
Theorem 14 (first Plotkin generalisation) |  Ax1, Ax8, Ax24 |  Ax1, Ax4, Ax6
Theorem 19 (n-ary version) |  Ax1, Ax14, Ax24 |  Ax9, Ax12, Ax13
Theorem 21 (no commutativity) |  Ax1, Ax8, Ax24 |  Ax1, Ax6, Ax7, Ax24
Theorem 26 (generalising idempotence) |  Ax1, Ax8, Ax24 |  Ax3, Ax4, Ax6
Theorem 30 (too many constants) | Ax11 |  Ax21, Ax22
Theorem 32 (times over plus) |  Ax2, Ax19, Ax23, Ax24 |  Ax2, Ax23, Ax24
Theorem 37 (lacking abides) |  Ax2, Ax19, Ax23, Ax24 |  Ax2, Ax5, Ax23, Ax24
Theorem 41 (idempotence and units) |  Ax1, Ax2, Ax19, Ax23, Ax24 |  Ax2, Ax23, Ax24
Theorem 46 (inverse trouble) |  Ax10, Ax16, Ax17 |  Ax20, Ax22
Theorem 48 (absorption trouble) |  Ax15, Ax18 |  Ax20, Ax22

## Acknowledgements

We are very grateful to Jeremy Gibbons, Bartek Klin, Hector Miller-Bakewell,
Julian Salamanca and our reviewers for their insightful feedback on earlier
versions of this paper. We also would like to thank Prakash Panangaden,
Fredrik Dahlqvist, Louis Parlant, Sam Staton, Ohad Kammar, Jules Hedges, and
Ralf Hinze for inspiring discussions, which all had a positive influence on
this paper.

This work was partially supported by Institute for Information &
communications Technology Promotion(IITP) grant funded by the Korea
government(MSIT) (No.2015-0-00565, Development of Vulnerability Discovery
Technologies for IoT Software Security).

## References

  * [1] M. Zwart and D. Marsden, “No-go theorems for distributive laws,” in _34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019_. IEEE, 2019, pp. 1–13. [Online]. Available: https://ieeexplore.ieee.org/xpl/conhome/8765678/proceeding
  * [2] E. Moggi, “Notions of computation and monads,” _Information and Computation_ , vol. 93, no. 1, pp. 55 – 92, 1991, selections from 1989 IEEE Symposium on Logic in Computer Science.
  * [3] P. Wadler, “Monads for functional programming,” in _Advanced Functional Programming_ , J. Jeuring and E. Meijer, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 1995, pp. 24–52.
  * [4] S. Peyton Jones, _Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell_. Amsterdam: IOS press, 2001, pp. 47–96.
  * [5] P. Hudak, S. Peyton Jones, P. Wadler, B. Boutel, J. Fairbairn, J. Fasel, M. M. Guzmán, K. Hammond, J. Hughes, T. Johnsson _et al._ , “Report on the programming language Haskell: a non-strict, purely functional language version 1.2,” _ACM SigPlan notices_ , vol. 27, no. 5, pp. 1–164, 1992.
  * [6] J. Beck, “Distributive laws,” in _Seminar on Triples and Categorical Homology Theory_ , B. Eckmann, Ed. Springer Berlin Heidelberg, 1969, pp. 119–140.
  * [7] M. Lenisa, J. Power, and H. Watanabe, “Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads,” _Electronic Notes in Theoretical Computer Science_ , vol. 33, pp. 230–260, 2000.
  * [8] M. M. Bonsangue, H. H. Hansen, A. Kurz, and J. Rot, “Presenting distributive laws,” in _Algebra and Coalgebra in Computer Science_ , R. Heckel and S. Milius, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 95–109.
  * [9] B. Jacobs, “Semantics of weakening and contraction,” _Annals of Pure and Applied Logic_ , vol. 69, pp. 73–106, 1994.
  * [10] F. Dahlqvist, L. Parlant, and A. Silva, “Layer by layer - combining monads,” in _Theoretical Aspects of Computing - ICTAC 2018 - 15th International Colloquium, Stellenbosch, South Africa, October 16-19, 2018, Proceedings_ , ser. Lecture Notes in Computer Science, B. Fischer and T. Uustalu, Eds., vol. 11187\. Springer, 2018, pp. 153–172. [Online]. Available: https://doi.org/10.1007/978-3-030-02508-3_9
  * [11] E. Manes and P. Mulry, “Monad compositions I: general constructions and recursive distributive laws,” _Theory and Applications of Categories_ , vol. 18, pp. 172–208, 04 2007.
  * [12] ——, “Monad compositions II: Kleisli strength,” _Mathematical Structures in Computer Science_ , vol. 18, no. 3, p. 613–643, 2008.
  * [13] B. Klin and J. Salamanca, “Iterated covariant powerset is not a monad,” in _Proceedings 34th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2018_ , 2018.
  * [14] D. Varacca and G. Winskel, “Distributing probability over non-determinism,” _Mathematical Structures in Computer Science_ , vol. 16, no. 1, pp. 87–113, 2006.
  * [15] F. Dahlqvist and R. Neves, “Compositional semantics for new paradigms: Probabilistic, hybrid and beyond,” _CoRR_ , vol. abs/1804.04145, 2018. [Online]. Available: http://arxiv.org/abs/1804.04145
  * [16] D. J. King and P. Wadler, “Combining monads,” in _Functional Programming, Glasgow 1992_. Springer, 1993, pp. 134–143.
  * [17] M. Piróg and S. Staton, “Backtracking with cut via a distributive law and left-zero monoids,” _Journal of Functional Programming_ , vol. 27, 2017.
  * [18] E. Cheng, “Distributive laws for Lawvere theories,” _CoRR_ , vol. abs/1112.3076v2, 2011. [Online]. Available: https://arxiv.org/abs/1112.3076v2
  * [19] R. Bird, _Lectures on Constructive Functional Programming_. Oxford University Computing Laboratory Programming Research Group, 1988.
  * [20] T. Uustalu, “A divertimento on monadplus and nondeterminism,” _Journal of Logical and Algebraic Methods in Programming_ , vol. 85, no. 5, Part 2, pp. 1086 – 1094, 2016.
  * [21] F. E. Linton, “Some aspects of equational categories,” in _Proceedings of the Conference on Categorical Algebra_. Springer, 1966, pp. 84–94.
  * [22] F. W. Lawvere, “Functorial semantics of algebraic theories,” _Proceedings of the National Academy of Sciences of the United States of America_ , vol. 50, no. 5, pp. 869–872, 1963.
  * [23] E. G. Manes, _Algebraic theories_. Springer, 1976, vol. 26.
  * [24] G. Plotkin and J. Power, “Notions of computation determine monads,” in _International Conference on Foundations of Software Science and Computation Structures_. Springer, 2002, pp. 342–356.
  * [25] B. Jacobs, “Convexity, duality and effects,” in _IFIP International Conference on Theoretical Computer Science_. Springer, 2010, pp. 1–19.
  * [26] M. H. Stone, “Postulates for the barycentric calculus,” _Annali di Matematica Pura ed Applicata_ , vol. 29, no. 1, pp. 25–30, 1949.
  * [27] S. Lack, “Composing props,” _Theory and Applications of Categories_ , vol. 12, no. 9, pp. 147–163, 2004.
  * [28] F. Zanasi, “Interacting hopf algebras, the theory of linear systems,” Ph.D. dissertation, Laboratoire de l’Informatique du Parallélisme, École Doctorale en Informatique et Mathématiques de Lyon, Université de Lyon, 2015\.
  * [29] M. Zwart, “On the non-compositionality of distributive laws,” Ph.D. dissertation, Department of Computer Science, University of Oxford, 2020.
  * [30] D. Varacca, “Probability, nondeterminism and concurrency: Two denotational models for probabilistic computation,” Ph.D. dissertation, BRICS, Department of Computer Science, University of Aarhus, November 2003.
  * [31] P. Panangaden, “Private communication,” 2018.
  * [32] E. Cheng, “Iterated distributive laws,” in _Mathematical Proceedings of the Cambridge Philosophical Society_ , vol. 150, no. 3. Cambridge University Press, 2011, pp. 459–487.
  * [33] M. P. Jones and L. Duponcheel, “Composing monads,” Technical Report YALEU/DCS/RR-1004, Department of Computer Science. Yale …, Tech. Rep., 1993\.
  * [34] J. Salamanca, “Private communication,” 2018.
  * [35] L. Meertens, “Algorithmics, towards programming as a mathematical activity,” in _Mathematics and Computer Science: Proceedings of the CWI Symposium, November 1983_ , ser. CWI monographs, J. De Bakker, M. Hazewinkel, and J. Lenstra, Eds. North-Holland, 1986, pp. 289–334.
  * [36] S. Spackman, “private communication,” 2019.
  * [37] H. J. Boom, “Further thoughts on abstracto.”
  * [38] A. Kock, “Monads on symmetric monoidal closed categories,” _Archiv der Mathematik_ , vol. 21, no. 1, pp. 1–10, 1970.


# Point Cloud Resampling Through Hypergraph Signal Processing

###### Abstract

Three-dimensional (3D) point clouds serve as an important data representation
for visualization applications. The rapidly growing utility and popularity of
point cloud processing strongly motivate a plethora of research activities on
large-scale point cloud processing and feature extraction. In this work, we
investigate point cloud resampling based on hypergraph signal processing
(HGSP). We develop a novel method to extract sharp object features and reduce
the size of point cloud representation. By directly estimating hypergraph
spectrum based on hypergraph stationary processing, we design a spectral
kernel-based filter to capture high-dimensional interactions among the signal
nodes of point clouds and to better preserve their surface outlines.
Experimental results validate the effectiveness of hypergraph in representing
point clouds, and demonstrate the robustness of the proposed resampling method
in noisy environment.

Index Terms—  Hypergraph signal processing, compression, point cloud
resampling, virtual reality.

##  1 Introduction

Given the broad deployment of networked sensors and cameras, 3D point clouds
provide efficient data representation of external surfaces for complicated
objects and their surroundings. Point clouds have found wide applications in
recent years, including surface reconstruction [1], rendering [2] and feature
extraction [3]. High data volume of point cloud representation poses
challenges to data transmission and storage. One of the important point cloud
processing tasks involves resampling aimed at reducing the number of points in
a point cloud while preserving vital 3D structural features. Point cloud
resampling can be an important practical tool in applications such as
segmentation, object classification, and data compression.

The literature contains a variety of works on different aspects of point cloud
resampling. A centroidal Voronoi tessellation based method in [4] can
progressively generate high-quality resampling results with isotropic or
anisotropic distributions from a given point cloud. The authors of [5]
developed a 3D downsampling technique based on a growing neural gas network,
to deal with outliers in the input data and to represent 3D spaces by an
induced Delaunay triangulation of the input space. In particular, graph-based
resampling has exhibited desirable capability to capture the underlying
structures of point clouds [6, 7]. For example, the work [8] focused on
computationally efficient resampling and proposed several graph-based filters
to capture the distribution of point data. Another graph-based example is a
graph-based contour-enhanced resampling method presented by [9]. We also note
a different, feature-based, approach to point cloud resampling based on edge
detection and feature extraction. In [10], the authors presented a sharp
feature detector using Gaussian map clustering on local neighborhoods.
Bazazian and co-authors [11] extended this principle by leveraging principal
component analysis (PCA) to develop a new agglomerative clustering method.
This work improved the speed and accuracy by analyzing the eigenvalues of
covariance matrix defined by $k-$nearest neighbors.

Despite the aforementioned successes, graph-based and feature-based resampling
methods still exhibit some limitations. For graph-based methods, each graph
edge can only model pairwise relationships even though multilateral
interactions of point data represent highly informative characteristics of 3D
objects. For example, bilateral connections cannot represent multilateral
relationship among points on the same surface directly since each surface
covers more than two points. Another open issue is the efficient construction
of a graph for an arbitrary point cloud. Among feature-based methods, how to
select adequate features and filter parameters remains a challenge. How to
develop a general model with robust parameter selection remains an open
problem.

Some recent works have successfully applied hypergraphs to model and
characterize the multilateral interactions among multimedia data points [12].
Hypergraph consists of nodes and hyperedges. Since each hyperedge can include
more than two nodes, hypergraph provides a more general representation of
point clouds to model multilateral point relationships on object surfaces.
Furthermore, by generalizing graph signal processing (GSP) [13], hypergraph
signal processing (HGSP) [14, 15] has demonstrated notable successes in
processing point clouds for segmentation, sampling, and denoising [16, 17].

In this paper, we propose a novel 3D point cloud resampling method using
kernel filtering based on hypergraph signal processing. Based on hypergraph
stationary process, we first estimate hypergraph kernel basis for point cloud.
We define a local smoothness with respect to high-pass filtering in the
spectral domain for resampling. In order to test the model preserving property
on complex models, we apply a simple method for point cloud recovery based on
alpha complex and Poisson sampling. We then present experimental results to
demonstrate the compression efficiency and robustness of our proposed point-
cloud resampling method.

##  2 Background

###  2.1 Point Cloud

A point cloud is a collection of positions in 3D space. In point clouds, each
point consists of its 3D coordinates and may contain additional features, such
as colors and normals [18]. In this work, we focus on the coordinates of these
points when resampling the point clouds. These point coordinates are
represented by the location matrix
$\mathbf{p}=[\mathbf{p}_{1}^{T}\cdots\mathbf{p}_{N}^{T}]^{T}$, where $N$ is
the number of points in the point cloud and $\mathbf{p}_{i}$ is the 3D
coordinates of the $i$-th point.

###  2.2 Hypergraph Signal Processing

Hypergraph signal processing (HGSP) is a framework based on the tensor
representation of hypergraphs to capture high-order signal interactions [14].
In this framework, an $M$th-order $N$-dimensional representing tensor
$A=(a_{i_{1}i_{2}\cdots i_{M}})\in\mathbb{R}^{N^{M}}$represents a hypergraph
with $N$ vertices with hyperedges capable of connecting at most $M$ nodes.
Weights of hyperedges connecting fewer than $M$ nodes are normalized according
to combinations and permutations [19].

Orthogonal CANDECOMP/PARAFAC (CP) decomposition enables the (approximate)
decomposition of a representing tensor into

$\mathbf{A}\approx\sum_{r=1}^{N}\lambda_{r}\cdot\underbrace{\mathbf{f}_{r}\circ\ldots\circ\mathbf{f}_{r}}_{M\text{
times}},\vspace*{-3mm}$

where $\circ$ denotes tensor outer product,
$\\{\mathbf{f}_{1},\cdots,\mathbf{f}_{N}\\}$ are orthonormal basis to
represent spectrum components, and $\lambda_{r}$ is corresponding frequency
coefficient. Spectrum components {$\mathbf{f}_{1},\cdots,\mathbf{f}_{N}$} form
the full hypergraph spectral space. Other HGSP concepts, such as filtering,
hypergraph Fourier transform, and sampling theory can be defined as in [14].

##  3 HGSP Point Cloud Resampling

In this section, we introduce our kernel-based resampling method. Generally,
our proposed method consists of three main steps: i) hypergraph spectrum
construction, ii) Fourier transform, iii) high-pass filtering and resampling.

We first estimate the hypergraph spectrum based on hypergraph stationary
process. Shown in [17], a stochastic signal $\mathbf{x}$ is weak-sense
stationary if and only if it has zero-mean and its covariance matrix has the
same eigenvectors as the hypergraph spectrum basis, i.e.,
$\mathbb{E}[\mathbf{x}]=\mathbf{0}$ and
$\mathbb{E}[\mathbf{x}\mathbf{x}^{H}]=\mathbf{V}\Sigma_{\mathbf{x}}\mathbf{V}^{H},$
where $\mathbf{V}$ is the hypergraph spectrum. Since the three coordinates can
be viewed as three observations of points from different projection
directions, we can estimate the hypergraph spectrum from the covariance matrix
of three coordinates by assuming the signals to be stationary. Here, we use
the same spectrum estimation strategy as [17], and consider the adjacency
tensor as a third-order tensor which is the minimal number of nodes to form a
surface.

We define a $k\times k\times k$ 3D cube as the kernel to define the local
signal $\mathbf{s}_{i}$. For simplicity, we use a $3\times 3\times 3$ 3D cube
as the kernel in this paper, although larger kernel can be used to facilitate
flexibility in filter design at the cost of computational complexity. Let $d$
be the center distance between two nearby voxels in the kernel. A proper
selection of $d$ should allow $\mathbf{s}_{i}$ to capture local geometric
information. If $d$ is too small, only a few neighbors of the $i$-th point are
included in the $\mathbf{s}_{i}$, leading to noise-sensitivity. If $d$ is too
large, many neighbors are included in each voxel, which may lead to blurred
local geometric information. A typical choice of $d$ is the intrinsic
resolution of a point cloud.

Let $\mathbf{s}=[\mathbf{X_{1}}\ \mathbf{X_{2}}\
\mathbf{X_{3}}]\in\mathbb{R}^{N_{k}\times 3}$ be the coordinates of the total
$N_{k}$ voxel centers in the kernel. For our selected $3\times 3\times 3$
kernel, $N_{k}=27$. We then normalize the coordinates $\mathbf{s}$ to define a
zero mean signal $\mathbf{s^{\prime}}$. By calculating eigenvectors
$\mathbf{f}_{1},\cdots,\mathbf{f}_{N_{k}}$ for
$R_{\mathbf{s^{\prime}}}=\mathbf{s^{\prime}}\mathbf{s^{\prime}}^{T}$, we can
obtain the estimated hypergraph spectrum
$\mathbf{V}=[\mathbf{f}_{1},\cdots,\mathbf{f}_{N_{k}}]$.

Algorithm 1 Hypergraph Kernel-based Resampling

Input: A 3D point clouds with $N$ nodes characterized by its coordinates
$\mathbf{p}=[\mathbf{p}_{1}^{T}\cdots\mathbf{p}_{N}^{T}]^{T}$ of the point
cloud, resampling ratio $\alpha$.

1. Calculate the intrinsic resolution of point cloud;

2. Use the intrinsic resolution as $d$ to get the coordinates $\mathbf{s}=[\mathbf{X_{1}}\ \mathbf{X_{2}}\ \mathbf{X_{3}}]$ of voxel centers in the kernel;

3. Calculate the mean $\mathbf{\bar{s}}$ of each row in $\mathbf{s}$;

4. Normalize the original point cloud data as zero-mean in each row, i.e., $\mathbf{s^{\prime}}=[\mathbf{X_{1}-\bar{s}}\ \mathbf{X_{2}-\bar{s}}\ \mathbf{X_{3}-\bar{s}}]$;

5. Calculate the eigenvectors $\mathbf{f}_{1},\cdots,\mathbf{f}_{N_{k}}$, the eigenvalues $0\leq\lambda_{1}\leq\lambda_{2}\leq\ldots\leq\lambda_{N_{k}}$ and the threshold $\theta$ of eigenvalues for $R_{\mathbf{s^{\prime}}}=\mathbf{s^{\prime}}\mathbf{s^{\prime}}^{T}$;

for $i=1,2,\cdots,N$ do

6.Use hypergraph spectrum
$\mathbf{V}=[\mathbf{f}_{1},\cdots,\mathbf{f}_{N_{k}}]$ to calculate the
Fourier transform $\hat{\mathbf{s}}_{i}$ in Eq. (1);

7.Calculate the local smoothness $\sigma(\mathbf{p}_{i})$ in Eq. (2);

end for

8. Sort the local smoothness $\sigma(\mathbf{p}_{i})$ and select the bottom $N_{r}=\alpha N$ points as the resampled point cloud.

Next, for $i$-th point in the point cloud, its corresponding local signal
$\mathbf{s}_{i}\in\mathbb{R}^{N_{k}}$ is defined according to the number of
points in the voxel of kernel centered at $i$-th point. Since we consider the
third-order tensor and only care about the signal energies in spectral domain,
we could utilize the hypergraph spectrum to calculate a simplified-form of
hypergraph Fourier transform $\hat{\mathbf{s}}_{i}$ as

$\displaystyle{\hat{\mathbf{s}}_{i}=\mathbf{V}^{T}\mathbf{s}_{i}}.$ (1)

For edge-preserving purpose, we would like to separate high frequency
coefficients from low frequency coefficients in spectral domain. Since the
spectrum bases corresponding to smaller $\lambda$ represent higher frequency
components[14], we can sort the eigenvalues of $R_{\mathbf{s^{\prime}}}$ as
$0\leq\lambda_{1}\leq\lambda_{2}\leq\ldots\leq\lambda_{N_{k}}$ with
corresponding eigenvectors {$\mathbf{f}_{1},\cdots,\mathbf{f}_{N_{k}}$}. We
can then devise a threshold $\theta$ to divide the high frequency components
from the low frequency components if there exist a sharp jump between a pair
of adjacent eigenvalues.

Given a threshold selection of $\theta$, we could further define a local
smoothness $\sigma(\mathbf{p}_{i})$ to select resampled points:

$\displaystyle{\sigma(p_{i})=\frac{\sum_{k\in\\{1,2,\cdots,\theta\\}}|\hat{\mathbf{s}}_{i}(k)|}{\sum_{k\in\\{1,\cdots,{N_{k}}\\}}|\hat{\mathbf{s}}_{i}(k)|}},$
(2)

which is the fraction of high frequency energy.

Finally, we resample the point cloud by selecting points with smaller
$\sigma(p_{i})$, which corresponds to points containing larger amount of high
frequency in the hypergraph. We summarize our algorithm as Algorithm 1. Since
the resampled point clouds favor high-frequency points, they tend to contain
sharper features and are less smooth.

| Kernel Filtering | Fast Resampling
---|---|---
Noise Level | Precision | Recall | F1-Score | Precision | Recall | F1-Score
No noise | 0.3545 | 0.9332 | 0.5125 | 0.3827 | 1 | 0.5522
20% | 0.2556 | 0.6689 | 0.3690 | 0.2326 | 0.6086 | 0.3357
40% | 0.1052 | 0.2745 | 0.1518 | 0.0995 | 0.2600 | 0.1436
Table 1: Numerical results of methods for edge preserving resampling without
and with Gaussian noise.

##  4 Experimental results

We now describe our experiment setup and present test results of the proposed
resampling algorithm.

###  4.1 Edge Preserving on Simple Synthetic Point Clouds

As we mentioned in Section 3, one important resampling objective is to
preserve sharp features in a point cloud such as edges and corners. In this
part, we study the edge preserving capability of our proposed algorithms by
testing over several simple synthetic point clouds. The reason for selecting
synthetic point clouds for this test is to take advantage of the known ground
truth regarding edges and our ability to label them. We generate these
synthetic point clouds by uniformly sampling the external surface of models
constructed from combinations of cubes with various sizes. One example of
synthetic point clouds is shown in Fig. 1, where the points on edges are
marked with red and the rest points are in blue.

Fig. 1: A synthetic point cloud with labeled edge.

To measure the accuracy of the edge preserving features, we use the $F_{1}$
score, which is defined as:

$\displaystyle
F_{1}=2\times\frac{\rm{Precision}\times\rm{Recall}}{\rm{Precision}+\rm{Recall}},$
(3)

where precision is defined as the proportion of points correctly preserved by
the resampling algorithm while the recall rate is the ratio of correctly
preserved edge points versus all ground truth edge points.

We compare our method with graph-based fast resampling method in [8]. We set
the resampling ratio $\alpha=0.2$ for all point clouds. More results on
different sampling ratios will be discussed in Section 4.3. The parameters of
fast resampling method are set to the typical value suggested in [8]. In order
to study the robustness of algorithms, we add 20% and 40% of Gaussian noise to
the coordinates of point cloud. The results are shown in Table 1. The test
results show that our hypergraph kernel-based filtering method has better
performance in preserving edges in noisy data compare to GSP-based method.

###  4.2 Edge Detection on Complex Real Point Cloud

To test our proposed algorithm in a more general setting, we also implement
edge-detection based on our resampled data in more complex practical point
clouds. For these datasets, there are no known ground truth edges. Therefore,
we shall present the visual results shown in Fig. 2, where the left column are
the original point clouds and the right column are the resampled point clouds.
The results show that our resampling method could draw the contour of 3D
objects.

Fig. 2: Examples of edge detection for real point cloud. Categories | HGSP Kernel Filtering | GSP Fast Resampling | Eigenvalues Analysis | PCA and Clustering
---|---|---|---|---
Cap | 0.0101 | 0.0102 | 0.0087 | 0.0115
Chair | 0.0113 | 0.0118 | 0.0125 | 0.0126
Mug | 0.0134 | 0.0141 | 0.0150 | 0.0147
Rocket | 0.0069 | 0.0070 | 0.0070 | 0.0073
Skateboard | 0.0080 | 0.0079 | 0.0082 | 0.0083
Table 2: Mean distance between the best point cloud and the corresponding
original point cloud with $\alpha=0.2$.

###  4.3 Point Cloud Recovery from Resampled Point Clouds

To study the model preservation of our proposed method, we recover the point
cloud from the resampled ones and evaluate the distance between original and
the recovered point cloud.

Recovery Method: The point cloud recovery contains two steps: 1) reconstruct
the surface of object from the resampled point cloud, and 2) sample on
reconstructed surface to generate the recovered point cloud. Since many points
in the edge preserving resampled point clouds are located in areas with high
local variation, such as surface edges, the resampled point clouds is non-
uniform, as shown in Fig. 4(b). Therefore, most commonly used surface
reconstruction methods such as Poisson reconstruction [20] may perform poorly
on these point clouds. In order to reconstruct such surfaces, we build alpha
complex [21] of the resampled point cloud. To minimize the effect of the
imperfect reconstruction, we reconstruct six different surface models based on
different parameters for each resampled point cloud. We then use Poisson-disk
resampling method to sample over the alpha complex to obtain the recovered
point cloud. Only the recovered point cloud with smallest distance to the
original point cloud is kept.

Distance between two point clouds: To measure the difference between the
original and recovered point clouds, we define a distance metric

$\displaystyle
D_{0}=\frac{1}{N_{1}}\Sigma_{i=1}^{N_{1}}\min_{j:\|p_{i}-p_{c,j}\|<d_{\theta}}\|p_{i}-p_{c,j}\|,$
(4)

where $N_{1}$ is the number of points in the original point cloud, $p_{i}$ and
$p_{c,j}$ are the points in the original and recovered point clouds,
respectively. Although we use different parameters in the reconstruction,
errors such as wrong surfaces that does not exist in the original point cloud
are hard to avoid. Therefore, we select a threshold $d_{\theta}$ to be three
times the intrinsic resolution of the original point cloud. $D_{0}$ is the
average distance for points that are within the original point cloud within
$d_{\theta}$ from the closest points within the best recovered point cloud.

Fig. 3: Performance of Recovery with Different Resampling Ratio.

(a) Original Cap.

(b) Resampled Result.

(c) Recovered Result.

Fig. 4: Example of Recovered Point Cloud.

Visual and numerical results. Our experiment uses models in six different
categories in Shapenet [22] as the original point clouds. We compare our
hypergraph kernel-based filtering method with the GSP-based method in [8]. We
also compare to two edge detection methods, i.e., eigenvalues analysis and PCA
clustering methods in [11]. We resample the same number of nodes for all the
methods.

Our experiment follows the following steps: First, we use resampling and edge
detection methods to calculate the resampled point clouds with different
resampling ratio $\alpha$; Next, we use the proposed recovery method to
generate the recovered point clouds; We then calculate the distance between
the recovered point clouds and the corresponding original ones; Finally, we
calculate the mean distance between the best recovered point cloud and their
original point cloud for each method. An example of the recovered point cloud
is shown in Fig. 4(c). Numerical results for $\alpha=0.2$ are shown in Table
2. From our test results, the mean distance of the proposed method is lower
than that from GSP-based resampling. When compared with edge detection
methods, our proposed algorithm generates similar or smaller mean distance in
most categories. We also examine the effect of different resampling ratio
$\alpha$ in Fig. 3 using the same set of point clouds. Our proposed methods
exhibit superior performance over traditional methods in terms of mean
distance for various resampling ratios. These tests demonstrate the efficiency
of our point cloud recovery. It also shows that hypergraph can model the point
clouds better than graph in certain applications.

##  5 Conclusion

In this work, we developed a 3D point cloud resampling method using kernel
filtering based on hypergraph signal processing (HGSP). The proposed HGSP
resampling is simple and the experimental results demonstrated that our
hypergraph-based method outperforms traditional graph-based methods or
feature-based methods such as edge detection in the terms of robustness to the
noise and model preserving. We establish HGSP as an efficient tool to model
multilateral relationship and to extract features in point cloud applications.

## References

  * [1] Z. C. Marton, R. B. Rusu and M. Beetz, “On fast surface reconstruction methods for large and noisy point clouds,” 2009 IEEE International Conference on Robotics and Automation, Kobe, Japan, May 2009, pp. 3218-3223.
  * [2] R. Schnabel, S. Möser and R. Klein, “A Parallelly Decodeable Compression Scheme for Efficient Point-Cloud Rendering,” in SPBG, Prague, Czech Republic, Sep. 2007, pp. 119-128.
  * [3] S. Gumhold, X. Wang and R. S. MacLeod, “Feature Extraction From Point Clouds,” in IMR, Newport Beach, USA, Oct. 2001, pp. 293-305.
  * [4] Z. Chen, T. Zhang, J. Cao, Y. J. Zhang and C. Wang, “Point cloud resampling using centroidal Voronoi tessellation methods,” Computer-Aided Design, vol. 102, pp. 12-21, Apr. 2018.
  * [5] S. Orts-Escolano, V. Morell, J. García-Rodríguez and M. Cazorla, “Point cloud data filtering and downsampling using growing neural gas,” The 2013 International Joint Conference on Neural Networks (IJCNN), Dallas, TX, USA, Aug. 2013, pp. 1-8.
  * [6] A. Anis, P. A. Chou and A. Ortega, “Compression of dynamic 3D point clouds using subdivisional meshes and graph wavelet transforms,” 2016 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), Shanghai, China, Mar. 2016, pp. 6360-6364.
  * [7] W. Hu, G. Cheung, A. Ortega and O. C. Au, “Multiresolution graph fourier transform for compression of piecewise smooth images,” in IEEE Transactions on Image Processing, vol. 24, no. 1, pp. 419-433, Jan. 2015.
  * [8] S. Chen, D. Tian, C. Feng, A. Vetro and J. Kovačević, “Fast Resampling of Three-Dimensional Point Clouds via Graphs,” in IEEE Transactions on Signal Processing, vol. 66, no. 3, pp. 666-681, Feb. 2018.
  * [9] S. Chen, D. Tian, C. Feng, A. Vetro and J. Kovačević, “Contour-enhanced resampling of 3D point clouds via graphs,” 2017 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), New Orleans, USA, Mar. 2017, pp. 2941-2945.
  * [10] C. Weber, S. Hahmann and H. Hagen, “Sharp feature detection in point clouds,” 2010 Shape Modeling International Conference, Aix-en-Provence, France, Jun. 2010, pp. 175-186.
  * [11] D. Bazazian, J. R. Casas and J. Ruiz-Hidalgo, “Fast and Robust Edge Extraction in Unorganized Point Clouds,” 2015 International Conference on Digital Image Computing: Techniques and Applications (DICTA), Adelaide, Australia, Nov. 2015, pp. 1-8.
  * [12] S. Zhang, S. Cui and Z. Ding, “Hypergraph-Based Image Processing,” 2020 IEEE International Conference on Image Processing (ICIP), Abu Dhabi, United Arab Emirates, Oct. 2020, pp. 216-220.
  * [13] A. Ortega, P. Frossard, J. Kovačević, J. M. F. Moura and P. Vandergheynst, “Graph Signal Processing: Overview, Challenges, and Applications,” in Proceedings of the IEEE, vol. 106, no. 5, pp. 808-828, May 2018.
  * [14] S. Zhang, Z. Ding and S. Cui, “Introducing Hypergraph Signal Processing: Theoretical Foundation and Practical Applications,” in IEEE Internet of Things Journal, vol. 7, no. 1, pp. 639-660, Jan. 2020.
  * [15] S. Barbarossa and M. Tsitsvero, “An introduction to hypergraph signal processing,” 2016 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), Shanghai, China, Mar. 2016, pp. 6425-6429.
  * [16] S. Zhang, S. Cui and Z. Ding, “Hypergraph Spectral Clustering for Point Cloud Segmentation,” in IEEE Signal Processing Letters, vol. 27, pp. 1655-1659, Sep. 2020.
  * [17] S. Zhang, S. Cui and Z. Ding, “Hypergraph Spectral Analysis and Processing in 3D Point Cloud,” arXiv preprint arXiv:2001.02384, Jan. 2020
  * [18] R. B. Rusu, Z. C. Marton, N. Blodow, M. Dolha and M. Beetz, “Towards 3D point cloud based object maps for household environments,” Robotics and Autonomous Systems, vol. 56, no. 11, pp. 927-941, Nov. 2018.
  * [19] A. Banerjee, A. Char and B. Mondal, “Spectra of general hypergraphs,” Linear Algebra and its Applications, vol. 518, pp. 14-30, Apr. 2017.
  * [20] M. Kazhdan, M. Bolitho and H. Hoppe, “Poisson surface reconstruction,” in Proceedings of the fourth Eurographics symposium on Geometry processing, vol. 7, Jun. 2006.
  * [21] H. Edelsbrunner and E. P. Mücke, “Three-dimensional alpha shapes,” ACM Transactions on Graphics (TOG), vol. 13, no. 1, pp. 43-72, Jan. 1994.
  * [22] A. X. Chang, T. Funkhouser, L. Guibas, P. Hanrahan, Q. Huang, Z. Li, S. Savarese, M. Savva, S. Song, H. Su and J. Xiao, “Shapenet: An information-rich 3d model repository,” arXiv preprint arXiv:1512.03012, Dec. 2015.