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.