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)].

**errata**:

- 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
`mds`

should be_{M}x ⇑_{d}win (a:x)`mds`

;_{M}x ⇑_{d}wp (trim (a:x))`a : x <`

and_{b}L`a : x ≥`

should respectively be_{b}L`trim (a : x) <`

and_{b}L`trim (a : x) ≥`

._{b}L

Thanks to Josh Ko for pointing out both errors.

### 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 =`

for all _{d} mds_spec (lb,ub) x`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`DTree`

s 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.