Horner’s Rule

This post is about my all-time favourite calculation, of a linear-time algorithm for the maximum segment sum problem, based on Horner’s Rule. The problem was popularized in Jon Bentley’s Programming Pearls series in CACM (and in the subsequent book), but I learnt about it from Richard Bird’s lecture notes on The Theory of Lists and Constructive Functional Programming and his paper Algebraic Identities for Program Calculation, which he was working on around the time I started my DPhil. It seems like I’m not the only one for whom the problem is a favourite, because it has since become a bit of a cliché among program calculators; but that won’t stop me writing about it again.

Maximum segment sum

The original problem is as follows. Given a list of numbers (say, a possibly empty list of integers), find the largest of the sums of the contiguous segments of that list. In Haskell, this specification could be written like so:

\displaystyle  \begin{array}{lcl} \mathit{mss} &=& \mathit{maximum} \cdot \mathit{map}\,\mathit{sum} \cdot \mathit{segs} \end{array}

where {\mathit{segs}} computes the contiguous segments of a list:

\displaystyle  \begin{array}{lcl} \mathit{segs} &=& \mathit{concat} \cdot \mathit{map}\,\mathit{inits} \cdot \mathit{tails} \\ \mathit{tails} &=& \mathit{foldr}\,f\,[[\,]] \quad\mathbf{where}\; f\,\mathit{x}\,\mathit{xss} = (\mathit{x}:\mathit{head}\,\mathit{xss}):\mathit{xss} \\ \mathit{inits} &=& \mathit{foldr}\,g\,[[\,]] \quad\mathbf{where}\; g\,\mathit{x}\,\mathit{xss} = [\,] : \mathit{map}\,(\mathit{x}:)\,\mathit{xss} \end{array}

and {\mathit{sum}} computes the sum of a list, and {\mathit{maximum}} the maximum of a nonempty list:

\displaystyle  \begin{array}{lcl} \mathit{sum} &=& \mathit{foldr}\,(+)\,0 \\ \mathit{maximum} &=& \mathit{foldr}_1\,\max \end{array}

This specification is executable, but takes cubic time; the problem is to do better.

We can get quite a long way just with standard properties of {\mathit{map}}, {\mathit{inits}}, etc:

\displaystyle  \begin{array}{ll} & \mathit{mss} \\ = & \qquad \{ \mbox{definition of~} \mathit{mss} \} \\ & \mathit{maximum} \cdot \mathit{map}\,\mathit{sum} \cdot \mathit{segs} \\ = & \qquad \{ \mbox{definition of~} \mathit{segs} \} \\ & \mathit{maximum} \cdot \mathit{map}\,\mathit{sum} \cdot \mathit{concat} \cdot \mathit{map}\,\mathit{inits} \cdot \mathit{tails} \\ = & \qquad \{ \mbox{naturality of~} \mathit{concat} \} \\ & \mathit{maximum} \cdot \mathit{concat} \cdot \mathit{map}\,(\mathit{map}\,\mathit{sum}) \cdot \mathit{map}\,\mathit{inits} \cdot \mathit{tails} \\ = & \qquad \{ \mathit{maximum} \cdot \mathit{concat} = \mathit{maximum} \cdot \mathit{map}\,\mathit{maximum} \} \\ & \mathit{maximum} \cdot \mathit{map}\,\mathit{maximum} \cdot \mathit{map}\,(\mathit{map}\,\mathit{sum}) \cdot \mathit{map}\,\mathit{inits} \cdot \mathit{tails} \\ = & \qquad \{ \mbox{functors} \} \\ & \mathit{maximum} \cdot \mathit{map}\,(\mathit{maximum} \cdot \mathit{map}\,\mathit{sum} \cdot \mathit{inits}) \cdot \mathit{tails} \end{array}

For the final step, if we can write {\mathit{maximum} \cdot \mathit{map}\,\mathit{sum} \cdot \mathit{inits}} in the form {\mathit{foldr}\,h\,e}, then the {\mathit{map}} of this can be fused with the {\mathit{tails}} to yield {\mathit{scanr}\,h\,e}; this observation is known as the Scan Lemma. Moreover, if {h} takes constant time, then this gives a linear-time algorithm for {\mathit{mss}}.

