The Pruning Theorem: Thinning Based on a Loose Notion of Monotonicity

The reason I studied the thinning theorem again is because I need a slightly generalised variation. The following seems to be what I need. The general idea and the term “pruning” emerged from discussion with Sharon Curtis. The term “lax preorder” is invented by myself. I am not good at naming, and welcome suggestions for better names.

The notation below are mostly taken from the book Algebra of Programming. Not many people, even among functional programmers, are familiar with these notations involving relational intersection, division, etc. One starts to appreciate their benefits once he/she gets used to using their calculation rules. Most of the time when I was doing the proof, I was merely manipulating the symbols. I could not have managed the complexity if I had to fall back to the semantics and think about what they “mean” all the time.

A relation Q :: PA ← A between a set of A and an element is called a lax preorder if it is

1. reflexive in the sense that ∋ ⊆ Q, and
2. transitive in the sense that (Q/∋) . Q ⊆ Q.

A relation S :: A ← FA is monotonic on lax preorder Q if S . FQ˘ ⊆ Q˘. Λ(S . F∈).

Given a lax preorder, we define:

$prune Q = \in \\in \cap Q/\ni$

The definition induces the universal property:

Any preorder R induces a lax preorder ∋ . R. If a relation S is monotonic on , it is monotonic on lax preorder ∋ . R. Furthermore, prune (∋ . R) = thin R. Therefore, pruning is a generalisation of thinning. We need the notion of lax preorders because, for some problems, the generating relation S is monotonic on a lax preorder, but not a preorder.

Theorem: if S is monotonic on lax preorder Q, we have:

$fold \left(prune Q . \Lambda \left(S . F\in \right)\right) \subseteq prune Q . \Lambda \left(fold S\right)$

Proof. Since Λ(fold S) = fold (Λ(S . F∈)), by fold fusion, the theorem holds if

$prune Q . \Lambda \left(S . F\in \right) . F\left(prune Q\right) \subseteq prune Q . \Lambda \left(S . F\in \right)$

By the universal property of prune, the above is equivalent to:

prune Q . Λ(S . F∈) . F(prune Q) . (S . F∈)˘ ⊆ Q

The first inclusion is proved by:

⊆     { since prune Q ⊆ ∈\∈ }
∈ . ∈\∈ . Λ(S . F∈) . F(thin Q)
⊆     { division }
∈ . Λ(S . F∈) . F(thin Q)
=     { power transpose }
S . F∈ . F(thin Q)
⊆     { since prune Q ⊆ ∈\∈ }
S . F∈ . F(∈\∈)
⊆     { division }
S . F∈

And the second by:

⊆     { since prune Q ⊆ Q/∋, converse }
prune Q . Λ(S . F∈) . F(Q/∋) . F∋ . S˘
⊆     { division }
prune Q . Λ(S . F∈) . FQ . S˘
⊆     { monotonicity: FQ . S˘⊆ Λ(S . F∈)˘. Q }
prune Q . Λ(S . F∈) . Λ(S . F∈)˘. Q
⊆     { since Λ(S . F∈)˘is a function, that is, f . f˘⊆ id }
prune Q . Q
⊆     { since thin Q ⊆ Q/∋, division }
Q/∋ . Q
⊆     { since Q transitive }
Q

Endproof.

The proof above uses transitivity of Q but not reflectivity. I need reflectivity to construct base cases, for example, to come up wit this specialised Pruning Theorem for lists:

$foldr \left(prune Q . \Lambda \left(S . \left(id × \in \right)\right)\right) \left\{e\right\} \subseteq prune Q . \Lambda \left(foldr S e\right)$

if S . (id × Q˘) ⊆ Q˘. Λ(S . (id × ∈)).

Proving the Thinning Theorem by Fold Fusion

Algebra of Programming records two proofs of the greedy and the thinning theorems slightly shorter than proofs using fold fusion. Of course, one can still use fold fusion. In fact, proving them by fold fusion are exercises in Chapter 8 (PDF) of Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, of which I myself is listed among the authors.

A while ago when I needed to consider some variations of the thinning theorem I tried to do the proof again. And, horrifyingly, I could not do it anymore! Have my skills become rusty due to lack of practice in the past few years? In panic, I spent an entire afternoon fighting with it, until I realised that it was just a typical copying error from the very beginning: when I copied a property from the book I put in an extra Λ. Then I trapped myself in the maze of expanding ΛR into ∈\R ∩ (R\∈) and using modular law and ….

Having fixed the error, I get my trivial and easy proof back again. Anyway, I am going to record it below, in case I run into the same panic again.

Given a preorder Q, the relation thin Q is defined by:

$thin Q = \in \\in \cap \left(\ni . Q\right)/\ni$

The definition induces the universal property:

And here are some basic properties we will make use of later:

∈ . ΛS = S       (power transpose)
ΛR . R˘ ⊆ ∋
R . R\S ⊆ S,       R/S . S ⊆ R       (division)

