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\; =\; foldr\; (\ll )\; e\; f\; =\; foldl\; (\gg )\; e$

there exists some associative binary operator

$f\; []\; =\; e\; f\; [a]\; =\; a\; \ll \; e\; =\; e\; \gg \; a\; f\; (xs\; \u29fa\; ys)\; =\; f\; xs\; \u229a\; 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

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

Can we come up with a method to derive

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\; (\ll )\; (x:xs,a)\; =\; x\; \ll \; foldrp\; (\ll )\; (xs,a)\; foldlp\; (\gg )\; (a,[])\; =\; a\; foldlp\; (\gg )\; (a,\; xs\u29fa[x])\; =\; foldlp\; (\gg )\; (a,xs)\; \gg \; 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\u29fays)\; =\; foldrp\ll \; (xs,\; foldr\ll \; e\; ys)\; foldl\; (\gg )\; e\; (xs\u29fays)\; =\; foldlp\ll \; (foldl\; \ll \; 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

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\; .\; S\xb0\; .\; S\; =\; S$

where

Recall our aim: given

### Proving the Theorem

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

Lemma 1:

f = foldr (≪) e = f = foldl (≫) e implies thatf is prefix and postfix insensitive. That is:$f\; xs\; =\; f\; xs\u2019\; \wedge \; f\; ys\; =\; f\; ys\u2019\; \Rightarrow \; f\; (xs\u29fays)\; =\; f\; (xs\u2019\u29fays\u2019).$

In point-free style:

f . cat . (f°. f × f°. f) = f . cat .

Once we have the lemma proved, the theorem follows by taking

The proof of Lemma 1 is simply some applications of (1), (2), and

$f\; .\; cat\; =\{\; (1)\; \}foldrp\; (\ll )\; .\; (id\; \times \; f)\; =\{\; since\mathrm{f\; .\; f\xb0\; .\; f\; =\; f}\}foldrp\; (\ll )\; .\; (id\; \times \; f)\; .\; (id\; \times \; f\xb0\; .\; f)\; =\{\; (1)\; \}f\; .\; cat\; .\; (id\; \times \; f\xb0\; .\; f)\; =\{\; (2)\; \}foldlp\; (\gg )\; .\; (f\; \times \; id)\; .\; (id\; \times \; f\xb0\; .\; f)\; =\{\; since\mathrm{f\; .\; f\xb0\; .\; f\; =\; f}\}foldlp\; (\gg )\; .\; (f\; \times \; id)\; .\; (f\xb0\; .\; f\; \times \; f\xb0\; .\; f)\; =\{\; (2)\; \}f\; .\; cat\; .\; (f\xb0\; .\; f\; \times \; f\xb0\; .\; 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

For example, consider the special case

For

### Some more Properties

Some more properties are needed to deal with

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

When simple approaches of refining

$\u229a\; =\; f\; .\; cat\; .\; (f\xb0\times \; f\xb0)\; =\{\; (1)\; \}foldrp\; (\ll )\; .\; (id\; \times \; f)\; .\; (f\xb0\times \; f\xb0)\; \supseteq \{\; since\mathrm{f\; .\; f\xb0\; \supseteq \; ran\; f}\}foldrp\; (\ll )\; .\; (f\xb0\times \; ran\; f)\; =\{\; since\mathrm{f\; =\; foldl\; \gg \; []}\}foldrp\; (\ll )\; .\; ((foldl\; \gg \; [])\xb0\times \; ran\; f)$

Symetrically,

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

### Scanr “from the Middle”

Finally, consider

$scanr\; \u229b\; e\; =\; foldr\; \ll \; [e]\; x\; \ll \; (y\; :\; xs)\; =\; x\; \u229b\; y\; :\; y\; :\; xs\; scanr\; \u229b\; e\; =\; foldl\; \gg \; [e]\; xs\; \gg \; x\; =\; map\; (\u229bx)\; xs\; \u29fa\; [e]$

From

$xs\; \u229a\; (x\; :\; y\; :\; ys)\; =\{\; (4)\; \}foldlp\; (\gg )\; (xs,\; (foldr\; \ll \; [e])\xb0\; (x\; :\; y\; :ys))\; =\{\; definition\; of\ll ,\; let\mathrm{z\; \u229b\; y\; =\; x}\}foldlp\; (\gg )\; (xs,\; z\; :\; (foldr\; \ll \; [e])\xb0\; (y\; :ys))\; =\{\; (3)\; \}foldlp\; (\gg )\; (xs\; \gg \; z,\; (foldr\; \ll \; [])\xb0\; (y\; :ys))\; =\{\; (4)\; \}(xs\; \gg \; z)\; \u229a\; (y\; :\; ys)\; =\{\; induction\; \}map\; (\u229b\; y)\; (xs\; \gg \; z)\; \u29fa\; ys\; =\{\; definition\; of\gg \}map\; (\u229b\; y)\; (map\; (\u229b\; z)\; xs\; \u29fa\; [e])\; \u29fa\; ys\; =\{\; map,eidentity\; \}map\; (\lambda v\; \to \; (v\; \u229b\; y)\; \u229b\; z)\; xs\; \u29fa\; [y]\; \u29fa\; ys\; =\{\; associtivity\; of\u229b\}map\; (\lambda v\; \to \; v\; \u229b\; (y\; \u229b\; z))\; xs\; \u29fa\; [y]\; \u29fa\; ys\; =\{\mathrm{z\; \u229b\; y\; =x}\}map\; (\u229b\; x)\; xs\; \u29fa\; [x]\; \u29fa\; (y:ys)$

### Prologue

Given the complexity of the proof above, I did not think there was a hope to automatically construct

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,

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.

Pingback: Tiempo finito y logarítmico » Tercer teorema de homomorfismo