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.