Partial Evaluations 1
Posted by John Baez
guest post by Martin Lundfall and Brandon Shapiro
This is the third post of Applied Category Theory School 2019.
In this blog post, we will be sharing some insights from the paper Monads, partial evaluations and rewriting by Tobias Fritz and Paolo Perrone.
Introduction
Algebras over a monad provide a categorical interpretation of what it means to evaluate an expression of a particular theory. The process of summing natural numbers, for example, can be understood as the algebra where is the free commutative monoid monad. Given a particular expression in , say , it’s natural to consider the expression as a partial evaluation of it. If we bracket the expression as , this becomes more explicit—the expression is given by evaluating the bracketed subexpressions.
To express this in the language of category theory, we utilize the fact that for an arbitrary algebra over a monad , there are two maps and . If we think of the elements of as formal expressions over the variables of , the elements as formal expressions over the formal expressions of , the map flattens formal expressions of formal expressions to “mere” formal expressions, while evaluates the inner formal expressions. In our example above, the situation is illustrated in the following picture:
The expression is witnessing the partial evaluation between and . To generalize this notion to arbitrary algebras and monads not necessarily over Set, we cannot refer to the elements of a set. Instead, we will formulate things in terms of generalized elements—we will call a morphism from an arbitrary object a generalized element (with shape ) of .
Given a monad and an algebra with evaluation map , a partial evaluation from to consists of a morphism such that the following diagram commutes:
Since the algebra laws ensure that , we see if there is a partial evaluations from to , we always have a generalized element which we call the total evaluation or the result of and . Furthermore, the unit law of the monad ensures that any expression will always be a partial evaluation of itself, as illustrated by the following diagram:
Partial evaluations induce a relation on the morphisms between and , which by the argument above turns out to be reflexive. Later, we will see that for a broad class of monads, this relation will be transitive as well.
So far in this blog post, we have talked about monads as a way of generating formal expressions in a given theory. This is a perspective that is most accurate for finitary monads, but partial evaluations turn out to have a meaningful interpretation in infinitary settings as well.
Partial evaluations as conditional expectations
One of the settings where partial evaluations play an interesting role is in the context of probability monads. As we learned in Paolo Perrone’s recent nCafé blog post, probability monads come in slightly different flavors, but can generally be thought of as a way of taking a set of outcomes to a set of probability distributions of random variables over those outcomes. The multiplication map of such monads combines a probability distribution of probability distributions by a simple averaging. Algebras over these monads are spaces which come equipped with a way of taking the expected value of a convex combinations of its points. Such algebras will correspond to some flavor of convex spaces.
It turns out that for such monads, partial evaluations correspond to a notion familiar from probability theory — conditional expectations. More precisely, given an algebra over a probability monad and distributions , whenever there exists a partial evaluation of and , there exists two -valued random variables and , with probability distribution and , respectively, such that is a conditional expectation of with respect to some coarser -algebra.
We won’t spell out the correspondence between partial evaluations and conditional expectations in full detail here, but refer the curious reader to section 4.2.1. of Paolo’s PhD thesis. Instead we will provide an example that hopefully provides some intuition for why this might be the case.
Take to be and let be two probability distributions that assign an equal probability to four distinct points of the real plane, marked in blue and red, respectively, in the figure below.
In words, assigns the probability of to each corner of the unit square, while assigns a probability of to the north, south, east and west points of the unit circle.
We can express and as a convex combination of probabilities and points as and .
In this example, the red points can be expressed as an averaging, or expected value of blue points. The top red point, for example, is the expected value of the two top blue points, i.e. given that the outcome will lie in the upper half plane. Similarly, the left red point is the expected value of the two blue points in the left half plane, and so on. In other words, is the probability distribution of a random variable (the position of the red point) which is a conditional expectation of the position of the blue point. By the correspondence alluded to above, we therefore expect there to be a partial evaluation from to .
How do we find the element witnessing this partial evaluation? The key here is in our description of the points of as a combination of averages of the points of .
We can write this combination of averages as a convex combination of probability distributions, i.e. as an element of , as
Applying the multiplication map simplifies the expression to yield :
while applying to returns the expected values of the inner brackets, yielding :
This demonstrates that is a partial evaluation of , as witnessed by the element .
Transitivity of partial evaluation
Partial evaluations can be thought of as taking incremental steps towards completely evaluating a formal expression. This makes them start to look like arrows in a category of formal expressions, but for that we need a way to compose them. For example, for the free monoid monad, the algebra of natural numbers with addition, and the terminal set (so a map is just an element of ), the expression partially evaluates to by the partial evaluation , and partially evaluates to by . In this example we could certainly find a way of adding parentheses to to partially evaluate it into , but can we construct this as a composite of and in some sense?
Consider the doubly nested expression . Applying removes the outer parentheses to get , and applying evaluates the innermost expressions to get . We can also apply to get , which is precisely the partial evaluation we want. It’s no coincidence that this worked: the monad, algebra, and naturality laws for maps out of assemble into a triangle
This means if we have partial evaluations from to and from to , and an element with and , then is a partial evaluation from to . There may be a partial evaluation from to without such an , but it would not then be a “composite” of and in any meaningful way, just as in a category there can be a triangle of morphisms
where is not the composition of and . We can then think of as a triangle filling in this diagram of partial evaluations on its boundary, and witnessing that and can be composed into . Unlike a category, however, there may be many such triangles, since elements of with , , are not generally unique. These triangles can also be considered as strategies for composing partial evaluations, so given and as above one way to find a partial evaluation from to is to look for a strategy for composing and into .
Using this approach, we can consider the class of weakly cartesian monads where such a strategy always turns out to exist. A monad is weakly cartesian if it preserves weak pullbacks and the naturality squares of and are weak pullbacks. A weak pullback square
has the property that any pair of maps from into and commuting with and factors through , but not necessarily uniquely (unlike the usual pullback squares). In particular, and as above fit into a diagram
where the square in the diagram is a naturality square of . If is weakly cartesian, we get a map which agrees with and after applying and , respectively. This is a composition, so applying gives a composite of and :
So partial evaluations can always be composed when is weakly cartesian, though perhaps in more than one way (since is not unique). If is cartesian, as in its naturality squares are pullbacks, then there is a canonical choice of composition and furthermore partial evaluations form a category. This is the case for the free monoid monad, so our choice of in the example above was no accident.
Bar construction
In the previous section, was interpreted as a triangle, with the arrows , , and as its edges. Partial evaluations do more than just reduce formal expressions: they give a nested expression encoding how to compute that reduction. Likewise tells us not just that and have a composite, but how they compose, in the language of the monad , and that information has the “shape” of a triangle. This suggests that hosts a richer notion of computation than merely reducing formal expressions, where elements of have some sort of computational meaning.
We don’t yet know much about what elements of mean for computation, but we know a lot about their shape. These objects and the maps between them derived from , , and assemble into a simplicial object
meaning we can see elements of as vertices, as edges, as triangles, as tetrahedra, and in general as -simplices with dimensional faces identified by and , . This simplicial object (in the category of -algebras) is called the bar construction of .
The bar construction thus expresses that there is a whole space of computations in . The expressions in are the points, partial evaluations in form the paths between points, and nested expressions in describe higher dimensional cells. Even more, the space is directed, as 1-simplices have a direction from to , and that directedness comes from partial evaluation.
However, not much is currently known about this space, and we are left with several open questions. How can we interpret the computational meaning of the higher simplices? Can computational properties of a monad relate to topological properties of the space? What kinds of compositional properties exist for partial evaluations in more general monads? What does this all tell us about probability? Answers to these questions could illuminate a relationship between computation and homotopy theory with implications well beyond either of those fields.
Re: Partial Evaluations
Thanks to Martin and Brandon for this fascinating post!
A question that has fascinated us for a while is whether the partial evaluation relation for a finitary monad on is transitive: if are such that partially evaluates to , and partially evaluates to , then does partially evaluate to ? This is a natural property that one might expect to be satisfies at least in well-behaved cases. And as the post explains, this is indeed true for weakly cartesian monads. We also found this to be case for many other monads that we’ve looked at. So could this be true in general? The answer will be revealed in the second post of our group :)