The crucial observation is based on Horner’s Rule for evaluation of polynomials, which is the first important thing you learn in numerical computing—I was literally taught it in secondary school, in my sixth-year classes in mathematics. Here is its familiar form:

\displaystyle  \sum_{i=0}^{n-1} a_i x^i = a_0 + a_1 x + a_2 x^2 + \cdots + a_{n-1} x^{n-1} = a_0 + x(a_1 + x(a_2 + \cdots + x\,a_{n-1}))

but the essence of the rule is about sums of products:

\displaystyle  \sum_{i=0}^{n-1} \prod_{j=0}^{i-1} u_j = 1 + u_0 + u_0u_1 + \cdots + u_0u_1\ldots u_{n-1} = 1 + u_0(1 + u_1(1 + \cdots + u_{n-1}))

Expressed in Haskell, this is captured by the equation

\displaystyle  \mathit{sum} \cdot \mathit{map}\,\mathit{product} \cdot \mathit{inits} = \mathit{foldr}\,(\oplus)\,e \quad \mathbf{where}\; e = 1 \mathbin{;} u \oplus z = e + u \times z

(where {\mathit{product} = \mathit{foldr}\,(\times)\,1} computes the product of a list of integers).

But Horner’s Rule is not restricted to sums and products; the essential properties are that addition and multiplication are associative, that multiplication has a unit, and that multiplication distributes over addition. This the algebraic structure of a semiring (but without needing commutativity and a unit of addition, or that that unit is a zero of multiplication). In particular, the so-called tropical semiring on the integers, in which “addition” is binary {\max} and “multiplication” is integer addition, satisfies the requirements. So for the maximum segment sum problem, we get

\displaystyle  \mathit{maximum} \cdot \mathit{map}\,\mathit{sum} \cdot \mathit{inits} = \mathit{foldr}\,(\oplus)\,e \quad \mathbf{where}\; e = 0 \mathbin{;} u \oplus z = e \max (u + z)

Moreover, {\oplus} takes constant time, so this gives a linear-time algorithm for {\mathit{mss}}.

Tail segments, datatype-generically

About a decade after the initial “theory of lists” work on the maximum segment sum problem, Richard Bird (with Oege de Moor and Paul Hoogendijk) came up with a datatype-generic version of the problem in the paper Generic functional programming with types and relations. It’s clear what “maximum” and “sum” mean generically, but not so clear what “segment” means for nonlinear datatypes; the point of their paper is basically to resolve that issue.

Recalling the definition of {\mathit{segs}} in terms of {\mathit{inits}} and {\mathit{tails}}, we see that it would suffice to develop datatype-generic notions of “initial segment” and “tail segment”. One fruitful perspective is given in Bird & co’s paper: a “tail segment” of a cons list is just a subterm of that list, and an “initial segment” is the list but with some tail (that is, some subterm) replaced with the empty structure.

So, representing a generic “tail” of a data structure is easy: it’s a data structure of the same type, and a subterm of the term denoting the original structure. A datatype-generic definition of {\mathit{tails}} is a little trickier, though. For lists, you can see it as follows: every node of the original list is labelled with the subterm of the original list rooted at that node. I find this a helpful observation, because it explains why the {\mathit{tails}} of a list is one element longer than the list itself: a list with {n} elements has {n+1} nodes ({n} conses and a nil), and each of those nodes gets labelled with one of the {n+1} subterms of the list. Indeed, {\mathit{tails}} ought morally to take a possibly empty list and return a non-empty list of possibly empty lists—there are two different datatypes involved. Similarly, if one wants the “tails” of a data structure of a type in which some nodes have no labels (such as leaf-labelled trees, or indeed such as the “nil” constructor of lists), one needs a variant of the datatype providing labels at those positions. Also, for a data structure in which some nodes have multiple labels, or in which there are different types of labels, one needs a variant for which every node has precisely one label.

