In the Software Construction course next week we will, inevitably, talk about maximum segment sum. A natural next step is to continue with the theme of segment problems, which doesn’t feel complete without mentioning Hans Zantema’s Longest Segment Problems.
The paper deals with problem of this form:
ls = max# ∘ p ◁ ∘ segsThat is, computing the longest consecutive segment of the input list that satisfies predicate p. When writing on paper I found it much easier denoting filter p by the Bird-Meertens style p ◁ and I will use the latter for this post too. The function segs :: [a] → [[a]], defined by segs = concat ∘ map inits ∘ tails returns all consecutive segments of the input list, and max# :: [[a]] → [a] returns the longest list from the input list of lists. To avoid long nesting parenthesis, I denote function application by an infix operator ▪ that binds looser than function composition ∘. Therefore f ∘ g ∘ h ▪ x means f (g (h x)).
Standard transformation turns the specification to the form
ls = max# ∘ map (max# ∘ p ◁ ∘ inits) ∘ tails
Therefore we may solve ls if we manage to solve its sub-problem on prefixes:
lp = max# ∘ p ◁ ∘ initsthat is, computing the longest prefix of the input list satisfying predicate p. One of the key propositions in the paper says:
Proposition 1: If
pis suffix-closed (that is,p (x ⧺ y) ⇒ p y), we have:p ◁ ∘ inits ▪ (a : x) = p ◁ ∘ inits ▪ (a : max# ∘ p ◁ ∘ inits ▪ x)
It is useful because, by composing max# on both sides we get
lp (a : x) = max# ∘ p ◁ ∘ inits ▪ (a : lp x)that is, lp can be computed by a foldr.
Of course, we are not quite done yet. We then have to somehow simplify p ◁ ∘ inits ▪ (a : lp x) to something more efficient. Before we move on, however, proving Proposition 1 turns out to be an interesting challenge in itself.
Intuition
What does Proposition 1 actually say? Let x = [1,2,3] and a = 0. On the left-hand side, we are performing p ◁ on
[] [0] [0,1] [0,1,2] [0,1,2,3]The right hand side says that we may first filter the tails of [1,2,3]:
[] [1] [1,2] [1,2,3]Assuming that only [] and [1,2] get chosen. We may then keep the longest prefix [1,2] only, generate all its prefixes (which would be [] [1] [1,2]), and filter the latter again. In other words, we lost no information dropping [1,2,3] if it fails predicate p, since by suffix-closure, p ([0] ⧺ [1,2,3]) ⇒ p [1,2,3]. If [1,2,3] doesn’t pass p, p [0,1,2,3] cannot be true either.
Zantema has a nice and brief proof of Proposition 1 by contradiction. However, the theme of this course has mainly focused on proof by induction and, to keep the possibility of someday encoding our derivations in tools like Coq or Agda, we would like to have a constructive proof.
So, is it possible to prove Proposition 1 in a constructive manner?
The Proof
I managed to come up with a proof. I’d be happy to know if there is a better way, however.
For brevity, I denote if p then x else y by p → x; y. Also, define
a ⊕p x = p a → a : x ; xTherefore p ◁ is defined by
p ◁ = foldr ⊕p []Here comes the the main proof:
Proposition 1
p ◁ ∘ inits ▪ (a : x) = p ◁ ∘ inits ▪ (a : max# ∘ p ◁ ∘ inits ▪ x) if p is suffix-closed.
Proof.
∎
The main proof refers to two “decomposition” lemmas, both are of the form f ∘ g = f ∘ g ∘ f:
- Lemma 1:
p ◁ ∘ map (a:) = p ◁ ∘ map (a:) ∘ p ◁ifpsuffix-closed. - Lemma 2:
p ◁ ∘ inits ∘ max# ∘ p ◁ ∘ inits = p ◁ ∘ initsfor all predicatep.
Both are proved by structural induction. For Lemma 1 we need the conditional distribution rule:
f (p → x; y) = (p → f x; f y)If we are working in CPO we need the side condition that f is strict, which is true for the cases below anyway:
Lemma 1
p ◁ ∘ map (a:) = p ◁ ∘ map (a:) ∘ p ◁ if p is suffix-closed.
Proof. Structural induction on the input.
Case []: trivial.
Case (x : xs):
p ◁ ∘ map (a:) ∘ p ◁ ▪ (x : xs)
= { definition of p ◁ }
p ◁ ∘ map (a:) ▪ (p x → x : p ◁ xs ; p ◁ xs)
= { map distributes into conditionals }
p ◁ ▪ (p x → (a : x) : map (a :) ∘ p ◁ ▪ xs ; map (a :) ∘ p ◁ ▪ xs)
= { p ◁ distributes into conditionals }
p x → p ◁ ((a : x) : map (a :) ∘ p ◁ ▪ xs) ;
p ◁ ∘ map (a :) .p ◁ ▪ xs
= { definition of p ◁ }
p x → (p (a : x) → (a : x) : p ◁ ∘ map (a :) ∘ p ◁ ▪ xs) ;
p ◁ ∘ map (a :) ∘ p ◁ ▪ xs) ;
p ◁ ∘ map (a :) ∘ p ◁ ▪ xs
= { induction }
p x → (p (a : x) → (a : x) : p ◁ ∘ map (a :) ▪ xs) ;
p ◁ ∘ map (a :) ▪ xs) ;
p ◁ ∘ map (a :) ▪ xs
= { since p (a : x) ⇒ p x by suffix closure }
p (a : x) → (a : x) : p ◁ ∘ map (a :) ▪ xs) ;
p ◁ ∘ map (a :) ▪ xs
= { definition of p ◁ }
p ◁ ((a : x) : map (a :) xs)
= { definition of map }
p ◁ ∘ map (a :) ▪ (x : xs)∎
For Lemma 2, it is important that p is universally quantified. We need the following map-filter exchange rule:
p ◁ ∘ map (a :) = map (a :) ∘ (p ∘ (a:)) ◁The proof goes:
Lemma 2 For all predicate p we have
p ◁ ∘ inits ∘ max# ∘ p ◁ ∘ inits = p ◁ ∘ initsProof. Structural induction on the input.
Case []: trivial.
Case (a : x):
p ◁ ∘ inits ∘ max# ∘ p ◁ ∘ inits ▪ (a : x)
= p ◁ ∘ inits ∘ max# ∘ p ◁ ▪ ([] : map (a :) (inits x)) Consider two cases:
1. Case p [] ∧ null (p ◁ ∘ map (a :) ∘ inits ▪ x):
If ¬ p [], both sides are undefined. Otherwise:
...
= p ◁ ∘ inits ∘ max# ▪ []
= []
= p ◁ ▪ ([] : p ◁ ∘ map (a : ) ∘ inits ▪ x)
= p ◁ ∘ inits ▪ (a : x) 2. Case ¬ (null (p ◁ ∘ map (a :) ∘ inits ▪ x)):
...
= p ◁ ∘ inits ∘ max# ∘ p ◁ ∘ map (a :) ∘ inits ▪ x
= { map-filter exchange }
p ◁ ∘ inits ∘ max# ∘ map (a :) ∘ (p ∘ (a:)) ◁ ∘ inits ▪ x
= { since max# ∘ map (a :) = (a :) ∘ max# }
p ◁ ∘ inits ∘ (a :) ∘ max# ∘ (p ∘ (a :)) ◁ ∘ inits ▪ x
= { definition of inits }
p ◁ ([] : map (a :) ∘ inits ∘ max# ∘ (p ∘ (a :)) ◁ ∘ inits ▪ x)
= { definition of p ◁ }
p ⊕p (p ◁ ∘ map (a :) ∘ inits ∘ max# ∘ (p ∘ (a :)) ◁ ∘ inits ▪ x)
= { map-filter exchange }
p ⊕p (map (a :) ∘ (p ∘ (a :)) ◁ ∘ inits ∘ max# ∘ (p ∘ (a :)) ◁ ∘ inits ▪ x)
= { induction }
p ⊕p (map (a :) ∘ (p ∘ (a :)) ◁ ∘ inits ▪ x)
= { map-filter exchange }
p ⊕p (p ◁ ∘ map (a :) ∘ inits ▪ x)
= { definition of p ◁ }
p ◁ ( [] : map (a :) ∘ inits ▪ x)
= { definition of inits }
p ◁ ∘ inits ▪ (a : x)∎
Reference
- H. Zantema. Longest Segment Problems Sci. Comput. Program. 18(1): 39-66 (1992).