Theory and applications of inverting functions as folds.
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.
Introduction
The purpose of this paper is to describe one technique for inverting functions.
Why bother with inverse functions? The reader might ask. The reason is that
many problems in computation can be specified in terms of computing the
inverse of an easily constructed function. Indeed, compression is best specified
as the inverse of decompression, parsing the inverse of printing, and so on.
But these are not the only applications; inverse sometimes arise in unexpected
situations. To illustrate this, we will discuss three problems and solve them as
instances of a sinlge technique.
The first problem is that of breadth-first labelling. To breadth-first label a
tree with respect to a given list is to augment the nodes of the tree with
values in the list in breadth-first order. Figure 1 shows the result of breadth-first
labelling a tree with 13 nodes with the infinite list [1. While everybody
knows how to do breadth-first traversal, the closely related problem of e#cient
breadth-first labelling is not so widely understood.
How would one specify this problem, and what does it have to do with inverse
us call the type of binary trees Tree A and assume that we
Preprint submitted to Elsevier Science 16 May
a,1
a
f
l
Fig. 1. Breadth-first labelling a tree on the left with [1.
have at hand the function bft :: Tree A # List A, for breadth-first traversal,
and zipTree :: Tree A # Tree B # Tree zipping
together two trees of the same shape. To perform breadth-first labelling given
a tree t and a list x , we want to zip t with another tree u. What, then, does
this tree u has to satisfy? Firstly, it must be of the right shape, a condition
that can be enforced by zipTree. Secondly, its breadth-first traversal must be
a prefix of the given list x . We thus come up with the following specification:
where bft
y
Now look at the flow of information in the above specification. The functions
bft and ++ appear on the left-hand side, meaning that we wish the data to
go backwards through them. Let us denote the inverse of a function f by f # ,
pronounced "the converse of f " or more briefly "f wok". The formal definition
of f # will be delayed to Section 2.1. For now, let us say that f # y non-deterministically
yields some x such that f We rewrite the specification
as a pipeline from the right to the left, resulting in the following equivalent
point-free specification:
fst - cat #
non-deterministically splits the input list
in two, therefore fst -cat # takes an arbitrary prefix of the input list. The inverse
of bft gives us a tree whose breadth-first traversal matches the prefix. The tree
is then zipped with the input t .
This is an example where inverses arise unexpectedly in specification. Concise
as it is, how does one derive an algorithm from it? The answer, among two
other examples, is to be presented in this paper.
In the second problem, we are given a list of trees. The task is to combine
them into a single tree, retaining the left-to-right order of the subtrees. How
can we do this to make the height of the resulting tree as small as possible?

Figure

illustrates one such tree, of height 11, for given subtrees of heights
Fig. 2. A tree with height 11 built from trees with heights [2, 9, 8, 3, 6, 9]
[2, 9, 8, 3, 6, 9]. As the actual content of the subtrees isn't important, we can
think of them simply as numbers representing the heights.
The third problem is a classical one. It is well-known that given the preorder
and inorder traversals of an internally labelled binary tree, the tree can be
reconstructed uniquely if it contains no duplicated elements. The challenge is
to derive a linear time algorithm to do this.
All three problems involve building (or rebuilding) a tree of some kind, and
all can be specified in terms of the converse operation of flattening a tree
into a list of its values. Functional programmers are aware that flattening a
structure is usually performed by a fold operation. Consequently, building a
structure is usually performed by the converse operation, unfold. However,
there is no reason why the converse operation should necessarily involve an
unfold. The converse-of-a-function theorem, to which this paper is devoted,
gives us conditions under which the inverse of a function can be written as a
fold.
In the following sections we will show how this theorem can be applied to
derive solutions to the above problems. Functional programmers make use of
a handful of laws and theorems to transform specifications to optimising code.
The converse-of-a-function theorem is another useful tool worth adding to the
functional programmer's arsenal. Its joint use with the fold fusion theorem
turns out to be a recurring pattern in program derivation. Finally, we will
present and prove a generalised theorem allowing one to write the inverse of
a partial function as a hylomorphism.
Theory
The converse of a function is a relation, so our framework is of necessity a
calculus of relational programs [4,6]. In this section we will present enough
notation to describe the main ideas. Further concepts are introduced in Section
7.
2.1 Relations
Set-theoretically speaking, a relation R :: A # B is a set of pairs (a, b) where
a has type A and b type B . The converse of a relation is defined by flipping
the pairs, that is,
(b, a) # R # (a, b) # R
For the composition R - S :: C # A is defined
by
(c, a) # R -
Converse is contravariant with respect to composition, so (R - S
For each type A, a relation id A is defined by id
omit the subscript when it is clear from the context. A relation R :: A # B is
called simple if R - R # id . That is, every value in A is mapped to at most
one value in B . In other words, R is a partial function. A relation R is called
entire if id # R # - R, that is, every value in A is mapped to at least one value
in B . A relation is a (total) function if it is both simple and entire.
In this paper we write the type of a function as A # B , that of a partial
function as A -+# B , and that of a relation as A # B .
A relation is called a coreflexive if it is a subset of id . We use coreflexives
to model predicates. The ? operator converts a boolean-valued function to a
coreflexive:
(a, a) # p? # p a
For convenience, we let (a, a) # p? both when p a yields False and when a
is not in the domain of p. If we perform two consecutive tests, one of them
being stronger than the other, the stronger one can absorb the weaker one:
(p a # q a) # p? -
Given a relation R :: A # B , the coreflexive dom R :: A -+# A determines the
domain of R and is defined by
(a, a) # dom R #b
Alternatively, dom set intersection. It follows
that
dom R # R # - R (2)
The coreflexive ran R determines the range of a relation and is defined by
ran
When writing in a pointwise style, relations can be introduced by the choice
operator #. The expression x # y non-deterministically yields either x or y .
For example, the following relation prefix maps a list to one of its prefixes:
prefix :: List A # List A
where step :: A # List A # List A
step a
In each step of the fold we can choose either to cons the current item to some
prefix of the sublist, or just return the empty sequence [ ], which is a prefix of
every list. For a more rigorous semantics of #, the reader is referred to [29].
2.2 Folds
Datatypes come with fold functions. For lists, the Haskell Prelude function
List A # B is well known. A slight variation
for non-empty lists can be defined by
a
tip-valued binary tree by the following datatype:
data Tree
Its fold function can be defined as:
a
All of these folds are instances of a more general definition. A regular datatype
T can be defined as the fixed-point of a base functor F. That is to say, there
is an isomorphism
Datatypes are often parameterised. In that case # F has type FA (TA) # TA.
For example, cons-lists over an arbitrary is the fixed-point of FA
denoting types, we will write F(A, X ) instead of FA X , thinking of
F as a bifunctor. For more example, the base functor for non-empty lists is
and that for Tree is F(A, X
Given a base functor F for a datatype and a function f of type F(A, B) #
the catamorphism ([f ]) F :: is the unique function
satisfying
([f
The di#erent folds are special cases of ([f ]) F instantiated to di#erent base func-
tors, except that in Haskell, we usually divide f into several functions or
constants, each of which corresponds to the operation on a particular operand
of the coproduct in the base functor.
A functor on relations that takes functions to functions and is monotonic under
relational inclusion is called a relator. By switching from functors to relators,
the above theory extends to relations as well. A catamorphism ([R]) F , where R
is a relation of type F(A, B) # B , now has type . For a fuller account
of relator theory and relational catamorphisms, the reader is referred to [3,4].
3 The Converse-of-a-Function Theorem
The converse-of-a-function theorem, introduced in [6,29], tells us how we can
write the inverse of a function as a fold. It reads:
Theorem 1 (Converse of a be a function and
F the base functor for T. If R :: F(A, B) # B is surjective and f - R # F - Ff ,
The specialisation of this theorem to functions over lists reads as follows:
jointly surjective (meaning that {(base, base)} # a#A ran (step
and satisfy
f (step a x
Similarly, to invert a total function f on non-empty lists, Theorem 1 states
that if base :: A # B and step :: A # B # B are jointly surjective (that is,
ran base # a#A ran (step
f (base a) = [a]
We will postpone the proof of Theorem 1 to Section 7, where in fact a more
general result is proved. For now, let us see some of its applications.
4 Rebuilding a Tree from its Traversals
It is well known that, given the inorder and preorder traversal of a binary tree
whose labels are all distinct, one can reconstruct the tree uniquely. The problem
has been recorded in [27, Section 2.3.1, Exercise 7] as an exercise, where
Knuth briefly described why it can be done and commented that it "would
be an interesting exercise" to write a program for the task. Indeed, it has become
a classical problem to tackle for those who study program inversion to
derive a linear time algorithm, such as in [8,36]. As van de Snepscheut noted
in [36], one class of solution attempts to invert an iterative algorithm while
the other class delivers a recursive algorithm. In this section we will see how
our theorem helps to derive a functional program to solve the problem. Inter-
estingly, although we start with a recursive specification, Theorem 1 delivers
an algorithm falling into the first category.
We define the following datatype for internally labelled binary trees and its
fold function foldTree:
data Tree
Inorder and preorder traversal on the trees can then be defined in terms of
foldTree:
where inf a x
pre [
where pre a x
Assume a predicate distinct which yields true for a tree whose values in the
nodes are all distinct. The aim is to construct distinct?-(fork (preorder , inorder)) # ,
where fork (f , g)
Fig. 3. Adding a new node to a tree
We will try to apply Theorem 1 to construct the converse of a function as a
relational fold. However, due to its type, (fork (preorder , inorder)) # apparently
cannot be a fold on a recursive datatype. Instead, we define rebuild to be
rebuild
The relation inorder # constructs all trees whose inorder traversals meet a
given list. The coreflexive ((x )-preorder)? then picks the one whose preorder
traversal is the list x . Apparently, (fork (preorder , rebuild .
Furthermore, the predicate distinct can be enforced by the constrain that x
must not contain duplicated elements. The aim now is thus to derive rebuild x .
The derivation proceeds in two parts: to invert inorder as a fold on lists, and
to fuse ((x ) - preorder)? into the resulting fold.
4.1 Building a Tree by a Fold
According to Theorem 1, in order to invert inorder , we need a tree zero and
a relation add :: A # Tree A # Tree A that are jointly surjective and satisfy
inorder
inorder (add a x
Look at the second equation. It says that if we have a tree x whose inorder
traversal is as, the relation add must be able to create a new tree y out of
a and x such that the order traversal of y is a : as. One way to do that is
illustrated in Figure 3. We divide the left spine of x in two parts, move down
the lower part for one level, and attach a to the end.
To facilitate this operation, we introduce an alternative spine representation.
A tree is represented by the list of values and subtrees along the left spine.
type Spine List
For example, The tree to the left in Figure 3 is represented by the list
[(b,
The function roll converts a spine back into a single tree, and is in fact an
isomorphism between Spine A and Tree A.
roll :: Spine A # Tree A
where join u (a,
The advantage of this representation is that we can trace the spine upward
from the left-most leaf, rather than downwards from the root. As we will see
in the end of the next section, this is necessary for an e#cient algorithm.
The function inorder - roll flattens a spine tree. Our task now is to invert it
as a fold. We need a spine tree zero :: Spine A and a relation add :: A #
Spine A # Spine A satisfying
inorder (roll
inorder (roll (add a
An easy choice for zero would be [ ]. As for add , we claim that the following
definition satisfies (3):
add :: A # Spine A # Spine A
add a us = (a, roll vs) : ws
where vs ++ ws = us
The non-deterministic pattern in the definition of add , dividing the list us
into two parts, indicates that add a is a relation. For example, the tree to
the right in Figure 3 results from cutting the spine in the middle, yielding
[(a, roll [(b,
To show that add satisfies (3), we will need the following fact, whose proof is
left to the diligent reader:
inorder
(:). The proof of (3) goes:
{since concat and map distributes over ++}
concat (map (cons - (id - inorder)) ws)
{definition of concat and map}
concat (map (cons - (id - inorder)) ((a, roll vs) : ws))
inorder (roll ((a, roll vs) : ws))
It is also not di#cult to see that [ ] and add are jointly surjective: any non-null
tree can be a result of add . We therefore conclude that (inorder - roll)
4.2 Enforcing a Preorder
Having inverted inorder - roll , we can start the derivation:
rebuild x
{roll is an isomorphism}
{converse is contravariant}
{inverting inorder - roll as in the last section}
let hasPreorder
Except for the introduction of roll , the derivation so far is mostly mechanical.
As roll - (hasPreorder x)? is a partial function, it can be easily implemented in
Haskell. However, add is still a relation. If we can fuse (hasPreorder x)? into
the fold and thereby refine add to a partial function, the whole expression will
be implementable. Unfortunately, (hasPreorder x)? is a rather strong condition
to enforce. It is not possible to maintain this invariant within the fold before
and after each application of add - obviously, after adding a new element to
a tree, the new tree will certainly have a di#erent preorder traversal. Can we
invent something weaker that can be fused into the fold?
Define preorderF to be the preorder traversal of forests:
preorder
Look at Figure 3 again. The preorder traversal of the tree on the left-hand
side is [e, d , c, b] ++ preorderF [t , u, v , w that is, to go down along the left
spine, then traverse through the subtrees upwards. In general, given a spine
tree us, its preorder traversal is reverse (map fst us)++preorderF (map snd us).
We will call the part before ++ the prefix and that after ++ the su#x of the
traversal. Now look at the tree on the right-hand side. Its preorder traversal
is [e, d , a, c, b] ++ preorderF [t , u, v , w ]. It is not di#cult to see that when we
add a node a to a spine tree us, the su#x of its preorder traversal does not
change. The new node a is always inserted to the prefix.
With this insight, we split hasPreorder into two parts:
hasPreorder :: List A # Spine A # Bool
hasPreorder x us = prefixOk x us # su#xOk x us
su#xOk x us = preorderF (map snd us) isSu#xOf x
prefixOk x us = reverse (map fst us)
removes y from the tail of x and is defined by:
The expression x isSu#xOf y yields true if x is a su#x of y . The use of
boldface font here indicates that it is an infix operator (and binds looser than
function application). The plan is to fuse only su#xOk x into the fold while
leaving prefixOk x outside.
There is a slight problem, however. The invariant su#xOk x does not prevent
the fold from generating, say, a leftist tree with all Null along the spine, since
the empty list is indeed a su#x of any list. Such a tree may be bound to
be rejected later. Look again at the right-hand side of Figure 3. Assume we
know that the preorder traversal of the tree we want is
preorderF [t , u, v , w ]. The tree in Figure 3, although satisfying su#xOk x , is
bound to be wrong because d is the next immediate symbol but a now stands
in the way between d and c, and there is no way to change the order afterwards.
Thus when we find a proper location to insert a new node, we shall be more
aggressive and consume as much su#x of x as possible. The following predicate
lookahead x ensures that in the constructed tree, the next immediate symbol
in x will be consumed:
lookahead :: List A # Spine A # Bool
lookahead x us = length us # 1 # (map fst us) !! 1
=last x #
Apparently lookahead x is compatible with hasPreorder x . We will use both
su#xOk x and lookahead x as our invariant. Define
ok x us = su#xOk x us # lookhead x us
The derivation continues:
rebuild x
{as in the beginning of this section}
{since hasPreorder x us = prefixOk x us # ok x us}
{fold fusion, assume nodup x}
roll - (prefixOk x)? - foldr (add # x
The fold fusion theorem used in the last step is well-known (see, for example,
[6, Chapter 6]):
To justify the fusion step, it can be shown that if x contains no duplicated
elements, the following fusion condition holds:
(ok x)? (add a
where add # is defined by:
up :: A # Tree A # (Spine A - List
up a v ([
up a v ((b,
| us
In words, the function up traces the left spine upwards and consumes the
values on the spine if they match the tail of x . It tries to roll as much as
possible before adding a to the end of the spine.
We are now ready for the final optimisation. To avoid computing x #preorderF
(map snd us) from scratch each time, we can apply a tupling transformation
(see, for example [22] or [6, Chapter 3]), having the fold returning a pair. The
Haskell implementation is shown in Figure 4. The fold in rebuild returns a pair,
the first component being a tree and the second component being a list representing
x # preorderF (map snd us). Since the list is consumed from the end,
we represent it in reverse. The function rollpf implements roll - (prefixOk x )?.
data Tree a = Null | Node a (Tree a) (Tree a) deriving (Show,Eq)
rebuild :: Eq a => [a] -> [a] -> Tree a
rebuild
where add' a
up a v
up a v ((b,u):us, b':x)
| b ==
|
rollpf :: Eq a => ([(a,Tree a)],[a]) -> Tree a
| b ==
Fig. 4. Rebuilding a tree from its traversals via a fold.
a b c d e f
a b c d e f
a b d e f
a b d e f
a b d e f
a b c d e f
Fig. 5. Building a tree from its preorder. The preorder traversals of the trees under
the spine is printed in boldface font.

Figure

5 shows an example of this algorithm in action. The part in boldface
font indicates preorderF (map snd us). Notice how the preorder traversals of
the trees under the spine always form a su#x of the given list [a, b, c, d , e, f ].
We have actually reinvented the algorithm proposed in [8], but in a functional
style. The first step in [8] was to transform the recursive definition of
fork (preorder , inorder) into an iteration by introducing a stack. The same
e#ect we achieved by introducing the spine representation.
4.3 Building Trees with a Given Preorder
Hold on! The reader might complain: the derivation works because, by luck,
we choose the correct order. Had we started
preorder #
Now, we would have to invert preorder , and then enforce, on the resulting fold,
the constraint that the tree built must have a given inorder traversal. Does it
still work? In fact, it does, and the result is a new but complicated algorithm.
Therefore, we are only going to sketch an outline of its development.
We first seek to invert preorder . For this problem it turns out that it makes
more sense to work on forests rather than trees. Abbreviate List (Tree A) to
Forest A. Recall preorderF :: Forest A # List A defined by preorderF =
concat - map preorder . The reader can easily verify that preorderF can be
inverted as below:
preorderF
where step (a, us
us
us
# Node a
where the helper functions tip, lbr and rbr respectively creates a tip tree, a
tree with only the left branch, and a tree with only the right branch. They
are defined by:
lbr (a,
rbr (a,
In words, step extends a forest in one of the four possible ways, when applica-
ble: adding a new tip tree, extending the left-most tree in the forest by making
it a left-subtree or a right-subtree, or combining the two left-most trees.
The next step is to find out a rule deciding which of the four operations to
perform when adding a new value to a forest. We need to invent an invariant
to enforce in the body of the fold. To begin with, we reason:
preorder #
{some trivial manipulation}
b d c a e f
b c a e f
b c a e f
b d c a e f
b d c a e f
b d c a e f
Fig. 6. Building a tree from its preorder. The inorder traversals of the constructed
subtrees are printed in boldface font. The "skipped" subsequences between subtrees
are underlined. In the optimised code in Figure 7, they are paired with the subtrees.
Thus the type AForest .
Again, the condition inorder is too strong to maintain.
Luckily, it turns out that the weaker constraint
will do, where (isSubSeqOf x
subsequence of x . That is, we require that during the construction of the
forest, the inorder traversal of each tree shall always form segments of x , in
correct order. Figure 6 demonstrates the process of constructing the same
tree as that in Figure 5. This time notice how the inorder traversal of the
constructed forest always forms a subsequence of the given list [b, d , c, a, e, f ].
After some pencil-and-paper work, it is not di#cult to work out the rules to
extend the forest while maintaining the invariant. However, the rules consists
of totally eight cases and is relatively complicated comparing to the simpler
algorithms in Section 4.2. It is owing to the fact that we have four possible
operations to choose from, while in Section 4.2 there were only two - either to
go upwards one node along the spine or to stop and attach a new node. For
that reason we will just present the result.
A program implementing the algorithm is presented in Figure 7, where each
tree in the forest is annotated with some extra information to avoid recomputing
them (represented by the type AForest). After this optimisation, the
program runs in linear time, but with a bigger constant overhead than that
in Section 4.2.
rbr a
lbr a
type AForest a = [(Tree a, [a])]
rebuild :: Eq a => [a] -> [a] -> Tree a
rebuild fst . unwrap . snd . foldr add (reverse x, [])
where add :: Eq a => a -> ([a],AForest a) -> ([a],AForest a)
add a xu@(x, newtree a xu
add a xu@(x, (t,[]):us)
| isNext x a = (tail x, (rbr a t, []):us)
| newtree a xu
add a xu@(x,(t,b:bs):us)
| a ==
| isNext x a = (tail x, (rbr a t, b:bs):us)
| newtree a xu
join a (t,[])
join a (t,[]) us
join a (t,bs) us = (lbr a t, bs):us
newtree a
isNext [] a = False
isNext (b:bs) a = a == b
locate a [] x
where locate a y
locate a y (b:x) | a ==
| locate a (b:y) x
Fig. 7. Another way to rebuild a tree from its traversals via a fold.
Building Trees with Minimum Height
Next we consider the second problem of building a tree with minimum height.
A linear-time algorithm to this problem has been proposed in [5], but here we
will demonstrate how a similar algorithm can be derived.
We start with giving a formal specification of the problem. Define tip-valued
binary tree by the following datatype:
data Tree
The function flatten, which takes a tree and returns its tips in left-to-right
order, can be written as a fold:
flatten :: Tree A # List
Here wraps an item into a singleton list and foldTree is the fold
function for Tree, defined in Section 2.2.
Given a tip-valued binary tree whose tip values represent the heights of trees,
the function computing the height of the combined tree can also be defined as
a fold in the obvious way:
height :: Tree Int # Int
where ht a
where # returns the larger of its two arguments. The problem is thus to find,
among all the trees which flatten to the given list, one for which height yields
the minimal value. The specification needs to consider all possible results. For
that we need the power transpose operator #, also called the breadth function.
The power transpose operator # converts a relation R :: A # B to a function
. For a # A, the set (#R)a contains all values in B to which
a is mapped:
To extract a value from a set we need the relation min (#) :: Set A # A,
defined by
For this definition to be of any use, (#) has to be a connected preorder,
meaning an ordering which is reflexive, transitive, and compares everything
of the correct type. The relation min (#) will not in general be a function
because a preorder is not necessarily anti-symmetric.
For our problem, define (#) to be a comparison between the heights of two
trees:
Our problem can then be specified as:
Fig. 8. Adding a new node to a tip-valued binary tree
Similar to the last problem, the derivation also proceeds in two steps: to invert
flatten as a relational fold, and fusing something into the fold to eliminate its
non-determinism.
The function flatten can be inverted in a way similar to that in Section 4.1.
It is also helpful to switch to a spine representation. We define the following:
type Spine
A tree is represented by the list of subtrees along the spine, together with the
leftmost leaf. The conversion from a spine tree to the ordinary representation
can be performed by:
roll :: Spine A # Tree A
Since the range of flatten is the set of non-empty lists, we seek to invert it
to foldrn, the fold on non-empty lists. Theorem 1 says that (flatten - roll)
foldrn add one if the relations add and one satisfy:
flatten (roll (one
flatten (roll (add a (b,

Figure

8 illustrates the idea. We claim that the following definition satisfies
the requirement.
one
add a (b,
where ys ++
The proof is similar to that in Section 4.1 and is left to the reader as an
exercise.
Having inverted flatten, we get:
Furthermore, roll can be factored out of #:
where xs # ys # roll xs # roll ys, i.e., (# ) is the counterpart of (#) defined
on spine trees.
Since the relation add has choices when given a spine tree of length n,
the above specification generates an exponential number of trees. To eliminate
the non-determinism in add and thereby improve the e#ciency, we make use
of the following greedy theorem. Presented below is a special case of the more
general version proved in [6].
Theorem 2 (The Greedy Theorem (for non-empty lists)) Let base ::
be two relations. If step is monotonic on a
connected preorder (#), that is,
then we have
Informally, the monotonicity condition means that a worse partial solution in
some stage of the fold always gives a worse result. If this condition holds, then
at each stage of the fold we need only retain one of the best results computed
so far. Thus min (#) gets promoted into foldrn.
Had add satisfied the monotonicity condition (5) with respect to (# ), we
could apply the greedy theorem. However, that is not true: a tree with the
smallest height does not always remain the smallest after being extended by
add .
Fortunately, add is monotonic on a stronger ordering. We define:
heights (a,
In words, heights returns a list of heights along the left spine, starting from
the root. The relation add is then monotonic on #, defined by:
where (#) is the lexicographic ordering on sequences. This choice does make
sense: to ensure monotonicity, we need to optimise not only the whole tree,
but also all the subtrees on the left spine. The proof that add is monotonic
on (#), however, is quite involved and will not be presented here. The reader
is referred to [7] for more detailed discussion.
type
bmh :: [Int] -> (Tree Int, Int)
one
minadd :: Int -> SpineI -> SpineI
minadd a
where minsplit x
minsplit x (y:xs) | a < height y
&& height x < height
|
bin (x,a) y, ht a b)
ht a
roll :: SpineI -> (Tree Int, Int)
roll
Fig. 9. Code for building trees with minimum height
Applying the greedy theorem, we get:
Since one is a function, min (#one = one. With some analysis, we can
further optimise min (#add . Let (b, [x 1 , x 2 , -, x n ]) be the spine tree to
which we are about to insert a value a. It can be shown that in order to
construct the best tree under the ordering (#), we do not need to actually
check through all the n +1 possibilities. We can always break the list between
x i and x i+1 such that i is the smallest index such that a < height x i+1 and
height (roll (b, [x 1 , x 2 , -, x i ])) < height x i+1 . We will also omit the details and
refer the interested readers to [7].
The code is shown in Figure 9. As in the first problem, we annotate each tree
with its height to avoid re-computation. This algorithm is also linear in the
number of nodes in the tree.
6 Breadth-First Labelling
To breadth-first label a tree with respect to a given list is to label the nodes
in the tree in breadth-first order, using the values in the list. Jones and Gibbons
[17] proposed a neat solution to this problem, based on a clever use of
cyclic data structures. The problem was recently revisited by Okasaki [31]. We
are going to show how Okasaki's algorithm can be derived using the converse-
of-a-function theorem.
Let us go through again the specification in finer detail. Recall the data structure
for internally and externally labelled binary trees:
data Tree
The queue-based algorithm for breadth-first traversal is well-known:
List A
typeForest List (Tree
bftF :: Forest A # List A
bftF (Bin a x y
To perform the labelling, we use the following partial function zipTree:
zipTree :: Tree A # Tree B -+# Tree
zipTree (Tip a) (Tip
zipTree (Bin a x y) (Bin b u
Breadth-first labelling of a tree x can then be seen as zipping x with another
tree y , in which the breadth-first traversal of y is a prefix of the given list as:
bfl as
Equivalently,
bfl as
prefix ) as x
This completes the specification. The relation prefix non-deterministically
maps a list to one of its finite prefixes. The prefix is then passed to bft # ,
yet again being non-deterministically mapped to a tree whose breadth-first
traversal equals the chosen prefix. It is important that zipTree is a partial
function which yields a value only when the given two trees are of exactly the
same shape. Therefore, the tree composed by bft # - prefix can be zipped with
the input tree only if it is of the correct size and shape. The partial function
zipTree plays the role of a filter.
Since breadth-first traversal is an algorithm more naturally defined in terms
of queues of trees (or forests) rather than of a single tree, it is reasonable to
try to invert bftF rather than bft . The problem can be rephrased in terms of
bfl as ((zipForest - bftF # - prefix ) as [x ])
Here zipForest :: Forest A # Forest B -+# Forest (A-B) is a simple extension
of zipTree to forests, which, like zipTree, is a partial function:
zipForest
zipForest zipForest xs ys
Once the decision to focus on bftF is made, the rest is mechanical. To invert
bftF , we are to find base and step such that
bftF (step a
The value of base can only be [ ]. The derivation for step is not too di#cult
either. We start with the general case which does not assume any structure in
xs:
{definition of bftF }
bftF (Tip a : xs)
Therefore step a xs might contain (Tip a : xs) as one of the possible values.
But this choice alone does not make step jointly surjective with [ ], since it
cannot generate a forest with a non-tip tree as its head. We therefore consider
the case when xs contains more than two trees:
{definition of bftF }
bftF (Bin a x y : xs)
Therefore we define step to be:
step :: A # Forest A # Forest A
step a
Since a forest either begins with a tip tree, begins with a non-tip tree, or
is empty, step is jointly surjective with [ ]. The converse of bftF is thus constructed
as
Knowing that bftF # :: List A # Forest A is a fold, we can fuse zipForest and
bftF # as a fold :
zipForest - bftF
revZip a f (Tip b : ts
revZip a f (Bin b
where ys ++ [x , y
The expression zipForest -bftF # has type List A # Forest B # Forest (A-B ).
Consider (zipForest - bftF # ) x where x is a list of labels. Constructors building
x are replaced by revZip and stop, yielding a relation mapping an unlabelled
forest to a labelled forest. A pattern matching error will be invoked by stop
if x is too short, and by revZip if x is too long. Applying fold fusion again to
fuse zipForest - bftF # with prefix in e#ect adds another case for revZip, that
is, revZip a f [ which cuts the list of labels when the forest is consumed
earlier than the list. Still, the list of labels cannot be too short.
The resulting code is shown in Figure 10. It can be made linear if we use
an implementation of deques supporting constant-time addition and deletion
[9,30] for both the input and output of revZip. For clarity, we will just leave it
as it is. It is nothing more than an adaption of Okasaki's algorithm in [31] to
lists. In his paper, Okasaki raised the question why most people did not come
up with this algorithm but instead appealed to more complicated approaches.
Our answer is because they did not know the converse-of-a-function theorem.
7 The Generalised Converse-of-a-Function Theorem
The aim of this section is to prove the following generalisation of Theorem 1
to hylomorphisms:
Theorem 3 (Generalised converse-of-a-function theorem) Let S :: B
# A be a simple relation. If there exists a relation R :: F(C , B) # B and
a simple relation T :: F(C , are such that (i) dom
data Tree a = Tip a | Bin a (Tree a) (Tree a) deriving Show
where stop
revzip a f
revzip a f (Tip ts
revzip a f (Bin b u v
last (init ys), last ys)
Fig. 10. Code for breadth-first labelling
In words, Theorem 3 gives conditions under which the converse of a simple
relation can be expressed as a hylomorphism. Its relationship with Theorem 1,
as well as other notions we need to establish such a connection, will be given
in Section 7.1.
The new ingredient in Theorem 3 is F-well-foundedness. The notions of well-foundedness
and admitting induction are of great importance in computing
science. In [13], Doornbos gave a careful analysis of the relationship of these
two notions and proposed several di#erent generalisations of them. The notion
of F-well-foundedness is defined in [13, page 102] as
relation R is F-well-founded if and
only if, for all relations T , the equation has a unique solution
for X .
Now we will give a proof of Theorem 3. Taking converses of both sides, the
aim is to prove that under the given conditions. We know
that the hylomorphism ([T ]) F - ([R]) # F can be characterised as the least solution
for X of the equation assumption (iii) that R # is
F-well-founded, we know that ([T ]) F - ([R]) # F is in fact the unique solution. Now
we will show that S is also a solution. The proof goes:
by assumption (i)}
{since ran R # R - R # }
# {by assumption
by assumption (i)}
{since dom S # S # - S}
# {by assumption
{since T - FS is simple}
Theorem 3 is thus proved.
7.1 Well-foundedness and Reductivity
The proof of Theorem 3 makes use of F-well-foundedness to guarantee the
uniqueness of solution. For practical proposes, however, a stronger property
is needed. The reason is that F-well-foundedness alone does not guarantee
termination if we view a hylo-equation as a left-to-right rewrite rule and evaluation
of non-determinism as demonic. As a counterexample 1 , take
and consider the relation #f , id# a = (f a, a). The recursive program
does not terminate if S is strict on the second component
of the input pair. Yet #f , id# is F-well-founded.
It was shown in [13, Section 7.5], however, that termination is guaranteed for
F-reductive relations. The notion of F-reductivity was introduced in [14,15]
and [13, Section 6.3] as one of the ways to generalise the notion of admitting
induction to arbitrary datatypes.
is said to be F-
reductive if and only if for all coreflexives C # id A :
Here the monotype factor operator \ is defined by the Galois connection
(R - D) # C
1 Due to [13, page 104].
2 For more intuition behind the monotype factor, the reader is referred to [14].
for all relations R and coreflexives C and D . Property (6) can be translated
to point-level to aid understanding 3 :
In words, R is F-reductive if it can be used for inductive proofs in the following
way: we may conclude that a property C is universally true if we can show
that all a satisfies C , given that any "R-predecessor" a # of a is an F-structure
containing only elements satisfying C .
Several properties concerning F-reductivity are handy for our purpose. The
following facts are respectively Theorem 6.25, Theorem 6.19, and Theorem
6.22 of [13]:
Fact 6 F-reductivity implies F-well-foundedness.
Fact 7 If T is F-reductive, so is FS # - T - S for simple S .
Fact 8 # F is F-reductive.
Since F-reductivity guarantees termination and, according to Fact 6, is stronger
than F-well-foundedness, the F-well-foundedness requirement in Theorem 3 is
always strengthened to F-reductivity in practice. The question of how to construct
F-reductive relations has been discussed in depth in [14,13].
We have yet talked about the relationship between Theorem 1 and Theorem
3. To begin with, note the following lemma:
Lemma
Theorem 1 follows as a special instance of Theorem 3 by taking
S to be an entire relation as well as a simple one, that is, a function. An
entire relation S is one for which dom translates to
the requirement that R be a surjective relation. As for condition (iii), R # is
F-reductive if T # is, according to Lemma 9 and Fact 7. However, Fact 8 says
that T #
F is indeed F-reductive. Since ([# F ]) we then obtain the
the conclusion of Theorem 1.
The proof for Lemma 9 can simply be extracted from the proof for Theorem
3. For completeness, it is given below:
R
# {since
dom S - R
3 On the other hand, (6) can be written more concisely as -(R\ -
- stands for the least fixed-point operator.
{since dom S # S # - S}
# {since S - R # T - FS}
8 Applications of the Generalised Theorem
Theorem 3 can potentially be very powerful since it allows the functor F,
which determines the pattern of recursion, to be independent from the input
and output types. A much wider class of algorithms can thus be covered. One
application we have found for Theorem 3 is to prove that a loop implements
the inverse of some function. A loop can be specified relationally by
The relation S initialises the loop, while R serves as the loop body. The domain
of T represents the terminating condition and therefore ought to be disjoint
from the domain of R. Given a relation R, the reflexive transitive closure R #
is the smallest reflexive transitive relation containing R. More generally, the
can be defined
as a least fixed-point:
A key observation here is that a closure can also be written as a hylomorphism,
with the base functor
{definition of closure}
Here the unfolding phase wraps the input value with an inl , before wrapping
it with an indefinite number of inr s. The folding phase then replaces the inl
with S and each inr with an R. The exact number of iterations performed is
determined the termination test T .
Given a function f , let us instantiate Theorem 3 to discover the conditions
under which f
. Since dom instantiates to ran [S , That is, S
and R shall be jointly surjective.
. Condition (ii) can be divided into two parts:
Shunting the functions to the other side, we get:
which looks familiar enough! Think of f # as an invariant. The first half
says that the initial values satisfies the invariant, while the second half says
that given inputs satisfying the invariant, the loop body R maintains the
invariant.
. Condition (iii) requires that [S , R] # be F-well-founded. Intuitively speaking,
we want R to "decrease" the loop variables in some sense.
Assume we wish to prove that T - R # - S correctly implements a specification
X . As will be shown in the next two sections, in some occasions X can be
quite naturally factored into T - f # for some f . We then just need to check the
three conditions above.
8.1 The String Edit Problem
The string edit problem [10, Chapter 15] is a typical example for dynamic
programming. Recently it has drawn much attention due to its application in
DNA sequence matching. In its simplest form, we are given two strings, one
as the source and one as the target, and some available commands. Imagine
a cursor positioned to the left of the source string. We assume the following
commands:
. Ins c: to insert a character c at the current position.
. Del c: to delete the character c in the current position.
. Cpy c: to skip the current character c and move the cursor one position to
the right.
The task is to find the shortest sequence of commands to transform the source
string to the target string. In more complicated variations we might be given
more commands and their weights may vary.
We represent the three commands with a datatype Op:
data Ins Char | Del Char | Cpy Char
To specify the problem, one might attempt to construct a relation taking the
pair of strings and return an arbitrary sequence of commands relating the
strings. In fact, it is easier to construct its inverse. The function exec below
executes a sequence of commands, starting from a pair of empty strings, and
yields two strings:
where step
The exec function starts with two empty strings and tries to reconstruct the
original source and target strings. After an Ins operation, an extra character
is added to the target string. The Del operation is treated as a statement that
the source string has an extra character. A Cpy command can be viewed as
saying that the two strings has a common character at the current position.
The converse of exec, on the other hand, takes two strings and yields a sequence
of commands reducing them to a pair of empty strings (thus showing that the
commands transform one string to another). The string edit problem is thus
defined by:
In [6, Section 9.2], Bird and de Moor derived from this specification a dynamic
programming algorithm using their dynamic programming theorem for
converse of folds.
Yet some others prefer to describe exec # as an iterative process. That is, they
claim that exec
start
move Ins (last
# (init x , y , Del (last x
# ((init x , init y , Cpy (last x last x last y)
The loop starts with the two strings and an empty list of commands. The
non-deterministic loop body move then try to recover what the last command
might be by trying all possible commands. The iteration repeats until both
strings become empty. Notice that move is defined as a partial relation which
yields value only when not both of x and y are empty. This was the view taken
by Curtis in [11]. Once a specification is written in terms of a min R after a
loop, theories in [11] are ready to transform it to a dynamic programming
algorithm, if certain conditions are satisfied.
We will not go into how the problem can be solved using the developed the-
ories. Instead we will bridge the gap between the two views on exec. In other
words, how do we know the claim that exec
With the discussions in the opening of Section 8 in mind, we generalise exec
to execWith such that
The function execWith has type (String-String-List Op) # (String-String)
and is defined by:
execWith
It is just replacing the constant ([ ], [ ]) in the definition of exec with a given
argument y). The task is then to show that execWith One
may also think of it as that we have just invented and proposed execWith # to
be the loop invariant, and are about to check whether this invariant works.
The invariant says that, denoting the input pair of strings by (x , y), and the
intermediate values at any point of computing move # - start by
executing the commands ops on
Now we will check the conditions one by one:
. Condition (i) holds: start and move are jointly surjective.
. Condition (ii) requires:
execWith - start # id
execWith - move # execWith
The first one trivially holds. The second inclusion holds because move undoes
the last step of execution. Thus the domain of the left-hand side is
restricted to triples where one of the two strings is not empty. The execution
still yields the same result.
. For condition (iii): move is well-founded because it always reduces the length
of the first two components of the triple.
Therefore, we conclude that execWith
start .
8.2 Building Trees by Combining Pairs
Recall again the following datatype for leaf-valued binary trees:
data Tree
And yes, we are about to introduce yet another approach to building trees out
of a list.
The majority of this paper has been focusing on inverting flatten to a fold.
There is yet another alternative way to build a tree from a list: starting from
a list of tips, keep combining adjacent trees until only one is left. The process
can be characterised by
where join
Our aim is, of course, to show that flatten
that
We have just proposed this invariant
for the loop: that during the iterations, the forest always flattens to the given
list. Now we check that flattenF
. Indeed, map Tip and join are jointly surjective. The former covers any lists
of tip trees while the latter covers the rest.
. We need to verify that:
concat - map flatten - map Tip # id
concat - map flatten - join # concat - map flatten
The first inclusion obviously holds. The second holds because join restricts
the domain of the left-hand side to lists with at least two trees, but not
a#ecting the result returned.
. Finally, join is well-founded because it reduces the length of the forest.
It then follows that flattenF consequently, flatten
One might relate this small exercise to merge sort. There are two ways to
implement merge sort: one is to implement it as a hylomorphism, where the
unfolding phase expands a tree and the folding phase performs merging at
each node. The other is to implement it as a loop: to start with a map wrap,
converting the input to a list of singleton lists, and then to iteratively merge
adjacent lists until only one list is left. The first can be said to be top-down
and the second bottom-up. A similar reasoning converts the former to the
latter. However, an additional distributivity property of list merging will be
needed in the proof. A similar problem was treated in [21], where a top-down
algorithm was also transformed to a bottom-up one.
9 Conclusions and Related work
The idea of program inversion can be traced back to Dijkstra [12]. However,
given the importance of inversion as a specification technique, relatively few
papers have been devoted to the topic. Of those that have, most deal with program
inversion in the context of imperative programs and refinement calculus.
A program is inverted by running it "backwards" and the challenging part is
when we encounter a branch or a loop [37,2,34]. The classic example was to
construct a binary tree given its inorder and preorder traversal [18,19,8,36,35].
Inversion of functional programs has received even less attention. Most published
results (e.g. [28,20]) are based on a "compositional" approach, which is
essentially the same as its imperative counterpart: if h is defined by f - g , then
. The inverse of f and g are then recursively constructed until we
reach primitives whose inverses are pre-defined. This rather control-oriented
view is complemented by a more data-oriented view in [23,24]. The paper
generalised functions to arrows. They then considered polytypic operations
on datatypes and ensured that an operation and its inverse carrying things
out in reverse order (such as "map from the left" and "map from the right")
are always constructed in pairs. E#orts have also been made to automate the
process, such as in [1]. This paper also contains a detailed bibliography.
The converse-of-a-function theorem, however, takes a non-compositional approach
to invert a function. To invert a function, what matters is not how
it is defined but what properties it satisfies. We have applied the converse-
of-a-function theorem to three examples. The inverted function is usually a
non-deterministic fold. To make it useful, it is often composed before some
other function which acts as a filter. The fold fusion theorem is then applied
to fuse the filter into the fold to remove the non-determinism, refining the
specification to an implementable function. This pattern of derivation turned
out to be useful in solving many problems.
This technique is not new. Similar techniques have been adopted in, for exam-
ple, [25] and [32]. However, to the best our knowledge, it was de Moor [6,29]
who first presented the technique as a theorem, suggesting a wider range of
application. The problem dealt with in [29] was precedence parsing, leading
to a derivation of Floyd's algorithm. It is therefore not a coincidence that the
algorithms we developed in Section 4 resemble parsing. The authors believe
that it is possible, although a tiresome task, to derive a shift-reduce parsing
algorithm by generalising the reasoning in Section 4.
It was also pointed out that the problem of building trees of minimum height
can be seen as a special case of Knuth's generalised shortest path problem [26].
The problem addressed was, given a context-free grammar and a cost function
on parse trees, to construct a word and its parse tree whose cost is minimum.
Given a list of numbers, we can construct an ambiguous grammar whose only
word is the list, while the possible parse trees include all binary trees. The
cost of a parse tree would simply be its height. Knuth's algorithm can thus
be applied to find the best parse yielding the minimum height. It would be
interesting to investigate whether the linear time algorithm in Section 5 is an
optimised special case and how they relate to each other.
One natural question is how widely the theorem can be applied. In other words,
how to determine whether the converse-of-a-function theorem can be applied
to a particular function. Part of the answer is given in [16]: if the converse of
a function can be written as a fold, the function itself must be an unfold. The
necessary and su#cient conditions for a function to be an unfold given in [16]
can thus be used as a test before applying the converse-of-a function theorem.
One possible reason why inverting imperative programs were more often talked
about could be that theories about non-determinism in the context of refinement
calculus are more established. In [37,2], for instance, Dijkstra's guarded
command language was extended to include angelic choices as well as demonic
choice. It was then shown that the inverse of a demonic program is angelic.
Corresponding theories for relations are still being developed [33]. It is interesting
to see how that would benefit the research about inverses for relations.
We have not fully exploited the generality of Theorem 3. It can potentially
be very useful since it allows the functor F, which determines the pattern of
recursion, to be independent from the input and output types. A much wider
class of algorithms can thus be covered. We have applied the theorem to the
simple cases that F(A, X verify some loop-based algorithms.
The authors are enthusiastic to see more examples for which the more general
theorem is necessary.

Acknowledgements

Thanks are due to members of the Algebra of Programming group in Oxford
University Computing Laboratory, to Oege de Moor, for his interest, encouragement
and comments throughout the development of this paper, and to
Roland Backhouse, who kindly pointed out the relation with Henk Doorn-
bos's work and the advantage of basing the theorem on F-reductivity. The
authors would also like to thank the anonymous referees for detailed and useful
advices.



--R

The universal resolving algorithm: inverse computation in a functional language.
Statement inversion and strongest postcondition.
Relational catamorphisms.
Elements of a relational theory of datatypes.
On building trees with minimum height.
Algebra of Programming.
Algebraic methods for optimization problems.
Program inversion: more than fun!

Introduction to Algorithms.
A Relational Approach to Optimization Problems.
Program inversion.
Reductivity Arguments and Program Construction.

Reductivity. Science of Computer Programming
When is a function a fold or an unfold?

The Science of Programming.
Inorder traversal of a binary tree and its inversion.
On the synthesis of function inverses.
Constructing tournament representations: An exercise in pointwise relational programming.
Construction of list homomorphisms via tupling and fusion.
compact printing and parsing.
data conversion programs.
Relational Programming
A generalization of Dijkstra's algorithm.
The Art of Computer Programming Volume
Inversion of applicative programs.
relational programming.
Simple and e


Binary multirelations.
Running programs backwards: the logical inversion of imperative computation.
Inorder traversal of a binary heap and its inversion in optimal time and space.
Inversion of a recursive tree traversal.
Program inversion in the refinement calculus.
--TR
Inorder traversal of a binary tree and its inversion
Program inversion in the refinement calculus
Program inversion
On the synthesis of function inverses
Statement inversion and strongest postcondition
Real-time deques, multihead Turing machines, and purely functional programming
Reductivity
Algebra of programming
Synthesis of functions by transformations and constraints (poster)
The art of computer programming, volume 1 (3rd ed.)
Breadth-first numbering
The Science of Programming
Introduction to Algorithms
data conversion programs
Compact Printing and Parsing
Construction of List Homomorphisms by Tupling and Fusion
Invited Talk
Elements of a Relational Theory of Datatypes
Inorder Traversal of a Binary Heap and its Inversion in Optimal Time and Space
Induction and Recursion on Datatypes
The Universal Resolving Algorithm
Constructing Tournament Representations
Algebraic methods for optimization problems
Inversion of a Recursive Tree Traversal
FUNCTIONAL PEARL

--CTR
Kiminori Matsuzaki , Hideya Iwasaki , Kento Emoto , Zhenjiang Hu, A library of constructive skeletons for sequential style of parallel programming, Proceedings of the 1st international conference on Scalable information systems, p.13-es, May 30-June 01, 2006, Hong Kong
program derivation;program inversion