Constructing List Homomorphism from Left and Right Folds

Since Josh has already mentioned it, I had better give it a full account.

Back in 2003 when I just started my postdoc in PSD Lab in University of Tokyo, my colleagues there were discussing about the third homomorphism theorem. The theorem says that if a function f can be expressed both as a foldr and a foldl:

$f\; =\; foldr\; (\ll )\; e$
f = foldl (≫) e

there exists some associative binary operator ⊚ such that

$f\; []\; =\; e$
f [a] = a ≪ e = e ≫ a
f (xs ⧺ ys) = f xs ⊚ f ys

Being a list homomorphism implies the potential of parallel computation.

The paper we studied was, of course, The Thrid Homomorphism Theorem by Jeremy. The aim then was to automatically, or semi-automatically, derive ⊚, given ≪, ≫, and e. The motivating examples include:

• f = sum, where ⊚ can simply be +.
• f = sort, where ⊚ can be the function merge merging two sorted lists.
• f = scanr ⊛ e. While scanr appears to be an inherently sequential function, it is actually possible to compute f “from the middle”, provided that ⊛ is associative, if we take xs ⊚ (y : ys) = map (⊛y) xs ⧺ (y : ys).

Can we come up with a method to derive ⊚ for all these examples?

I myself was not particularly interested in automation. I was interested in the challenge for two reasons. Firstly, it appears that some kind of inverse function is needed. Secondly, when I looked at Jeremy’s proof, I felt there is a relational proof inside waiting to be discovered. So I tried.

Setting the Stage

For the ease of point-free calculation, we define alternatives of folds where the input is paired with the base-cases:

$foldrp\; (\ll )\; ([],a)\; =\; a$
foldrp (≪) (x:xs,a) = x ≪ foldrp (≪) (xs,a)
foldlp (≫) (a,[]) = a
foldlp (≫) (a, xs⧺[x]) = foldlp (≫) (a,xs) ≫ x

The advantage is that we can shift a suffix or a prefix of the input list to the base case. That is:

$foldr\; (\ll )\; e\; (xs⧺ys)\; =\; foldrp\ll \; (xs,\; foldr\ll \; e\; ys)$
foldl (≫) e (xs⧺ys) = foldlp≪ (foldl ≪ e xs, ys)

or, in point-free style:

$foldr\; (\ll )\; e\; .\; cat\; =\; foldrp\; (\ll )\; .\; (id\; \times \; foldr\; (\ll )\; e)$(1)
foldl (≫) e . cat = foldlp (≫) . (foldlp (≫) e × id) (2)

where cat (xs,ys) = xs ⧺ ys and (f × g) (a,b) = (f a, g b).

The key property, however, is one that was shown in (possibly among other literature) Algebra of Programming: for a simple relation (i.e. a partial function) S, we have:

$S\; .\; S°\; .\; S\; =\; S$

where ° stands for relational converse (the relational concept of an “inverse function”).

Recall our aim: given f, look for ⊚ such that f xs ⊚ f ys = f (xs⧺ys). It translates to point-free style as ⊚ . (f × f) = f . cat.

Proving the Theorem

The third homomorphism theorem is a direct corollary of the following lemma:

Lemma 1: f = foldr (≪) e = f = foldl (≫) e implies that f is prefix and postfix insensitive. That is:

$f\; xs\; =\; f\; xs’\; \wedge \; f\; ys\; =\; f\; ys’\; \Rightarrow \; f\; (xs⧺ys)\; =\; f\; (xs’⧺ys’).$

In point-free style: f . cat . (f°. f × f°. f) = f . cat.

Once we have the lemma proved, the theorem follows by taking ⊚ = f . cat . (f °× f °). It has to be a (partial) function because ⊚ . (f × f) = f . cat is a function. Futhermore, ⊚ is associative because cat is.

The proof of Lemma 1 is simply some applications of (1), (2), and S . S° . S = S:

$\; f\; .\; cat$
=      { (1) }
     foldrp (≪) . (id × f)
=      { since f . f° . f = f }
     foldrp (≪) . (id × f) . (id × f° . f)
=      { (1) }
     f . cat . (id × f° . f)
=      { (2) }
     foldlp (≫) . (f × id) . (id × f° . f)
=      { since f . f° . f = f }
     foldlp (≫) . (f × id) . (f° . f × f° . f)
=      { (2) }
     f . cat . (f° . f × f° . f)

The proof is still the same as that of Jeremy’s, but in a relational disguise.

Refining to Functions

To derive actual algorithms, we have yet to refine ⊚ = f . cat . (f°× f°) so that it uses functional components only. We shall pick some g ⊆ f° whose domain equals the range of f, such that ⊚ = f . cat . (g × g). (An equality, rather than inclusion, holds because ⊚ in both definitions are partial functions having the same domain.)

For example, consider the special case sum = foldr (+) 0 = foldl (+) 0. Here ⊚ = sum . cat . (sum°× sum°). One simple choice is to pick wrap ⊆ sum°, where wrap a = [a]. In this case a ⊚ b = sum [a, b] = a + b.

