### Partial Evaluations 2

#### Posted by John Baez

*guest post by Carmen Constantin*

This post belongs to the series of the Applied Category Theory Adjoint School 2019 posts. It is a follow-up to Martin and Brandon’s post about partial evaluations.

Here we would like to use some results by Clementino,
Hofmann, and Janelidze
to answer the following questions: *When can we compose
partial evaluations?* and more generally *When is the
partial evaluation relation transitive?*

## Introduction

In this post, for simplicity, we study monads over the category of sets. A similar discussion can be had in more general categories by replacing elements of a set $X$ by generalized elements, that is, arrows into the object $X$. See this previous blog post for more details about this.

An algebra $(A,e)$ of a monad $T$ comes equipped with a way of evaluating the expressions in $T A$ via the map $e \colon T A \rightarrow A$

This algebra map has to interact nicely with the multiplication of the monad, in particular making $e$ the coequalizer of the pair $\mu, Te \colon T T A \rightarrow T A.$

This can be used to refine the notion of evaluation: a term
$t_1$ is a *partial evaluation* of a term $t_0$, written $t_0 \rightsquigarrow t_1$ if there is a ‘one dimension higher’
term $\tau_{01}$ in $T T A$ which witnesses the partial
evaluation in the sense that $\mu(\tau_{01})=t_0$ and
$Te(\tau_{01})=t_1$ in the diagram

The blue line expresses the partial evaluation relation, that is, the existence of such an element in $T T A$ given $t_0$ and $t_1$. Note that, since the black arrows of the diagram above commute, a necessary condition for the existence of such $\tau_{01}$ is that $e(t_0)$ agrees with $e(t_1)$ in $A$.

We have seen in a previous blog post that the partial evaluation relation is reflexive, and for some monads, e.g. the Free Monoid/List monad, it is also transitive: if $t_0 \rightsquigarrow t_1$ and $t_1\rightsquigarrow t_2$ are witnessed by $\tau_{01}$ and $\tau_{12}$ respectively, then there is some $\tau_{02}$ witnessing $t_0 \rightsquigarrow t_2$

One could ask whether there is a term $\Theta$ in $T T T A$ such that $\mu_T(\Theta)=\tau_{01}$ and $TTe(\Theta)=\tau_{12}$. If such a term exists, then one can simply take $\tau_{02}:=T\mu(\Theta)$ to be the desired witness for transitivity.

The existence of such a term $\Theta$ corresponds to the existence of a strategy for finding a transitivity witness.

This can be summarised in the following picture:

where we have indicated the existence of partial evaluations by a pair of squiggly lines highlighted in dark blue (to avoid confusion with the diagram’s actual arrows), while their composite is highlighted in light blue.

**Remark 1.**
A strategy $\Theta$ always exists if the back
square of the cube above (which we shall refer to as ‘the
monad’s cube’) is a weak pullback.

A weak pullback square is a commutative square with the existence but not necessarily the uniqueness condition of the universal property of pullbacks (see the nLab page on weak limits). Of course, a transitivity witness might exist even if there is no strategy for finding it.

Note also that the partial evaluations and their composite form a triangle, i.e. a 2-simplex, if view the bar construction as a simplicial set—see the previous blog post.

Moreover, in simplicial language, the outer green arrows correspond to the two edges forming an inner 2-horn, while the one labeled ‘transitivity witness’ is the missing edge of the horn. The existence of the strategy arrow corresponds to the existence of what is called a horn filler. As we have previously noted, a transitivity witness $\tau_{02}$ might exist even if there is no horn filler.

A quick intuitive example to illustrate the transitivity property is given by the free commutative monoid monad, where $T A$ consists of formal sums of elements in $A$. If $A=\mathbb{N}$, the algebra map simply evaluates a formal sum to return an element in $\mathbb{N}$. We can draw a picture of the terms $t_0=1+2+3+4$, $t_1=3+3+6$ and $t_2=6+4$ which illustrates the transitivity of the partial evaluation relation $t_0\rightsquigarrow t_1\rightsquigarrow t_2$.

Of course, if the partial evaluation relation is transitive, then we can think about forming even longer composites. For example, for three composable back-to-back partial evaluations (depicted in dark blue in the figure below) the existence of an associator (and hence a coherent way to compose them) would be given by a 3-simplex, i.e. a filled tetrahedron, which corresponds to an element of $T^4A$. This element should restrict under $\mu$, $T\mu$, $T^2\mu$ and $T^3e$ respectively to the corresponding elements in $T^3A$ that give the strategies for the binary composites.

