### Yet Another Small Exercise

The following problem description is taken from exercise 7.39 of AoP:

(The answer to the small question is that a prefix of a given length is unique.) My aim, however, is to play with functional derivation. ThereforeThe function

`takeWhile`

of functional programming can be specified bytakeWhile p = max R . Λ(list p . prefix)where`R = lengthº . leq . length`

. In word,`takeWhile p x`

returns the longest prefix of`x`

with the property that all its elements satisfy`p`

. (Question: whythelongest here rather thanalongest?) Using`prefix = cata [nil, cons ∪ nil]`

and the greedy theorem, derive the standard implementation of`takeWhile`

.

The purpose of the first fusion is to transform the generating part into a fold, in hope that the greedy theorem can be applied.

One small property I didn't prove is `filter ((t ∧) . p) = (const t → filter p, nil . !)`

, which is a rather straightforward one.

And the second fusion tries to promote `max`

into the generating fold, which is the spirit of the greedy theorem. I didn't formulate the greedy theorem in functional form, though, so I simply do the fusion.

In fact I don't know precisely which part should be called the monotonicity condition. Maybe it will become clear to me after I prove the greedy theorem (by fold fusion) and compare the proof to this derivation and the derivation of maximum prefix sum. Having experience dealing with maximum prefix sum, I guess the following property is an essential one.

This is the fusion condition for `(x:) . max ≤`

. Applying type functor fusion to _{ℓ}`max ≤`

, we would have _{ℓ} . map (x:)`max ≤`

, a premise used in the second fusion.
_{ℓ} . map (x:) = (x:) . max ≤_{ℓ}

The entire derivation is very similar to maximum prefix sum, which is certainly no surprise. They are both applications of the greedy theorem. I mixed Haskell and AoP syntax as well as curried and uncurried forms. Hope it's not too confusing.

--

Time to study AoP chap. 7!

Labels: Program Derivation

<< 回到主頁