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.

8 thoughts on “Determining List Steepness in a Homomorphism”

  1. Just 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

    1. Thanks 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.

  2. WordPress 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].

    1. Thanks 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.

      1. 1) 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?

  3. If 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]

    1. Sorry, 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!

Leave a Comment

Your email address will not be published. Required fields are marked *