Bird & co call this the labelled variant of the original datatype; if the original is a polymorphic datatype {\mathsf{T}\,\alpha = \mu(\mathsf{F}\,\alpha)} for some binary shape functor {\mathsf{F}}, then the labelled variant is {\mathsf{L}\,\alpha = \mu(\mathsf{G}\,\alpha)} where {\mathsf{G}\,\alpha\,\beta = \alpha \times \mathsf{F}\,1\,\beta}—whatever labels {\mathsf{F}} may or may not have specified are ignored, and precisely one label per node is provided. Given this insight, it is straightforward to define a datatype-generic variant {\mathit{subterms}} of the {\mathit{tails}} function:

\displaystyle  \mathit{subterms}_{\mathsf{F}} = \mathit{fold}_{\mathsf{F}}(\mathit{in}_{\mathsf{G}} \cdot \mathit{fork}(\mathit{in}_{\mathsf{F}} \cdot \mathsf{F}\,\mathit{id}\,\mathit{root}, \mathsf{F}\,!\,\mathit{id})) :: \mathsf{T}\,\alpha \rightarrow \mathsf{L}(\mathsf{T}\,\alpha)

where {\mathit{root} = \mathit{fst} \cdot \mathit{in}_{\mathsf{G}}^{-1} = \mathit{fold}_{\mathsf{G}}\,\mathit{fst} :: \mathsf{L}\,\alpha \rightarrow \alpha} returns the root label of a labelled data structure, and {!_{\alpha} :: \alpha \rightarrow 1} is the unique arrow to the unit type. (Informally, having computed the tree of subterms for each child of a node, we make the tree of subterms for this node by assembling all the child trees with the label for this node; the label should be the whole structure rooted at this node, which can be reconstructed from the roots of the child trees.) What’s more, there’s a datatype-generic scan lemma too:

\displaystyle  \begin{array}{lcl} \mathit{scan}_{\mathsf{F}} &::& (\mathsf{F}\,\alpha\,\beta \rightarrow \beta) \rightarrow \mathsf{T}\,\alpha \rightarrow \mathsf{L}\,\beta \\ \mathit{scan}_{\mathsf{F}}\,\phi &=& \mathsf{L}\,(\mathit{fold}_{\mathsf{F}}\,\phi) \cdot \mathit{subterms}_{\mathsf{F}} \\ &=& \mathit{fold}_{\mathsf{F}}(\mathit{in}_{\mathsf{G}} \cdot \mathit{fork}(\phi \cdot \mathsf{F}\,\mathit{id}\,\mathit{root}, \mathsf{F}\,!\,\mathit{id})) \end{array}

(Again, the label for each node can be constructed from the root labels of each of the child trees.) In fact, {\mathit{subterms}} and {\mathit{scan}} are paramorphisms, and can also be nicely written coinductively as well as inductively. I’ll return to this in a future post.

Initial segments, datatype-generically

What about a datatype-generic “initial segment”? As suggested above, that’s obtained from the original data structure by replacing some subterms with the empty structure. Here I think Bird & co sell themselves a little short, because they insist that the datatype {\mathsf{T}} supports empty structures, which is to say, that {\mathsf{F}} is of the form {\mathsf{F}\,\alpha\,\beta = 1 + \mathsf{F}'\,\alpha\,\beta} for some {\mathsf{F}'}. This isn’t necessary: for an arbitrary {\mathsf{F}}, we can easily manufacture the appropriate datatype {\mathsf{U}} of “data structures in which some subterms may be replaced by empty”, by defining {\mathsf{H}\,\alpha\,\beta = 1 + \mathsf{F}\,\alpha\,\beta} and {\mathsf{U}\,\alpha = \mu(\mathsf{H}\,\alpha)}.

As with {\mathit{subterms}}, the datatype-generic version of {\mathit{inits}} is a bit trickier—and this time, the special case of lists is misleading. You might think that because a list has just as many initial segments as it does tail segments, so the labelled variant ought to suffice just as well here too. But this doesn’t work for non-linear data structures such as trees—in general, there are many more “initial” segments than “tail” segments (because one can make independent choices about replacing subterms with the empty structure in each child), and they don’t align themselves conveniently with the nodes of the original structure.