For sort, define sorted = ran sort. It is a partial function such that sorted xs = xs iff xs is sorted. Notice that sorted ⊆ sort°. Therefore, a possible choice for ⊚ would be sort . cat . (sorted × sorted) — concatenating two sorted lists, and sort them again. Jeremy then went on with this definition and proved that ⊚ = merge, taking advantage of the fact that both input lists are sorted.

Some more Properties

Some more properties are needed to deal with scanr. The following properties allow foldrp and foldrp to proceed by shifting elements of the list to the base case:

$foldrp\; (\ll )\; (xs⧺[x],a)\; =\; foldrp\; (\ll )\; (xs,\; x\; \ll \; a)$
foldlp (≫) (a, x:xs) = foldlp (≫) (a ≫ x, xs) (3)

When simple approaches of refining ⊚ = f . cat . (f°× f°) does not work, the following approach sometimes does. Since f is a fold, one may attempt to take one of the f° as an unfold, thus forming an “unfold, then fold” pattern:

$⊚\; =\; f\; .\; cat\; .\; (f°\times \; f°)$
=      { (1) }
    foldrp (≪) . (id × f) . (f°× f°)
⊇      { since f . f° ⊇ ran f }
    foldrp (≪) . (f°× ran f)
=      { since f = foldl ≫ [] }
    foldrp (≪) . ((foldl ≫ [])°× ran f)

Symetrically,

$⊚\; =\; foldlp\; (\gg )\; .\; (ran\; f\; \times \; (foldr\; \ll \; [])°)$(4)

Scanr “from the Middle”

Finally, consider f = scanr ⊛ e for some associative ⊛ with identity e (that is, e ⊛ x = x ⊛ e = x). A scan can be defined both as a foldr and a foldl as below:

$scanr\; ⊛\; e\; =\; foldr\; \ll \; [e]$
    x ≪ (y : xs) = x ⊛ y : y : xs
scanr ⊛ e = foldl ≫ [e]
    xs ≫ x = map (⊛x) xs ⧺ [e]

From ⊚ = f . cat . (f°× f°), we can prove that xs ⊚ (y : ys) = map (⊛ y) xs ⧺ ys. Here is the inductive case:

$xs\; ⊚\; (x\; :\; y\; :\; ys)$
=      { (4) }
    foldlp (≫) (xs, (foldr ≪ [e])° (x : y :ys))
=      { definition of ≪, let z ⊛ y = x }
    foldlp (≫) (xs, z : (foldr ≪ [e])° (y :ys))
=      { (3) }
    foldlp (≫) (xs ≫ z, (foldr ≪ [])° (y :ys))
=      { (4) }
    (xs ≫ z) ⊚ (y : ys)
=      { induction }
    map (⊛ y) (xs ≫ z) ⧺ ys
=      { definition of ≫ }
    map (⊛ y) (map (⊛ z) xs ⧺ [e]) ⧺ ys
=      { map, e identity }
     map (λv → (v ⊛ y) ⊛ z) xs ⧺ [y] ⧺ ys
=      { associtivity of ⊛ }
     map (λv → v ⊛ (y ⊛ z)) xs ⧺ [y] ⧺ ys
=      { z ⊛ y =x }
    map (⊛ x) xs ⧺ [x] ⧺ (y:ys)

Prologue

Given the complexity of the proof above, I did not think there was a hope to automatically construct ⊚ for a reasonably useful set of list homomorphisms. My colleagues were talking about “weak inverses” — their attempts to look for a refinement of f°, which I considered too ad-hoc.

Being just graduated from AoP, I was perhaps too arrogant and proud of all the clever derivation we did to care about automatic program construction. (Like Jeremy, in the end of my thesis I quoted “善數不用籌策 (Those who good at calculation need no mechanical aids)” from 老子 Lao Tzu. And didn’t Dijkstra say “I hardly used the computer they gave me. I was perfectly happy without it.”?) The relational method, which seemed to cover everything, gave me a false feeling that I knew the problem inside out.

Last year, however, my colleagues and I met again and I was told that they eventually published a paper on this subject:

Kazutaka Morita, Akimasa Morihata, Kiminori Matsuzaki, Zhenjiang Hu, Masato Takeichi. Automatic Inversion Generates Divide-and-Conquer Parallel Programs, PLDI 2007.

They focused on weak inverses that returns only lists with fixed lengths. The advantage is that calculations like the one above are no longer necessary — since the lists are of fixed-length, ⊚ always takes constant time. On the other hand, scanr and scanl are special cases dealt with on a different level. Such distinction is enforced by the language they allow to construct f. No, they do not seem to have handled sort. But their approach still covered a reasonably useful collection of functions.

Well, I think the moral is that we cannot just stop when it appears that is no elegant solution that suits our taste. It sometimes pays to get our hands dirty, through which we may eventually discover the beauty within.