Virtual Data Structures

Doaitse Swierstra^{1} and Oege de Moor^{2}

1 Department of Computer Science, Utrecht University, P.O. Box 80.089, 3508 TB Utrecht, The

Netherlands 2 Programming Research Group, Computing Laboratory, 11 Keble Road, Oxford OX1 3QD,

United Kingdom

1 Introduction

The purpose of this paper is to demonstrate a number of techniques which may be used in calculating algorithms for sequence-oriented problems. It may be considered as a further step in the development of a programming method which started with [5]. The basic observation underlying this method is that algorithms can be the result of a systematic development, in which all design decisions and applied insights are clearly identifiable. One might even claim that the essence of an algorithm is its derivation, and not the program text that results from such a derivation.

Originally the theory for algorithm derivation was presented in an imperative setting, using predicate calculus as the main tool for reasoning about the various steps in a derivation. A complicating factor has been that, in deriving a program, the designer has to cope with two different formalisms and an often intricate relationship, namely between the programming language itself and the formalism for reasoning about the program under development. Unfortunately, the rich expressiveness of the predicate calculus, which has been used for the latter, has not forced algorithm developers to express themselves in more structured and more abstract ways. As a result this approach can still be considered as fairly ad hoc, although various attempts have been made to merge the two components of the formalism [10].

In [7] a more calculational style of program development has been advocated, in which the program itself, instead of appearing as a side-effect of a derivation, is the subject of transformations. The idea is that the process of developing an algorithm consists of a sequence of transformations, starting with an inefficient specification, which may even be nonexecutable, and resulting in an executable, efficient program. In [2] this process has been demonstrated to be effective, introducing the so-called Segment Decomposition Theorem, which captures many instances of the design steps replacing a constant by a variable and strengthening the invariant, which are well known from the imperative school [6].

The relative success of this approach lies in a well-chosen combination of a notation for functions, which lends itself to easy manipulation, and the introduction of higher order functions which enables a more abstract view of many algorithms. As a result of this work the insight has come that control constructs like maps, filters and reductions, which were originally used in a a sequence oriented setting, could be formulated more abstractly by making use of the concept of a homomorphism. Homomorphisms naturally come into existence when one generalises reduce over lists (corresponding to looping over an array in an imperative setting) to any inductively defined type. Generalisations of other oftoccurring control structures, i.e. recursion patterns, has led to a wealth of other classes of morphisms; an overview is given in [9].

The way data structures are considered has shifted in recent years from a more implementation and representation oriented view towards an algebraic view. Within the field of transformational functional programming, the beginning of this shift was marked by the identification of the Boom[4]-hierarchy (“boom” is also the Dutch word for tree), which shows clearly the algebraic relationship between binary trees, sequences, bags and sets. This hierarchy is established by starting from the signature describing binary trees, and subsequently adding laws to this signature:

JV ::= □ : ϵ [−] : A ++ : JV × JV,

where we are assuming that A is the base type over which the structures are defined and that the following law holds for the unit element □:

□ ++ s = s ++ □ = s

If ++ satisfies no further laws, JV is the data type of unlabelled binary trees. Other data types can be obtained by postulating further laws. One thus obtains the hierarchy summarised below:

associativity (x ++ y) ++ z = x ++ (y ++ z) sequences
commutativity  x ++ y = y ++ x  bags or multisets
idempotency  x ++ x = x  sets

The structure of this paper is as follows. In Sect. 2 we will introduce the class of problems that is the subject of this paper. In Sect. 3 we will introduce the concepts which are necessary to understand the derivations to be given in Sect. 5. In Sect. 4 we will introduce the concept of a virtual data structure, which allows one to optimise certain function compositions. The importance of this optimisation is that one can reason at the level of function composition as long as possible, only eliminating intermediate results in the final transformation step.

In this paper there is no separate section on notation. This reflects our view that at the current state of research, there is no such thing as a fixed notation. Indeed, part of the research is to discover which concepts are worth a notation of their own, and what notations are useful in finding derivations. For this reason notation will be introduced on the fly.

The calculus used in this paper will be rather informal. Current active research in this area has provided a formal underpinning of the presented notation, and of the laws formulated using the notation. These foundations are however not the subject of the research described here; the interested reader is referred to [1][11]. A reader feeling that a proper understanding of functional programming is lacking is referred to [3].

At the end of this section we want to stress that most of the techniques we are presenting here have been known for a long time in the area of compiler construction, and as such belong to the tool-box of most compiler writers. It is the different use and formulation of these concepts which makes them applicable in a calculational style of program derivation. Where appropriate we will indicate such correspondences.

2 The Problem Class

In this paper we study problems of the following form:

f = compose/ ∘ property^{∗} ∘ generator ,  (1)

where ∘ denotes function composition. The generator is a set-valued function that generates candidates for a solution. For each of these candidates a property is computed (hence the ^{∗} symbol, which indicates that the function is supposed to be applied to each element of the sequence, bag or set which is returned by the generating part), and finally all these intermediate results are used in computing the final value, by making use of a so-called reduction in combination with the binary function compose. Hence if generator.x = { a_{0}, a_{1}, …, a_{n} } then

