Because I find this exercise ([1]) very instructive, I want to show you how the foldr fusion law can be used to derive an efficient program from a very inefficient one.

This note will let you see some important points:
– you can use mathematical theorems to actually improve your code in terms of execution efficiency;
– using theorems, you can derive solutions which are hard to construct just in an intuitive manner;
– a highly efficient solution has, in many cases, a powerful theory standing behind it

That being said, we can state the problem:

Problem. Find the ascending lists of the cartesian product of non-empty lists of integers.

Solution.

Aside.
For the solution we clearly need a way to compute the cartesian product of lists. For this, you can read a more detailed post here: http://myhaskelljournal.com/cartesian-product-of-lists/

As an example: cartprod [ [2], [1,3] ] = [ [2,1], [2,3] ]
End of Aside

Back to the solution. It’s clear that, if we take only the ascending lists from the lists produced by the cartesian product, we have all the ascending lists of this cartesian product (it’s a useful truism, so let’s use it:) ).

In symbols, what we said reduces to:

fcp = filter n . cp, where cp is the cartesian product of lists and n is a function that, given a list of integers, it’s true if and only if this list it’s ascending.

Remark. This is a correct definition of our desired function, but in order to evaluate it, we need to take into account each element produced by the cartesian product, in order to see if it’s an ascending list or not. But there are a lot of these elements (actually this algorithm is an exponential one). So what to do next?

We can think of alternative ways to solve the problem. What if we can generate from the start only the ascending lists of the cartesian product? This would be, indeed, a much much faster algorithm, because instead of searching an exponential space and filtering, we’ll generate directly the ascending lists desired.

But here stops our intuition. It’s hard to derive a directly generating algorithm from just pure intuition. Other mechanisms must be employed to arrive at a correct and efficient solution.

First of all, we’ll use a definition of cartesian product in therms of folding (exercise 1):

In this moment, we have that fcp = filter n . cp, so fcp is a composition between a foldr (the cp function) and another function.

And here comes into use the foldr fusion theorem (law) which states that, under certain precise conditions, a composition between a function and a foldr is also a foldr. This “fusioned” foldr will generate directly the ascending lists from the cartesian product, as we’ll see in what comes next.

Let’s state the foldr fusion law:

Theorem (foldr fusion law)

If we have the following properties:

  1. f is a strict function.
  2. f(g x y) = h x (f y), for all x and y in the appropriate ranges

 Put b = f(a).

Then: f . foldr g a = foldr h b.

This theorem will enable us to reduce fcp to a foldr which will generate directly the ascending lists needed.

Let’s write again what we have by now:

fcp = filter n . cp = filter n . foldr f [ [ ] ], where f xs yss = [x:ys | x <- xs, ys <- yss];

We’ll apply all we know about the stated foldr fusion law in order to transform fcp into a foldr.

First of all, the property 1 of the theorem is satisfied, because filter n is a strict function.

We’ll put b = filter n [ [ ] ] = [ [ ] ], so we have that b = [ [ ] ].

It remains to construct the function h from the theorem.

The property 2 from the theorem becomes the following in our context:

filter n (f xs yss) = h xs (filter n yss). (E1)

In this step, we can try to make something like an inductive construction based on xs or yss (the only variables we’re dealing with). As a confess, doing an induction based on xs was a pain in the neck, it is hard to do and involves too much reasoning steps.

We’ll do a kind of inductive reasoning based on yss.

Because the step 2 in the theorem must be valid for all yss, it must be valid (obviously) for concrete examples of yss.

Case 0 (Base Case). The simplest concrete case is yss = []. Using it in the equation E1, we’ll have:

filter n (f xs [ ]) = h xs (filter n [ ]) <=> filter n [ ] = h xs [ ]

Computing the left part, we have that h xs [ ] = [ ] (E2)

Case 1 (Inductive case). Let’s decompose into head and tail: ys:yss

h xs (filter n ys:yss) = filter n (f xs ys:yss)

We’ll look only at the case when ys is not ascending (the other one is similar):

filter n (f xs ys:yss) = h xs (filter n ys:yss) = {ys is not ascending} h xs (filter n yss) (E3)

But f xs ys:yss = [x:zs | x <- xs, zs <- ys:yss]

=> filter n (f xs ys:yss) = filter n [x:zs | x <- xs, zs <- ys:yss]. (E4)

Knowing that ys is not ascending, we’ll not take ys into account, so:

