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.

cmcqIf you guess g(s,c)=[a,b] then a bit of algebra gives:

a = max(s-c, (s+c)/2)

b = min(c, s-c/2)

If s>=3c this gives [s-c,c]

If s<=3c this gives [(s+c)/2, (s-c)/2]

cmcqSorry, that’s wrong; both those expressions only work for s>=3c. In a list of length n with rcap c, the last element must be at least c, so the second-to-last element must be at least 2c, etc. The sum is therefore at least (2^n-1)c. For c>=0 this gives g(s,s)=[s] and g(s,c)=[s-c,c] for s>=3c. For s<3c=(2^n-1)c and use g(s,c)=[s+2^(n-1)c, 2^(n-2)c, ..., 2c, c].

Surely the definition of sumcap won’t come from this inverse though!

cmcqWordPress ate my definition of g:

For s<3c<0, pick n such that s<=(2^n-1)c and use g(s,c)=[s+2^(n-1)c, 2^(n-2)c, ..., 2c, c].

ShinPost authorThanks for the interesting comments, cmcq. Indeed it is harder than it looks.

The first guess of mine (and some students here) was:

`g (s, c) = [(s+c)/2, (s-c)/2]`

. Not only was that wrong (it fails for, e.g,`(8,8)`

, output of`sumcap [8]`

), but also forces us to move from integer to rational (that was why I was vague about the type of “numbers” in the post).I’ve been thinking: 1) is it possible to find an inverse that produces a constant-length list? 2) Can we stay within

`Int`

, if the input is`Int`

? Goal 1) is essential for deriving`⊚`

, and 2) is desirable because the`⊚`

that eventually worked does operate on integers only.You seem to have shown that goal 1) is hard to achieve. Well, perhaps the construction of list homomorphism by inverses is just not as widely applicable as we’ve expected.

cmcq1) No, because s>=(2^n-1)c where n is the list length. For negative c this puts a lower bound on n. For example [-8,-4,-2,-1] has s=-15, c=-1, so -15>=(2^n-1)*(-1), which gives n>=4.

A technique based on fixed-length inverses is very restricted: they can’t compute length!

2) You don’t need rationals ever: for sumcaps of two element lists you can use g(s,c)=[s-c,c]. Though personally I would not hesitate to extend the ring of numbers if it gave a simpler proof! Isn’t that what proof irrelevance is all about?

Matías GiovanniniGreat post! Shin-Cheng, your RSS feed is broken. I’d love to subscribe, but unfortunately the XML parser in Firefox 3.0.x complains.

ShinPost authorThanks for the encouragement! I’ve been relying on WordPress to generate the RSS (was this the link you tried?). What error message did you see? I’ll check whether other WordPress users had the same problem.

Mark EsselJust had time to scan the top few paragraphs, I’m interested enough to come back and do some homework. In a world with no free time, we still find time to have some fun :D