f.x = (property.a_{0})compose(property.a_{1})compose(property.a_{2}) … (property.a_{n}) .

A typical generator is the function segs, which returns all contiguous subsequences of its arguments:

segs.x = {y|∃u, v : u ++ y ++ v = x} .

Other examples of generators are

inits.[a_{0}, a_{1}, …, a_{n}] = \{ \begin{matrix}[ ], [a_{0}], [a_{0}, a_{1}], \\ …, \\ [[a_{0}, a_{1}, …, a_{n}]] \} \end{matrix}

splits.[a_{0}, a_{1}, …, a_{n}] = \{ \begin{matrix}([ ], [a_{0}, a_{1}, …, a_{n}]), \\ ([a_{0}], [a_{1}, a_{2}, …, a_{n}]), \\ …, \\ ([a_{0}, a_{1}, …, a_{n−1}], [a_{n}]), \\ ([a_{0}, a_{1}, …, a_{n}], [ ]) \} . \end{matrix}

For example the following specification says that a sequence is ascending:

asc = ∧/ ∘ (≤ ∘ (↑/ ×↓/))^{∗} ∘ splits ,

where ↑/ computes the maximum value of a sequence, by reducing it with the maximum operator ↑, and ↓/ the minimum value. The functions splits is defined by

splits.x = {⟨u, v⟩|u ++ v = x} .

The × operator takes two functions as its arguments and returns a function which applies these functions to both components of its argument and returns the pair of the two results, i.e.:

(f × g).⟨x, y⟩ = ⟨f.x, g.y⟩ .

These pairs are subsequently each subjected to a comparison (≤), and finally the conjunction of all these comparisons is taken (∧/). In words, this would mean that we consider a sequence ascending if, whichever the way a sequence has been split in two, the maximum value of the left part is always at most the minimum value of the right part.

Another property that might occur in our generic specification is that a sequence is balanced:

(= 0) ∘ +/ ,

which describes that the sum of the elements should be equal to zero. Yet a third example of a property is low:

(≤) ∘ ⟨↑/, #⟩,

which indicates that the maximum value of a structure should be less than its size, returned by the function #. We have used ⟨f, g⟩.x = ⟨f.x, g.x⟩.

A further useful operator we will use is the filter ◁, which takes as its left operand a predicate, applies this function to all elements of a structure, and returns the structure containing all elements which satisfy the predicate. So the specification of a function which computes the length of the longest ascending sequence might be written as:

lup = ↑/ ∘ #^{∗} ∘ asc ◁ ∘ subs .

3 Design Steps

In this section we discuss a strategy for solving problems of the aforementioned kind; in doing so we will show how different design decisions may lead to totally different solutions, which are not easily related without taking their derivations into consideration. The strategy consists of both the identification of a number of decision points where a design decision has to be taken, and the identification of the alternatives between which a choice may be made.

As we will see these decision points are described in a rather blunt way, using informal phrases like pick the right one. It will not always be immediately clear what will be the right choice, and learning what will be the right choice is a matter of experience, trial and error. Keep in mind, however, that once we have found the right path, it will be possible to clearly indicate which decisions have been taken, and probably even why those decisions eventually turned out to be successful. In this respect the process of deriving more and more algorithms resembles the process of putting up maps at the branches in a highly structured maze; a more useful approach than putting up maps in a flat desert without any landmarks.

3.1 Algebraic Views

The Concept of a View. When giving an algebraic specification of an abstract data type, it is easily overlooked that such a description is not unique. Most programming languages only provide a single built-in construct for a specific class of data types, and thus favour only one specific algebraic view. Often it is possible to provide a different view, containing different operations and different laws. What makes two different views equivalent is that it is possible to express the operations of one view in the operations of the other view and vice versa, and that the laws obeyed by these mapped operations remain valid in the target view.

The choice of an algebraic view resembles the choice for a specific context free grammar in describing a language. There may be many grammars describing the same language, as there are many views describing the same data. The parsing process corresponds in this case to a conversion from one view, i.e. a list of characters with some structure, into a value of the initial data type of another view, in this case described by the grammar.

Possible Views. In this paragraph we will discuss some useful views on sequences. We stress however that the number of alternatives is almost unbounded, and that having a library of such possible views at hand is quite a useful tool in deriving algorithms.

Most functional languages take the cons view for granted in which sequences over A are elements of the following initial data type for which we will reserve the word list:

CV ::= □ : ϵ ⊢ ≻ : A × CV .

Equally acceptable, and well known views are provided by the join view:

JV ::= □ : ϵ [−] : A ++ : JV × JV ,

the snoc view:

SV ::= □ : ϵ ⊣≺ : SV × A ,

the labelled tree view:

LTV ::= □ : ϵ − ≺ − ≻ − : LTV × A × LTV ,

and the spine view:

SPV ::= □ : ϵ ≺: SPV × (LTV × A) ,

which is a mixture between the labelled tree view and the snoc view. In [13] some examples of views and the conversions between them may be found. In the sequel we will encounter such a conversion.

We will now introduce our first decision point.

Algebraic View: Inspect what algebraic view the program is supposed to accept, and decide whether it is useful to convert the data into a different view.