The approach I prefer here is just to use an unstructured collection type to hold the “initial segments”; that is, a monad. This could be the monad of finite lists, or of finite sets, or of finite bags—we will defer until later the discussion about precisely which, and write simply {\mathsf{M}}. We require only that it provide a {\mathit{MonadPlus}}-like interface, in the sense of an operator {\mathit{mplus} :: \mathsf{M}\,\alpha \times \mathsf{M}\,\alpha \rightarrow \mathsf{M}\,\alpha}; however, for reasons that will become clear, we will expect that it does not provide a {\mathit{mzero}} operator yielding empty collections.

Now we can think of the datatype-generic version of {\mathit{inits}} as nondeterministically pruning a data structure by arbitrarily replacing some subterms with the empty structure; or equivalently, as generating the collection of all such prunings.

\displaystyle  \mathit{prune} = \mathit{fold}_{\mathsf{F}}(\mathsf{M}\,\mathit{in}_{\mathsf{H}} \cdot \mathit{opt}\,\mathit{Nothing} \cdot \mathsf{M}\,\mathit{Just} \cdot \delta_2) :: \mu(\mathsf{F}\,\alpha) \rightarrow \mathsf{M}(\mu(\mathsf{H}\,\alpha))

Here, {\mathit{opt}} supplies a new alternative for a nondeterministic computation:

\displaystyle  opt\,a\,\mathit{mx} = \mathit{return}\,a \mathbin{\underline{\smash{\mathit{mplus}}}} \mathit{mx}

and {\delta_2 :: (\mathsf{F}\,\alpha)\mathsf{M} \mathbin{\stackrel{.}{\to}} \mathsf{M}(\mathsf{F}\alpha)} distributes the shape functor {\mathsf{F}} over the monad {\mathsf{M}} (which can be defined for all {\mathit{Traversable}} functors {\mathsf{F}\,\alpha}). Informally, once you have computed all possible ways of pruning each of the children of a node, a pruning of the node itself is formed either as {\mathit{Just}} some node assembled from arbitrarily pruned children, or {\mathit{Nothing}} for the empty structure.

Horner’s Rule, datatype-generically

As we’ve seen, the essential property behind Horner’s Rule is one of distributivity. In the datatype-generic case, we will model this as follows. We are given an {(\mathsf{F}\,\alpha)}-algebra {(\beta,f)}, and a {\mathsf{M}}-algebra {(\beta,k)}; you might think of these as “datatype-generic product” and “collection sum”, respectively. Then there are two different methods of computing a {\beta} result from an {\mathsf{F}\,\alpha\,(\mathsf{M}\,\beta)} structure: we can either distribute the {\mathsf{F}\,\alpha} structure over the collection(s) of {\beta}s, compute the “product” {f} of each structure, and then compute the “sum” {k} of the resulting products; or we can “sum” each collection, then compute the “product” of the resulting structure. Distributivity of “product” over “sum” is the property that these two different methods agree, as illustrated in the following diagram.

For example, with {f :: \mathsf{F}\,{\mathbb Z}\,{\mathbb Z} \rightarrow {\mathbb Z}} adding all the integers in an {\mathsf{F}}-structure, and {k :: \mathsf{M}\,{\mathbb Z} \rightarrow {\mathbb Z}} finding the maximum of a (non-empty) collection, the diagram commutes. (To match up with the rest of the story, we have presented distributivity in terms of a bifunctor {\mathsf{F}}, although the first parameter {\alpha} plays no role. We could just have well have used a unary functor, dropping the {\alpha}, and changing the distributor to {\delta :: \mathsf{F}\mathsf{M} \mathbin{\stackrel{.}{\to}} \mathsf{M}\mathsf{F}}.)

Note that {(\beta,k)} is required to be an algebra for the monad {\mathsf{M}}. This means that it is not only an algebra for {\mathsf{M}} as a functor (namely, of type {\mathsf{M}\,\beta \rightarrow \beta}), but also it should respect the extra structure of the monad: {k \cdot \mathit{return} = \mathit{id}} and {k \cdot \mathit{join} = k \cdot \mathsf{M}\,k}. For the special case of monads for associative collections (such as lists, bags, and sets), and in homage to the old Squiggol papers, we will stick to reductions{k}s of the form {\oplus/} for associative binary operator {{\oplus} :: \beta \times \beta \rightarrow \beta}; then we also have distribution over choice: {\oplus / (x \mathbin{\underline{\smash{\mathit{mplus}}}} y) = (\oplus/x) \oplus (\oplus/y)}. Note also that we prohibited empty collections in {\mathsf{M}}, so we do not need a unit for {\oplus}.

