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)].
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
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
PTrees, and functions like
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 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.