In the example derivations we will encounter some criteria on which such a decision might be based. Notice however that this observation is not a very deep one; it is just a different way of expressing that we store the input to be treated into a convenient data structure, which is a common step in program design.

Catamorphisms. The views introduced in the previous parts may all be considered as the definitions of initial algebras, where the operators may be considered as termconstructors. Since we will encounter many (uniquely defined) homomorphisms from such initial algebras into other algebras we will give them a special name, i.e. catamorphisms, and introduce a special notation for such morphisms. Since such a catamorphism is uniquely defined by the algebra that is its codomain, we will denote them by summing up the operators associated with the codomain between banana-brackets.

As an example consider the function length, which computes the length of a list, and which might be defined as follows:

length.(a ⊢ ≻ x) = 1 + (length.x)
length.□  = 0 .

In our notation this function, which is a catamorphism from lists to the algebra of integers, may be written as (|0, (1 ˆ+)|), where (1 ˆ+) is the operator corresponding to the ⊢ ≻ -constructor and 0 the operator corresponding to the □-constructor. In this notation the ˆ+ is a so-called lifted operator which is defined by (f ˆ+g).⟨x, y⟩ = (f.x) + (g.y), and 1 is the constant function always returning 1. We will use the expression ⊗/ as an abbreviation for catamorphisms of the form (|1_{⊗}, ⊗|) operating on CV or SV, when (1_{otimes}, ⊗) is a monoid.

As a final notion in this section we define the so-called accumulation //, which may be expressed in terms of reductions and inits by:

⊘// = ⊘/^{∗} ∘ inits .  (2)

The concept is important in the derivation of many programs, since its use in general introduces a considerable reduction in the complexity of the program. So it is the case for lists that the left hand side of (2) may be computed in O(n) steps, whereas a naive implementation of the right hand side will take O(n^{2}) steps. That this is indeed the case may be deduced from the following alternative, but equivalent, definition of //:

⊘// = π_{2} ∘ (|⟨1_{⊘}, [1_{⊘}]⟩, ˜⊘|)
⟨a, b⟩ ˜⊘c = ⟨a ⊘ c, b⊣≺ (a ⊘ c)⟩ .

3.2 Algebraic laws

Once a specific algebraic view has been chosen, there is often a further choice to be made. Due to the algebraic laws associated with the view, there may exist freedom in the way a value is represented, and thus the conversion from the given data type into the required data type is a non-deterministic function (or relation). The laws define equivalence classes of terms, and any element of such a class might be chosen. Depending on the further functions which will be applied to the representation, it may be worthwhile to make use of the available freedom to choose a specific element from the class.

Here we will discuss shortly some of the laws associated with the different views. There are no laws associated with CV and SV views on sequences: the representation of a sequence as a list is unique, and the associativity of the ++-operator is heavily used when converting from the join-view to the cons- or snoc-view. When representing bags in CV however we will get the following additional law, representing the translation of the law of commutativity as formulated in JV in the previous section.

a ⊢ ≻ (b ⊢ ≻ x) = b ⊢ ≻ (a ⊢ ≻ x) ,

and the following law for representing the idempotency of set union:

a ⊢ ≻ (a ⊢ ≻ x) = (a ⊢ ≻ x) .

A similar line of reasoning holds for LTV, where we have assumed that every next law is used in the context of the laws introduced earlier, i.e. the formulation of the law of commutativity makes use of associativity:

associativity : (x ≺ a ≻ y) ≺ b ≻ z = x ≺ a ≻ (y ≺ b ≻ z)
commutativity :  x ≺ a ≻ y = y ≺ a ≻ x
idempotency : □ ≺ a ≻ □ ≺ a ≻ y = □ ≺ a ≻ y

and for the spine-view, assuming the corresponding laws for LTV part are introduced accordingly:

associativity : (x ≺ ⟨k, a⟩) ≺ ⟨l, b⟩ = x ≺ ⟨(k ≺ a ≻ l), b⟩
commutativity : (x ≺ ⟨k, a⟩) ≺ ⟨l, b⟩ = (x ≺ ⟨k, b⟩) ≺ ⟨l, a⟩
idempotency : (x ≺ ⟨l, a⟩) ≺ ⟨l, b⟩ = x ≺ ⟨Nil ≺ a ≻ Nil ≺ b ≻ l⟩

We will conclude this part with formulating our second decision point:

Algebraic Laws: Inspect what algebraic laws apply to the chosen view, and make use of these laws to pick useful elements from congruence classes of terms.

As a guideline in choosing the right element one may inspect properties of the generators and further functions in the expression at hand.

One may compare this freedom of choice with the use of an ambiguous context free grammar, giving rise to several different parse trees for a given sentence. So a grammar might contain a production of the form:

< expr >::=< expr >< operator >< expr >,

and a parser might use the priorities of the operators to return a parse tree which reflects the intended meaning of the expression.

3.3 Generators

Once a specific view has been chosen and a special element within this view for representing the value at hand, there is still choice left in picking a convenient function for generating the candidates for further processing. This choice is surprisingly rich.