This can be illustrated by a 4-dimensional cube diagram, where again dark blue lines represent the partial evaluations, light blue lines represent their binary composites and the labels of the monad’s cube have been suppressed to avoid clutter.

Each 3-horn corresponds to a union of all but one of the faces of the $3$-simplex. When the omitted face is the one opposite to the first or last of the corners of the tetrahedron, one speaks of outer horns, otherwise they are called inner horns. This terminology is important because aside from transitivity, which we shall talk about in the remainder of the blog post, we have also looked at the possibility of finding horn fillers for inner horns (for monads which allow binary composites), as their existence would make the structures arising from the bar construction into a quasicategory. However, it turned out that even when binary composites exist for all composable partial evaluations, it is not always possible to find such fillers.

## Weakly cartesian monads

When a monad is *weakly cartesian*, the partial evaluation
relation is transitive. A
monad $(T,\mu,\eta)$ is weakly cartesian if the functor $T$
preserves weak pullbacks, and all naturality squares of
$\mu$ and $\eta$ are weak pullbacks. In particular the back square of the monad’s cube discussed in Remark 1 is a weak pullback, meaning that the aforementioned $\Theta$ in $T T T A$ exists.

Here is a well-known fact:

**Remark 2.** If a monad $T$ is associated to a variety of
universal algebras, and the variety is operadic, then the
functor $T$ is cartesian (and so, in particular, weakly
cartesian).

To understand this statement note that a variety
$\mathcal{C}$ comes equipped with a monadic free-forgetful
adjunction between $\mathcal{C}$ and the category of sets,
that is, the Eilenberg-Moore category of algebras for the
monad $T$ is isomorphic to $\mathcal{C}$. Now consider a
presentation $(\Omega, \phi)$ of the variety $\mathcal{C}$,
where $\Omega$ is a *signature* (a set $\coprod_{n\geq 0}
\Omega_n$ of function symbols of arbitrary but finite arity
$n$, including the constants of arity zero), and $\phi$ is a
set of *equational laws* or identities between terms in
$\Omega$. A variety is *operadic* if it can be presented using
a set of identities which have the same variables appearing
in the same order, without repetition, on each side. For
example, $a\cdot b+c=a-b\cdot c$ would be an admissible identity for
an operadic theory, but $a\cdot b=b\cdot a$ and $a\cdot b=a$ would not.

Operadic (and hence cartesian) varieties include

- all varieties that can be presented with no identities, i.e. by a pair $(\Omega, \phi)$ where $\phi=\emptyset$ and in particular also all varieties in which $\Omega=\Omega_0$, such as sets and pointed sets.
- the variety of monoids, where $\Omega_2=\{*\}$ only contains the monoid multiplication and $\Omega_0=\{e\}$ is the constant representing the unit of the monoid. The identities in $\phi$ corresponding to the law of associativity and the unit law are clearly operadic.
- the variety of semigroups
- all varieties of the form $\mathbf{Set}^M$ where $M$ is a monoid, that is, of monoid actions on sets (including group actions).

The theory of groups on the other hand is not operadic: it contains the identity $g g^{-1}=e$, which is not allowed.

Since the monads associated to these varieties are cartesian, and so weakly cartesian, for these monads the partial evaluation relation is transitive. How, then, do partial evaluations behave for monads which are not weakly cartesian?

## Monads which are not weakly cartesian

The paper The monads of classical algebra are seldom weakly cartesian lists several necessary and several sufficient conditions for weak cartesianness of the functor $T$, the unit $\eta$ and the multiplication $\mu$ respectively for monads defined over algebraic varieties in general and free semimodule monads in particular.

Notably, even if a monad is not weakly cartesian, a strategy for composing partial evaluations can be found by applying the map $T\mu:T^3A\rightarrow T^2A$ within the monad’s cube, as long as the square in Lemma 2 is a weak pullback—a much weaker condition than requiring weak cartesianness of $\mu$ as a natural transformation.

In fact we noticed that some monads which are not weakly cartesian still have transitive partial evaluations, such as the monad corresponding to the variety of $\mathbb{N}$-sets which satisfy the identity $2x=2y$, which in the paper is discussed in Example 3.4.

### A counterexample