The Thinning Theorem

The thinning theorem says :
Theorem: if S is monotonic on preorder Q, that is, S . FQ˘⊆ Q˘. S, we have:

$fold \left(thin Q . \Lambda \left(S . F\in \right)\right) \subseteq thin Q . \Lambda \left(fold S\right)$

Proof. By fold fusion, the theorem holds if

$thin Q . \Lambda \left(S . F\in \right) . F\left(thin Q\right) \subseteq thin Q . \Lambda \left(S . F\in \right)$

By the universal property of thin, the above inclusion is equivalent to

thin Q . Λ(S . F∈) . F(thin Q) . (S . F∈)˘ ⊆ ∋.Q

The first inclusion is proved by:

{ since thin Q ⊆ ∈\∈ }
∈ . ∈\∈ . Λ(S . F∈) . F(thin Q)
{ division }
∈ . Λ(S . F∈) . F(thin Q)
= { power transpose }
S . F∈ . F(thin Q)
{ since thin Q ⊆ ∈\∈ }
S . F∈ . F(∈\∈)
{ division }
S . F∈

And the second by:

{ since thin Q ⊆ (∋ . Q)/∋, converse }
thin Q . Λ(S . F∈) . F((∋ . Q)/∋) . F∋ . S˘
{ functor, division }
thin Q . Λ(S . F∈) . F(∋ . Q) . S˘
{ monotonicity: FQ . S˘ ⊆ S˘. Q }
thin Q . Λ(S . F∈) . F∋ . S˘. Q
{ since ΛR . R ⊆ ∋ }
thin Q . ∋ . Q
{ since thin Q ⊆ (∋.Q)/∋, division }
∋ . Q . Q
{ since Q transitive }
∋ . Q

Endproof.

By the way, the variation of thinning theorem I need is “fold (thin Q . Λ(S . F∈)) ⊆ thin Q . Λ(fold S) if S . F(Q˘. ∈) ⊆ Q˘. S . F ∈ “, whose proof is, luckily, trivial once you write down the original proof.

Zipping Half of a List with Its Reversal

I found this note with one page of Haskell code, without comments, when I was cleaning up my files. It took me quite a while to figure out what it might probably be about: given a list, zip its first half with the reverse of its second half, in only “one and a half” traversals of the list. It gives us a fast algorithm to, for example, check whether a list is a palindrome. I thought it was probably something we discussed in AoP, but it turns out that I must have taken the note when people in IPL were studying There and Back Again of Danvy and Goldberg. Recorded in the note was my attempt to understand it.

Let `convolute (xs,ys) = zip xs (reverse ys)` and `half` be a function cutting a list in half, the problem is simply specified by `revzip = convolute . half`. The first trick is that `convolute` can be expressed in terms of its generalisation:

``````> convolute :: ([a],[b]) -> [(a,b)]
> convolute = fstn . uncurry walk
>   where fstn (xs,[]) = xs``````

where `walk` is defined by:

``````  walk xs ys = (zip xs (reverse (take n ys)), drop n ys)
where n = length xs``````

The reason introducing `walk` is that it can be defined as a fold:

``````> walk = foldr ((.).shift) (split (nil, id))
> shift x (zs,y:ys) = ((x,y):zs, ys)
> nil _ = []``````

But the definition below is probably a lot more comprehensible:

``````  walk [] ys = ([],ys)
walk (x:xs) ys = shift x (walk xs ys)``````

Some of these auxiliary functions should be part of the Haskell Prelude:

``````> prod (f,g) (a,b) = (f a, g b)
> split (f,g) a = (f a, g a)``````

The following implementation of `half` splits a list into two halfs using two pointers:

``````> half :: [a] -> ([a],[a])
> half = race . dup
> race (xs,[]) = ([],xs)
> race (_:xs,[_]) = ([],xs)
> race (x:xs,_:_:ys) = cross ((x:),id) (race (xs,ys))
> dup a = (a,a)``````

Furthermore, `uncurry f = apply . prod (f,id)` where

``> apply (f,a) = f a``

Therefore the specification has become:

``  revzip = fstn . apply . prod (walk,id) . race . dup``

Now we try to fuse `prod (walk,id) . race` and get

``````> wrace (xs,[]) = (split (nil, id), xs)
> wrace (_:xs, [_]) = (split (nil, id), xs)
> wrace (x:xs, _:_:ys) = prod ((shift x .), id) (wrace (xs,ys))``````

Hence the result:

``> revzip = fstn . apply . wrace . dup``

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.

Countdown: a case study in origami programming

R. S. Bird and S-C. Mu. In Journal of Functional Programming Vol. 15(5), pp. 679-702, 2005.
[GZipped Postscript]

