Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

May 16, 2019

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 e:Te : T{\mathbb{N}} \to \mathbb{N} where TT is the free commutative monoid monad. Given a particular expression in TT\mathbb{N}, say 1+2+31 + 2 + 3, it’s natural to consider the expression q=1+5q = 1 + 5 as a partial evaluation of it. If we bracket the expression as (1)+(2+3)(1) + (2 + 3), this becomes more explicit—the expression 1+51 + 5 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 e:TAAe : T A \to A, there are two maps μ:TTATA\mu : T T A \to T A and Te:TTATAT e : T T A \to T A. If we think of the elements of TAT A as formal expressions over the variables of AA, the elements TTAT T A as formal expressions over the formal expressions of TAT A, the map μ:TTATA\mu : T T A \to T A flattens formal expressions of formal expressions to “mere” formal expressions, while TeT e evaluates the inner formal expressions. In our example above, the situation is illustrated in the following picture:

The expression (1)+(2+3)TTA(1) + (2 + 3) \in T T A is witnessing the partial evaluation between 1+2+31 + 2 + 3 and 1+51 + 5. 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 p:STAp : S \to T A from an arbitrary object SS a generalized element (with shape SS) of TAT A.

Given a monad (T,η,μ)(T, \eta, \mu) and an algebra AA with evaluation map e:TAAe : T A \to A, a partial evaluation from p:STAp : S \to T A to q:STAq : S \to T A consists of a morphism k:STTAk : S \to T T A such that the following diagram commutes:

Since the algebra laws ensure that eμ=eTee \circ \mu = e \circ T e, we see if there is a partial evaluations from pp to qq, we always have a generalized element ep=eμk=eTek=eqe \circ p = e \circ \mu \circ k = e \circ T e \circ k = e \circ q which we call the total evaluation or the result of pp and qq. 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 SS and TAT A, 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 e:PAAe: P A \to A over a probability monad and distributions p,qPAp, q \in P A, whenever there exists a partial evaluation of pp and qq, there exists two AA-valued random variables XX and YY, with probability distribution pp and qq, respectively, such that YY is a conditional expectation of XX with respect to some coarser σ\sigma-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 AA to be 2\mathbb{R}^2 and let p,qPAp, q \in P A 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, pp assigns the probability of 14\frac{1}{4} to each corner of the unit square, while qq assigns a probability of 14\frac{1}{4} to the north, south, east and west points of the unit circle.

We can express pp and qq as a convex combination of probabilities and points as p=14((1,1)+(1,1)+(1,1)+(1,1))p = \frac{1}{4}\big( (-1,1) + (-1,-1) + (1,-1) + (1,1) \big ) and q=14((0,1)+(1,0)+(1,0)+(0,1))q = \frac{1}{4}((0,1) + (1,0) + (-1,0) + (0,-1)).

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, qq 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 pp to qq.

How do we find the element kPPAk \in P P A witnessing this partial evaluation? The key here is in our description of the points of qq as a combination of averages of the points of pp.

We can write this combination of averages as a convex combination of probability distributions, i.e. as an element kk of PPAP P A, as

k=14(12(1,1)+12(1,1))+14(12(1,1)+12(1,1))+14(12(1,1)+12(1,1))+14(12(1,1)+12(1,1)).k = \frac{1}{4}\big (\frac{1}{2}(-1,1) + \frac{1}{2}(1,1) \big ) + \frac{1}{4}\big (\frac{1}{2}(-1,-1) + \frac{1}{2}(1,-1) \big ) + \frac{1}{4}\big (\frac{1}{2}(-1,-1) + \frac{1}{2}(-1,1) \big ) + \frac{1}{4}\big (\frac{1}{2}(1,-1) + \frac{1}{2}(1,1) \big ).

Applying the multiplication map simplifies the expression to yield pp:

μ(k)=18(1,1)+18(1,1)+18(1,1)+18(1,1)+18(1,1)+18(1,1)+18(1,1)+18(1,1)=p\mu(k) = \frac{1}{8}(-1,1) + \frac{1}{8}(1,1) + \frac{1}{8}(-1,-1) + \frac{1}{8}(1,-1) + \frac{1}{8}(-1,-1) + \frac{1}{8}(-1,1) + \frac{1}{8}(1,-1) + \frac{1}{8}(1,1) = p

while applying TeT e to kk returns the expected values of the inner brackets, yielding qq:

Te(k)=14E[12(1,1)+12(1,1)]+14E[12(1,1)+12(1,1)]+T e(k) = \frac{1}{4}E[\frac{1}{2}(-1,1) + \frac{1}{2}(1,1)] + \frac{1}{4}E[\frac{1}{2}(-1,-1) + \frac{1}{2}(1,-1) ] + 14E[12(1,1)+12(1,1)]+14E[12(1,1)+12(1,1)]=q.\frac{1}{4}E[\frac{1}{2}(-1,-1) + \frac{1}{2}(-1,1) ] + \frac{1}{4}E[\frac{1}{2}(1,-1) + \frac{1}{2}(1,1) ] = q.

