Sharon Curtis and Shin-Cheng Mu. Journal of Functional Programming, Vol. 25, 2015.
[Paper (doi: 10.1017/S095679681500026X)| Supplementary Proofs | Code]
The problem of finding a densest segment of a list is similar to the well-known maximum segment sum problem, but its solution is surprisingly challenging. We give a general specification of such problems, and formally develop a linear-time online solution, using a sliding window style algorithm. The development highlights some elegant properties of densities, involving partitions that are decreasing and all right-skew.
The Code
The accompanying Haskell programs and Agda proofs are available on GitHub:
https://github.com/scmu/mds
The Haskell program consists of the following files:
FDSList.hs
: a main program that, for expository purpose, represents sequences by lists.FDSSeq.hs
: a linear-time implementation of the algorithm, using refined data structures as described in the paper.ProbMDS.hs
: problem specification for the MDS problem. To be imported byFDSList.hs
orFDSSeq.hs
.ProbMMS.hs
: problem specification for the MMS problem. To be imported byFDSList.hs
orFDSSeq.hs
.MDSTest.hs
: QuickCheck tests for the MDS problem.MMSTest.hs
: QuickCheck tests for the MMS problem.