I spent most of the week preparing for the lecture on Monday, in which we plan to talk about segment problems. One of the things we would like to do is to translate the derivations in Hans Zantema’s Longest Segment Problems to Bird-Meertens style. Here is a summary of the part I managed to do this week.

Zantema’s paper considered problems of this form:

`max# ∘ p ◁ ∘ segs`

where `segs :: [a] → [[a]]`

, defined by `segs = concat ∘ map inits ∘ tails`

returns all consecutive segments of the input list; `p ◁`

is a shorter notation for `filter p`

, and `max# :: [[a]] → [a]`

returns the longest list from the input list of lists. In words, the task is to compute the longest consecutive segment of the input that satisfies predicate `p`

.

Of course, we have to assume certain properties from the predicate `p`

. A predicate `p`

is:

*suffix-closed*, if `p (xs ⧺ ys) ⇒ p ys`

;
*overlap-closed*, if `p (xs ⧺ ys) ∧ p (ys ⧺ zs) ∧ ys ≠ [] ⇒ p~(xs ⧺ ys ⧺ zs)`

.

For example, `ascending`

is suffix and overlapping-closed, while `p xs = (all (0 ≤) xs) ∧ (sum xs ≤ C)`

for some constant `C`

is suffix-closed but not overlap-closed. Note that for suffix-closed `p`

, it is reasonable to assume that `p []`

is true, otherwise `p`

would be false everywhere. It also saves us some trouble being sure that `max#`

is always applied to a non-empty set.

I denote function application by an infix operator `▪`

that binds looser than function composition `∘`

but tighter than other binary operators. Therefore `f ∘ g ∘ h ▪ x`

means `f (g (h x))`

.

### Prefix/Suffix Decomposition

Let us begin with the usual prefix/suffix decomposition:

```
max# ∘ p ◁ ∘ segs
= max# ∘ p ◁ ∘ concat ∘ map inits ∘ tails
= max# ∘ concat ∘ map (p ◁) ∘ map inits ∘ tails
= max# ∘ map (max# ∘ p ◁ ∘ inits) ∘ tails
```

Like what we do with the classical maximum segment sum, if we can somehow turn `max# ∘ p ◁ ∘ inits`

into a fold, we can then implement `map (foldr ...) ∘ tails`

by a `scanr`

. Let us denote `max# ∘ p ◁ ∘ inits`

by `mpi`

.

If you believe in structural recursion, you may attempt to fuse `map# ∘ p ◁`

into `inits`

by fold-fusion. Unfortunately, it does not work this way! In the fold-fusion theorem:

`h ∘ foldr f e = foldr g (h e) ⇐ h (f x y) = g x (h y)`

notice that `x`

and `y`

are universally quantified, which is too strong for this case. Many properties we have, to be shown later, do need information from the context — e.g. some properties are true only if `y`

is the result of `inits`

.

### Trimming Unneeded Prefixes

One of the crucial properties we need is the following:

**Proposition 1**: If `p`

is suffix-closed, we have:

```
p ◁ ∘ inits ▪ (x : xs) =
p ◁ ∘ inits ▪ (x : max# ∘ p ◁ ∘ inits ▪ xs)
```

For some intuition, let `x = 1`

and `xs = [2,3,4]`

. The left-hand side first compute all prefixes of `xs`

:

`[] [2] [2,3] [2,3,4]`

before filtering them. Let us assume that only `[]`

and `[2,3]`

pass the check `p`

. We then pick the longest one, `[2,3]`

, cons it with `1`

, and compute all its prefixes:

`[] [1] [1,2] [1,2,3]`

before filtering them with `p`

again.

The right-hand side, on the other hand, performs filtering on all prefixes of `[1,2,3,4]`

. However, the proposition says that it is the same as the left-hand side — filtering on the prefixes of `[1,2,3]`

only. We lose nothing if we drop `[1,2,3,4]`

. Indeed, since `p`

is suffix-closed, if `p [1,2,3,4]`

were true, `p [2,3,4]`

would have been true on the right-hand side.

Proof of Proposition 1 was the topic of a previous post. The proposition is useful for us because:

```
mpi (x : xs)
= max# ∘ p ◁ ∘ inits ▪ (x : xs)
= { Proposition 1 }
max# ∘ p ◁ ∘ inits ▪ (x : max# ∘ p ◁ ∘ inits ▪ xs)
= mpi (x : mpi xs)
```

