# Okasaki's PFDS, Chapter 4

This post contains my solutions to the exercises in chapter 4 of Okasaki’s “Purely Functional Data Structures”. The latest source code can be found in my GitHub repo.

## Notation

Okasaki uses $ to indicate suspensions. But beware! Haskell also has this symbol but it means something completely different, namely function application. In symbols: ($) :: (a -> b) -> a -> b
($) f a = f a We can use it like any other function in haskell. For example: two = (1 +)$ 1

It has nothing to do with suspensions, evaluation, forcing, etc.

It is also important to note that a ‘list’ in haskell is not what Okasaki calls a ‘list’. He would call haskell’s lists ‘streams’. We will stick with haskell’s notation, calling Okasaki’s list a ‘strict list’.

## Exercise 1

Show that both definitions of drop are equivalent.

## Solution 1

The code in this solution is NOT Haskell.

For convenience, we give names to the three different functions.

fun drop (0, s)            = s
| drop (n, $Nil) =$Nil
| drop (n, $Cons (x, s)) = drop (n-1, s) fun lazy dropA (0, s) = s | dropA (n,$Nil)         = $Nil | dropA (n,$Cons (x, s)) = dropA (n-1, s)
fun lazy dropB (n, s) = drop (n, s)

The proof proceeds in three steps.

Lemma
Let s be a suspension. Then $force s is equivalent to s. Proof. Suppose s is $e for some expression e. Then $force s $$\cong$$ $force $e $$\cong$$ $e $$\cong$$ s.

Lemma
dropA is equivalent to drop

Proof. We prove this by induction on $$n$$.

For the base step, dropA (0, s) = $force s$s = drop (0, s), where the middle equivalence follows by the previous lemma.

Note that dropA (n, $Nil) = $force $Nil = $Nil = drop (n, $Nil) follows by the previous lemma. Now suppose dropA (n, s) $$\cong$$ drop (n, s) for some $$n \in \mathbb N$$ and any stream s. We can write s as $Cons (x, s'). Then dropA (n+1, s) = dropA (n+1, $Cons (x, s')) = $force dropA (n, s') $$\cong$$ dropA (n, s') $$\cong$$ drop (n, s') = drop (n+1, s).

Lemma
dropA is equivalent to dropB

Proof. Using the previous two lemmas, we obtain dropB (n, s) = $force drop (n, s) = $force dropA (n, s) = dropA (n, s) for any $$n \in \mathbb N$$ and any stream s.

## Exercise 2

Implement insertion sort on streams and show that extracting the first $$k$$ elements takes only $$\mathcal O (nk)$$ time, where $$n$$ is the length of the input list.

## Solution 2

See source. Note that lists in Haskell are what Okasaki calls streams, so we need no special annotations or data structures.

Let $$T (n, k)$$ be the asymptotic complexity of computing take k $sort xs, where xs is a list of length $$n$$. By definition of take, $$T (n, 0) = \mathcal O (1)$$ and $$T (0, k) = T (0, 0)$$. In take k$ sort xs the function take k needs to put sort xs into weak head normal form. Let $$S (m)$$ be the complexity of puting sort ys into weak head normal form for a list ys of length $$m$$. Clearly $$S (0) = \mathcal O (1)$$. Since sort (y:ys) = ins y $sort ys, we have $$S (m) = S (m-1) + \mathcal O (1)$$, since ins y only needs to put sort ys into weak head normal form. This is solved by $$S (m) = \mathcal O (m)$$. Now, take k$ sort xs = take k \$ y : ys = y : take (k-1) ys, where sort xs = y : ys`. Thus $$T (n, k) = T (n-1, k-1) + \mathcal O (n)$$. This recurrence is solved by $$T (n, k) = \mathcal O (nk)$$.