Countdown is the name of a game in which one is given a list of source numbers and a target number, with the aim of building an arithmetic expression out of the source numbers to get as close to the target
as possible. Starting with a relational specification we derive a number of functional programs for solving Countdown. These programs are obtained by exploiting the properties of the folds and unfolds of various data types, a style of programming Gibbons has aptly called origami programming. Countdown is attractive as a case study in origami programming both as an illustration of how different algorithms can emerge from a single specification, as well as the space and time trade-offs that have to be taken into account in comparing functional programs.

Inverting the Burrows-Wheeler transform

R. S. Bird and S-C. Mu. In Journal of Functional Programming Vol. 14(6) Special Issue on Functional Pearls, pp. 603-612, Novermber 2004.
[PDF][GZipped Postscript]

The Burrows-Wheeler Transform is a string-to-string transform which, when used as a preprocessing phase in compression, significantly enhances the compression rate. However, it often puzzles people how the inverse transform can be carried out. In this pearl we to exploit simple equational reasoning to derive the inverse of the Burrows-Wheeler transform from its specification. We also outline how to derive the inverse of two more general versions of the transform, one proposed by Schindler and the other by Chapin and Tate.

Theory and applications of inverting functions as folds.

S-C. Mu and R. S. Bird. In Science of Computer Programming Vol. 51 Special Issue for Mathematics of Program Construction 2002, pp. 87-116, 2003.
[PDF][GZipped Postscript]

This paper is devoted to the proof, applications, and generalisation of a theorem, due to Bird and de Moor, that
gave conditions under which a total function can be expressed as a relational fold. The theorem is illustrated with three problems, all dealing with constructing trees with various properties. It is then generalised to give conditions under which the inverse of a partial function can be expressed as a relational hylomorphism. Its proof makes use of Doornbos and Backhouse’s theory on well-foundedness and reductivity. Possible applications of the generalised theorem is discussed.

Rebuilding a tree from its traversals: a case study of program inversion

S-C. Mu and R. S. Bird. In The First Asian Symposium on Programming Languages and Systems, LNCS 2895, pp. 265-282, Bejing, 2003.
[GZipped Postscript]

Given the inorder and preorder traversal of a binary tree whose labels are all distinct, one can reconstruct
the tree. This article examines two existing algorithms for rebuilding the tree in a functional framework, using existing theory on function inversion. We also present a new, although complicated, algorithm by trying another possibility not explored before.

A Calculational Approach to Program Inversion

S-C. Mu, A Calculational Approach to Program Inversion. D.Phil Thesis. Oxford University Computing Laboratory. March 2003
[GZipped Postscript][PDF]

Many problems in computation can be specified in terms of computing the inverse of an easily constructed function. However, studies on how to derive an algorithm from a problem specification involving inverse functions are relatively rare. The aim of this thesis is to demonstrate, in an example-driven style, a number of techniques to do the job. The techniques are based on the framework of relational, algebraic program derivation.

Simple program inversion can be performed by just taking the converse of the program, sometimes known as to “run a program backwards”. The approach, however, does not match the pattern of some more advanced algorithms. Previous results, due to Bird and de Moor, gave conditions under which the inverse of a total function can be written as a fold. In this thesis, a generalised theorem stating the conditions for the inverse of a partial function to be a hylomorphism is presented and proved. The theorem is applied to many examples, including the classical problem of rebuilding a binary tree from its preorder and inorder traversals.

This thesis also investigates into the interplay between the above theorem and previous results on optimisation problems. A greedy linear-time algorithm is derived for one of its instances — to build a tree of minimum height. The necessary monotonicity condition, though looking intuitive, is difficult to establish. For general optimal bracketing problems, however, the thinning strategy gives an exponential-time algorithm. The reason and possible improvements are discussed in a comparison with the traditional dynamic programming approach. The greedy theorem is also generalised to a generic form allowing mutually defined algebras. The generalised theorem is applied to the optimal marking problem defined on non-polynomial based datatypes. This approach delivers polynomial-time algorithms without the need to convert the inputs to polynomial based datatypes, which is sometimes not convenient to do.

The many techniques are applied to solve the Countdown problem, a problem derived from the popular television program of the same name. Different strategies toward deriving an efficient algorithm are experimented and compared.

Finally, it is shown how to derive from its specification the inverse of the Burrows-Wheeler transform, a string-to-string transform useful in compression. Not only do we identify the key property why the inverse algorithm works, but, as a bonus, we also outline how two generalisations of the transform may be derived.

Inverting functions as folds

S-C. Mu and R. S. Bird. In Sixth International Conference on Mathematics of Program Construction, Dagstuhl, Germany, July 2002
[GZipped Postscript]

This paper is devoted to the proof and applications of a theorem giving conditions under which the inverse of a partial function can be expressed as a relational hylomorphism. The theorem is a generalisation of a previous result, due to Bird and de Moor, that gave conditions under which a total function can be expressed a relational fold. The theorem is illustrated with three problems, all dealing with constructing trees with various properties.