The first interesting result for our project comes from the subsequent discussion in the paper, which can be used to show that counterexamples to transitivity also occur.

In particular, it is interesting to look at the free $S$-semimodule monad (let $(T,\eta,\mu)$ denote this monad), where $S$ is a particular semiring. There are a number of conditions stated in the paper such that, if any of them is satisfied by the semiring $S$, then the functor $T$ is a weakly cartesian functor:

no non-zero elements in $S$ can have an additive inverse

for every $a,b\in S$ there exists $x\in S$ such that either $a+x=b$ or $b+x=a$

the additive monoid of $S$ is a monoid with cancellation (equivalently, it can be embedded into an abelian group).

Once $T$ is a weakly cartesian functor, the multiplication is weakly cartesian if and only if additionally

No non-zero element in $S$ has an additive inverse

$S$ has no (non-zero) zero divisors

for any generating subset $C$ of $S$ and any $a,b,c,d\in S$ with $c\in C$ such that $cd=a+b$, there exists a map $t:\{(x,y)\in S\times S \ | \ x+y =d\}\longrightarrow S$ with $\sum_{x+y=d} t(x,y)x=a, \ \ \sum_{x+y=d}t(x,y)y=b, \ \ and \sum_{x+y=d}t(x,y)=c$

The counterexamples we are interested in arise from semirings which satisfy the first 5 conditions but fail to satisfy the last one.

Consider for example the free semimodule monad $T$ over the semiring $S=\mathbb{N}[x]/\langle x^2=2\rangle$. This monad is given by

$T(X):=\{t:X\rightarrow S \ | \ t \ \text{ has finite support}\}$. To keep the presentation more intuitive, we can use a simpler notation for the elements of $T(X)$, writing each element as a formal sum $\sum s_i\cdot x_i,$ which consists of a finite number of terms in $X$ with coefficients in $S$. Note that two such formal sums represent the same element if and only if they have the same elements of $X$ with the same corresponding coefficients, but perhaps appearing in a different order in the expansion.

the intuitive equivalent description of the unit is then $\eta_X(x)= 1\cdot x$

the multiplication represents the familiar distributivity property: if $\tau=\sum_i z_i\cdot \sum_{j_i} s_{j_i}\cdot x_{j_i}$ then $\mu_X(\tau)=\sum_{i,j_i} (z_i s_{j_i})\cdot x_{j_i}$

An algebra map $e$ then simply evaluates the formal weighted sum $\sum s_i\cdot x_i$ to some element $\hat{x}\in X$. Thus an algebra for this monad corresponds to an actual semimodule over $S$, in the classical sense of the term.

Note that the map $T e:T T X\rightarrow TX$ is then given by

$Te\left(\sum_i z_i\cdot \sum_{j_i}s_{j_i}\cdot x_{j_i}\right)=\sum_i z_i\cdot \widehat{x_i}$ where $\widehat{x_i}=e\left(\sum_{j_i}s_{j_i}\cdot x_{j_i}\right)$ is the evaluation of the corresponding sum.

We can not only show that the back square of the monad’s
cube is not a weak pullback for this monad, and hence no
*strategies* for finding transitivity witnesses exist, but
also that transitivity itself fails to hold for this monad.
Let $A:=\{ \ast \}$ be the one element $T$-algebra, i.e. the
zero semimodule. The elements of $T A$ are formal sums with
just one term $s_i\cdot \ast$ and the evaluation map is
trivial in the sense that the value of $s_i\cdot \ast$ is
just $\ast$, as one would expect from multiplication acting
on zero. There is a partial evaluation between the $T A$ terms
$1\cdot \ast$ and $2\cdot \ast$ witnessed by the $T T A$
element $\tau=1\cdot 1\cdot \ast + 1\cdot 0\cdot \ast$
since $\mu(\tau)=(1\cdot 1)\cdot \ast +(1\cdot 0)\cdot \ast
=1\cdot \ast +0\cdot \ast =1\cdot \ast$ and also
$Te(\tau)=1\cdot e(1\cdot \ast)+ 1\cdot e(0\cdot
\ast)=1\cdot \ast + 1\cdot \ast = 2\cdot \ast$

