# Determining List Steepness in a Homomorphism

The steep list problem is an example we often use when we talk about tupling. A list of numbers is called steep if each element is larger than the sum of elements to its right. Formally,

```steep [] = True steep (x : xs) = x > sum xs ∧ steep xs```

The definition above is a quadratic-time algorithm. Can we determine the steepness of a list in linear time? To do so, we realise that we have to compute some more information. Let `steepsum = ⟨steep, sum⟩` where `⟨f, g⟩ x = (f x, g x)`, we discover that `steepsum` can be computed as a `foldr`:

``````steepsum = foldr step (True, 0)
where step x (b, s) = (x > s ∧ b, s + b)``````

which takes linear time. After computing `steepsum`, simply take `steep = fst . steepsum`.

In the Software Construction course we also talked about list homomorphism, that is, functions that can be defined in the form

```h [] = e h [a] = f a h (xs ⧺ ys) = h xs ⊚ h ys```

where `⊚` is associative and `e` is the identity element of `⊚`. The discussion would be incomplete if we didn’t mention the third homomorphism theorem: if a function on lists can be computed both from right to left and from left to right, that it, both by a `foldr` and a `foldl`, it can be computed from anywhere in the middle by a homomorphism, which has the potential of being parallelised. Hu sensei had this idea using `steepsum` as an exercise: can we express `steepsum` as a `foldl`, and a list homomorphism?

Unfortunately, we cannot — `steepsum` is not a `foldl`. To determining the steepness from left to right, we again have to compute some more information — not necessarily in the form of a tuple.

### Right Capacity

The first idea would be to tuple `steepsum` with yet another element, some information that would allow us to determine what could be appended to the right of the input. Given a list of numbers `xs`, let `rcap xs` (for right capacity) be an (non-inclusive) upperbound: a number `y < rcap xs` can be safely appended to the right of `xs` without invalidating the steepness within `xs`. It can be defined by:

```rcap [] = ∞ rcap (x : xs) = (x - sum xs) ↓ rcap xs```

where `↓` stands for binary minimum. For an explanation of the second clause, consider `x : xs ⧺ [y]`. To make it a steep list, `y` has to be smaller than `x - sum xs` and, furthermore, `y` has to be small enough so that `xs ⧺ [y]` is steep. For example, `rcap [9,5]` is `4`, therefore `[9,5,3]` is still a steep list.

Following the theme of tupling, one could perhaps try to construct `⟨steep, sum, rcap⟩` as a `foldl`. By doing so, however, one would soon discover that `rcap` itself contains all information we need. Firstly, a list `xs` is steep if and only if `rcap xs` is greater than `0`:
Lemma 1: `steep xs ⇔ rcap xs > 0`.
Proof: induction on `xs`.
case `[]`: `True ⇔ ∞ > 0`.
case `(x : xs)`:

``````         steep (x : xs)
⇔ x > sum xs ∧ steep xs
⇔ x - sum xs > 0  ∧ steep xs
⇔   { induction }
x - sum xs > 0 ∧ 0 < rcap xs
⇔ ((x - sum xs) ↓ rcap xs) > 0
⇔ rcap (x : xs) > 0``````

Secondly, it turns out that `rcap` is itself a `foldl`:
Lemma 2: `rcap (xs ⧺ [x]) = (rcap xs - x) ↓ x`.
Proof: induction on `xs`.
case `[]`: `rcap [x] = x = (∞ - x) ↓ x`.
case `(y : xs)`:

``````         rcap (y : xs ⧺ [x])
= ((y - sum xs) - x) ↓ rcap (xs ⧺ [x])
=   { induction }
((y - sum xs) - x) ↓ (rcap xs - x) ↓ x
=   { since (a - x) ↓ (b -x) = (a ↓ b) -x }
(((y - sum xs) ↓ rcap xs) - x) ↓ x
= (rcap (y : xs) - x) ↓ x``````

Therefore we have `rcap = foldl (λ y x → (y - x) ↓ x) ∞`. If the aim were to determine steepness from left to right, our job would be done.

However, the aim is to determine steepness from both directions. To efficiently compute `rcap` using a `foldr`, we still need to tuple `rcap` with `sum`. In summary, the function `⟨sum, rcap⟩` can be computed both in terms of a `foldl`:

``````⟨sum, rcap⟩ = foldl step (0, ∞)
where step (s, y) x = (s + x, (y - x) ↓ x)
``````

and a `foldr`:

``````⟨sum, rcap⟩ = foldr step (0, ∞)
where step x (s, y) = (x + s, (x - s) ↓ y)
``````

Now, can we compute `⟨sum, rcap⟩` by a list homomorphism?

### List Homomorphism

Abbreviate `⟨sum, rcap⟩` to `sumcap`. The aim now is to construct `⊚` such that `sumcap (xs ⧺ ys) = sumcap xs ⊚ sumcap ys`. The paper Automatic Inversion Generates Divide-and-Conquer Parallel Programs by Morita et al. suggested the following approach (which I discussed, well, using more confusing notations, in a previous post): find a weak inverse of `⟨sum, rcap⟩`, that is, some `g` such that `sumcap (g z) = z` for all `z` in the range of `sumcap`. Then we may take `z ⊚ w = sumcap (g z ⧺ g w)`.

For this problem, however, I find it hard to look for the right `g`. Anyway, this is the homomorphism that seems to work:

``````
sumcap [] = (0, ∞)
sumcap [x] = (x, x)
sumcap (xs ⧺ ys) = sumcap xs ⊚ sumcap ys
where (s1,c1) ⊚ (s2,c2) = (s1+s2, (c1-s2) ↓ c2)
``````

However, I basically constructed `⊚` by guessing, and proved it correct afterwards. It takes a simple inductive proof to show that `rcap (xs ⧺ ys) = (rcap xs - sum ys) ↓ rcap ys`.

I am still wondering what weak inverse of `sumcap` would lead us to the solution above, however.

# 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 \left(\ll \right) e$
f = foldl (≫) e

there exists some associative binary operator such that

$f \left[\right] = 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 \left(\ll \right) \left(\left[\right],a\right) = 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 \left(\ll \right) e \left(xs⧺ys\right) = foldrp\ll \left(xs, foldr\ll e ys\right)$
foldl (≫) e (xs⧺ys) = foldlp≪ (foldl ≪ e xs, ys)

or, in point-free style:

$foldr \left(\ll \right) e . cat = foldrp \left(\ll \right) . \left(id × foldr \left(\ll \right) e\right)$(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’ ⇒ f \left(xs⧺ys\right) = f \left(xs’⧺ys’\right).$

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:

=      { (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 \left(\ll \right) \left(xs⧺\left[x\right],a\right) = foldrp \left(\ll \right) \left(xs, x \ll a\right)$
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 as an unfold, thus forming an “unfold, then fold” pattern:

=      { (1) }
foldrp (≪) . (id × f) . (f°× f°)
⊇      { since f . f° ⊇ ran f }
foldrp (≪) . (f°× ran f)
=      { since f = foldl ≫ [] }
foldrp (≪) . ((foldl ≫ [])°× ran f)

Symetrically,

$⊚ = foldlp \left(\gg \right) . \left(ran f × \left(foldr \ll \left[\right]\right)°\right)$(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 \left[e\right]$
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:

=      { (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 , 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.