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 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
ghci and invoke the function
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))
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
The gzipped file consists of the following Haskell modules:
Main: containing the main program
mds, our variant of zygomorphism
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
densitydefined are collected into a type class
Block, and functions like
maxChopare define on the type class.
DRSP: specification of right-skew segments and DRSP, with functions including
PTrees, and functions like
prependDallowing 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 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.