Recall that we modelled an “initial segment” of a structure of type {\mu(\mathsf{F}\,\alpha)} as being of type {\mu(\mathsf{H}\,\alpha)}, where {\mathsf{H}\,\alpha\,\beta = 1 + \mathsf{F}\,\alpha\,\beta}. We need to generalize “product” to work on this extended structure, which is to say, we need to specify the value {b} of the “product” of the empty structure too. Then we let {g = \mathit{maybe}\,b\,f :: \mathsf{H}\,\alpha\,\beta \rightarrow \beta}, so that {\mathit{fold}_{\mathsf{H}}(g) :: \mu(\mathsf{H}\,\alpha) \rightarrow \beta}.

The datatype-generic version of Horner’s Rule is then about computing the “sum” of the “products” of each of the “initial segments” of a data structure:

\displaystyle  {\oplus/} \cdot \mathsf{M}(\mathit{fold}_{\mathsf{H}}(g)) \cdot \mathit{prune}

We will use fold fusion to show that this can be computed as a single fold, given the necessary distributivity property.

\displaystyle  \begin{array}{ll} & \mathord{\oplus/} \cdot \mathsf{M}(\mathit{fold}_{\mathsf{H}}(g)) \cdot \mathit{prune} \cdot \mathit{in}_{\mathsf{F}} \\ = & \qquad \{ \mbox{evaluation for~} \mathit{prune} \} \\ & \mathord{\oplus/} \cdot \mathsf{M}(\mathit{fold}_{\mathsf{H}}(g)) \cdot \mathsf{M}\,\mathit{in}_{\mathsf{H}} \cdot \mathit{opt}\,\mathit{Nothing} \cdot \mathsf{M}\,\mathit{Just} \cdot \delta_2 \cdot \mathsf{F}\,\mathit{id}\,\mathit{prune} \\ = & \qquad \{ \mbox{functors; evaluation for~} \mathit{fold}_{\mathsf{H}} \} \\ & \mathord{\oplus/} \cdot \mathsf{M}(g \cdot \mathsf{H}\,\mathit{id}\,(\mathit{fold}_{\mathsf{H}}(g))) \cdot \mathit{opt}\,\mathit{Nothing} \cdot \mathsf{M}\,\mathit{Just} \cdot \delta_2 \cdot \mathsf{F}\,\mathit{id}\,\mathit{prune} \\ = & \qquad \{ \mathsf{M}\,h \cdot \mathit{opt}\,a = \mathit{opt}\,(h\,a) \cdot \mathsf{M}\,h \} \\ & \mathord{\oplus/} \cdot \mathit{opt}\,(g\,\mathit{Nothing}) \cdot \mathsf{M}(g \cdot \mathsf{H}\,\mathit{id}\,(\mathit{fold}_{\mathsf{H}}(g))) \cdot \mathsf{M}\,\mathit{Just} \cdot \delta_2 \cdot \mathsf{F}\,\mathit{id}\,\mathit{prune} \\ = & \qquad \{ \mbox{functors;~} \mathit{Just} :: \mathsf{F}\,\alpha \mathbin{\stackrel{.}{\to}} \mathsf{H}\,\alpha \} \\ & \mathord{\oplus/} \cdot \mathit{opt}\,(g\,\mathit{Nothing}) \cdot \mathsf{M}\,g \cdot \mathsf{M}(\mathit{Just} \cdot \mathsf{F}\,\mathit{id}\,(\mathit{fold}_{\mathsf{H}}(g))) \cdot \delta_2 \cdot \mathsf{F}\,\mathit{id}\,\mathit{prune} \\ = & \qquad \{ \mbox{functors;~} \delta_2 :: (\mathsf{F}\alpha)\mathsf{M} \mathbin{\stackrel{.}{\to}} \mathsf{M}(\mathsf{F}\alpha) \} \\ & \mathord{\oplus/} \cdot \mathit{opt}\,(g\,\mathit{Nothing}) \cdot \mathsf{M}(g \cdot \mathit{Just}) \cdot \delta_2 \cdot \mathsf{F}\,\mathit{id}\,(\mathsf{M}(\mathit{fold}_{\mathsf{H}}(g))) \cdot \mathsf{F}\,\mathit{id}\,\mathit{prune} \end{array}