In [2] only a two views are considered, i.e. CV and SV. Neither of these views has laws associated with it, and a single form of generating segments is studied, leading to the aforementioned segment decomposition theorem.

The generator used for generating all segments may be defined as:

segs = ++/ ∘ tails^{∗} ∘ inits  (3)
inits.(x⊣≺ a) = (inits.x)⊣≺ (x⊣≺ a)
inits.□ = □⊣≺ □  (4)
tails.(a ⊢ ≻ x) = (a ⊢ ≻ x) ⊢ ≻ (tails.x)
tails.□ = □ ⊢ ≻ □ ,  (5)

which corresponds to summing the segments up by grouping them according to common end-points. Unfortunately, in this definition neither inits nor tails is expressed as a catamorphism, and thus we provide a different set of definitions which are:

inits.(a ⊢ ≻ x) = □ ⊢ ≻ ((a ⊢ ≻ )^{∗} ∘ inits.x)
inits.□ = □ ⊢ ≻ □  (6)
tails.(x⊣≺ a) = ((⊣≺a)^{∗} ∘ tails.x)⊣≺ □
tails.□ = □⊣≺ □ .  (7)

A different approach for generating the tails in SV and CV, which will be useful in finding a different solution for the problem of the maximum segment sum, is to remove all initial segments from a sequence:

tails = ++/ ∘ X^{⇀}_{≫} ∘ ⟨id, inits⟩  (8)

with:

X^{⇀}_{≫}.⟨l, m⟩ = (l ≫)^{∗}.m ,

where ≫ is defined by (a ++ b) ≫ a = b and provided of course that the list l contains only proper prefixes of m, which is indeed the case in (8).

For JV there are several approaches too for summing up all segments, e.g.:

segs.□  = □ ⊢ ≻ □
segs.(x ++ y) = segs.x ++ segs.y ++ ++^{∗}.(tails.xXinits.y) .

This generator makes it easy to identify all segments which span a specific point in the sequence. Of course the function mapping the input into this view should select that representation where the point to be inspected first ends up highest in the term representing the sequence in JV. A useful generator corresponding to LTV is defined as follows;

segs.□ = □ ⊢ ≻ □
segs.(x ≺ a ≻ y) = segs.x ++ segs.y ++ (a⊙)^{∗}.(tails.x X inits.y)  (9)
where a ⊙ ⟨u, v⟩ = u ++ [a] ++ v

The advantage of this view is that it may be used to separate out those segments which have a specific element in common, again assuming of course that a useful representative has been chosen.

We will now formulate our last decision point.

Choice of generator: Choose a useful generator. This choice depends primarily on the chosen view, and on further functions to be applied to the result of the chosen generator.

We finally want to note that in providing the different generators we have used the JV for representing the generated segments. One should keep in mind however that, when considering these segments as a bag, similar choices are to be made for these intermediate data structures.

4 Virtual Data Structures

In this section we will introduce an important transformation, which enables us to construct a link with the imperative style of programming. Through the abundant use of function composition in functional programs, many data structures are first constructed and immediately afterwards inspected and destroyed by the next function to be applied.

In many implementations it will, by using lazy evaluation in the machine model, not be the case that the data structure is ever completely present in memory. In these models the constructing phase and the destructing phase act like coroutines, with the constructing phase producing the next part of the data structure only when it is needed by the destructing phase. This phenomenon is also present when using the pipe construct in the Unix operating system. One process is filling the pipe, as if it were writing on a file, and another process is reading from the pipe as if it were a file. The complete file, however, is never present as such. It is to be noticed that this technique may introduce a considerable space optimisation, but does not reduce the number of computation steps.

A simple example of this phenomenon may be found in the following program, which sums the integers from 1 to n:

a upto b = a ⊢ ≻ (a + 1) upto b, if a ≤ b
a upto b = □, otherwise
sum.1.n = +/.(1 upto n) .

In this example first a list of integers is constructed, and in the next step this list is consumed by the catamorphism +/. If one would translate this algorithm directly into an imperative program this would give rise to two loops: one for constructing the list, and one for iterating over the constructed list. It would be hard to imagine someone really programming it like this, because every programmer would immediately merge the two loops into one, and not construct the list at all. This shows a remarkable difference between the two styles of programming. In the functional style one would use a number of higher order constructs, in this case function composition, to construct an algorithm out of existing components, whereas the imperative programmer would write this program from scratch. The question which now arises is whether it is possible to keep the elegance of the functional style, while achieving the efficiency and compactness of the imperative style.

When a catamorphism is applied to a constructed data structure the optimisation is straightforward: substitute the operators of the catamorphism directly into the data structure building algorithm, at those places where the operators of the initial algebra of its domain contribute in constructing the result. As a result it is not the input for the catamorphism which is constructed, but the result of applying the catamorphism to this input. Since this transformation can always be performed, and often there is not a specific point in the derivation at which this transformation is done at best, one is free to postpone this optimisation until the algorithm derivation has been completed.

We will call data structures which have played a catalytic rôle in the derivation of the algorithm, but have disappeared from the final algorithm virtual data structures.

