The following is superseded by our later work Functional pearl: finding a densest segment.
- Page 3: “This input sequence does not have a solution…” what we meant was “This input does not have a prefix that is within bounds.” We used another example where the input does not have a feasible segment at all before changing to example, but I forgot to change the text accordingly.
- Page 4, Proof of Theorem 3.2: the first
mdsM x ⇑d win (a:x)should be
mdsM x ⇑d wp (trim (a:x));
a : x <b Land
a : x ≥b Lshould respectively be
trim (a : x) <b Land
trim (a : x) ≥b L.
Thanks to Josh Ko for pointing out both errors.
The problem of finding a maximally dense segment (MDS) of a list is a generalisation of the well-known maximum segment sum (MSS) problem, but its solution is more challenging. We extend and illuminate some recent work on this problem with a formal development of a linear-time online algorithm, in the form of a sliding window zygomorphism. The development highlights some elegant properties of densities, involving partitions which are decreasing and all right-skew.
Code and supplementary proofs are available online.
keywords: program derivation, segment problem, maximum density, sliding window, zygomorphism, right-skew.