(Sadly, I have to break this calculation in two to get it through WordPress’s somewhat fragile LaTeX processor… where were we? Ah, yes:)

\displaystyle  \begin{array}{ll} & \mathord{\oplus/} \cdot \mathit{opt}\,(g\,\mathit{Nothing}) \cdot \mathsf{M}(g \cdot \mathit{Just}) \cdot \delta_2 \cdot \mathsf{F}\,\mathit{id}\,(\mathsf{M}(\mathit{fold}_{\mathsf{H}}(g))) \cdot \mathsf{F}\,\mathit{id}\,\mathit{prune} \\ = & \qquad \{ g = \mathit{maybe}\,b\,f \} \\ & \mathord{\oplus/} \cdot \mathit{opt}\,b \cdot \mathsf{M}\,f \cdot \delta_2 \cdot \mathsf{F}\,\mathit{id}\,(\mathsf{M}(\mathit{fold}_{\mathsf{H}}(g))) \cdot \mathsf{F}\,\mathit{id}\,\mathit{prune} \\ = & \qquad \{ {\oplus/} \cdot \mathit{opt}\,b = (b\oplus) \cdot {\oplus/} \} \\ & (b\oplus) \cdot {\oplus/} \cdot \mathsf{M}\,f \cdot \delta_2 \cdot \mathsf{F}\,\mathit{id}\,(\mathsf{M}(\mathit{fold}_{\mathsf{H}}(g))) \cdot \mathsf{F}\,\mathit{id}\,\mathit{prune} \\ = & \qquad \{ \mbox{distributivity:~} {\oplus/} \cdot \mathsf{M}\,f \cdot \delta_2 = f \cdot \mathsf{F}\,\mathit{id}\,(\oplus/) \} \\ & (b\oplus) \cdot f \cdot \mathsf{F}\,\mathit{id}\,(\oplus/) \cdot \mathsf{F}\,\mathit{id}\,(\mathsf{M}(\mathit{fold}_{\mathsf{H}}(g))) \cdot \mathsf{F}\,\mathit{id}\,\mathit{prune} \\ = & \qquad \{ \mbox{functors} \} \\ & (b\oplus) \cdot f \cdot \mathsf{F}\,\mathit{id}\,({\oplus/} \cdot \mathsf{M}(\mathit{fold}_{\mathsf{H}}(g)) \cdot \mathit{prune}) \end{array}


\displaystyle  {\oplus/} \cdot \mathsf{M}(\mathit{fold}_{\mathsf{H}}(\mathit{maybe}\,b\,f)) \cdot \mathit{prune} = \mathit{fold}_{\mathsf{F}}((b\oplus) \cdot f)

(Curiously, it doesn’t seem to matter what value is chosen for {b}.)

Maximum segment sum, datatype-generically

We’re nearly there. We start with the traversable shape bifunctor {\mathsf{F}}, a collection monad {\mathsf{M}}, and a distributive law {\delta_2 :: (\mathsf{F}\,\alpha)\mathsf{M} \mathbin{\stackrel{.}{\to}} \mathsf{M}(\mathsf{F}\alpha)}. We are given an {(\mathsf{F}\,\alpha)}-algebra {(\beta,f)}, an additional element {b :: \beta}, and a {\mathsf{M}}-algebra {(\beta,{\oplus/})}, such that {f} and {\oplus} take constant time and {f} distributes over {\oplus/} in the sense above. Then

\displaystyle  {\oplus/} \cdot \mathsf{M}(\mathit{fold}_{\mathsf{H}}(\mathit{maybe}\,b\,f)) \cdot \mathit{segs}

can be computed in linear time, where

\displaystyle  \mathit{segs} = \mathit{join} \cdot \mathsf{M}\,\mathit{prune} \cdot \mathit{contents}_{\mathsf{L}} \cdot \mathit{subterms} :: \mu(\mathsf{F}\,\alpha) \rightarrow \mathsf{M}(\mu(\mathsf{H}\,\alpha))

and where

\displaystyle  \mathit{contents}_{\mathsf{L}} :: \mathsf{L} \mathbin{\stackrel{.}{\to}} \mathsf{M}

computes the contents of an {\mathsf{L}}-structure (which, like {\delta_2}, can be defined using the traversability of {\mathsf{F}}). Here’s the calculation:

\displaystyle  \begin{array}{ll} & \mathord{\oplus/} \cdot \mathsf{M}(\mathit{fold}_{\mathsf{H}}(\mathit{maybe}\,b\,f)) \cdot \mathit{segs} \\ = & \qquad \{ \mbox{definition of~} \mathit{segs} \} \\ & \mathord{\oplus/} \cdot \mathsf{M}(\mathit{fold}_{\mathsf{H}}(\mathit{maybe}\,b\,f)) \cdot \mathit{join} \cdot \mathsf{M}\,\mathit{prune} \cdot \mathit{contents}_{\mathsf{L}} \cdot \mathit{subterms} \\ = & \qquad \{ \mbox{naturality of~} \mathit{join} :: \mathsf{M}\mathsf{M} \mathbin{\stackrel{.}{\to}} \mathsf{M}\mbox{; functors} \} \\ & \mathord{\oplus/} \cdot \mathit{join} \cdot \mathsf{M}(\mathsf{M}(\mathit{fold}_{\mathsf{H}}(\mathit{maybe}\,b\,f)) \cdot\mathit{prune}) \cdot \mathit{contents}_{\mathsf{L}} \cdot \mathit{subterms} \\ = & \qquad \{ \oplus/ \mbox{~is an~} \mathsf{M}\mbox{-algebra; functors} \} \\ & \mathord{\oplus/} \cdot \mathsf{M}({\oplus/} \cdot \mathsf{M}(\mathit{fold}_{\mathsf{H}}(\mathit{maybe}\,b\,f)) \cdot\mathit{prune}) \cdot \mathit{contents}_{\mathsf{L}} \cdot \mathit{subterms} \\ = & \qquad \{ \mbox{naturality of~} \mathit{contents} :: \mathsf{L} \mathbin{\stackrel{.}{\to}} \mathsf{M} \} \\ & \mathord{\oplus/} \cdot \mathit{contents}_{\mathsf{L}} \cdot \mathsf{L}({\oplus/} \cdot \mathsf{M}(\mathit{fold}_{\mathsf{H}}(\mathit{maybe}\,b\,f)) \cdot\mathit{prune}) \cdot \mathit{subterms} \\ = & \qquad \{ \mbox{Horner's Rule} \} \\ & \mathord{\oplus/} \cdot \mathit{contents}_{\mathsf{L}} \cdot \mathsf{L}(\mathit{fold}_{\mathsf{F}}((b\oplus)\cdot f)) \cdot \mathit{subterms} \\ = & \qquad \{ \mbox{Scan Lemma} \} \\ & \mathord{\oplus/} \cdot \mathit{contents}_{\mathsf{L}} \cdot \mathit{scan}_{\mathsf{F}}((b\oplus)\cdot f) \end{array}

The scan can be computed in linear time, because its body takes constant time; moreover, the “sum” {\oplus/} and {\mathit{contents}} can also be computed in linear time (and what’s more, they can be fused into a single pass).

For example, with {f :: \mathsf{F}\,{\mathbb Z}\,{\mathbb Z} \rightarrow {\mathbb Z}} adding all the integers in an {\mathsf{F}}-structure, {b = 0 :: {\mathbb Z}}, and {{\oplus} :: {\mathbb Z}\times{\mathbb Z} \rightarrow {\mathbb Z}} returning the greater of two integers, we get a datatype-generic version of the linear-time maximum segment sum algorithm.

Monads versus relations

As the title of their paper suggests, Bird & co carried out their development using the relational approach set out in the Algebra of Programming book; for example, their version of {\mathit{prune}} is a relation between data structures and their prunings, rather than being a function that takes a structure and returns the collection of all its prunings. There’s a well-known isomorphism between relations and set-valued functions, so their relational approach roughly looks equivalent to the monadic one I’ve taken.

I’ve known their paper well for over a decade (I made extensive use of the “labelled variant” construction in my own papers on generic downwards accumulations), but I’ve only just noticed that although they discuss the maximum segment sum problem, they don’t discuss problems based on other semirings, such as the obvious one of integers with addition and multiplication—which is, after all, the origin of Horner’s Rule. Why not? It turns out that the relational approach doesn’t work in that case!

There’s a hidden condition in the calculation, which relates back to our earlier comment about which collection monad—finite sets, finite bags, lists, etc—to use. When {\mathsf{M}} is the set monad, distribution over choice ({\oplus / (x \mathbin{\underline{\smash{\mathit{mplus}}}} y) = (\oplus/x) \oplus (\oplus/y)})—and consequently the condition {{\oplus/} \cdot \mathit{opt}\,b = (b\oplus) \cdot {\oplus/}} that we used in proving Horner’s Rule—require {\oplus} to be idempotent, because {\mathit{mplus}} itself is idempotent; but addition is not idempotent. For the same reason, the distributivity property does not hold for addition with the set monad. But everything does work out for the bag monad, for which {\mathit{mplus}} is not idempotent. The bag monad models a flavour of nondeterminism in which multiplicity of results matters—as it does for the sum-of-products instance of the problem, when two copies of the same segment should be treated differently from just one copy. Similarly, if the order of results matters—if, for example, we were looking for the “first” solution—then we would have to use the list monad rather than bags or sets. Seen from a monadic perspective, the relational approach is programming with just one monad, namely the set monad; if that monad doesn’t capture your effects faithfully, you’re stuck.

(On the other hand, there are aspects of the problem that work much better relationally. We have carefully used {\max} only for a linear order, namely the usual ordering of the integers. A partial order is more awkward monadically, because there need not be a unique maximal value. For example, it is not so easy to compute a segment with maximal sum, unless we refine the sum ordering on segments to make it once more a linear order; relationally, this works out perfectly straightforwardly. We can try the same trick of turning the relation “maximal under a partial order” into the collection-valued function “all maxima under a partial order”, but I fear that the equivalent trick on the ordering itself—turning the relation “{<}” into the collection-valued function “all values less than this one”—runs into problems from taking us outside the world of finite nondeterminism.)


About jeremygibbons

Jeremy Gibbons is Professor of Computing in Oxford University Department of Computer Science, and a fan of functional programming and patterns of computation.
This entry was posted in Uncategorized. Bookmark the permalink.

6 Responses to Horner’s Rule

  1. Graham says:

    Great post. Can’t wait for the book.

  2. Earlier this year, I implemented a proof of the program transformation for “Maximum Segment Sum” in Isabelle/HOL. If anybody is interested in getting started with Isabelle for stuff like this, you can look into it here:
    http://soren.gawis.dk/acpl/sorenh07-ACPL-final.zip (contains report and source code)

    I’m confident your book will be very enlightening, and look forward to it :-). Especially the idea of using a monadic approach instead of restricting to the relational approach taken by Bird and de Moor. Maybe this will also be more amenable to implementation in a mechanized proof environment – I haven’t looked much into that yet.

  3. Hm. I fear that the “strictly non-empty collections” idea doesn’t sit nicely with the use of distributivity of the shape over the monad: for shapes that allow empty structures (such as the “nil” of lists), empty collections turn up. So I need to allow empty collections (MonadZero as well as MonadPlus, if you like), and to assume an additional element e :: Beta as the result of k on the empty collection; e should be the unit of oplus, and in some suitable sense the zero of f (it’ll be the zero of otimes, in the next post.) Oh well.

  4. rogushy says:

    Delightful exploration of the scope of applicability of Horner’s Rule. What’s your second most favorite calculation?

  5. Pingback: Distributivity in Horner’s Rule | Patterns in Functional Programming

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s