This approach is again well known in the compiler construction world, and corresponds to the use of an attribute grammar which has synthesised attributes only. Here the optimisation may be used in which not the parse tree as such is constructed by the parser, but the computations which were to be performed on the parse tree, are performed by the parser directly. In a simpler form this transformation is also known as vertical loop-fusion to imperative programmers.

In [14] this process has been dubbed deforestation, indicating how the intermediate tree constructions and reductions have disappeared from the final execution trace.

5 Derivations

In this section we will provide a number of derivations of segment based problems using the views and choices introduced before. As a first example we will present the problem of computing the maximum segment sum [5]. This derivation shows how, using two different segment constructors, two completely different derivations may be given. Our first derivation is heavily influenced by [2]. The second problem we will treat is the computation of the longest low segment. This problem illustrates the advantage of choosing the right algebraic view on lists and has been surprisingly hard to solve when attention is confined to the snoc and cons view.

Before delving into the details of these algorithms we will introduce some laws which will be used over and over again, and thus deserve a separate introduction. Those interested in the proofs of these indentities may consult [1][11].

map-distributivity f^{∗} ∘ g^{∗} = (f ∘ g)^{∗}
map-promotion f^{∗} ∘ ++/ = ++/ ∘ f^{∗}^{∗}
reduce-promotion ⊗/ ∘ ++/ = ⊗/ ∘ (⊗/)^{∗} .

This last law is an instance of the so-called promotion law. The promotion law says that

h ∘ ⊕/ = ⊙/ ∘ h^{∗}

if

h.(a ⊕ b) = h.a ⊙ h.b and h.1_{⊕} = 1_{⊙} .

5.1 Maximum Segment Sum

The specification for the computation of the maximum segment sum reads as follows:

↑/ ∘ +/^{∗} ∘ segs

and is an instantiation of the problem class given in (1).

Inits/Tails Decomposition. Recall the generic specification (1). The property in the maximum segment sum to be computed for every segment is a catamorphism. Therefore we start with deriving some properties of such catamorphisms, generalising the +/ to ⊕/, and the compose operator ↑ to ⊗. This will be done assuming that SV is the chosen view, and segs = ++/ ∘ tails^{∗} ∘ inits the chosen generator, leading to:

mss = ⊗/ ∘ ⊕/^{∗} ∘ ++/ ∘ tails^{∗} ∘ inits .

We start by moving the ++/ part forward:

⊗/ ∘ ⊕/^{∗} ∘ ++/ ∘ tails^{∗} ∘ inits = map-promotion = ⊗/ ∘ ++/ ∘ ⊕/^{∗}^{∗} ∘ tails^{∗} ∘ inits = reduce-promotion = ⊗/ ∘ ⊗/^{∗} ∘ ⊕/^{∗}^{∗} ∘ tails^{∗} ∘ inits = map-distributivity = ⊗/ ∘ (⊗/ ∘ ⊕/^{∗} ∘ tails)^{∗} ∘ inits = define F = ⊗/ ∘ ⊕/^{∗} ∘ tails = ⊗/ ∘ F^{∗} ∘ inits

Using point-wise reasoning we now derive some properties of F. In this calculation we shall accumulate a number of desirable properties of ⊗ and ⊕. These properties become the applicability conditions of one of our theorems. Our first assumption is that ⊗ and ⊕ have unit elements 1_{⊗} and 1_{⊕} respectively.

F.(x⊣≺ a) = definition of F = ⊗/ ∘ ⊕/^{∗} ∘ tails.(x⊣≺ a) = definition of tails = ⊗/ ∘ ⊕/^{∗}.(((⊣≺a)^{∗} ∘ tails.x) ⊣≺ □) = definition of map, reduce on □ = ⊗/.((⊕/^{∗} ∘ (⊣≺a)^{∗} ∘ tails.x) ⊣≺ 1_{⊕}) = map distributivity = ⊗/.(((⊕/ ∘ (⊣≺a))^{∗} ∘ tails.x) ⊣≺ 1_{⊕}) = definition of reduction = ⊗/.((((⊕a) ∘ ⊕/)^{∗} ∘ tails.x) ⊣≺ 1_{⊕}) = map distributivity = ⊗/.(((⊕a)^{∗} ∘ ⊕/^{∗} ∘ tails.x) ⊣≺ 1_{⊕}) = definition of reduction = (⊗/ ∘ (⊕a)^{∗} ∘ ⊕/^{∗} ∘ tails.x) ⊗ 1_{⊕} = assume (⊕a) factors out of ⊗ = ((⊕a) ∘ ⊗/ ∘ ⊕/^{∗} ∘ tails.x) ⊗ 1_{⊕} = folding the definition of F = ((⊕a) ∘ F.x) ⊗ 1_{⊕} As similar derivation may be given for the empty case:

F.□

= definition of F = ⊗/ ∘ ⊕/^{∗} ∘ tails.□ = definition of tails = ⊗/ ∘ ⊕/^{∗}.(□⊣≺ □) = definition of map = ⊗/.(□⊣≺ 1_{⊕}) = definition of reduction = 1_{⊕} ⊗ 1_{⊗} = definition of 1_{⊗} = 1_{⊕}

