Bottom-up computation using trees of sublists (Functional Pearl)

TL;DR

This work gives this algorithm a proper derivation and discovered a key property that allows it to work, and builds trees that have certain shapes—the sizes along the left spine is a prefix of a diagonal in Pascal's triangle.

Abstract

Some top-down problem specifications, if executed directly, may compute sub-problems repeatedly. Instead, we may want a bottom-up algorithm that stores solutions of sub-problems in a table to be reused. It can be tricky, however, to figure out how the table can be represented and efficiently maintained. We study a special case: computing a function $h$ taking lists as inputs such that $h~xs$ is defined in terms of all immediate sublists of $xs$. Richard Bird studied this problem in 2008, and presented a concise but cryptic algorithm without much explanation. We give this algorithm a proper derivation, and discover a key property that allows it to work. The algorithm builds trees that have certain shapes -- the sizes along the left spine is a diagonal in Pascal's triangle. The crucial function we derive transforms one diagonal to the next.

Figures (6)

• Figure 1: Computing $\mathit{h}\;\text{\ttfamily " abcd"}$ top-down. String constants are shown using monospace font but without quotes, to save space.
• Figure 2: Computing $\mathit{h}\;\text{\ttfamily " abcde"}$ bottom-up.
• Figure 3: Results of $\mathit{ch}$.
• Figure 4: Applying $\mathit{B}\;\mathit{g}\;\mathrel{\hbox{$\circ$}}\mathit{up}$ to $\mathit{B}\;\mathit{h}\;(\mathit{ch}\;\mathrm{2}\;\mathtt{abcde})$. We abbreviate $\mathit{zipBW}\;\mathit{snoc}$ to $\mathit{zip}$.
• Figure 5: An Agda implementation of $\mathit{up}$.

Theorems & Definitions (4)

• Lemma 1
• proof
• Theorem 1
• proof