Therefore `mpi`

is a fold!

`mpi = foldr (λx ys → mpi (x : ys)) []`

### Refining the Step Function

We still have to refine the step function `λx ys → mpi (x : ys)`

to something more efficient. Luckily, for overlap-closed `p`

, `mpi (x : ys)`

is either `[]`

, `[x]`

, or `x : ys`

— if `ys`

is the result of `mpi`

.

**Proposition 2**: If `p`

is overlap-closed, `mpi (x : mpi xs) = x ⊙ xs`

, where `⊙`

is defined by:

```
x ⊙ ys | p (x : xs) = x : ys
| p [x] = [x]
| otherwise = []
```

To see why Proposition 2 is true, consider `mpi (x : mpi xs)`

.

- If
`mpi (x : mpi xs) = []`

, we are done.
- Otherwise it must be
`x : zs`

for some `zs ∈ inits (mpi xs)`

. And we have `p~(x : zs)`

because it is a result of `mpi`

. Again consider two cases:
- If
`zs = []`

, both sides reduce to `[x]`

, otherwise…
- Let us not forget that
`p (mpi xs)`

must be true. Also, since `zs ∈ inits (mpi xs)`

, we have `mpi xs = zs ⧺ ws`

for some `ws`

. Together that implies `p (x : zs ⧺ ws) = p (x : mpi xs) `

must be true.

Notice that the reasoning above (from Zantema) is a proof-by-contradiction. I do not yet know how hard it is to build a constructive proof.

With Proposition 1 and 2 we have turned `mpi`

to a fold. That leads to the derivation:

```
max# ∘ p ◁ ∘ segs
= { derivation above }
max# ∘ map (max# ∘ p ◁ ∘ inits) ∘ tails
= max# ∘ map (foldr (⊙) []) ∘ tails
= max# ∘ scanr (⊙) []
```

with the definition of `⊙`

given above. It turns out to be a rather simple algorithm: we scan through the list, and in each step we choose among three outcomes: `[]`

, `[x]`

, and `x : ys`

. Like the maximum segment sum problem, it is a simple algorithm whose correctness is that that easy to justify.

The algorithm would be linear-time if `⊙`

can be computed in constant-time. With the presence of `p`

in `⊙`

, however, it is unlikely the case.

### Efficient Testing

So let us compute, during the fold, something that allows `p`

to be determined efficiently. Assume that there exists some `φ :: [A] → B`

that is a fold (`φ = foldr ⊗ ι`

for some `⊗`

and `ι`

), such that `p (x : xs) = p xs ∧ f x (φ xs)`

for some `f`

. Some example choices of `φ`

and `f`

:

Let us tuple mpi with φ, and turn them into one fold. Let `⟨ f , g ⟩ x = (f x, g x)`

, we derive:

```
max# ∘ p ◁ ∘ inits
= { f = fst ∘ ⟨ f , g ⟩, see below}
fst ∘ ⟨ max# ∘ p ◁ ∘ inits , φ ⟩
= fst ∘ foldr step ([], ι)
```

where `step`

is given by

```
step x (xs, b)
| f x b = (x : xs , x ⊗ b)
| f x ι = ([x], x ⊗ ι)
| otherwise = ([], ι)
```

Notice that the property `f = fst ∘ ⟨ f , g ⟩`

is true when the domain of `f`

is in the domain of `g`

, in particular, when they are both total, which again shows why we prefer to work in a semantics with total functions only.

Let us restart the main derivation again, this time use the tupling:

```
max# ∘ p ◁ ∘ segs
= max# ∘ map (max# ∘ p ◁ ∘ inits) ∘ tails
= max# ∘ map (fst ∘ ⟨ max# ∘ p ◁ ∘ inits , φ ⟩) ∘ tails
= { since map# ∘ map fst = fst ∘ map#', see below}
fst ∘ max#' ∘ map ⟨ max# ∘ p ◁ ∘ inits , φ ⟩ ∘ tails
= { derivation above }
fst ∘ max#' ∘ map (foldr step ([], ι) ∘ tails
= fst ∘ max#' ∘ scanr step ([], ι)
```

where `map#'`

compares the lengths of the first components. This is a linear-time algorithm.

### Next… Windowing?

What if `p`

is not overlap-closed? Zantema used a technique called *windowing*, which I will defer to next time…

### Reference