filter n [x:zs | x <- xs, zs <- ys:yss] = filter n [x:zs | x <- xs, zs <- yss], or changing for convenience the notation:

filter n [x:zs | x <- xs, zs <- ys:yss] = filter n [x:ys | x <- xs, ys <- yss] (E5)

From E3, E4 and E5, we conclude that:

h xs (filter n yss) = filter n [x:ys | x <- xs, ys <- yss] =

{it’s obvious I can restrict yss to the ascending lists – filter n yss}

filter n [x:zs | x <- xs, zs <- filter n yss]

So we have that:  h xs (filter n yss) =  filter n [x:zs | x <- xs, zs <- filter n yss]

Having filter n yss in both parts of the previous equation (we were heading for it), we use the standard technique to raise filter n yss to a fresh variable zss, and we have:

h xs zss = filter n [x:zs | x<-xs, zs <- zss] (E6)

Putting together E2 and E6, we constructed the function h needed:

h xs [ ] = [ ]
h xs zss = filter n [x:zs | x<-xs, zs <- zss]

Using the foldr fusion theorem, we arrived at a definition of fcp = filter n . cp in terms of foldr (of course, the function n isn’t defined for the moment, we don’t need it for the time! ):

This is all fine and good, and (giving a recursive definition for the function n that decides if a list is ascending or not) we’re done. But remains a little problem: we still have this filter n which occurs in our foldr definition and can be a source of inefficiency.

To remove the filtering and to actualy generate directly the ascending lists, let’s see what actually foldr means:

In general setting, foldr f e [x1,x2,…,xn] = f x1(f x2 (..(f xn e))..)

In our case: foldr h [ [ ] ] [l1,l2,…,ln] = h l1 (h l2 (h l3(…(h ln [ [ ] ]))..) (foldr expansion)

h xs zss = filter n [x:zs | x<-xs, zs<-zss]

h ln [ [ ] ] = [ [x] | x <- ln]

h l(n-1) (h ln [ [ ] ]) = filter n [y:zs | y <- l(n-1), zs <- [ [x] | x<-ln]], so it’s sufficient that y <= x = head zs in order to have filtered only ascending lists!

So h l(n-1) zss = [y:zs | y <- l(n-1), zs <- zss, y<= head zs]

And the reasoning goes exactly like before for all the terms of the foldr expansion.

So it’s clear by now that h can be redefined by:
h xs [ [ ] ] = [ [x] | x<-xs]
h xs zss = [y:zs | y <- xs, zs <- zss, y <= head zs]

And in this way we constructed the final definition of fcp, which (by the foldr expansion) is clear that generates only the ascending lists of the cartesian product:

End of solution.

Remark1. Doing a comparison test in WinGHCi, the inefficient solution of fcp (I’ve named it fcpi) is taking a long time:

*Main>  last (fcpi [[1..3] | i<-[1..14]])
[3,3,3,3,3,3,3,3,3,3,3,3,3,3]
(6.27 secs, 4,051,273,576 bytes)

The efficient solution derived (named fcp) is doing a lot better (time and space usage!)

*Main> last (fcp [[1..3] | i<-[1..14]])
[3,3,3,3,3,3,3,3,3,3,3,3,3,3]
(0.05 secs, 379,392 bytes)

Evaluating compiled versions of fcpi and fcp doesn’t make any difference, of course, the difference remains the same.

So indeed the fusion law helped us to optimize in space and time!

Remark2. Behind an optimization usually stands a powerful mathematical theorem. This was noticed by others too – Edsger Dijkstra said one time that the most efficient algorithms are derived by taking into account powerful mathematical theorems.

Remark3. Intuition is helped a lot when we have a little more knowledge of what’s going on mathematically. Derivation by mathematical laws is a tool that we must use in the more difficult problems that we encounter – they are precise in nature and help us to see why our programs must work in all cases!

So, in a more leibnizian note,
Calculemus!

Exercises:
  1. Derive (using the universal property of foldr) the definition of cp in terms of foldr.
  2. Verify that h from the final definition of fcp satisfies the property 2 of the foldr fusion theorem.
  3. Compute the complexity of the first definition of fcp and the last one.

————————————————–
[1] Bird, Richard. (2015) Thinking Functionally with Haskell. Cambridge University Press. (Exercise D, page 173)

Constantin Liculescu

Facebook 

Share Button