Based on these derivations we may now conclude that, using the binary operator x ⊙ a =^{def} (x ⊕ a) ⊗ 1_{⊕}, F may be written as a catamorphism (|1_{⊕}, ⊙|). Note that this derivation would not have been possible when using the first definition of tails, since this definition is not a homomorphism (it is a paramorphism, [8]).

Completing the derivation of the segment decomposition schema is now straightforward by using (2). Using these results we have derived the following schema for segment problems:

⊗/ ∘ ⊕/^{∗} ∘ segs = ⊗/ ∘ ⊙//
where x ⊙ a = (x ⊕ a) ⊗ 1_{⊕}
provided (b ⊗ c) ⊕ a = (b ⊕ a) ⊗ (c ⊕ a) .

By now noticing that indeed it is the fact that (b↑c) + a = (b + a)↑(c + a) we may conclude that:

mss = ↑/ ∘ ⊙//
where x ⊙ a = (x + a)↑1_{+} = (x + a)↑0.

Finally we may substitute the operations of ↑/ in the definition of //, considering this as a virtual data structure, giving:

mss = \begin{matrix}π_{2} ∘ (|⟨1_{⊙}, 0⟩, ˜⊙|) \\ where \\ ⟨a, b⟩ ˜⊙c = ⟨a ⊙ c, (a ⊙ c)↑b⟩ \end{matrix}

which corresponds directly to its imperative counterpart, using a single loop and one additional variable:

\begin{matrix}a, b, i := 0, 0, 0 \\ do i ≠ n → a := (a + x[i])↑0; b := b↑a; i := i + 1 od \end{matrix}

Inits/Inits Decomposition. In this section we will present a different derivation for the maximum segment problem, starting from the alternative definition of tails as given in (8).

We already discussed this generator in Sect. 3.3. Before embarking upon the derivation, it will be expedient to mention two algebraic properties that will be useful in the sequel. We start by noticing:

+/.b = +/.((a ++ b) ≫ a) = (+/.(a ++ b) − +/.a)

and consequently:

+/^{∗} ∘ X^{⇀}_{≫} ∘ ⟨id, inits⟩

= relation between ≫, + and − =  (10)

X^{⇀}_{−} ∘ ⟨+/ ∘ id, +/^{∗} ∘ inits⟩

A second important observation is:

