# Fully Polynomial-Time Approximation by Thinning

Last update: August 26, 2013

Code and supplementary proofs accompanying the paper: Constructing Datatype-Generic Fully Polynomial-Time Approximation Schemes Using Generalised Thinning, by Yu-Han Lyu, Akimasa Morihata, and me.

The supplementary proofs mainly consist of proofs regarding the individual problems in the paper.

The file fptas.zip consists of the following Haskell modules:

• `KnapsackSpec`: specification of the 0-1 knapsack problem.
• `Knapsack`: a thinning algorithm solving knapsack (`knapsack`), and an approximation algorithm (`knapsack_apx`).
• `KnapsackTest`: some QuickCheck properties to test the code.
• `PartTreesSpec`: specification of the maximal tree partition problem.
• `PartTrees`: a thinning algorithm solving the tree partition problem (`mtp`), and an approximation algorithm (`mtp_apx`).
• `PartTreesTest`: some QuickCheck properties to test the code.
• `Utilities`: some utilities used by `PartTreesSpec`.
• `Merging`: generalised merging and bumping functions for both programs.

The problem instances generated by QuickCheck very rapidly get too large in size. The function `smallCheck` defined in both `*Test` modules restricts the sizes of instances generated.

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

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 `mdsM x ⇑d win (a:x)` should be `mdsM x ⇑d wp (trim (a:x))`; `a : x <b L` and `a : x ≥b L` should respectively be `trim (a : x) <b L` and `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 =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 `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.

# AoPA — Algebra of Programming in Agda

2011.06.01 Part of the library is updated to use universe polymorphism, and it now type checks with Agda 2.2.11. This is a temporary update yet to be finished. The unfinished parts are commented out in Everything.agda.

An Agda library accompanying the paper Algebra of Programming in Agda: Dependent Types for Relational Program Derivation, developed in co-operation with Hsiang-Shang Ko and Patrik Jansson.

Dependent type theory is rich enough to express that a program satisfies an input/output relational specification, but it could be hard to construct the proof term. On the other hand, squiggolists know very well how to show that one relation is included in another by algebraic reasoning. The AoPA library allows one to encode Algebra of Programming style program derivation, both functional and relational, in Agda.

### Example

The following is a derivation of insertion sort in progress:

```isort-der : ∃ (\f → ordered? ○ permute ⊒ fun f ) isort-der = (_ , (   ⊒-begin       ordered? ○ permute   ⊒⟨ (\vs -> ·-monotonic ordered? (permute-is-fold vs)) ⟩       ordered? ○ foldR combine nil   ⊒⟨ foldR-fusion ordered? ins-step ins-base ⟩       foldR (fun (uncurry insert)) nil   ⊒⟨ { foldR-to-foldr insert []}0 ⟩       { fun (foldr insert [])   ⊒∎ }1))```

``` ```

```isort : [ Val ] -> [ Val ] isort = proj₁ isort-der ```

The type of `isort-der` is a proposition that there exists a function `f` that is contained in `ordered ? ◦ permute` , a relation mapping a list to one of its ordered permutations. The proof proceeds by derivation from the speciﬁcation towards the algorithm. The ﬁrst step exploits monotonicity of `◦` and that `permute` can be expressed as a fold. The second step makes use of relational fold fusion. The shaded areas denote interaction points — fragments of (proof ) code to be completed. The programmer can query Agda for the expected type and the context of the shaded expression. When the proof is completed, an algorithm `isort` is obtained by extracting the witness of the proposition. It is an executable program that is backed by the type system to meet the speciﬁcation.

The complete program is in the Example directory of the code.

### The Code

The code consists of the following files and folders:

• AlgebraicReasoning: a number of modules supporting algebraic reasoning. At present we implement our own because the `PreorderReasoning` module in earlier versions of the Standard Library was not expressive enough for our need. We may adapt to the new Standard Library later.
• Data: defining relational fold, unfold, hylomorphism (using well-founded recursion), the greedy theorem, and the converse-of-a-function theorem, etc, for list and binary tree.
• Examples: currently we have prepared four examples: a functional derivation of the maximum segment sum problem, a relational derivation of insertion sort and quicksort (following the paper Functional Algorithm Design by Richard Bird), and solving an optimisation problem using the greedy theorem.
• Relations: modules defining various properties of relations.
• Sets: a simple encoding of sets, upon with Relations are built.

To grab the latest code, install darcs and check our the code from the repository:

```darcs get http://pc-scm.iis.sinica.edu.tw/repos/AoPA ```

AoPA makes use of the Standard Library, to install which you will need darcs.

# Push: Improving Heap Residency for Lazy Stream Processing by Concurrency

Prototype implementation of a language Push, accompanying our recently submitted paper. The prototype is implemented and prepared by Ta-Chung Tsai.

While studying XML stream processing, we noticed that programmers need concurrency to save space, especially in a lazy language. We propose the idea of pushing datatypes — when a pushing closure is demanded, all expressions referring to it are evaluated concurrently to weak head normal forms. The closure is no more alive and may thus be garbage collected.

# Maximum Segment Sum and Density with Bounded Lengths

It may be surprising that variations of the maximum segment sum (MSS) problem, a textbook example for the squiggolists, are still active topics for algorithm designers. These literate Haskell scripts presents a program solving two recently studied variations:

1. mssu.lhs: an amortised linear-time algorithm computing the maximum sum of segments not longer than an upper-bound;
2. msdlb.lhs: an O(n log L) algorithm computing the maximum density (average) of segments not shorter than a lower-bound;
3. msdll.lhs: computing the maximum density (average) of segments not shorter than a lower-bound. With the discovery of Glodwasser et al. we are able to refine the algorithm to amortised linear time again.

2007/06/26 Update: fixed binary search.
2007/11/04 Update: linear time algorithm for MSDL.