This demonstrates that qq is a partial evaluation of qq, as witnessed by the element kPPAk \in P P A.

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 TT the free monoid monad, AA the algebra of natural numbers with addition, and SS the terminal set (so a map SXS \to X is just an element of XX), the expression 1+2+3+4+51 + 2 + 3 + 4 + 5 partially evaluates to 3+3+93 + 3 + 9 by the partial evaluation h=(1+2)+(3)+(4+5)T 2Ah = (1 + 2) + (3) + (4 + 5) \in T^2 A, and 3+3+93 + 3 + 9 partially evaluates to 3+123 + 12 by k=(3)+(3+9)T 2Ak = (3) + (3 + 9) \in T^2 A. In this example we could certainly find a way of adding parentheses to 1+2+3+4+51 + 2 + 3 + 4 + 5 to partially evaluate it into 3+123 + 12, but can we construct this as a composite of hh and kk in some sense?

Consider the doubly nested expression ((1+2))+((3)+(4+5))T 3A((1 + 2)) + ((3) + (4 + 5)) \in T^3 A. Applying μ\mu removes the outer parentheses to get hh, and applying T 2eT^2 e evaluates the innermost expressions to get kk. We can also apply TμT \mu to get (1+2)+(3+4+5)(1 + 2) + (3 + 4 + 5), 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 T 2AT^2 A assemble into a triangle

This means if we have partial evaluations hh from pp to qq and kk from qq to rr, and an element aT 3Aa \in T^3 A with μ(a)=h\mu(a) = h and T 2e(a)=kT^2 e(a) = k, then Tμ(a)T\mu(a) is a partial evaluation from pp to rr. There may be a partial evaluation ll from pp to rr without such an aa, but it would not then be a “composite” of hh and kk in any meaningful way, just as in a category there can be a triangle of morphisms

where ll is not the composition of hh and kk. We can then think of aa as a triangle filling in this diagram of partial evaluations on its boundary, and witnessing that pp and qq can be composed into ll. Unlike a category, however, there may be many such triangles, since elements aa of T 3AT^3 A with μ(a)=h\mu (a) = h, T 2e(a)=kT^2 e(a) = k, Tμ(l)T \mu (l) are not generally unique. These triangles can also be considered as strategies for composing partial evaluations, so given hh and kk as above one way to find a partial evaluation from pp to rr is to look for a strategy aa for composing hh and kk into Tμ(a)T \mu (a).

Using this approach, we can consider the class of weakly cartesian monads where such a strategy always turns out to exist. A monad (T,η,μ)(T,\eta,\mu) is weakly cartesian if it preserves weak pullbacks and the naturality squares of η\eta and μ\mu are weak pullbacks. A weak pullback square

has the property that any pair of maps from WW' into XX and YY commuting with ff and gg factors through WW, but not necessarily uniquely (unlike the usual pullback squares). In particular, hh and kk as above fit into a diagram

where the square in the diagram is a naturality square of μ\mu. If TT is weakly cartesian, we get a map a:ST 3Aa : S \to T^3 A which agrees with hh and kk after applying μ\mu and T 2eT^2 e, respectively. This aa is a composition, so applying TμT\mu gives a composite of hh and kk:

So partial evaluations can always be composed when TT is weakly cartesian, though perhaps in more than one way (since aa is not unique). If TT 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 aa in the example above was no accident.

Bar construction

In the previous section, a:ST 3Aa : S \to T^3 A was interpreted as a triangle, with the arrows hh, kk, and Tμ(a)T\mu(a) as its edges. Partial evaluations do more than just reduce formal expressions: they give a nested expression encoding how to compute that reduction. Likewise aa tells us not just that hh and kk have a composite, but how they compose, in the language of the monad TT, and that information has the “shape” of a triangle. This suggests that TT hosts a richer notion of computation than merely reducing formal expressions, where elements of T nAT^n A have some sort of computational meaning.

We don’t yet know much about what elements of T nAT^n A mean for computation, but we know a lot about their shape. These objects and the maps between them derived from η\eta, μ\mu, and ee assemble into a simplicial object

meaning we can see elements of TAT A as vertices, T 2AT^2 A as edges, T 3AT^3 A as triangles, T 4AT^4 A as tetrahedra, and in general T n+1AT^{n+1} A as nn-simplices with n1n-1 dimensional faces identified by T neT^n e and T iμT^i \mu, 0i<n0 \leq i &lt; n. This simplicial object (in the category of TT-algebras) is called the bar construction of AA.

The bar construction thus expresses that there is a whole space of computations in AA. The expressions in TAT A are the points, partial evaluations in T 2AT^2 A form the paths between points, and nested expressions in T nT^n describe higher dimensional cells. Even more, the space is directed, as 1-simplices kT 2Ak \in T^2 A have a direction from μ(k)\mu (k) to Te(k)T e(k), 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.

Posted at May 16, 2019 9:54 PM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/3111

1 Comment & 0 Trackbacks

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 Set\mathsf{Set} is transitive: if p,q,rTAp,q,r\in TA are such that pp partially evaluates to qq, and qq partially evaluates to rr, then does pp partially evaluate to rr? 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 :)

Posted by: Tobias Fritz on May 20, 2019 9:31 PM | Permalink | Reply to this

Post a New Comment