(⊗/ ∘ ⊕//) ∗ ∘ inits = tl ∘ ⊗// ∘ ⊕// ,  (11)

where tl.(a ⊢ ≻ x) = x. Using these properties we may now derive:

↑/ ∘ +/^{∗} ∘ X^{⇀}_{≫} ∘ ⟨id, inits⟩

= (10) =

↑/ ∘ X^{⇀}_{−} ∘ ⟨+/, +/^{∗} ∘ inits⟩

= definition of accumulate =

↑/ ∘ X^{⇀}_{−} ∘ ⟨+/, +//⟩

= (a − b)↑(a − c) = a − (b↓c) = (−) ∘ ⟨+/,↓/ ∘ +//⟩

We present now the following derivation of mss:

mss = inits/inits generator, promotion =

↑/ ∘ (↑/ ∘ +/^{∗} ∘ X^{⇀}_{≫} ⟨id, inits⟩)^{∗} ∘ inits

= above derivation =

↑/ ∘ ((−) ∘ ⟨+/,↓/ ∘ +//⟩)^{∗} ∘ inits

= map distributivity =

↑/ ∘ (−)^{∗} ∘ ⟨+/,↓/ ∘ +//⟩^{∗} ∘ inits = ⟨f, g⟩^{∗} = zip ∘ ⟨f^{∗}, g^{∗}⟩ = ↑/ ∘ (−)^{∗} ∘ zip ∘ ⟨+/^{∗} ∘ inits, (↓/ ∘ +//)^{∗} ∘ inits⟩ = definition of accumulate, property (11) = ↑/ ∘ (−)^{∗} ∘ zip ∘ ⟨+//, tl ∘ ↓// ∘ +//⟩ = product = ↑/ ∘ (−)^{∗} ∘ zip ∘ ⟨id, tl ∘ ↓//⟩ ∘ +//

By making the intermediate data structures virtual again, this directly corresponds to the following imperative program: s, m, r := 0, ∞, −∞ {unit elements for +,↓,↑} r, i := 0, 0 {initialise loop and compute tl} do i ≠ n → s := s + x[i]; m := m↓s; r := r↑(s − m); i := i + 1 od

In this program we maintain in s the sum of the elements seen thus far, in m the minimum value seen thus far, and in r the greatest difference between these values seen thus far. Since one is only interested in this difference the previous program can be seen as an optimisation of this program with an extra invariant a = (s−m). An interesting aspect of this program schema is that the accumulation of the input data is explicitly maintained. If one tries to solve the computation of the longest balanced segment this generator is a useful starting point.

This algorithm resembles the Wall-street approach, where the list of numbers indicates the daily changes in the Dow-Jones index, and the question to be answered is what would have been the best time for a one-time investment.

5.2 Length of a Longest Low Segment

In this paragraph we will derive a solution for the problem of computing the length of a longest low segment. A very similar problem is the computation of a largest rectangle under a histogram, the solution and derivation of which may be found in [12], and which may be compared with the derivation given here.

The problem may be stated as follows:

llls = ↑/ ∘ #^{∗} ∘ low ◁ ∘ segs
where low = (≤) ∘ ⟨↑/, #⟩

with (a↑_{f}b) = (f.a)↑(f.b).

We start by noticing first that the predicate used in the filter is monotonic in the second component:

↑/ ∘ (a ≤)◁ = (a ≤)? ∘ ↑/  (12)

where the ? is a one-point filter that either returns its argument, or returns minus infinity. Let v_{a} denote a set of segments with a common maximum element a. We may reason as follows:

↑/ ∘ #^{∗} ∘ low◁.v_{a}

= expand definition of low = ↑/ ∘ #^{∗} ∘ ((≤) ∘ ⟨↑/, #⟩)◁.v_{a} = maximum of elements of v_{a} equals a = ↑/ ∘ #^{∗} ∘ ((a ≤) ∘ #)◁.v_{a} = move ^{∗} through ◁ = ↑/ ∘ (a ≤) ∘ #^{∗}.v_{a} = (12) =

(a ≤)? ∘ ↑/ ∘ #^{∗}.v_{a} (13)

This suggests that, when summing up the segments by common maximum element, we might be very efficient in skipping some of these elements in the generating process, and thereby getting a more efficient algorithm. We thus will try to push the filter into the generating process. Since we want to sum up the elements by common element we choose the LTV, with the generator given in (9).

Since it furthermore is the case that x ∈ segs.y ⇒ ↑/.x ≤ ↑/.y, it is profitable to first sum up all the segments with a common maximum value, and then the rest of the segments grouped according to their maximum value.

We will now make use of our freedom in choosing an element in LTV which makes this an easy task. Since the generator introduced in (9) sums up segments by common element, it is now sufficient if we have an element in the equivalence class generated by the associative law, for which it is the case that a label value in the tree is at least the maximum of the label values in the subtrees, i.e. it is a heap.

llls.(x ≺ a ≻ y)

= definition llls =

↑/ ∘ #^{∗} ∘ low ◁ ∘ segs.(x ≺ a ≻ y) = unfold definition (9) = ↑_{#}/ ∘ #^{∗} ∘ low ◁.(segs.x ++ segs.y ++ (a⊙)^{∗}.(tails.x X inits.y)) = filter and reduce promotion, folding llls = (llls.x)↑(llls.y)↑(↑/ ∘ #^{∗} ∘ low ◁ ∘ (a⊙)^{∗}.(tails.x X inits.y))

Although this already looks like a catamorphism it isn’t one as yet. We now concentrate on the last part, which may be rewritten, assuming that the predicate

a = ↑/.(x ++ [a] ++ y)  (14)

holds:

(↑/ ∘ #^{∗} ∘ low ◁ ∘ (a⊙)^{∗} ∘ (tails.x X inits.y)

= (13) =

(a ≤)? ∘ ↑/ ∘ #^{∗} ∘ (a⊙)^{∗} ∘ (tails.x X inits.y)

= map distributivity, (# ∘ (a⊙) = (1+) ∘ # ∘ ++) = (a ≤)? ∘ ↑/ ∘ (1+)^{∗} ∘ (# ∘ ++)^{∗} ∘ (tails.x X inits.y) = promotion: (1 + a)↑(1 + b) = 1 + (a↑b) = (a ≤)? ∘ (1+) ∘ ↑/ ∘ (# ∘ ++)^{∗}.(tails.x X inits.y) = length is a homomorphism = (a ≤)? ∘ (1+) ∘ ↑/ ∘ (+ ∘ (# × #))^{∗}.(tails.x X inits.y) = map distributivity, map over cross = (a ≤)? ∘ (1+) ∘ ↑/ ∘ (+)^{∗}.(#^{∗} ∘ tails.x X #^{∗} ∘ inits.y) = addition is monotonic = (a ≤)? ∘ (1+) ∘ (+).⟨↑/ ∘ #^{∗} ∘ tails.x,↑/ ∘ #^{∗} ∘ inits.y⟩ = longest tail of x is x, idem for inits = (a ≤)? ∘ (1+) ∘ (+).⟨#.x, #.y⟩ = notation = (a ≤)?(1 + x + y)

Tupling this expression with the computations of #.x and #.y leads now to the following catamorphism on a suitably chosen element in the LTV:

llls = π_{1} ∘ (|⟨0, 0⟩, f|) ∘ SVintoLTV  (15)
where f.⟨⟨m, x⟩, a, ⟨n, y⟩⟩ = ⟨m↑n↑((a ≤)?(x + 1 + y)), (x + 1 + y)⟩ (16)

The only problem which now remains open is to find the suitable representation for the input in LTV-form; this is easily solved by using the well-known algorithm for the construction of a heap. The algorithm used corresponds directly to precedence parsing. The only difference is that all operators are equal to the empty tree, and the priority of the operators is the reverse of what one finds usual. We thus use SPV as an intermediate representation: svintoltv = SPVintoLTV ∘ SVintoSPV.

The transformation of SV into SPV is a straightforward application of parsing, where the values in the LTV-parts are always at most their associated value in the pair in the spine:

SVintoSPV = (|□, (id ˆ⊖⟨□, −⟩)|)  (17)
where \begin{matrix}(s ≺ ⟨t, v⟩) ⊖ (u, w) = \begin{matrix}v ≥ w → (s ≺ ⟨t, v⟩) ≺ ⟨u, w⟩ \\ v ≤ w → s ⊖ ⟨(t ≺ v ≻ u), w⟩ \end{matrix} \\ □ ⊖ ⟨u, w⟩ = □ ≺ ⟨u, w⟩ . \end{matrix}

The function converting an SPV-value into an LTV-value (maintaining the heap property) is given by

SPVintoLTV.s = π_{1} ∘ π_{2} ∘ ≺^{−1} ∘ (s ⊖ ⟨□, ∞⟩) .  (18)

So we are finished, and gathering the intermediate results in (15), (17) and (18), we get

llls = π_{1} ∘ (|⟨0, 0⟩, f|) ∘ π_{1} ∘ π_{2} ∘ ≺^{−1} ∘ (⊖⟨□, ∞⟩) ∘ (|□, (id ˆ⊖⟨□, −⟩)|) .

To this result again the virtual data structure optimisation may be applied, effectively preventing the labelled tree coming into existence at all. In the final result only a parse stack is maintained, containing the results and lengths of already processed subtrees, and label values which have not found their corresponding right subtree parts.

The final algorithm now becomes:

llls =

π_{1} ∘ (⊘⟨⟨0, 0⟩, ∞⟩) ∘ (|□, (id ˆ⊘⟨⟨0, 0⟩, −⟩)|)

where \begin{matrix}s ≺ ⟨⟨m, x⟩, v⟩ ⊘ ⟨⟨n, y⟩, w⟩ = \begin{matrix}v ≥ w → (s ≺ ⟨⟨m, x⟩, v⟩) ≺ ⟨⟨n, y⟩, w⟩ \\ v ≤ w → s ⊘ ⟨⟨m↑n↑((v ≤)?(xy1)), xy1⟩, w⟩ \\ where xy1 = x + y + 1 \end{matrix} \\ □ ⊘ ⟨⟨n, y⟩, w⟩ = □ ≺ ⟨⟨n, y⟩, w⟩ . \end{matrix}

6 Acknowledgements

The authors wish to thank Lambert Meertens, Richard Bird, and the participants and lecturers of the Ameland meetings for working together in a cooperative way in developing the calculus employed in this paper. This research was supported by the Dutch Organization for Scientific Research, grant NFI 62-518.

References

1. R.C. Backhouse. An exploration of the Bird–Meertens formalism. Computing Science Note CS 8810, Department of Computing Science, Groningen University, P.O. Box 800, 9700 AV Groningen, The Netherlands, 1988.

2. R.S. Bird. An introduction to the theory of lists. In M. Broy, editor, Logic of Programming and Calculi of Discrete Design, volume 36 of NATO ASI Series F, pages 3–42. Springer– Verlag, 1987.

3. R.S. Bird and P. Wadler. Introduction to Functional Programming. Prentice–Hall, 1988.

4. Hendrik Boom. private communication, 1979. IFIP Working Group 2.1, Jablonna, Warschau.

5. E.W. Dijkstra. A Discipline of Programming. Prentice–Hall, 1976.

6. David Gries. The Science of Programming. Springer, 1983. 366p.

7. L. Meertens. Algorithmics — towards programming as a mathematical activity. In J.W. de Bakker, M. Hazewinkel, and J.K. Lenstra, editors, Mathematics and Computer Science, volume 1 of CWI Monographs, pages 3–42. North–Holland, 1987.

8. L. Meertens. Paramorphisms. Technical Report CS-R9005, CWI, Amsterdam 1990. To appear in Formal Aspects of Computing.

9. Erik Meijer, Maarten Fokkinga, and Ross Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In FPCA, LNCS. Springer-Verlag, 1991.

10. C.C. Morgan. Programming from Specifications. Prentice–Hall, 1990.

11. M. Spivey. A categorical approach to the theory of lists. In J.L.A. van de Snepscheut, editor, Mathematics of Program Construction, volume 375 of Lecture Notes in Computer Science, pages 399–408. Springer–Verlag, 1989.

12. J.C.S.P. van der Woude. Rabbitcount := rabbitcount - 1. In J.L.A. van de Snepscheut, editor, Mathematics of Program Construction, volume 375 of Lecture Notes in Computer Science, pages 409–420. Springer–Verlag, 1989.

13. Philip Wadler. Views: a way for pattern matching to cohabit with data abstraction. In Proc. 14th Symposium of Principles of Programming Languages, pages 307–313. ACM, January 1987.

14. Philip Wadler. Deforestation: transforming programs to eliminate trees. In H. Ganzinger, editor, ESOP ’88 (= Proc. 2nd European Symposium on Programming, volume 300 of LNCS, pages 345–358. Springer-Verlag, March 1988.

This article was processed using the LaTEX macro package with LMAMULT style