There is also a partial evaluation between $2\cdot \ast$ and $x\cdot \ast$ witnessed by the $T T A$ element $\tau'=x\cdot x\cdot \ast$ namely, $\mu(\tau')=(x\cdot x)\cdot \ast = 2\cdot \ast$ and also $Te(\tau')=x\cdot(x\cdot \ast)=x\cdot \ast$ However, there can be no partial evaluation from $1\cdot \ast$ to $x\cdot \ast$ because $T e$ maps any $\tau''=\sum_i z_i\cdot s_i\cdot \ast$ in $T T A$ to $\sum_i z_i\cdot \ast = \left(\sum_i z_i\right)\cdot \ast.$ So if $\tau''$ were a transitivity witness, we would need $\sum_i z_i= x.$ But $x$ is additively indecomposable in $S$. Hence $\tau''=x\cdot s\cdot \ast$, for some $s\in S$. But then $\mu(\tau'')=(x\cdot s)\cdot \ast$ which cannot equal $1\cdot \ast$, since $x$ is not a unit in $S$.

## Some further thoughts

It was quite satisfying to find a concrete answer to the transitivity question we started from. There are several directions that we could explore further.

On the one hand, there are interesting connections with probability which Paolo Perrone has discussed in a previous blog post, and Brandon and Martin have written about.

On the other hand, it has been pointed out to us that it is likely to find connections with multi-stage programming and partially static data structures which have been used by computer scientists to describe computations that give the programmer a fine-grained control over beta reduction. Being able to control evaluation provides a basis for optimisation of binding times.

We can also further investigate these structures by trying for example to find out when partial evaluations are invertible. Together with transitivity, this would turn the partial evaluation into an equivalence relation.

If the algebra structure square

is a weak pullback, then the partial evaluation relation is an equivalence relation. One can ask if the converse also holds.

A more sophisticated question than whether the relation being an equivalence is the following: when is the 1-truncation of the bar construction a groupoid? That is, in case we can form a category with partial evaluations as morphisms, when are all morphisms there invertible?

For example, let $G$ be a group. The theory of $G$-sets is operadic, so the associated monad $T(X)=G\times X$ is (strongly) cartesian, and the bar construction gives the nerve of a category. The 0-simplices are the elements $(g,x)$ of $G\times X$, the 1-simplices from $(g,x)$ to $(h,y)$ are the elements $(j,h,x)$ of $G\times G\times S$ such that $g= jh$ and $h\cdot x=y$, and so on. The partial evaluation relation here is an equivalence relation (the multiplication square is even an actual pullback – not just a weak one) and for this theory the bar construction of an algebra $A$ is the nerve of a groupoid.

This is probably very related to group cohomology: in this case, the bar construction is indeed a resolution of $A$, i.e. weakly equivalent to $A$. (The bar construction was actually first invented to compute the cohomology of $G$-modules, which are basically this example, just in an abelian category.)

One can also ask higher-dimensional questions, such as when is the bar construction an infinity-groupoid (i.e. a Kan complex)?

It turns out that this last question has a partial answer which involves Mal’cev theories.

A *Mal’cev operation* on a set $A$ is a ternary
operation $m:A\times A\times A\to A$ such that for each
$a,b\in A$, $m(a,b,b) = a \; \text{and} \; m(a,a,b) = b.$ A *Mal’cev theory* is an
algebraic theory which contains a Mal’cev operation.

In the algebraic theory of groups, there is a Mal’cev operation defined by $m(a,b,c) \; := \; a\,b^{-1}\,c.$ Therefore any theory whose algebras are groups, with possibly extra structures or properties, is a Mal’cev theory. These include for example the theories of groups, rings or modules over a fixed ring but not, for example, the theory of monoids, commutative monoids, semirings, and semimodules.

An example of a Mal’cev theory which is not a theory of particular groups is the theory of heaps.

A theorem by Carboni, Kelly and Pedicchio states that for any Mal’cev theory $T$ every simplicial object in the category of algebras is a Kan complex. This theorem can be found here. See also the nLab page about Kan complexes.

Therefore, for the theory of groups (and heaps, etc.), not only do we get an equivalence relation, but the whole bar construction is an $\infty$-groupoid, of which the equivalence relation is the shadow, i.e. the (0,1)-truncation.

## Re: Partial Evaluations 2

Nice stuff! It reminds me a little of my seminar on cohomology and computation, where I was advocating the bar construction as a systematic way of replacing equations by edges, equations between equations or ‘syzygies’ by triangles, and so on. But I spent the whole seminar explaining the bar construction and didn’t really get very far figuring out the computational aspects. It’s good to see people doing this now. I recommend bringing cohomology into the game.