$\newcommand{\defeq}{\mathrel{\mathop:}=}$

## 2008/05/12

### Details

I'm reading Shin's Maximum segment sum is back: deriving algorithms for two segment problems with bounded lengths and trying to work out the details as exercises. So far I've just gone through 3/4 of the first page deriving mssu.

The first claim we need is

  sum . fitlen
=   { split cancellation (backwards) }
fst . <sum, len> . fitlen
=   { claim: <R, S> . C = <R, S . C> }
fst . <sum, len . fitlen>
=   { len . fitlen = (≤ U) . len }
fst . <sum, (≤ U) . len>
=   { product relator }
fst . (id × (≤ U)) . <sum, len>
=   { definition of fit }
fst . fit . <sum, len>

The subclaim follows from R ∩ (S . C) = (R ∩ S) . C where C is coreflexive, since <R, S> = (outlº . R) ∩ (outrº . S).
  R ∩ (S . C)
⊆   { modular law }
((R . Cº) ∩ S) . C
⊆   { C coreflexive }
(R ∩ S) . C
=   { C simple }
(R . C) ∩ (S . C)
⊆   { C coreflexive }
R ∩ (S . C)


Next we have to invent R such that the fusion condition

  fit . <sum, len> . (const [] ∪ cons)
= R . (id × (fit . <sum, len>))

holds. We reason:
  fit . <sum, len> . (const [] ∪ cons)
=   { composition distributes over join }
(fit . <sum, len> . const []) ∪ (fit . <sum, len> . cons)
=   { naturality of const (??) }
const (0, 0) ∪ (fit . <sum, len> . cons)
=   { <sum, len> is a fold by banana-split law (??); fold evaluation }
const (0, 0) ∪ (fit . add . (id × <sum, len>))
=   { claim: fit . add = fit . add . (id × fit) }
const (0, 0) ∪ (fit . add . (id × (fit . <sum, len>)))
=   { naturality of const (??); composition distributes over join }
(const (0, 0) ∪ (fit . add)) . (id × (fit . <sum, len>))

Therefore we have R = const (0, 0) ∪ (fit . add). The subclaim holds since 1 + l ≤ U implies l ≤ U.

And now we reach the monotonicity condition. There is a somewhat irrelevant component left out in the antecedent given in the paper:

s₁ ≤ s₂ ∧ (s₃ = 0 ∨ (s₃ = a + s₁ ∧ 1 + l₁ ≤ U))


But 1 + l₁ ≤ U doesn't help ensuring that l₄ = 1 + l₂ ≤ U, since the two lengths are unrelated. Thus one can enhance the antecedent:

s₁ ≤ s₂ ∧ l₁ ≥ l₂ ∧ (s₃ = 0 ∨ (s₃ = a + s₁ ∧ 1 + l₁ ≤ U))

and we'll have 1 + l₂ ≤ 1 + l₁ ≤ U.

Finally, the proof of the thinning theorem is structurally equivalent to that of the greedy theorem.

It reveals that I haven't understood datatypes (products, coproducts, ...) and their properties in Rel. For example I am not certain whether naturality (in particular "theorems for free") can be applied as one would do in Fun. (And I don't understand theorems for free, either.)

--
I'll try to finish the rest in the evening...

Labels: