Maximally Dense Segments — Code and Proof

The following is superseded by our later work Functional pearl: finding a densest segment.

Code and proof accompanying a forthcoming paper of Sharon Curtis and me: Functional Pearl: Maximally Dense Segments.

Quick links: [expository program | linear time program | proofs (late update: 2010.04.17)].

Expository Code

The expository program [download here] intends to be an executable implementation of the code in the paper. For clarity we use Haskell lists for all sequences, and do not implement optimisations such as storing the areas and breadths of segments, thus the program is not linear time yet. A linear time implementation will follow soon.

The code is mostly consistent with the paper, with some minor differences: many functions take an additional argument of type BreadthSpec = (Breadth, Maybe Breadth). The first component is the lower bound, while the second component is an optional upperbound. The main function is:

mds :: BreadthSpec ->  [Elem] -> Maybe [Elem]

which takes a BreadthSpec and switches between the modes with or without an upper bound.

To try the code, you may either load the module Main into ghci and invoke the function mds:

mds (lb, Just ub) [x1, x2, x3, ... ]

or load the module Test and run some QuickCheck properties:

Test.QuickCheck.quickCheck (prop_mds_correct bb (lb, Just ub))

where lb and ub are the lower and upper bounds, and bb is the bound on breadths of generated test elements. The property prop_mds_correct asserts that mds (lb,ub) x =d mds_spec (lb,ub) x for all x.

The gzipped file consists of the following Haskell modules:

• Main: containing the main program mds, our variant of zygomorphism zh, wp2, smsp2, maxChop, trim, etc.
• Spec: containing a specification of the maximally dense segment problem:

  mds_spec :: BreadthSpec -> [Elem] -> Maybe [Elem]
  mds_spec bs = maxlistM d . filter (bounds bs) . nonEmptySegs

  Many types having area, breadth, and density defined are collected into a type class Block, and functions like maxChop are define on the type class.

• DRSP: specification of right-skew segments and DRSP, with functions including rightSkew, sdars, lrsp, and drsp.
• DPTrees: defining DTrees and PTrees, and functions like addD and prependD allowing one to construct DRSPs in a fold.
• Utilities: some utility functions processing lists.
• Test: a module defining some QuickCheck properties to test the code.

Linear Time Implementation

A linear time implementation can be downloaded here. The program uses Data.Sequence to represent the compulsory part and the first level of the DForest and the PForest of the window, as well as annotating them with areas and breadths. The subtrees of a DTree and a PTree, however, can be represented simply by snoc-lists and cons-lists respectively.

Organisation of the code is the same as the first program.

Proofs

Proofs accompanying the paper [PDF]. Theorems and lemmas are labelled with both their own numbers as well as the numbers in the paper, if any. For example, Lemma A.1 (3.1) is Lemma 3.1 in the paper.