Practicing derivations: example #1

MSS.md

Thirty years ago, Jon Bentley wrote "Programming Pearls", a collection of great (imperative) algorithms. One of them was to find the maximum segment sum:

Given a list of numbers, the task is to compute the largest possible sum of a consecutive segment.

The "pearls" schtick caught on in the FP community, which came up with a research paper (of course) called "Functional pearls". In his book "Pearls of functional algorithm design", Richard Bird calculates an efficient version by derivation.

It starts with the specification:

mss :: [Int] -> Int
mss = max . map sum . segments

segments :: [Int] -> [[Int]]
segments = concat . map inits . tails

tails :: [a] -> [[a]]
tails [] = [[]]
tails (x:xs) = (x:xs) : tails xs

inits :: [a] -> [[a]]
inits xs = foldr (\x xss -> [] : map (x:) xss) [[]] xs

Imperative programming aficionados would laugh at this O(n^3) algorithm and walk away. Functional programmers have laws 😁

Let's look where we can go from here:

max . map sum . segments
= {- def of segments -}
max . map sum . concat . map inits . tails
= {- map f . concat = concat . map (map f) -}
max . concat . map (map sum) . map inits . tails
= {- max . concat = max . map max -}
max . map max . map (map sum) . map inits . tails
= {- functor law -}
max . map (max . map sum . inits) . tails

Nice! Notice that inits is a fold, so we can use the fold fusion law twice. That's our plan of attack! Let's focus on the inner expression first:

max . map sum . inits
= {- def of inits -}
max . map sum . foldr (\x xss -> [] : map (x:) xss) [[]]
= {- fusion law, b = g a = map sum [[]] = [0], f (g x y) = h x (g y) = zsum x (map sum y) -}
max . foldr zsum [0]

Of course we need to derive zsum 😅 Let's do that. All we need is start from the f (g x y) expression and derive the hell out of it.

map sum ([] : map (x:) xss)
= {- def of map -}
sum [] : map sum . (map (x:)) xss 
= {- functor law, sum [] = 0 -}
0 : map (sum . (x:)) xss
= {- sum . (x:) xs = sum x:xs = x + sum xs -}
0 : map (x+) (map sum xss)
= {- introduce zsum x xs = 0 : map (x+) xs -}
zsum x (map sum xss)

Good. Let's do the same exercise with max . foldr zsum [0]:

max . foldr zsum [0]
= {- fusion law, max [0] = 0, introduce zmax x (max y) -}
foldr zmax 0

The derivation of zmax is a piece of cake:

max (0 : map (x+) xss)
= {- max (0:xs) = 0 `maximum` max xs, where maximum is the binary version of max -} 
0 `maximum` max (map (x+) xss)
= {- max (map (x+)) xss = x + max xss -}
0 `maximum` x + max xss
= {- introduce zmax x y = 0 `maximum` x + y -}
zmax x (max xss)

We've already reduced the complexity by arriving at mss = max . map (foldr zmax 0) . tails. Additionally, the expression is an instance of the scan lemma, i.e. map (foldr f a) . tails = scanr f a. We can thus write

mss = max . scanr zmax 0

This version is linear in complexity. Some improvement is possible, namely reducing the space complexity to O(1), using the so-called "tupling method". We can look into it another time.