Generation of Eﬃcient Algorithms for
Maximum Marking Problems(和訳: 最大マーク付け問題の効率的解法の自動生成)Isao SasanoAcknowledgments
First I would like to thank to Prof. Masato Takeichi for giving useful comments to this work and letting me do this work freely. Second I would like tothank to Zhenjiang Hu for giving useful comments to this work and having
several discussions. Third I would like to thank to Mizuhito Ogawa for letting me know interesting papers about graph algorithms and having several
meetings on this work, and to Akihiko Takano for giving useful comments
and encouraging me.
This work owes much to the thoughtful and helpful discussion comments
made by Hideya Iwasaki, and other Tokyo CACA members. Thanks toJeremy Gibbons for his valuable comments on an earlier version of our paper
accepted to ICFP 2000, to Oege de Moor for providing us several interesting optimization problems, to Richard Bird for kindly sending us his draft
about deriving linear time algorithm for maximum marking problems using
relational calculus, to Shinichi Morishita for introducing us the problems ofdata mining.

iContents
1 Introduction
1
1.1 Optimization Problems . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Program Derivation . . . . . . . . . . . . . . . . . . . . . . . . 2
1.3 Maximum Marking Problems . . . . . . . . . . . . . . . . . . 4
1.4 Existing Approaches . . . . . . . . . . . . . . . . . . . . . . . 5
1.5 Program Generation . . . . . . . . . . . . . . . . . . . . . . . 6
1.6 Our proposing method . . . . . . . . . . . . . . . . . . . . . . 7
1.7 A Tour . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.7.1 Speciﬁcation . . . . . . . . . . . . . . . . . . . . . . . . 8
1.7.2 Derivation . . . . . . . . . . . . . . . . . . . . . . . . . 10
1.7.3 Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.8 Organization of this thesis . . . . . . . . . . . . . . . . . . . . 13
2 Preliminaries
2.1 Recursive Data Types . . . . . . . . . . . . . . . . . . . . . .
2.2 Catamorphism . . . . . . . . . . . . . . . . . . . . . . . . . .
2.3 Mutumorphisms . . . . . . . . . . . . . . . . . . . . . . . . . .
2.4 Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

14
14
15
16
16

3 Maximum Marking Problems
3.1 A Formal Deﬁnition . . . . . . . . . . . . . . . . . . . . . . . .
3.1.1 Marking . . . . . . . . . . . . . . . . . . . . . . . . . .
3.1.2 Weight . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.1.3 Maximum Weightsum Problem . . . . . . . . . . . . .
3.2 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.2.1 Tree Knapsack Problem . . . . . . . . . . . . . . . . .
3.2.2 r-MSS Problem . . . . . . . . . . . . . . . . . . . . . .
3.2.3 Party Planning Problem . . . . . . . . . . . . . . . . .

18
18
19
20
21
21
22
22
22

ii

3.3

3.2.4 Coloring Problem . . . . . . . . . . . . . . . . . . . . . 23
Existing Solution — Borie’s Approach . . . . . . . . . . . . . 23

4 Derivation of Eﬃcient Algorithms
4.1 A Suﬃcient Condition about Property . . . . . . . . . . . . .
4.2 A Suﬃcient Condition about Weight Function . . . . . . . . .
4.2.1 Homomorphic Weight Function . . . . . . . . . . . . .
4.2.2 Generalized Optimization Lemma . . . . . . . . . . . .
4.3 Decomposition Lemma . . . . . . . . . . . . . . . . . . . . . .
4.3.1 Property with Boolean Functions . . . . . . . . . . . .
4.3.2 Property with Finite-range Functions . . . . . . . . . .
4.4 The Main Theorem . . . . . . . . . . . . . . . . . . . . . . . .
4.5 Extension of property . . . . . . . . . . . . . . . . . . . . . . .
4.5.1 Finite Accumulative Property . . . . . . . . . . . . . .
4.5.2 Theorem . . . . . . . . . . . . . . . . . . . . . . . . . .
4.6 Calculation Strategy . . . . . . . . . . . . . . . . . . . . . . .

25
25
31
32
32
33
34
34
35
36
37
38
40

5 Examples
5.1 Paragraph Formatting Problem . . . . . . . . . . . . . . . . .
5.2 Security Van Problem . . . . . . . . . . . . . . . . . . . . . .
5.3 Knapsack Problem . . . . . . . . . . . . . . . . . . . . . . . .
5.3.1 Speciﬁcation . . . . . . . . . . . . . . . . . . . . . . . .
5.3.2 Property by Finite Mutumorphisms . . . . . . . . . . .
5.3.3 Property by Finite Accumulative Property . . . . . . .
5.3.4 Weight function . . . . . . . . . . . . . . . . . . . . . .
5.3.5 Derivation by Theorem 4 . . . . . . . . . . . . . . . . .
5.3.6 Derivation by Theorem 3 . . . . . . . . . . . . . . . . .
5.4 Knapsack Problem on List . . . . . . . . . . . . . . . . . . . .
5.4.1 Speciﬁcation . . . . . . . . . . . . . . . . . . . . . . . .
5.4.2 Derivation . . . . . . . . . . . . . . . . . . . . . . . . .
5.5 Tree Knapsack Problem . . . . . . . . . . . . . . . . . . . . .
5.5.1 Speciﬁcation . . . . . . . . . . . . . . . . . . . . . . . .
5.5.2 Derivation . . . . . . . . . . . . . . . . . . . . . . . . .
5.6 0-1 Multiple Knapsack Problem . . . . . . . . . . . . . . . . .
5.6.1 Speciﬁcation . . . . . . . . . . . . . . . . . . . . . . . .
5.6.2 Derivation . . . . . . . . . . . . . . . . . . . . . . . . .
5.7 Multidimensional Knapsack Problem . . . . . . . . . . . . . .
5.7.1 Speciﬁcation . . . . . . . . . . . . . . . . . . . . . . . .

47
47
49
51
51
52
52
53
53
53
54
54
54
55
55
57
57
57
58
58
59

iii

5.7.2 Derivation . . . . . . . . . . . . . . . . . . . . . . . . .
5.8 Weighted Interval Selection Problem . . . . . . . . . . . . . .
5.9 Mining Optimized Gain Association Rules . . . . . . . . . . .
5.9.1 The Problem of Mining Optimized Gain Association
Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.9.2 Constructing k-MSS Algorithm Manually . . . . . . . .
5.9.3 Deriving k-MSS Algorithm Automatically . . . . . . .
5.9.4 Speciﬁcation . . . . . . . . . . . . . . . . . . . . . . . .
5.9.5 Derivation . . . . . . . . . . . . . . . . . . . . . . . . .
5.9.6 Comparison . . . . . . . . . . . . . . . . . . . . . . . .
5.9.7 Dealing with Change of Speciﬁcation . . . . . . . . . .
5.9.8 Remarks . . . . . . . . . . . . . . . . . . . . . . . . . .
5.10 Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.10.1 Simplicity . . . . . . . . . . . . . . . . . . . . . . . . .
5.10.2 Generality . . . . . . . . . . . . . . . . . . . . . . . . .
5.10.3 Flexibility . . . . . . . . . . . . . . . . . . . . . . . . .

59
60
61
62
64
65
65
66
67
68
68
69
69
72
74

6 Automatic Generation of Eﬃcient Programs
77
6.1 MAG system . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
6.1.1 Implementation . . . . . . . . . . . . . . . . . . . . . . 78
6.2 Yicho System . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
6.2.1 Structure of automatic generation system . . . . . . . . 81
6.2.2 Calculation Carrying Program (CCP) . . . . . . . . . . 82
6.2.3 Execution of CCP and transformation to script . . . . 91
6.2.4 Example of maximum marking problems . . . . . . . . 96
6.2.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . 100
7 Related Work101

8 Conclusion

110

Bibliography

112

iv

Abstract
In existing work on graph algorithms, it is known that a linear time algorithm can be derived mechanically from a logical formula for a class of
optimization problems. But this has a serious problem that the derived algorithm has huge constant factor. In this work, we redeﬁne this problem
on recursive data structures as a maximum marking problem and propose
method for deriving a linear time algorithm for that. In this method, speciﬁcation is given using recursive functions instead of logical formula, which
results in a practical linear time algorithm. This method is mechanical and infact, based on this deriving method, we make a system which automaticallygenerates a practical linear time algorithm from speciﬁcation for a maximum
marking problem.

Chapter 1
Introduction
This thesis proposes an automatic method for deriving linear time algorithms
for a class of optimization problems, which we call maximum marking problems. In this chapter ﬁrstly we describe what kind of optimization problems
maximum marking problems include. Secondly we show why derivation is desired and what kind of methods one can use for deriving eﬃcient algorithms
generally. Thirdly we discuss about program generation and mention that
our method is appropriate for program generation. Fourthly we describe thecontribution of this thesis. Finally we show give an overview of our generation method through an example and then close this chapter by giving theorganization of this thesis.

1.1

Optimization Problems

Many problems can be speciﬁed in the way ”maximize (or minimize) certain
value under some condition”. Such problems are generally called optimization problems. For example, the knapsack problem [MT90] is an example
of optimization problems. Other examples include problems in data mining,e.g., optimal range problems [FMMT96a]. Eﬃcient algorithms for optimization problems are needed, so developing eﬃcient algorithms for optimization
problems is important task.
Here consider the three examples: the tree knapsack problem, r-MSS
problem, and the party planning problem. Developing eﬃcient algorithms
for these problems is not so trivial.
Tree Knapsack Problem [dM95] This problem is an extension of the or1

dinary knapsack problem [MT90] to one on tree. Input of the ordinary
knapsack problem is a set of items each of which has weight and value.
Output is a feasible selection of items whose value sum is maximum
in all the feasible item selections. A selection is feasible when sum of
weight of selected items does not exceed the given capacity C. Treeknapsack problem is an extended version of the ordinary knapsack problem so that items are arranged in a tree structure and selected items
are connected, that is, a set of items induces a connected subgraph of
the input given tree. We assume weight of items are integers.
r-MSS Problem [BRS99] This problem is an extension of the maximum
segment sum problem, which is a famous problem in program derivationﬁeld [Bir89, Gri90]. This problem appears in a problem of data mining,
optimum range association rules problem [BRS99]. Input is a sequenceof numbers. Output is a feasible selection of elements whose sum ismaximum in all the feasible element selections. A selection is feasible
when selected elements form up to r connected subsequences. Whenr = 1, it is the ordinary maximum segment sum problem.
Party Planning Problem [CLRS01] Professor McKenzie is consulting
for the president of the A.-B Corporation, a company that has a hierarchical structure. That is, the supervisory relations form a tree rooted
at the president. The personnel oﬃce has ranked each employee witha conviviality rating that is a positive or negative real number. The
president wants to have a company party. To make the party fun for
all attendees, the president does not want both an employee and hisor her direct supervisor to attend. The problem is to design a linear
algorithm making the guest list. The goal is to maximize the sum of
the conviviality ratings of the guests.
How can we develop eﬃcient algorithms for these problems? Using our
proposing method, one can obtain eﬃcient linear algorithms for these problems by a mechanical way and can obtain them fully automatically by using
our system for MMP.

1.2

Program Derivation

Consider the examples we showed in the previous section. When eﬃcientalgorithms are asked for, usually people ﬁrst think about how to solve them2and then write eﬃcient programs by hand. This is ordinary way which is
generally taken. But this ordinary method is not satisfactory because correctness of algorithms is not guaranteed. Developing a correct algorithm isimportant because if an algorithm is not correct, then anyone doesn’t want
to use it. If an algorithm is used for an important purpose, then correctness
is crucial. So, guaranteeing correctness of algorithm is needed.
But generally speaking, writing an correct and eﬃcient program by hand
directly is diﬃcult task. In many cases, after writing a program, one haveto repair syntax error or semantic error. In some cases, removing bugs froma program takes longer time than writing the program. Furthermore, speciﬁcation of a problem may be changed in the future. If it is changed, thenmodifying suitable part of the program is diﬃcult if an other programmer
than wrote the original program has to modify it. Even the programmer
who wrote the original one feels diﬃculty in it if it has passed long time since
writing the original one.
One way to remedy those problems is to use program derivation: deriving
an eﬃcient program from speciﬁcation [PP96]. The task is to obtain aneﬃcient program from speciﬁcation. To guarantee that the obtained programsatisﬁes speciﬁcation, it is only required that each derivation step should becorrect. Using program derivation, correctness and eﬃciency are obtained at
the same time. Furthermore, when the problem is changed slightly, then one
only has to change the speciﬁcation slightly and do a similar derivation in
the case it is possible.
Speciﬁcation is written in some language such as logical formula, function,
relation, and so on. In this thesis, we use speciﬁcation written in function.
Derivation process consists of several transformation steps. A transformation
step is a transformation that transforms a function to another function, which
preserves the meaning. A feature of functional speciﬁcation is that speciﬁcation itself can be executed. Programmer ﬁrst writes a program which may be
ineﬃcient but is guaranteed correct, which can be considered as a speciﬁcation. Here, eﬃciency of a function means the number of reduction steps forevaluating the function when implementing the function in some functional
language such as Haskell [PJH99, Bir98], ML [MTHM97, Pau96] or Scheme[ADH+ 98, AwJS96]. Program derivation is performed by applying certaintransformation rule to the function in each stage and ﬁnally an eﬃcient function will be obtained. Generally program derivation is not done mechanicallysince there are several possible selections in each stage.

3

1.3

Maximum Marking Problems

We concentrate on a class of optimization problems, which we call ” maximum marking problems” (MMP for short). The MMP can be speciﬁed asfollows: Given a data structure x, the task is to ﬁnd a way to mark someelements in x such that the marked data structure of x satisﬁes a certain
property p and has the maximum value with respect to certain weight function w. This means that no other marking of x satisfying p can produce alarger value with respect to w.
By restricting the class of optimization problems to MMP, it becomes
possible to derive mechanically a linear time algorithm for solving it from
simple speciﬁcations. Though of course it is not expected to derive a linear
one for every MMP problem since MMP includes NP-hard problems, we canderive a linear one mechanically if property p and weight function w satisﬁes
certain condition. Our method is mechanical, so we can implement it as asystem which automatically generates linear time algorithms for MMP.
MMP not only is suitable for automatic generation but also is generalenough to express wide range of optimization problems. So we can say that
MMP is an appropriate class of problems in that sense.
Originally MMP was considered in graph algorithms in less general form:
to ﬁnd a subset of the vertex set which satisﬁes certain property and has
maximum sum of weight of vertices [BLW87]. This is a sub-class of MMP,
which we call ”maximum weightsum problems” [SHTO00, SHTO01a], where
one can only allowed to use the wsum, which computes sum of selected elements, as the weight function and to use two kinds of marks, True and False,
which indicate select and non-select respectively. This sub-class includes
many graph problems and a suﬃcient condition of property p for linearity
was given by [BLW87].
By MMP, we can express various kinds of problems which include theproblems we show in Section 1.1. Though those examples seems a bit different, they can be formulated in the uniform way: Given a data x, ﬁnd a
feasible selection of elements whose weight is maximum in all the feasible selection. By expressing feasibility using a predicate p and giving weight using
a weight function w, we can write the speciﬁcation as follows:↑w / ◦ ﬁlter p ◦ gen [True, False]
Here gen is used for generating all the way of selecting elements with marks
True and False. Selection is expressed by marking selected elements and un4marking non-selected elements, where True corresponds to ”mark” and False
corresponds to ”unmark”. The operator ↑f is called the selection operator[Bir87] and is deﬁned bya ↑f b = b,
= a,

if f a ≤ f botherwise.

In this deﬁnition, the value of a ↑f b is b when f a = f b. The operator / iscalled the reduce operator [Bir87], which takes an associative binary operator
and a list, deﬁned as follows:⊕/[a1 , a2 , . . . , an ] = a1 ⊕ a2 ⊕ · · · ⊕ an
The diﬀerences between the three problems are in the diﬀerent deﬁnitions of
the property description of p.
The properties for the tree knapsack problem, r-MSS problem, the party
planning problem, respectively denoted by ptk , prmss , and ppp are as follows:• ptk : sum of weight of selected items does not exceed the given capacity
C and selected items are connected in the input tree.
• prmss : selected elements form up to r connected subsequences in the
input sequence.
• ppp : any two selected elements does not have direct parent-child relationship.
We shall refer to these kinds of problems, the main subject of this thesis,
as maximum marking problems. In general, a maximum marking problem is
to ﬁnd a way of feasible marking the input data that maximize the value ofthe given weight function w, where feasibility is given by certain property p.

1.4

Existing Approaches

The maximum marking problems are interesting in that they encompass avery large class of optimization problems [BLW87, BPT92]. Solving maximum marking problems, however, requires much insightful analysis. There
are basically two kinds of approaches.

5• The Algebraic Approach.
Using the algebraic laws of programs [Bir89, BdM96], one may try to
calculate eﬃcient solutions to the problems by program transformation.
For instance, Bird derived a linear algorithm to solve the maximum
segment sum problem [Bir89], which is a maximum marking problem
on lists. Bird and de Moor [BdM96] demonstrated the derivation ofa greedy linear functional algorithm for the party planning problem
based on the relational calculus.
However, the success of derivation usually depends on a powerful calculation theorem and requires careful and insightful justiﬁcation to meetthe conditions of the theorem. For many cases, such justiﬁcation is difﬁcult for (even experienced) functional programmers to mimic to solve
other similar problems.
• The Construction-from-predicates Approach.
Though little known in functional programming community, it has been
known for decades [AP89, Wim87, BLW87, BPT92] that if maximum
weightsum problems are speciﬁed by regular predicates [BPT92], they
are solvable in linear time on decomposable graphs and that linear-timealgorithms for them can be derived mechanically from the speciﬁcationsof the graph problems.
Though more systematic and constructive than the algebraic approach,this approach yields algorithms that suﬀer from a prohibitively large
table (see Section 3.3 and Chapter 7 for details). The algorithm forsolving the party planning problem, for instance, would need to con142
struct a table with more than 2(2 ) entries [BPT92]. The algorithms
thus cannot be put to practical use.

1.5

Program Generation

Program generation has seen an important role in a wide range of softwaredevelopment processes. A successful program generation system requires not
only a powerful language supporting coding of program generation, but also
a set of eﬀective transformation rules for the generation of programs. An
example, which convincingly shows the importance of the design of eﬀective transformation rules, is the well-known fold-build rule [GLP93] for fus6

ing composition of functions in Glasgow Haskell Compiler (GHC). It is thisgeneral, concise and cheap calculation rule that makes it possible for GHC
to practically generate from large-scale programs eﬃcient programs without
unnecessary intermediate data structures. Generally, the eﬀective rules for
program generation should meet several requirements.
• First, they should be general enough to be applied to a program pattern, by which a useful class of problems can be concisely speciﬁed.
• Second, they should be abstract enough to capture a big step of the
program generating process rather than being a set of small rewriting
rules.
• Third, they can be eﬃciently implemented by program generation systems.
In this thesis we shall propose such a rule for generating eﬃcient programsfrom the following program pattern
mmp w p ms =↑w / ◦ ﬁlter p ◦ gen ms,
which is the speciﬁcation of MMP. Our proposing method is a mechanical method that derives a linear time algorithm for MMP from the above
program pattern. So our method is appropriate for automatic program generation from speciﬁcation, and actually we implement our method as an
automatic program generation system for MMP in Chapter 6.

1.6

Our proposing method

In this thesis we propose a new approach to deriving practical linear- timealgorithms for maximum marking problems over data structures such as lists,
trees, and decomposable graphs. The key points of our approach are to
express the property p by recursive boolean functions over the structure x
rather than a usual logical predicate and to apply program transformation
techniques to reduce the constant factor, thereby exploiting the advantagesof the algebraic and construction-from -predicates approaches.
Our main contributions can be summarized as follows.

7• We propose an optimization theorem that gives a generic and practical linear-time algorithms for solving maximum marking problems(Chapter 4). By using the optimization theorem, we can derive practical linear-time algorithms for various kinds of problems which include
real-world problems such as knapsack problems, optimal range problems [FMMT96a] in the data mining, and many problems in Bird etal.’s textbook [BdM96], as partly shown in Chapter 5.
• Our method is simple, general, and ﬂexible. We demonstrate thisin Chapter 5 by deriving linear-time algorithms for various kindsof interesting and nontrivial maximum marking problems. The
Haskell codes for solving some problems in this thesis are available
at http://www.ipl.t.u-tokyo.ac.jp/˜ sasano/mws.html.
• We are the ﬁrst to successfully apply the algebraic approach to solving
the huge-table problem appearing in the derivation of linear-time algorithms on decomposable graphs [AP89, Wim87, BLW87, BPT92], aproblem not solved by table compression [BLW87] or by dynamic table
management [APT00]. This should be a signiﬁcant step in making thetheoretically appealing linear-time graph algorithms practically useful.
• We show that our proposing method can be implemented as an automatic program generation system for MMP (Chapter 6). Our method
can be implemented using the existing transformation systems likeMAG [dMS98], and eﬃcient programs can be obtained in a fully automatic way. We also implement a ﬂexible system called Yicho, in which
we can specify transformation strategies.

1.7

A TourHere we brieﬂy explain our idea by going through the list version of the party
planning problem.

1.7.1

Speciﬁcation

The list version of the party planning problem, which will be called the
maximum independent-sublist sum problem (mis for short), is to compute vs,
the set of elements from a non-empty list xs, such that no two elements in8

mis :: [Elem] -> [MElem]
mis xs = let opts = mis’ xs
in getdata (foldr1 (bmax second)[ (c,w,cand)| (c,w,cand) <- opts,
c==2 || c==3])

type Weight = Int
type Elem = Weighttype MElem = (Elem,Bool)type Class = Intweight::MElem -> Weightweight (w,_) = w

marked :: MElem -> Boolmis’ :: [Elem] -> [(Class,Weight,[MElem])]marked (_,m) = mmis’ [x] = [(2,x,[(x,True)]), (3,0,[(x,False)])]mis’ (x:xs) =mark :: Elem -> MElem
let opts = mis’ xsmark x = (x,True)in eachmax [ (table (marked mx) c,(if marked mx then weight mx
unmark :: Elem -> MElem
else 0) + w,
unmark x = (x,False)
mx:cand)| mx <- [mark x, unmark x],
table :: Bool ->(c,w,cand) <- opts]
Class -> Class
table True 0 = 0bmax f a b = if f a > f b then a else btable True 1 = 0
table True 2 = 0
eachmax xs = foldl f [] xs
table True 3 = 2
where f [] (c,w,cand) = [(c,w,cand)]table False 0 = 1
f ((c,w,cand) : opts) (c’,w’,cand’) =table False 1 = 1
if c==c’ thentable False 2 = 3
if w>w’ then (c,w,cand) : opts
table False 3 = 3else opts ++ [(c’,w’,cand’)]
else (c,w,cand):f opts (c’,w’,cand’)
second (_,x,_) = x
getdata (_,_,x) = x

Figure 1.1: A linear-time Haskell program for the mis problem.

9

vs are adjacent in xs. Clearly, it is one of the maximum marking problems
on lists, which can be speciﬁed bymis:: [α] → [α]mis xs = ↑ws / [vs | vs ← subs xs, pmis (xs, vs)]where subs enumerates all sublists (not necessarily contiguous) of a list.
What is left is to deﬁne pmis , the speciﬁc component of the problem.
Because vs is a sublist of xs, we can specify pmis in two steps: ﬁrst marking
the elements in xs which belong to vs, and then on the marked xs deﬁning
the property. Thus,
pmis (xs, vs) = p (marking xs vs).
Here p checks that all pairs of marked elements are not adjacent in the markedxs.
p:: [α] → Boolp [x]= Truep (x : xs) = if marked x
then not (marked (hd xs)) ∧ p xs
else p xs
hd:: [α] → α
hd [x]= x
hd (x : xs) = x
For later transformation, we deﬁne hd in the same way as p over the two cases
singleton list and cons list. So much for our speciﬁcation of the problem. It
is worth noting that our speciﬁcation is as natural as that in [BPT92] using
the monadic second-order logic (See Section 3.3). The critical diﬀerence is in
specifying p by using recursive functions instead of a logical predicate. This
enables us to use the functional program calculation for the later derivation.

1.7.2

Derivation

The derivation is based on our optimization theorem in Chapter 4, whichsays that if the property description p can be deﬁned in mutumorphisms[Fok89, Jeu93, HITT97], then a linear-time algorithm solving the maximum
marking problem with respect to p can be derived mechanically.
10

Therefore, the derivation of a linear-time algorithm for the mis problem
reduces to be a derivation of mutumorphisms for p. More precisely, we hopeto transform p to the following form:
p [x]= φ1 xp (x : xs) = φ2 x (p xs, p1 xs, . . . , pn xs)
where φi ’s denote some functions and pi ’s are auxiliary property descriptions
deﬁned in a fashion similar to that in which p is deﬁned:pi:: [α] → Boolpi [x]= φi1 xpi (x : xs) = φi2 x (p xs, p1 xs, . . . , pn xs).
Consider now the p for the mis problem. By introducing p1 deﬁned byp1:: [α] → Boolp1 [x]= not (marked x)
p1 (x : xs) = not (marked x)
we can transform p to the following form.
p [x] = Truep (x : xs) = if marked x then p1 xs ∧ p xs else p xs
Applying our optimization theorem for solving maximum marking problems
now soon yields a linear-time algorithm like that in Figure 1.1, where thealgorithm is coded in Haskell. The function bmax in Figure 1.1 corresponds
to the selection operator ↑. The main function mis takes a list as its argument
and returns the input list with the selected elements marked with True. For
example, mis [1..4] returns[(1,False),(2,True),(3,False),(4,True)].
Note that our initial speciﬁcation only returns [2,4]. The correctness of thealgorithm follows from our optimization theorem (see Chapter 4). The linear
property for mis comes from the following observation:• The argument to eachmax has at most 8 elements, and so does thesecond argument of f used to deﬁne eachmax. So eachmax costs O(1)time. Therefore, the auxiliary function mis’ is a linear-time program.
11• The opts in the body of mis has at most 4 elements, so it costs constanttime to produce the ﬁnal result after computing mis’ xs.
The function mis’ computes one optimal solution for each class, where classes
correspond to elements of range of h deﬁned as follows.
h:: [α] → (Bool, Bool )h x = (p x, p1 x)
Class 0 corresponds to (False, False), Class 1 to (False, True), Class 2 to(True, False), and Class 3 to (True, True). These classes can be interpreted
as follows.
• Class 0 means that p does not hold and p1 does not hold. This meansthat the head of the list is marked and the set of marked elements inthe list is not independent.
• Class 1 means that p does not hold and p1 holds. This means that thehead of the list is not marked and the set of marked elements in thelist is not independent.
• Class 2 means that p holds and p1 does not hold. This means that thehead of the list is marked and the set of marked elements in the list is
independent.
• Class 3 means that p holds and p1 holds. This means that the headof the list is not marked and the set of marked elements in the list is
independent.
From the function h, we can automatically derive the deﬁnition of table.
See Chapter 4 for details.

1.7.3

Remarks

Two remarks are worth making. First, the optimization theorem, which will
be discussed in detail in Chapter 4, plays a signiﬁcant role in our derivation.
To apply this theorem, the only thing one have to do is to ﬁnd the property
description in mutumorphic form.
Second, the property description in mutumorphic form can be derived
from a recursive property description by using the calculational strategy we
12present in Chapter 4. This derivation utilizes tupling and fusion transformations, which are nothing very special and for which a wealth of calculation
techniques have been developed [Jeu93, BdM96]. Our derivation is thus surprisingly simple and powerful.

1.8

Organization of this thesis

The organization of rest part of this thesis is as follows. In Chapter 2, we
brieﬂy describe the basic concepts of program calculation such as fusion andtupling, and explain the notation used in this thesis. In Chapter 3, we formally deﬁne maximum marking problems. In Chapter 4, we propose theoptimization theorem and our calculation framework. In Chapter 6 we show
the system which generates a practical linear time algorithms for maximum
marking problem, and show its eﬀectiveness by generating linear time algorithms for several examples. In Chapter 7, we discuss related work. In
Chapter 8, we make our concluding remarks.

13

Chapter 2
Preliminaries
In this chapter we brieﬂy review the notational conventions and some basic
concepts of program calculation [Bir87, MFP91, BdM96] used in this thesis.

2.1

Recursive Data Types

To simplify the presentation and proof of the optimization theorem in Chapter 4, we restrict ourselves to considering polynomial data types. And to
avoid categorical notations, we describe polynomial data types in the following form:
D α = C1 (α, D1 , . . . , Dn1 )| C2 (α, D1 , . . . , Dn2 )| ···| Ck (α, D1 , . . . , Dnk )Here Di ’s denote D α, and Ci ’s are called data constructors applying to anelement of type α and a bounded number of recursive components. Though
seemly restricted, these polynomial data types are powerful enough to cover
our commonly used data types, such as lists, binary trees, rooted trees[BLW87], and series-parallel graphs [TNS82]. Moreover, other data types
like the rose trees, a kind of regular data type deﬁned by
RTree α = Node α [RTree α],can be encoded into one of these polynomial data types. This will be demonstrated in Chapter 4.
14

For each data constructor Ci , we deﬁne Fi by
Fi f (e, x1 , . . . , xni ) = (e, f x1 , . . . , f xni ).

2.2

Catamorphism

Catamorphisms, one of the most important concepts in program calculation[MFP91, SF93, BdM96], form a class of important recursive functions overa given data type. They are the functions that promote through the data
constructors.
For example, for the type of lists, given e and ⊕ , there exists a unique
catamorphism cata satisfying the following equations:cata [ ]= ecata (x : xs) = x ⊕ (cata xs)
In essence, this solution is a relabeling: it replaces every occurrence of [ ] withe and every occurrence of : with ⊕ in the cons list. Because of the uniquenessproperty of catamorphisms (i.e., for this example e and ⊕ uniquely determines a catamorphism over cons lists), we usually denote this catamorphism
as cata = ([e, (⊕)]).
Deﬁnition 1 (Catamorphism) A catamorphism over a recursive data
type D is characterized by
f = ([φ1 , . . . , φk ])D ≡ f ◦ Ci = φi ◦ Fi f (i = 1, . . . , k)
If it is clear from the context, we usually omit the subscript D in([φ1 , . . . , φk ])D .
2
Catamorphisms play an important role in program transformation (program
calculation) because they satisfy a number of nice calculational properties inwhich the fusion theorem is of greatest importance:
Theorem 1 (Fusion)f ◦ ([φ1 , . . . , φk ])D = ([ψ1 , . . . , ψk ])D
provided that for every i with 1 ≤ i ≤ k
f ◦ φi = ψi ◦ Fi f.
2
15

The fusion theorem gives the condition that has to be satisﬁed in order to promote (fuse) a function into a catamorphism to obtain a new catamorphism.
It actually provides a constructive but powerful mechanism for deriving a“bigger” catamorphism from a program in a compositional style, a typicalstyle for functional programming. When applying the fusion theorem, we
may do generalization, which is an operation substituting a new function for
the target part of the fusion transformation.

2.3

Mutumorphisms

Mutumorphisms, generalizations of catamorphisms to mutually deﬁned functions, are deﬁned as follows [Fok89, Fok92, HITT97].
Deﬁnition 2 (Mutumorphisms) Functions f1 , f2 , . . ., fn are said to be
mutumorphisms on a recursive data type D α if each function fi is deﬁned
mutually byfi ◦ Cj = φij ◦ Fj (f1 4 f2 4 . . . 4 fn )for j ∈ {1, 2, . . . , k}.

2

Note that f1 4 f2 4 . . . 4 fn represents a function deﬁned as follows:(f1 4 f2 4 . . . 4 fn ) x = (f1 x, f2 x, . . . , fn x)
It is known that mutumorphisms can be turned into a single catamorphismby the tupling transformation [Fok89, Fok92, HITT97].
Theorem 2 (Mutu Tupling) If f1 , f2 , . . . , fn are mutumorphisms likethose in Deﬁnition 2, then
f1 4 f2 4 . . . 4 fn = ([φ1 , φ2 , . . . , φk ])D
where φi = φ1i 4 . . . 4 φni for i = 1, . . . , k.

2.4

2

Notation

Throughout this thesis, we use notation like the functional programming
language Haskell [PJH99]. Here, we explain about the list comprehension
and the deﬁnition of function foldl used in, e.g., Figure 4.1.
16

• List comprehension
List comprehension is a notation for describing a list, which is basedon the notation of set used in mathematics. List comprehension takes
the following form:[ hExpressioni | hQualiﬁeri, . . . , hQualiﬁeri ]hQualiﬁeri is an expression of boolean or a generator. Generator takes
the following form:hVariablei ← hListi(hVariablei, hVariablei) ← hList of tuplesi(hVariablei, hVariablei, hVariablei) ← hList of triplesi···
For example, [ x | x ← [1, 2, 3, 4], x × x ≤ 10 ] is an expression using list
comprehension, whose value is a list [ 1, 2, 3 ].
• The function foldl
foldl is one of the folding function on lists, which is deﬁned as follows:
foldl :: (α → β → α) → α → [β] → αfoldl f a [ ] = afoldl f a (x : xs) = foldl f (f a x) xs

17

Chapter 3
Maximum Marking Problems
In this chapter we deﬁne the maximum marking problems and clarify thecondition that weight should satisfy. At the last of this chapter we clarify
the limitations of the existing solutions.

3.1

A Formal Deﬁnition

A maximum marking problem can be rephrased as follows. Given a data
structure x, the task is to ﬁnd a way to mark some elements in x such thatthe marked data structure of x satisﬁes a certain property p and has the
maximum value with respect to certain weight function w. This means thatno other marking of x satisfying p can produce a larger value with respect
to w. A straightforward solution, whose complexity is exponential in thenumber of elements in x, is as follows:
mmp w p ms =↑w / ◦ ﬁlter p ◦ gen ms
We use gen ms to generate all possible markings of input data x using a set(list) of marks ms, and from those which satisfy the property p we use ↑w /to select one whose value with respect to the weight function w is maximum.
Here we assume that there is at least one possible markings of input data x
satisfying the property p.

18

3.1.1Marking

Here we describe about marking. We use the following function mark as
marking function:
mark:: [Mark ] → α → [α∗ ]mark ms x = [ (x, m) | m ← ms]
This function mark takes as its ﬁrst argument a list ms of all the marks used
for marking and as its second argument an element x, and returns a list of
all the possible marking of the element x. Mark is the type of marks. In
the simplest case, Mark = Bool. This means that there are two possibilities:
mark or unmark. We mean that if the element x is marked with True then it
is marked, and if marked with False then it is unmarked. In another case, forexample, Mark = {Red, Green, Yellow}. This is used for the coloring problem
in Chapter 4. When Mark consists of more than two marks, then we call the
problem ”maximum multi-marking problem” in particular.
We use the following function kind to get the mark from a marked element,
which is deﬁned as follows:kind:: α∗ → Markkind (x, m) = m.
We explain some of our notation for marking. For a data type of α, we use
α to extend α with marking information. It can be deﬁned more concretelybyα∗ = (α, Mark )∗where a boolean value indicates whether or not the element of type α ismarked. Accordingly, we use a∗ , b∗ , . . . , x∗ to denote variables of the type α∗or the type D α∗ (i.e., D (α∗ )).
The function gen, exhaustively enumerating all the possible ways of mark-19

ing every element, can be recursively deﬁned by
gen :: [Mark ] → D α → [D α∗ ]gen ms = ([η1 , . . . , ηk ])where
ηi (e, xs∗1 , . . . , xs∗ni ) =[ Ci (e∗ , x∗1 , . . . , x∗ni ) |e∗ ← mark ms e,
x∗1 ← xs∗1 ,x∗2 ← xs∗2 ,..
.
x∗ni ← xs∗ni ] (i = 1 . . . k)
So much for the speciﬁcation of mmp, with which we can deﬁne various
maximum marking problems. For example, the mis problem in Section 1.7
can be speciﬁed bymis =↑wsum / ◦ ﬁlter p ◦ gen [True, False]
where p is the description of the “independent” property speciﬁed in Section
1.7, and the function wsum computes the sum of weights of marked elements
in a data structure:
wsum :: D α∗ → Weight
wsum = ([φ1 , . . . , φk ])where
φi (e∗ , w1 , . . . , wni ) =(if marked e∗ then weight e∗ else 0) +w1 + · · · + wni
where marked is a function which takes as its argument an element e∗ andchecks whether or not e∗ is marked.
marked:: α∗ → Boolmarked (e, m) = m.
This function is only used for the case that Mark = Bool.

3.1.2

WeightHere we clarify the condition that weight should satisfy. In maximum marking problem, what we want is a marked data that has maximum value with20

respect to weight function w:
w :: D α∗ → Weight.
As we describe in Chapter 1, a maximum marked data is taken by the following function:↑w / :: [D α∗ ] → D α∗
where ↑f is deﬁned bya ↑f b = b,
= a,

if f a ≤ f botherwise.

So, the type Weight has to have the relation ≤. In order to guarantee thatthe obtained result by the function ↑w has the maximum value with respect
to the weight function w, we require that ≤ should be total order on Weight.
So, for example, weight can be integer, real number, natural number, and soon, with the usual total order ≤ on each set.

3.1.3

Maximum Weightsum Problem

Consider the following simple case of maximum marking problem:
mmp wsum p [True, False].
Here, wsum is a weight function that computes the sum of elements of marked
True. We call this kind of problem ”maximum weightsum problem”, which
is well studied in [SHTO00]. In the following, we use the function mws to
represent the above form:
mws p = mmp wsum p [True, False].

3.2

ExamplesHere we show several examples of maximum marking problems, including
the problems we showed in Chapter 1 and an example of maximum multimarking problem called the coloring problem [SHT01].

21

3.2.1

Tree Knapsack Problem

The input of this problem is a binary tree, which is deﬁned as follows:
Tree α ::= Leaf α | Bin (α, Tree α, Tree α)
The property which should be satisﬁed can be described by
p t = weightsum t ≤ C ∧ tc t
where weightsum takes as its argument a marked tree t and simply returns
the sum of weight of selected items, and tc also takes as its argument amarked tree t and checks whether marked elements are connected together.
Selection is represented by two marks, True and False. Weight function w
should computes the sum of value of selected items. By using these functions,the tree knapsack problem can be speciﬁed by↑w / ◦ ﬁlter p ◦ gen [True, False].
Detail description of these functions are in Chapter 5.

3.2.2

r-MSS Problem

Input of r-MSS problem is a sequence of numbers. We represent a sequence
by a list. Property which should be satisﬁed is that selected elements form up
to r connected subsequences in the input sequence. By letting the property
p, he r-MSS problem can be speciﬁed as follows:↑w / ◦ ﬁlter p ◦ gen [True, False].
Here, the weight function w only computes the sum of selected elements.
Detail description of these functions are in Chapter 5.

3.2.3

Party Planning Problem

The input of the party planning problem is a general tree, so we can use thefollowing recursive (regular) data structure.
Org α ::= Leader α [Org α]This does not belong to recursive data types we deﬁned in Section 2.1, so
data type conversion is needed (See section 4). The property which should be22satisﬁed is that any two selected elements does not have direct parent-childrelationship. By letting the property p, the party planning problem can be
speciﬁed as follows:↑w / ◦ ﬁlter p ◦ gen [True, False].
Here, the weight function w only computes the sum of selected elements.
Detail description of these functions are in Chapter 4.

3.2.4

Coloring Problem

Here we show an example of maximum multi-marking problems, the coloring
problem. Suppose there are three marks: Red, Blue, and Yellow. The problem is to ﬁnd a way of marking all the elements such that each sort of markdoes not appear continuously, and that the sum of the elements marked in
Red minus the sum of the elements marked in Blue is maximum.
This problem can be speciﬁed as follows:coloring = ↑w / ◦ ﬁlter indep ◦ gen [Red, Green, Yellow]
indep xs = indep0 xs 0
indep0 [ ] color = True
indep0 (x : xs) color = kind x 6= color ∧ indep0 xs (kind x)
w = + / ◦ map f
where f e∗ = case kind e∗ of
Red → weight e∗Blue → −(weight e∗ )Yellow → 0.
Of course, this deﬁnition is terribly ineﬃcient taking exponential time,
though it is straightforward. In the following chapters, we show that they
can be automatically transformed to an eﬃcient linear one.

3.3

Existing Solution — Borie’s Approach

The maximum marking problems have many instances in graph algorithms.
Bern et al. showed that many graph problems — such as the minimum vertex cover problem, the maximum independent set problem, the maximum
23matching problem, and the traveling salesman problem — can be describedby mws, and, more interestingly, that they can be solved in linear time on
decomposable graphs [BLW87]. Basing their work on Bern et al.’s and on
Courcelle’s [Cou90b], Borie et al. proposed a method for automatically constructing linear-time algorithms that solve the maximum-weightsum problems [BPT92].
The main idea is to restrict the property p to be described in terms ofa small canonical set of primitive predicates (such as the incident predicate
Inc (v, e)) or a combination of them by logical operators (∧, ∨, and ¬) and(either ﬁrst-order or second-order) quantiﬁers (∀ and ∃). For example, theproperty p for the maximum independent set problem is described byp= ∀v1 ∀v2 ¬ Adj (v1 , v2 )Adj (v1 , v2 ) = ∃e1 (Inc (v1 , e1 ) ∧ Inc (v2 , e1 ))∧ ¬ (v1 = v2 ).
With this restriction, it is possible to automatically construct a linear-timealgorithm for mws p from the predicative structure of p.
Though attractive in theory, a linear-time algorithm needs to create ahuge table, and this prevents these algorithms from actually being used
[BLW87, BPT92, APT00]. The table created for the maximum independent142
set problem, for instance, contains more than 2(2 ) entries. The functional
approach we propose can reduce this number to 8 (See Figure 1.1).

24

Chapter 4
Derivation of Eﬃcient
Algorithms
This chapter focuses on a formal study of our functional approach to solving
the maximum marking problems, in which approach our main theorem, theoptimization theorem, plays a signiﬁcant role. It not only clariﬁes a suﬃcientcondition for the existence of linear-time algorithms, but also gives a calculation rule for the construction of such algorithms. As will be seen later,
the key points of our calculation are the functional (rather than predicative)
structure of property descriptions, and the good use made of program transformation such as fusion and tupling [HITT97, Fok92, Fok89]. We begin hereby giving in Lemma 1 a suﬃcient condition under which eﬃcient linear-timealgorithms are guaranteed to exist. Then we use mutumorphisms to formalize in Lemma 3 the class of problems we can solve in linear time. Finally, wesummarize the two lemmas in our optimization theorem.

4.1

A Suﬃcient Condition about Property

It is obvious that not all optimization problems speciﬁed byspec :: D α → D α∗
spec = mws p
can be solved in linear time. Our ﬁrst result gives a suﬃcient condition for
p in the form of the composition of a function and a catamorphism.

25

opt accept φ1 . . . φk x =getdata (↑snd / [ (c, w, r∗ ) | (c, w, r∗ ) ← ([ψ1 , . . . , ψk ])D x, accept c] )where ψi (e, cand1 , . . . , candni ) =eachmax [ (φi (e∗ , c1 , . . . , cni ),(if marked e∗ then weight e∗ else 0) + w1 + . . . + wni ,Ci (e∗ , r1∗ , . . . , rn∗ i )) |e∗ ← [mark e, unmark e],(c1 , w1 , r1∗ ) ← cand1 , · · · , (cni , wni , rn∗ i ) ← candni ](i = 1, . . . , k)

Figure 4.1: Optimization function opt.
Lemma 1 (Optimization Lemma) Let spec be deﬁned byspec :: D α → D α∗
spec = mws (accept ◦ ([φ1 , . . . , φk ])).
If the domain of the predicate accept is ﬁnite, then spec can be solved in lineartime.
2
To prove the lemma, we deﬁne an optimization function opt in Figure 4.1.
We will show that opt solves spec correctly and that is computable in linear
time. In Figure 4.1, getdata is a function which takes as its argument a triple
and returns the third element.
getdata (c, w, r∗ ) = r∗Correctness
Here we show how the right-hand side of
spec x = opt accept φ1 . . . φk x

26

is transformed into the left-hand side. In the transformation rules we use theauxiliary functions ψi0 (i = 1, . . . , k) deﬁned by
ψi0 (e, cand1 , . . . , candni ) =[ (φi (e∗ , c1 , . . . , cni ),(if marked e∗ then weight e∗ else 0)+ w1 + . . . + wni ,Ci (e∗ , r1∗ , . . . , rn∗ i )) |e∗ ← [mark e, unmark e],(c1 , w1 , r1∗ ) ← cand1 , · · · ,(cni , wni , rn∗ i ) ← candni ].

27

opt accept φ1 . . . φk x=

{ unfold opt }getdata (↑snd / [ (c, w, r∗ )| (c, w, r∗ ) ← ([ψ1 , . . . , ψk ]) x,
accept c] )=00{ ([ψ1 , . . . , ψk ]) = eachmax ◦ ([ψ1 , . . . , ψk ]) }getdata (↑snd /00[ (c, w, r∗ ) | (c, w, r∗ ) ← eachmax (([ψ1 , . . . , ψk ]) x),
accept c] )={ filter (accept ◦ fst ) ◦ eachmax =eachmax ◦ filter (accept ◦ fst ) }getdata (↑snd / (eachmax00[ (c, w, r∗ ) | (c, w, r∗ ) ← ([ψ1 , . . . , ψk ]) x,
accept c] ))={ ↑snd / ◦ eachmax =↑snd / }getdata (↑snd / (eachmax00[ (c, w, r∗ ) | (c, w, r∗ ) ← ([ψ1 , . . . , ψk ]) x,
accept c] ))={ c = ([φ1 , . . . , φk ]) r∗ }getdata (↑snd /00[ (c, w, r∗ ) | (c, w, r∗ ) ← ([ψ1 , . . . , ψk ]) x,
accept (([φ1 , . . . , φk ]) r∗ ) ] )={ getdata ◦ ↑snd / =↑wsum / ◦ map getdata }00↑wsum / [r∗ | r∗ ← (map getdata ◦ ([ψ1 , . . . , ψk ])) x,
accept (([φ1 , . . . , φk ]) r∗ ) ]=00{ ([η1 , . . . , ηk ]) = map getdata ◦ ([ψ1 , . . . , ψk ]) }↑wsum / [r∗ | r∗ ← ([η1 , . . . , ηk ]) x,
accept (([φ1 , . . . , φk ]) r∗ ) ]={ fold mws }

mws (accept ◦ ([φ1 , . . . , φk ])) x={ fold spec }spec xThe ﬁrst transformation rule is simply an unfolding of opt.
The second transformation rule is00([ψ1 , . . . , ψk ]) = eachmax ◦ ([ψ1 , . . . , ψk ]).
28

The relation between ψi and ψi0 is as follows:ψi = eachmax ◦ ψi0
The function ([ψ1 , . . . , ψk ]) applies the function eachmax to the list of can00
didates at each stage. The function eachmax ◦ ([ψ1 , . . . , ψk ]), however, ﬁrst
creates all the markings of input data and corresponding weights and classes.
Then it applies the function eachmax. These two functions compute the samecandidate solutions because the function eachmax takes a list which contains
candidate solutions and returns a list which consists of the rightmost optimal
solution for each class in the input list, preserving the order, and the function
eachmax is idempotent (i.e., eachmax ◦ eachmax = eachmax).
The third transformation rule
ﬁlter (accept ◦ fst ) ◦ eachmax =eachmax ◦ ﬁlter (accept ◦ fst )means the commutativity between ﬁlter and eachmax functions, where ﬁlter
is the abbreviation of
λp. λxs. [ x | x ← xs, p x].
The function ﬁlter (accept ◦ fst ) ◦ eachmax ﬁrst applies the function eachmax
and then ﬁlters. The function eachmax ◦ ﬁlter (accept ◦ fst ) ﬁrst ﬁlters andthen applies the function eachmax. These two functions compute the same
result because the predicate (accept ◦ fst ) is concerned only with the classes
and because the functions ﬁlter and eachmax preserve the order.
The fourth transformation rule is↑snd / ◦ eachmax =↑snd /.
This equation holds because ↑snd / returns the rightmost optimal solution,and eachmax returns a list which consists of the rightmost optimal solution
for each class in the input list, preserving the order.
The ﬁfth transformation rule isc = ([φ1 , . . . , φk ]) r∗ .
This means that the class to which r∗ belongs is c, which can be shown by
induction.
29

The sixth transformation rule isgetdata ◦ ↑snd / =↑wsum / ◦ map getdata.
This holds because the second element is the weightsum of the third element,
which can be shown by induction.
The seventh transformation rule00([η1 , . . . , ηk ]) = map getdata ◦ ([ψ1 , . . . , ψk ])follows from Theorem 1.
The eighth and ninth transformation rules are simply the foldings of mws
and spec.
2

Linearity
Here we show that the function opt is linear.
opt accept φ1 . . . φk x =getdata (↑snd /[ (c, w, r∗ ) | (c, w, r∗ ) ← ([ψ1 , . . . , ψk ])D x, accept c] )The important observation is that the number of elements in the list([ψ1 , . . . , ψk ])D x is bounded by the number of classes1 (i.e., the number of
elements in the domain of accept or the range of the catamorphism) because
eachmax returns a list whose length is bounded by the number of classes.
Therefore, if ([ψ1 , . . . , ψk ])D x can be computed in linear time, so can opt.
To prove that ([ψ1 , . . . , ψk ])D is a linear-time algorithm, it is suﬃce to showthat ψi e cand1 . . . candni can be computed in constant time. Taking the factthat φi can be computed in O(1) time because the size of its argument is
independent of the input, we can see that the construction of each triple(c, w, r∗ ) (i.e., each element consumed later by eachmax) can be computedin O(1) time because c can be obtained in O(1) time by φi , w by performing
the + operation ni times, and r∗ simply by combining e∗ , r1∗ , . . . , rn∗ i . Hereni is bounded by
N = max {ni | 1 ≤ i ≤ k}.
1

From the condition that the domain of accept is finite, we know the range of thecatamorphism ([φ1 , . . . , φk ]) is finite. As seen in Section 1.7, this catamorphism projects
the input to this finite range, whose elements are called classes [BLW87].

30

Moreover, exactly (2×|cand1 |×. . .×|candni |) triples of (c, w, r) are generated,
and this number is bounded by the constant 2C N , where C is the number ofclasses. Therefore, the complexity of ψi e cand1 . . . candni is O(1). Though
the size of the bound increases exponentially with N , in many well-used datatypes, such as lists and binary trees, N is small (perhaps one or two).
2

Remarks
This lemma was inspired by Bern et al.’s work on decomposable graphs[BLW87], where a similar condition on decomposable graphs was given. We
generalize the idea from decomposable graphs2 to generic recursive datatypes. Moreover, we give a concrete linear time algorithm using the optimization function opt in Figure 4.1.
In the optimization lemma, we give the optimization function opt to compute an optimal solution. It is worth noting that by slightly changing thedeﬁnition of the optimization function opt, we can also do recognition andenumeration in linear time. Recognition means recognizing whether or nota solution satisfying the property description exists, and enumeration meanscounting the number of solutions satisfying the property description [BPT92].

4.2

A Suﬃcient Condition about Weight
FunctionIn the above, we only consider the case that marks are True and False andthe weight function w is wsum, which simply computes the sum of marked
elements. The previous work restricted the weight function w to be justthe sum of weight of marked elements [Bir00, SHTO00, BLW87, BPT92].
As seen in the coloring problem in Chapter 3, we often need to use a moregeneral weight function. Here, we generalize Lemma 1 with respect to marks
and weight function. First, we allow any ﬁnite number of elements that are
diﬀerent each other as marks. Second, we allow a class of weight functions.
We deﬁne the following general form, a kind of list homomorphism [Bir87],
which we call homomorphic weight function.

2

Decomposable graphs do not allow the addition of a new element when gluing smallergraphs.

31

4.2.1

Homomorphic Weight Function

Deﬁnition 3 (Homomorphic Weight Function) A function w is a homomorphic weight function if it is deﬁned as follows:
w
w

::
=

D α∗ → Weightplus ◦ map f
where plus = ([φ1 , . . . , φk ])φi (e, x1 , . . . , xni ) = e ⊕ x1 ⊕ · · · ⊕ xni

where ⊕ is an associative binary operator which can be computed in O(1)time, which has an identity element ι⊕ , and which satisﬁes the condition
called distributivity over ↑id :(↑id / xs) ⊕ (↑id / ys) = ↑id /[ x ⊕ y | x ∈ xs ∧ y ∈ ys ].

2A homomorphic weight function allows any O(1) computation f overeach marked element and a more general operation ⊕ rather than just +for “summing up”. This enables us to deal with the weight function for thecoloring problem in Chapter 3.
The function map appeared in the deﬁnition of homomorphic weight function is deﬁned as follows:map:: (α → β) → D α → D β
map f = ([φ1 , . . . , φk ])where φi (e, x1 , . . . , xni ) = Ci (f e, x1 , . . . , xni )This is not the map function map on lists but the map function on D α.
This is a little confusing, but we use the same name since we think it is clear
from context.

4.2.2

Generalized Optimization Lemma

Here we generalize Lemma 1 with respect to marks and weight function.
Lemma 2 (Generalized Optimization Lemma) Let spec be deﬁned byspec :: D α → D α∗
spec = mmp w (accept ◦ ([φ1 , . . . , φk ])) ms.
If the domain of the predicate accept is ﬁnite, w is a homomorphic weightfunction, and ms is a list of ﬁnite number of marks, then spec can be solved
in linear time.
2
32

opt (f, ⊕, ι⊕ ) accept φ1 . . . φk ms x =getdata (↑snd / [ (c, w, r∗ ) | (c, w, r∗ ) ← ([ψ1 , . . . , ψk ])D x, accept c] )where ψi (e, cand1 , . . . , candni ) =eachmax [ (φi (e∗ , c1 , . . . , cni ),f e∗ ⊕ w1 ⊕ . . . ⊕ wni ,Ci (e∗ , r1∗ , . . . , rn∗ i )) |e∗ ← mark ms e,(c1 , w1 , r1∗ ) ← cand1 , · · · , (cni , wni , rn∗ i ) ← candni ](i = 1, . . . , k)

Figure 4.2: Generalized optimization function opt
This lemma allows use of any ﬁnite number of marks and any homomorphic weight function. To prove the lemma, we deﬁne a generalized optimization function opt in Figure 4.2. The following equation similar to one in the
proof of Lemma 1 holds:
spec x = opt (f, ⊕, ι⊕ ) accept φ1 . . . φk ms x
where ⊕ and f appear in the deﬁnition of w:
w
w

::
=

D α∗ → Weightplus ◦ map f
where plus = ([φ1 , . . . , φk ])φi (e, x1 , . . . , xni ) = e ⊕ x1 ⊕ · · · ⊕ xni

We omit the proof since correctness and linearity can be shown in the same
way as in proof of Lemma 1. In the following, we use the name opt forindicating the function opt in Figure 4.2.

4.3

Decomposition Lemma

To apply the optimization lemma, we need to represent the property description p as accept ◦ ([φ1 , . . . , φk ]), where the domain of accept is ﬁnite.

33

4.3.1

Property with Boolean Functions

The following lemma gives a method for transforming the property description p into the above form when p is deﬁned using mutumorphisms.
Lemma 3 (Decomposition Lemma) If the property description p0 ::D α∗ → Bool can be deﬁned as mutumorphisms with other property descriptions pi :: D α∗ → Bool for i = 1, . . . , n, then p0 can be decomposed
into
p0 = accept ◦ ([φ1 , . . . , φk ]),2

where the domain of accept is ﬁnite.

Proof. To prove the lemma, we suppose that mutumorphisms p0 , p1 , . . . , pn
are deﬁned as follows. For each i ∈ {0, 1, . . . , n} and each j ∈ {0, 1, . . . , k},pi ◦ Cj = φij ◦ Fj (p0 4 p1 4 · · · 4 pn ).
By the mutu tupling theorem, we havep0 4 p1 4 . . . 4 pn = ([φ1 , . . . , φk ])D

(4.1)

where
φi = φ0i 4 φ1i 4 . . . 4 φni(i = 1, . . . , k).

By deﬁning
accept (x0 , x1 , . . . , xn ) = x0 ,we obtain
p0 = accept ◦ ([φ1 , . . . , φk ])D .
Next we show that the domain of accept, i.e., the range of ([φ1 , . . . , φk ])D ,is ﬁnite. Functions p0 , p1 , . . . , pn have ranges which consist of two elements,
True and False. So, from equation (4.1), the number of elements in therange of ([φ1 , . . . , φk ])D is 2n+1 , which is a ﬁnite number. This means that thedomain of accept is ﬁnite.
2

4.3.2

Property with Finite-range Functions

It is easy to see that property can be described using mutumorphisms which
consist of functions whose range is ﬁnite.
34

4.4

The Main Theorem

Combining the above two lemmas, we obtain the optimization theorem.
Theorem 3 (Optimization Theorem)
The maximum marking problem speciﬁed byspec :: D α → D α∗
spec = mmp w p0 ms
can be solved in linear time if the property description p0 :: D α∗ → Bool canbe deﬁned as mutumorphisms with other property descriptions pi :: D α∗ →Bool for i = 1, . . . , n, w is a homomorphic weight function, and ms is a listof ﬁnite number of marks.
2This theorem provides a friendly interface for the derivation of eﬃcientlinear-time algorithms solving the maximum marking problems. When theproperty description is deﬁned as mutumorphisms which consist of n property
descriptions, a derived catamorphism will have range which has 2n elements.
In many cases, property description p can be easily described as mutumorphisms which consist of a small number of property descriptions (two to fourfor examples in this thesis). For example, the party planning problem is described with mutumorphisms which consist of only two property descriptions.
This means that the linear-time algorithms obtained are practical.
To see how the theorem works, recall the mis problem in Section 1.7. The
property description p is deﬁned with p1 in the following mutumorphic form:
p [x] = Truep (x : xs) = if marked x then p1 xs ∧ p xs else p xs
p1 [x] = not (marked x)
p1 (x : xs) = not (marked x)
It follows from the optimization theorem that an eﬃcient linear-time algorithm solving the mis problem can be derived automatically.
It is easy to extend lemma 3 and theorem 3 to allow the property description p0 to be deﬁned as mutumorphisms with other functions whose ranges
are ﬁnite.

35

4.5

Extension of property

The property description p for the coloring problem can be naturally speciﬁed
as follows:
indep xs
= indep0 xs Neutral
indep0 [ ] color= True0indep (x : xs) color = kind x 6= color ∧ indep0 xs (kind x).
But this is not in a required mutumorphic form such that the rule in Sasano etal. [SHTO00] can be applied, because indep0 has an additional accumulating
parameter color. Here, Neutral is used as the initial value of the accumulating parameter, which is diﬀerent from all the colors used for coloring theelements. The function kind takes as its argument a marked element andreturns the kind of mark of the element. If we insist on specifying indep ina mutumorphic form, we would have to instantiate all the possible values ofcolor used by indep0 , and could reach the following complicated deﬁnition:
indep [ ]= Trueindep (x : xs) = case kind x of
Red → indepR xs
Blue → indepB xs
Yellow → indepY xs
indepR [ ]= TrueindepR (x : xs) = case kind x of
Red → False
Blue → indepB xs
Yellow → indepY xs
indepB [ ]= TrueindepB (x : xs) = case kind x of
Red → indepR xs
Blue → False
Yellow → indepY xs
indepY [ ]= TrueindepY (x : xs) = case kind x of
Red → indepR xs
Blue → indepB xs
Yellow → False.
36

In fact, this instantiation not only leads to a complicated deﬁnition, but also
makes the generated program less eﬃcient than that generated by Theorem
3.
For the property p which is to specify the feasible markings with multiple
kinds of marks, the existing approach [SHTO00] (as seen in the deﬁnition of
indep in Chapter 3) only allows p to be deﬁned in a mutumorphic form withseveral other functions, say p1 , . . . , pn , whose ranges are ﬁnite.
p []p (x : xs)= e= φ x (p xs, p1 xs, . . . , pn xs)..
.

pi [ ]= ei
pi (x : xs) = φi x (p xs, p1 xs, . . . , pn xs)..
.
If p is deﬁned in the mutumorphic form, by applying the tupling transformation [Fok92, HITT97], we can always come up with the following deﬁnition
for p, a composition of a project function with a foldr:
p = fst ◦ foldr ψ e0
where ψ x es = (φ x es, φ1 x es, . . . , φn x es)
e0 = (e, e1 , . . . , en ).

4.5.1

Finite Accumulative Property

To specify a history-sensitive property, we often want to use an accumulating
parameter. So we extend the above p to a composition of a function with afoldrh , a higher order version of foldr, which is deﬁned as follows:
foldrh (φ1 , φ2 ) δ [ ] e= φ1 efoldrh (φ1 , φ2 ) δ (x : xs) e = φ2 x e (foldrh (φ1 , φ2 ) δ xs (δ x e)).
Using this function foldrh , we deﬁne the following form, which we call ﬁnite
accumulative property.
Deﬁnition 4 (Finite Accumulative Property) A property p is a ﬁnite
accumulative property if it is deﬁned as follows:p :: [α∗ ] → Boolp xs = g (foldrh (φ1 , φ2 ) δ xs e0 )where the domain of g and range of δ is ﬁnite.
37

Though we only consider the property with an accumulating parameteron lists, it can be extended to any polynomial data type D α.

4.5.2

Theorem

Now we propose theorem for property description with an accumulating parameter.
Theorem 4 Suppose a speciﬁcation of a maximum multi-marking problem
is given as
mmp w p ms = ↑w / ◦ ﬁlter p ◦ gen ms.
If w is a homomorphic weight function
w = ⊕ / ◦ map f
and p is a ﬁnite accumulative property
p xs = g (foldrh (φ1 , φ2 ) δ xs e0 ),then the maximum multi-marking problem (mmp w p ms) can be solved by
optacc (f, ⊕, ι⊕ ) (λ(c, e) . g c ∧ e == e0 ) φ1 φ2 δ ms .
The deﬁnition of optacc is given in Figure 4.3.
This theorem has a form similar to Theorem 3 except for using array inthe deﬁnition of optacc for eﬃciency, and it can be proved by induction on
the input list. We omit the detailed proof in this thesis. One remark worth
making is about the cost of the derived program. Assuming that δ and ghave the types
δ :: α∗ → Acc → Acc
g :: Class → Bool,
we can conclude that the generated program using optacc can be computedin O(|Acc| · |Class| · |ms| · n) time, where n is the length of input list, |ms| isthe number of marks, and |Acc| and |Class| denote the size of the type Acc
and the type Class respectively. That means that our approach is applicable
only when the domain of g and the range of δ is ﬁnite. If our approach isapplicable, our generated program is much more eﬃcient than the initial
speciﬁcation program mmp w p ms, which is exponential.
38

optacc (f, ⊕, ι⊕ ) accept φ1 φ2 δ ms xs =let opts = foldr ψ2 ψ1 xs
in snd (↑fst / [ (w, r∗ ) | Just (w, r∗ ) ← [ opts!i | i ← range bnds,
opts!i 6= Nothing, accept i ] ])where ψ1 = array bnds [ (i, g i) | i ← range bnds]
ψ2 x cand = accumArray h Nothing bnds
[ ((φ2 x∗ e c, e), (f x∗ ⊕ w, x∗ : r∗ ))| x∗ ← mark ms x,e ← acclist,((c, ), Just (w, r∗ )) ←[ (i, cand!i) | i ← [ (c0 , δ x∗ e) | c0 ← classlist],
inRange bnds i,cand!i 6= Nothing ] ]g (c, e) = if (c == φ1 e) then Just (ι⊕ , []) else Nothingh (Just (w1 , x1 )) (w2 , x2 ) = if w1 > w2 then Just (w1 , x1 )else Just (w2 , x2 )h Nothing (w, x) = Just (w, x)
bnds = ((head classlist, head acclist), (last classlist, last acclist))
acclist = list of all the values in Acc
classlist = list of all the values in Class

Figure 4.3: Optimization function optacc.

39

An Example
To see how the theorem works, we demonstrate how to derive a linear algorithm for the coloring problem in Chapter 3. Recall that the speciﬁcation
for the coloring problem has been given in Chapter 3. The weight function
has been written in our required form, and the property indep can be easily
rewritten using foldrh as follows:
indep xs = id (foldrh (φ1 , φ2 ) δ xs 0)
where φ1 e = True
φ2 x e r = kind x 6= e ∧ r
δ x e = kind x.
Now applying the theorem quickly yields a linear time algorithm, whose
program coded in Haskell is given in Figure 4.4. Notice that in this example,
k = 3, |Acc| = 4, and |Class| = 2. Evaluating the expression> coloring [1,2,3,4,5]
gives the result of[(1, 1), (2, 3), (3, 1), (4, 3), (5, 1)].
It is worth while to compare the generated algorithms from the two property description with and without an accumulating parameter. Consider
the coloring problem with k colors and with certain homomorphic weightfunction w. By using property description with an accumulating parameter,O(k 2 n) algorithm is obtained because |Acc| = k + 1 and |Class| = 2. On thecontrary, by using property description in mutumorphic form without accumulating parameters as described in Chapter 3, O(2k n) algorithm would beobtained by applying the previous method [SHTO00], if it could deal withmultiple kinds of marks.

4.6

Calculation Strategy

In this section we show how to derive practical linear-time algorithms thatsolve the maximum marking problems by applying the optimization theorem.
Speciﬁcation Specify the property description for a given maximum marking problem using a recursive function p on a data structure R.
40

coloring = optacc (f, (+), 0) accept phi1 phi2 delta [1,2,3]
acclist = [0..3]
classlist = [False, True]
accept (c,e) = c && e==0
f = \x -> case kind x of
1 -> weight x
2 -> - (weight x)
3 -> 0phi1 e = True
phi2 x e c = kind x /= e && cdelta x e = kind x
kind (_,m) = m
weight (x,_) = x---------------(the first half)-----------------------------

Figure 4.4: A linear-time Haskell program for the coloring problem (the ﬁrsthalf).

41

---------------(the second half)---------------------------optacc (f, oplus, id_oplus) accept phi1 phi2 delta ms xs =let opts = foldr psi2 psi1 xs
in snd (getmax [(w,r) | Just (w,r) <- [ opts!i| i <- range bnds,
opts!i /= Nothing,
accept i]])where psi1 = array bnds [(i, g i) | i <- range bnds]
psi2 x cand = accumArray h Nothing bnds[((phi2 xm e c, e),(f xm ‘oplus‘ w, xm:r))| xm <- mark ms x,
e <- acclist,((c,_),Just (w,r)) <[ (i,cand!i)| i <- [ (c’,delta xm e)| c’ <- classlist],
inRange bnds i,cand!i /= Nothing]]
g (c,e) = if (c == phi1 e) then Just (id_oplus, [])else Nothingh (Just (w1,x1)) (w2,x2) = if w1 > w2 then Just (w1,x1)
else Just (w2,x2)
h Nothing (w,x) = Just (w,x)
bnds = ((head classlist,head acclist),(last classlist,last acclist))
getmax [] = error "No solution."getmax xs = foldr1 f xs
where f (w1,cand1) (w2,cand2)= if w1>w2 then (w1,cand1) else (w2,cand2)

Figure 4.5: A linear-time Haskell program for the coloring problem (thesecond half).

42

Step 1 If R is not a polynomial data type, ﬁnd a polynomial data structure
D into which R can be encoded, and then transform the property description p on R into p0 on D. If the data structure R is a polynomial
data structure, then do nothing. That is, let p0 = p and D = R.
Step 2 Derive p0 in terms of mutumorphisms which consist of several property descriptions p00 , p01 , . . . , p0n on D by generalizing some part in p0
and fusing it. If necessary, do tupling transformation to get a catamorphism, since a catamorphism must be obtained when applying thefusion theorem.
Step 3 Apply the optimization theorem to get a linear-time algorithm thatsolves the maximum marking problem.
We demonstrate these steps on the party planning problem.
The Party Planning Problem
Speciﬁcation The inputs in the party planning problem are trees, so we
can use the following recursive (regular) data structure.
Org α ::= Leader α [Org α]
The speciﬁcation of the problem is
pp :: Org α → Org α∗
pp = mws p
where the property description p of the party planning problem can be
written as follows:p :: Org α∗ → Boolp (Leader v [ ]) = Truep (Leader v (t : ts)) =not (bothmarked v (getLeader t)) ∧p t ∧ p (Leader v ts)
If the tree contains only a single node, then the property is satisﬁed.
Otherwise we check its root v1 with its children one by one to makecertain that both v1 and its child are not marked at the same time, andthen we check other parts of the tree recursively. Here bothmarked v1 v243

is used to check whether both v1 and v2 are marked, and getLeader
returns the root of the organization tree:
bothmarked :: α∗ → α∗ → Bool
bothmarked v1 v2 = marked v1 ∧ marked v2
getLeader :: Org α → α
getLeader (Leader v ts) = v.
Notice that our initial speciﬁcation is rather straightforward.
Step 1 The data type Org α is regular but non-polynomial data type whose
nodes can have arbitrarily many children. So we transform this data
type Org α into a polynomial data type. In fact, we can represent thetype Org α by the following binary tree structure, called a rooted tree
[BLW87].
RTree α ::= Root α|
Join (RTree α) (RTree α)
The relation between these two data types can be captured by thefollowing functions.
r2o :: RTree α → Org αr2o (Root v) = Leader v [ ]r2o (Join t1 t2 ) = let Leader v ts = r2o t2
in Leader v ((r2o t1 ) : ts)
o2r :: Org α → RTree αo2r (Leader v [ ]) = Root v
o2r (Leader v (t : ts)) =Join (o2r t) (o2r (Leader v ts))
These two functions convert data types in linear time.
Next we transform the property description p on Org α to p0 on RTree α.
Let p0 and getLeader0 be the functions on RTree α which correspond to
p and getLeader on Org α. These functions should satisfy the following
equations.
p0:: RTree α∗ → Boolp0 t
= p (r2o t)
getLeader0:: RTree α → Bool0
getLeader t = getLeader (r2o t)
44

A simple fusion calculation yields
p0 (Root v) = True
p0 (Join t1 t2 ) =not (marked (getLeader0 t1 ) ∧marked (getLeader0 t2 )) ∧p0 t1 ∧ p0 t2
getLeader0 (Root v) = v
getLeader0 (Join t1 t2 ) = getLeader0 t2 .
Step 2 To represent p0 using mutumorphisms which consist of only property
descriptions, we generalize the part marked ◦ getLeader0 and let it belm0 .
lm0 :: RTree α∗ → Boollm0 = marked ◦ getLeader0
By a simple fusion calculation we can get
lm0 (Root v)= marked v
0lm (Join t1 t2 ) = lm0 t2 .
Now we can represent p0 using mutumorphisms which consist of thefollowing two property descriptions.
p0 (Root v)
p0 (Join t1 t2 )= True= not (lm0 t1 ∧ lm0 t2 ) ∧p0 t1 ∧ p0 t2
lm0 (Root v)= marked v
lm0 (Join t1 t2 ) = lm0 t2

Step 3 By applying our optimization theorem, we get the following lineartime algorithm.
pp = r2o ◦ (opt accept φ1 φ2 ) ◦ o2r
where
accept (x0 , x1 ) = x0
φ1 v = (True, marked v)
φ2 (a1 , b1 ) (a2 , b2 ) =(not (b1 ∧ b2 ) ∧ a1 ∧ a2 , b2 )45

So much for the derivation. Note that we can go further to compute φistatically and store it in a table, though this is not necessary. To doso, deﬁne four classes by
c0 = (False, False)
c1 = (False, True)
c2 = (True, False)
c3 = (True, True)and simplify the functions accept, φ1 , and φ2 . We write φ2 as a table.
accept c = (c == c2 ) ∨ (c == c3 )φ1 v
= if marked v then c3 else c2
φ2
c0
c1
c2
c3

c0
c0
c0
c0
c0

46

c1
c1
c1
c1
c1

c2
c0
c0
c2
c2

c3
c1
c1
c3
c1

Chapter 5
ExamplesIn this chapter, we give more examples, showing that our proposed generation rule is quite general and powerful. Examples include several kinds ofknapsack problems, scheduling problem, a data mining problem mentioned in
Chapter 1, several problems in the book Algebra of Programming [BdM96].

5.1

Paragraph Formatting Problem

The paragraph formatting problem is the problem of breaking a sequence ofwords into lines to form a paragraph. At least one blank space must exist
between any adjacent two words in the same line. Line length, i.e., thenumber of characters each line holds, is ﬁxed as m. We want to minimize thesum of the number of blank spaces in all the lines excluding the last line. We
assume that the input sequence of words is given by a list of words and that aword is expressed by its length since the spelling of words is not needed. For
example, the sequence of words ”This is a dog. They are cats.” is expressedas the list [4, 2, 1, 4, 4, 3, 5].
We would like to treat this problem as a multi-marking problem, that is,
to describe this problem in the form
mmp w p ms.
We use three kinds of marks, 1, 2, and 3. So, k = 3. If a word is marked 2,then it indicates that the word is the last word of the line it belongs to. If aword is marked 3, then it indicates that the word belongs to the last line. The
other words are marked 1. We make special treatment of the last line in order47

to exclude the blank spaces when computing the sum of the number of blankspaces. The property p checks whether a marking represents a valid breaking
or not. We describe the property p by using an accumulating parameter. The
accumulating parameter holds the pair of position pos and mark mk, where
pos represents the last position ﬁlled by the previous words in the current
line, and mk represents the kind of mark of the previous word. We deﬁne
the property p as follows:p xs = p0 xs (0, 2)
p0 [ ] (pos, mk) = mk 6= 1
p0 (x : xs) (pos, mk) =case mk of
1 → case kind x of
1 → pos + l x + 1 ≤ m ∧ p0 xs (pos + l x + 1, 1)
2 → pos + l x + 1 ≤ m ∧ p0 xs (0, 2)
3 → False
2 → case kind x of
1 → pos + l x ≤ m ∧ p0 xs (pos + l x, 1)
2 → pos + l x ≤ m ∧ p0 xs (0, 2)
3 → pos + l x ≤ m ∧ p0 xs (pos + l x, 3)
3 → case kind x of
1 → False
2 → False
3 → pos + l x + 1 ≤ m ∧ p0 xs (pos + l x + 1, 1),
where we use the function l to compute the length of a word.
Next, we have to describe the weight function w. We want to minimize
the sum of the number of blanks except for the last line. The function white
which returns the sum can be written as follows:white = +/ ◦ map f
where f x = case kind x of
1 → −l x2→m−l x3 → 0.
Using this function, we can deﬁne the weight function w as follows:
w x = −(white x).
48This can be easily transformed into the following form:
w = +/ ◦ map f
where f x = case kind x of
1→lx
2 → −m + l x
3 → 0.
Now the paragraph formatting problem is written as follows:
mmp w p [1, 2, 3].
By applying the Theorem 4 (by using the rule mmpRule), we can obtainan O(mn) algorithm where n is the number of words. This complexity isachieved by the fact that the number of kinds of marks is three, the size ofthe accumulating parameter |Acc| is 3(m + 1), and the size of the function g(in this case id) |Class| is 2.

5.2

Security Van Problem

The security van problem can be speciﬁed as follows [BdM96].
Suppose a bank has a known sequence of deposits and withdrawals.
For security reasons the total amount of cash in the bank should
never exceed some ﬁxed amount N , assumed to be at least as
large as any single transaction. To cope with demand and supply,
a security van can be called upon to deliver funds to the bank or
to take away a surplus. The problem is to compute a schedule
under which the van visits the bank a minimum number of times.
In order to specify this problem as a maximum multi-marking problem, weconsider the security of transactions. A sequence [a1 , a2 , . . . , an ] of transactions is called secure if there is an amount r, indicating the total amount ofcash in the bank at the beginning of the sequence of transactions, such thateach of the sumsr, r + a1 , r + a1 + a2 , . . . , r + a1 + · · · + anlies between zero and N . For example, taking N = 10, the sequence [3, −5, 6]
is secure because the van can take away or deliver enough cash to make an49initial reserve of, for example, 5. Given the constraint that N is no smaller
than any single transaction, every singleton sequence is secure, so a valid
schedule certainly exists.
To formalize the constraint, deﬁneceiling = ↑+/ / ◦ inits
ﬂoor= ↓+/ / ◦ inits
where inits is a function which takes as its argument a list and returns thelist which has all the initial segments including empty list. A sequence x oftransactions is secure if and only if
ceiling x − ﬂoor x ≤ N.
Considering this condition, we can deﬁne property p in the following way.
We express the time the van visits by marking 1 to a transaction after which
the van visits. Transactions marked 2 represent the other transactions. The
accumulating parameter holds a triple of sum, ceiling, and ﬂoor for each
initial segment.
p xs = p0 xs (0, 0, 0)
p0 [ ] (s, c, f ) = True
p0 (x : xs) (s, c, f ) =let (s0 , c0 , f 0 ) = (s + w x, c ↑id s0 , f ↓id s0 )in case kind x of
1 → if c0 − f 0 ≤ N then p0 xs (w x, 0 ↑id w x, 0 ↓id w x)
else p0 xs (w x, 0 ↑id w x, 0 ↓id w x)
2 → if c0 − f 0 ≤ N then p0 xs (s0 , c0 , f 0 ))else False
Here, the function w takes as its argument a marked transaction and returns
the amount of it. We want to minimize the number of times the van visits,
so we ﬁrst deﬁne the function times which computes the times the van visits.
times= +/ ◦ map f
where f x = case kind x of
1→1
2→0

Using this function, we can deﬁne the weight function w as follows:
w x = − (times x).
50This can be easily transformed into the following form:+/ ◦ map f
where f x = case kind x of
1 → −1
2 → 0.

w =Now the security van problem is written as follows:
mmp w p [True, False].
The weight function w is written in the required form, and the property p
can be easily rewritten into the required form, though we omit the form. By
applying Theorem 4, we obtain O(N 3 n) algorithm because |Acc| = (N +1)2 (2N + 1), k = 2, and |Class| = 2.

5.3

Knapsack Problem

The knapsack problem [MT90] is a well known combinatorial optimization
problem. There are several problems called knapsack problem such as 0-1
knapsack problem, 0-1 multiple knapsack problem, multidimensional knapsack problem, and so on. Here we consider the simplest one, the 0-1 knapsackproblem and derive an eﬃcient linear time algorithm from simple speciﬁcation [SHTO01c].
Input of the 0-1 knapsack problem is a set of items each of which has
weight and value. Output is a feasible selection of items whose value sum
is maximum in all the feasible item selections. A selection is feasible whensum of weight of selected items does not exceed the given capacity C. We
assume weight of items are integers. Without this assumption, this problem
becomes NP-hard.

5.3.1

Speciﬁcation

We express an item by pair of weight and value (Weight, Value) and a set ofitems by non-empty list [(Weight, Value)]. Knapsack problem is a maximum
marking problem where weight function w computes sum of value of marked(selected) items and property knap checks that sum of weight of marked
items does not exceed the given capacity C.
51

knap xs = weightsum xs ≤ C
The argument of knap is a list of items, each of which is accompanied bya mark which indicates whether the item is selected or not.

5.3.2

Property by Finite Mutumorphisms

In order to express property knap as ﬁnite mutumorphisms on non-empty
list, we introduce the following function cut.
cut:: Weight → Weight
cut w = if w ≤ C then w else C + 1
This function cut takes weight w as its argument and returns C + 1 if w isgreater than C and returns w otherwise. By using this function cut, we can
express property knap as follows:
knap xs = sumw xs ≤ C
sumw [x] = cut (if marked x then weight x
else 0)sumw (x : xs) =cut ((if marked x then weight x
else 0) + sumw xs)
The function marked checks whether the element is marked or not.

5.3.3

Property by Finite Accumulative Property

We express selection by marking 1 to selected items and 2 to the others. The
property for 0-1 knapsack problem can be described as follows. The accumulating parameter holds a value from 0 to C, which indicates the remaining
capacity of knapsack.
knap xs= knap0 xs C
0knap [ ] e= True0
knap (x : xs) e = case kind x of
1 → if e ≥ w x then knap0 xs (e − w x) else False
2 → knap0 xs e
Here, the function w returns the weight of the item.
52

5.3.4Weight function

We want to maximize the value of selected items, so we can deﬁne the weightfunction w as follows:
w = +/ ◦ map f
where f x = case kind x of
1 → value x
2 → 0.
Here, the function value returns the value of the item.
Now the 0-1 knapsack problem is written as follows:
mmp w knap [True, False].
The weight function w is written in the required form, and the property knap
can be easily rewritten into the required form, though we omit the form.

5.3.5

Derivation by Theorem 4

By applying Theorem 4, we obtain O(Cn) algorithm because |Acc| = C + 1,
k = 2, and |Class| = 2.

5.3.6

Derivation by Theorem 3

Since the range of the property knap is {True,False} and the range of thefunction sumw is {0, 1, . . . , C + 1}, the functions knap, sumw constitute mutumorphisms on non-empty lists. So, by applying Theorem 3, we get thefollowing algorithm:
knapsack x = opt accept φ1 φ2 x
where
accept x = x ≤ C
φ1 x = cut (if marked x then weight x
else 0)φ2 (x, y) = cut ((if marked x thenweight x else 0) + y)
The complexity of this algorithm is O(Cn) where n is the number of
items.
53

5.4

Knapsack Problem on List

In the previous subsection, we considered the ordinary knapsack problem,
which does not have structure on items. In this section, we consider a variantof knapsack problem, where items have list structure. Here as an example
we consider an additional condition that we cannot select adjacent items.

5.4.1

Speciﬁcation

The condition that adjacent items cannot be selected is described as follows:
indep [x] = True
indep (x : xs) =if marked x thennot (marked (hd xs)) ∧ indep xs
else indep xs
hd [x] = x
hd (x : xs) = x
When the item list is a singleton [x], since the number of items is one andthus adjacent items cannot be selected, indep returns True. When the item
list is (x : xs), there are more than two items exist. When the top item x is
selected, from the remaining items xs we should select items independently
and must not select the head item of xs. The function hd takes a non-empty
list as its argument and returns the head element of the list. By using thisproperty indep, we can describe the property of this problem as follows:p xs = indep xs ∧ knap xs.

5.4.2

Derivation

This property p is not described as ﬁnite mutumorphisms, because the rangeof the function hd is not ﬁnite generally (for example, in the case that thetype of weight of item is Integer). In order to describe this property p as
ﬁnite mutumorphisms, let
p1 = not (marked (hd xs)).
By applying fusion transformation, p1 is transformed into the following form:
p1 [x]= not (marked x)
p1 (x : xs) = not (marked x)
54Thus the property indep is described as
indep [x] = True
indep (x : xs) = if marked x
then p1 xs ∧ indep xs
else indep xs,
so the functions p, indep, p1 , knap, sumw constitute ﬁnite mutumorphisms on
non-empty list. By applying Theorem 3, we get O(Cn) algorithm where n is
the number of items, though we omit the result.

5.5

Tree Knapsack Problem

In this section, we consider another variant of knapsack problem, where items
have tree structure. Here as an example we consider an additional condition
that selected items are connected by edges. In [dM95], by using relational
calculus, a linear time algorithm for a similar problem to this problem, but
one have to check two prerequisites when applying their theorem, whichmakes the derivation diﬃcult. In contrast, in our optimization theorem,
the prerequisites is simple enough for ordinary functional programmers tocheck, which results in easy derivation and makes it possible to automate thederivation, which will be seen in Chapter 6.

5.5.1

Speciﬁcation

We consider the binary tree which is deﬁned as follows:
Tree α ::= Leaf α | Bin (α, Tree α, Tree α)
The condition that sum of weight does not exceed the given capacity C canbe deﬁned as follows:
tk t = tws t ≤ C
tws (Leaf x) =cut (if marked x then weight x else 0)
tws (Bin (x, t1 , t2 )) =cut ((if marked x then weight x else 0)+ tws t1 + tws t2 )55

Next, the condition that selected items are connected by edges can be
described as follows:
tc (Leaf x) = Truetc (Bin (x, t1 , t2 )) =if marked x then tc0 t1 ∧ tc0 t2else (nm t1 ∧ tc t2 ) ∨ (tc t1 ∧ nm t2 )If the tree is Leaf x, then it satisﬁes the condition, so tc returns true. If thetree is (Bin (x, t1 , t2 )), then if the item x is selected then tc checks whether
t1 and t2 satisﬁes the condition that selected elements constitute a preﬁx ofthe tree, tc0 , otherwise one of t1 and t2 should not have any selected items
and the other one have to satisfy the property tc. The property that tree
does not have any selected items can be deﬁned as follows:
nm (Leaf x) = not (marked x)
nm (Bin (x, t1 , t2 )) =not (marked x) ∧ nm t1 ∧ nm t2
The property tc0 can be deﬁned as follows:
tc0 (Leaf x) = True
tc0 (Bin (x, t1 , t2 )) =if marked x then tc0 t1 ∧ tc0 t2else nm t1 ∧ nm t2
This property tc0 checks preﬁx property, that is, if an item x is selected, thenthe parent of x have to be selected. By using these properties, the propertyof the tree knapsack problem p can be described as follows:
p t = tk t ∧ tc t56

5.5.2Derivation

Since the functions p, tk, tc, tws, nm, tc0 constitute ﬁnite mutumorphisms, byapplying Theorem 3, we can obtain the following algorithm:
knaptree t = opt accept φ1 φ2 t
whereaccept (a, b, c, d) = a ≤ C ∧ b
φ1 x = (cut (if marked x then weight x
else 0),True, not (marked x), True)
φ2 (x, (a1 , b1 , c1 , d1 ), (a2 , b2 , c2 , d2 )) =(cut (if marked x then weight x
else 0) + a1 + a2 ),if marked x then d1 ∧ d2
else (c1 ∧ b2 ) ∨ (b1 ∧ c2 ),not (marked x) ∧ c1 ∧ c2 ,if marked x then d1 ∧ d2
else c1 ∧ c2 )The obtained algorithm is O(C 2 n) algorithm, where n is the number of
items.

5.6

0-1 Multiple Knapsack Problem

Here we consider the 0-1 multiple knapsack problem, a variant of knapsack problem. In this problem, there are m bags whose capacities are
k1 , k2 , . . . , km . Each item xi is given value vi and weight wi for i = 1, . . . , n.
Required is to ﬁnd a feasible assignment of items to bags that maximizes thesum of values of selected items. Here, an item can be assigned to no bag.
An assignment is feasible when sum of weight of items in each bag does notexceed the given capacity ki for i = 1, . . . , m. This problem can be speciﬁed
as a maximum multi-marking problem. We assume that weight of items areintegers.

5.6.1

Speciﬁcation

We express items using a list, as we did in the ordinary knapsack problem.
Property p can be deﬁned as follows:57

p xs = ∧ (p1 xs, p2 xs, . . . , pm xs)
pi xs = weightsumi xs ≤ ki (i = 1, . . . , m)
Weight function w can be deﬁned as follows:
w = +/ ◦ map f
where f x = case kind x of
0→0
→ value x
Here, the function value returns the value of the item.

5.6.2

Derivation

We introduce the functions cuti for i = 1, . . . , m and describe the property p
as ﬁnite mutumorphisms.
= ∧ (p1 xs, p2 xs, . . . , pm xs)= sumwi xs ≤ ki (i = 1, . . . , m)
= cuti (case kind x ofi → weight x→ 0) (i = 1, . . . , m)sumwi (x : xs) = cuti (case kind x ofi → weight x→ 0) + sumw xs (i = 1, . . . , m)cuti w= if w ≤ ki then w else ki + 1
p xs
pi xs
sumwi [x]By applying the Theorem, we obtain an O(k1 · k2 · · · km · m · n) algorithm.

5.7

Multidimensional Knapsack Problem

Here we consider the multidimensional knapsack problem, another variantof knapsack problem. In this problem, there are m kinds of resources whose
capacities are c1 , c2 , . . . , cm . Each item xi is given value vi and consumes rij
from ith resource, for i = 1, . . . , m and j = 1, . . . , n. Required is to ﬁnd a
feasible selection of items that maximizes the sum of values of selected items.
Here, a selection is feasible when consumption of each resource does notexceed the given capacity ci for i = 1, . . . , m. This problem can be speciﬁed
as a maximum marking problem. We assume that resource consumptions ofeach item are integers.
58

5.7.1

Speciﬁcation

We express items using a list, as we did in the ordinary knapsack problem.
Property p can be deﬁned as follows:p xs = ∧ (p1 xs, p2 xs, . . . , pm xs)
pi xs = resoucesumi xs ≤ ci (i = 1, . . . , m)
Here the function resoucesumi computes the sum of consumption of ith
resource.
Weight function w can be described as follows:
w = +/ ◦ map f
where f x = case kind x of
1 → value x
2 → 0.
Here, the function value returns the value of the item.

5.7.2

Derivation

In order to describe property p in ﬁnite mutumorphisms, we introduce theauxiliary functions cuti for i = 1, . . . , m and describe the property p as ﬁnite
mutumorphisms.
= ∧ (p1 xs, p2 xs, . . . , pm xs)= sumri xs ≤ ci (i = 1, . . . , m)
= cuti (case kind x of
1 → ri x
2 → 0) (i = 1, . . . , m)sumri (x : xs) = cuti (case kind x of
1 → ri x
2 → 0) + sumr xs (i = 1, . . . , m)cuti r= if r ≤ ci then r else ci + 1
p xs
pi xs
sumri [x]Here, ri takes an item as its argument and returns consumption of ith resource. By applying the Theorem, we obtain an O(c1 · c2 · · · cm · n) algorithm.

59

5.8

Weighted Interval Selection Problem

Given a set of weighted intervals, the weighted interval selection problem
is to select a maximum-weight subset such that any two selected intervals
are disjoint [ES00]. An application of this problem is a scheduling of jobs
whose start and end times are ﬁxed and only one job can be executed at atime. We assume that start and end times are represented by integers. This
assumption is natural in real-world jobs, where we mean that the time unit
is a day or an hour or a minute or a second, and so on.
Suppose the job set is given as a list of jobs in the order of start time,that is, if job A starts earlier than job B, then job A appears earlier thanjob B in the list. We express a job by a 3-tuple of the start time, the time
which it takes, and the weight of the job. Here we express start time by thediﬀerence from the previous job in the job list except for the ﬁrst job. We
express the time of the ﬁrst job as 0. This way of expressing start time is for
applying Theorem 4. For example, the list
jobs = [(0, 3, 2), (2, 4, 3), (3, 2, 5)].
is a job list, and jobs represents three jobs where the second job starts attime 2, and the third job starts at time 5, provided that the ﬁrst job starts attime 0. Feasible solutions are selecting the ﬁrst and the third job or selecting
only one job. So, the maximum solution is selecting the ﬁrst and the third
job. We express a selection by marking 1 to selected jobs and 2 to the others.
For example, maximum solution for jobs is expressed as[((0, 3, 2), 1), ((2, 4, 3), 2), ((3, 2, 5), 1)].
Property p checks that the selected jobs do not overlap each other. So, p canbe deﬁned as follows. The accumulating parameter represents the time thecurrently executed job takes until it ends.
p xs= p0 xs 0
p0 [ ] e= True0p (x : xs) e = case kind x of
1 → if e − s x > 0 then F alse else p0 xs (t x)
2 → if e − s x > 0 then p0 xs (e − s x) else p0 xs 0
Here the function s takes as its argument a job x and returns the start timeof it, that is, the ﬁrst element of the 3-tuple. The function t takes as its
60

argument a job x and returns the time it takes, that is, the second elementof the 3-tuple.
We want to maximize the sum of weight of selected jobs, so we can deﬁne
the weight function w as follows:
w = +/ ◦ map f
where f x = case kind x of
1→wx
2 → 0.
Here the function w takes as its argument a job x and returns the weight ofit, that is, the third element of the 3-tuple.
Now the weighted interval selection problem is written as follows:
mmp w p [True, False].
The weight function w is written in the required form, and the property p
can be easily rewritten into the required form, though we omit the form. By
applying Theorem 4, we obtain O(W n) algorithm, where W is the maximum
length among all jobs, because |Acc| = W + 1, |Class| = 2, and k = 2.

5.9

Mining
Rules

Optimized

Gain

Association

Data mining, which is a technology for obtaining useful knowledge from large
database, has been gradually recognized as an important subject. Algorithms
for data mining have to be eﬃcient, since target database is often huge.
There have been developed many eﬃcient algorithms for various kinds of data
mining problems, among which the problem of mining optimized association
rules has attracted researchers [BRS99, FMMT96a, FMMT96b].
To show concretely the problem of mining optimized association rules,
we consider the following example. Suppose there is a database recording
customers’ transactions in a shop, and we are interested in the association
rules like the following form:(age ∈ [a..b]) ⇒ BuyRibbon
whose conﬁdence exceeds a given threshold θ. There are many rules of theabove form by changing a and b. Among them, we would like to ﬁnd the61range of age that maximizes the gain: {the number of customers who boughtribbon whose age are between a and b} minus {the threshold number, i.e.,θ times the number of customers whose age is between a and b}. Supposethat the shop makes a proﬁt if 100θ% of customers buy ribbon. Then, theoptimized gain range [a..b] is the range of customers that maximizes the
shop’s proﬁt with respect to the section of ribbon.
This is an example of mining optimized gain association rules problem.
This problem is transformed to the problem called maximum segment sum
problem (MSS for short) [FMMT96a], and we have a linear time algorithm[Ben84]. Input of the MSS problem is a number list xs, and output is a consecutive sublist of xs that has the maximum sum among all the consecutive
sublists of xs. For example, in the case of xs = [5, −10, 20, −15, 30, −5], theresult is [20, −15, 30], which has the maximum sum 35.
Rule of the above form may not be satisfactory in some cases. For example, we may hope to ﬁnd up to k ranges of age for the rule∨

( ki=1 age ∈ [ai ..bi ]) ⇒ BuyRibbonthat maximizes the gain. This problem, which is transformed to a k-MSS
problem (Section 5.9.1), is more general and more diﬃcult to be solved efﬁciently. A smart O(kn) algorithm has been proposed in [BRS99], but its
correctness is not easy to verify. Furthermore, it is diﬃcult to adapt the algorithm even for a simple modiﬁcation. For instance, we may want to compute
up to k ranges such that the length of each range is between 5 and 10.
In this section, we show that an eﬃcient linear time algorithm for mining optimized gain association rules is systematically derived from a simple
speciﬁcation [SHTO01b]. Our approach not only automatically guarantee
the correctness of the derived algorithm, but also is easy to derive new algorithms for modiﬁcation of the problem.

5.9.1

The Problem of Mining Optimized Gain Association Rules

In this section, we show the problem of mining optimized gain association
rules [BRS99] can be transformed to the k-MSS problem.
Recall the problem in Chapter 1. Input database is a set of tuples, eachof which holds information about a customer, including an integer value thatindicates the age of the customer and a boolean value that indicates whether
or not the customer bought ribbon.
62

Table 5.1: Record of customers
age of customers
number of customers (u)number of customers who buy ribbon (v)
v−θ×u

15 16
200 300
45 50
5
-10

17
250
70
20

18
400
65
-15

19
100
50
30

20
100
15
-5

From the input database, we would like to mine a rule Rribbon of thefollowing form:(age ∈ [a..b]) ⇒ BuyRibbon.
This rule means that a customer of age between a and b often buys ribbon
in a conﬁdence no less than θ. There are many rules of the above form bychanging a and b. Among them, we would like to ﬁnd one that maximizes
the gain of the rule Rribbon :gain(Rribbon ) = sup(age ∈ [a..b] ∧ BuyRibbon)− θ × sup(age ∈ [a..b]).
For a condition C, sup(C) is deﬁned as the number of tuples that satisfy thecondition C in the database. Intuitively, this gain shows to what extent the
number of tuples establishing the rule Rribbon exceeds what is expected withrespect to the least conﬁdence θ.
As an assumption for an eﬃcient algorithm, input tuples are sorted according to customers’ age1 . Then, for each set of tuples that belong to thesame age, we compute g = v − θ × u, where u is the number of customers
and v is the number of customers who bought ribbon. As a result, a list gs
of values of g = v − θ × u is obtained. For example, suppose that recordof customers is as in Table 5.1, which is obtained after the sorting process,with θ = 0.2. For this example, gs = [5, −10, 20, −15, 30, −5]. The solution of the MSS problem for the list gs gives the solution of the original
problem [FMMT96a]. In this example, the solution of the MSS problem is[20, −15, 30], so the corresponding range of age [17..19] is the optimized gain
range. Generally, the problem of mining optimized gain association rules canbe transformed to the MSS problem [FMMT96a].
1

The same is assumed also in [BRS99, FMMT96a].

63

In similar way, the optimized gain problem that allows up to k ranges
can be transformed to the k-MSS problem. For details, refer to [BRS99,
FMMT96a].
Here, we formally deﬁne the k-MSS problem.
Deﬁnition 5 (k-MSS problem) Input of the k-MSS is a list xs of numbers, and output is up to k consecutive sublists of xs that have the maximum
sum among all the up to k consecutive sublists of xs.
For this problem, O(kn) algorithm was proposed in [BRS99], which will
be explained in the next section.

RemarkSince the numeric attribute can have real numbers, input tuples are usuallyclassiﬁed into the small number of buckets ordered with respect to the numeric attribute. This process is called bucketing [FMMT96a, FMMT96b].
After the bucketing, ﬁnd a rule considering only ranges consisting of consecutive buckets. Generally, this means that obtained rules are approximate
rules. The bucketing process takes O(n log m) time where n is the numberof tuples in database and m is the number of buckets [FMMT96b].

5.9.2

Constructing k-MSS Algorithm Manually

In this section, we explain the algorithm for k-MSS developed in [BRS99].
The algorithm is a k-path algorithm, at the i-th path of which a solution of
i-MSS is obtained.
• i = 1: At the ﬁrst path, solve 1-MSS as in [Ben84].
• i > 1: Let the solution of the (i − 1)-MSS be s1 , s2 , . . . , si and theremaining sublists be t1 , t2 , . . . , tj . Solve 1-MSS for t1 , t2 , . . . , tj and let
one that has the maximum solution be tmax . Solve 1-minimum segment
sum problem for s1 , s2 , . . . , si and let one that has the minimum solution
be smin . If the segment sum of tmax plus the segment sum of smin is lessthan 0, then split smin into three subintervals with the solution of smin
as the middle interval and delete smin from the solution of (i − 1)-MSS
and add the ﬁrst and third intervals to it, which gives the solution of
i-MSS. Otherwise, split tmax into three subintervals with the solution of64

tmax as the middle interval and add the solution of tmax to the solutionof (i − 1)-MSS, which gives the solution of i-MSS.
This algorithm iterates k times the process of ﬁnding the most eﬀective
sublist and splitting it, and its complexity is O(kn) [BRS99].
For
example,consider2-MSS
problem
for
input
list
[5, −10, 20, −15, 30, −5]. At the ﬁrst path, solve 1-MSS. As a result, thesublist [20, −15, 30] is obtained. At the second path, let s1 = [20, −15, 30],
t1 = [5, −10], and t2 = [−5]. In this case, we split s1 to [20], [−15], [30] andget the result [20], [30].
This algorithm is smart, but its correctness is not so obvious. In fact, verifying this algorithm needs careful consideration [BRS99]. On the contrary,
we will derive O(kn) algorithm from simple speciﬁcation, and the correctness
is automatically guaranteed.

5.9.3

Deriving k-MSS Algorithm AutomaticallyIn this section, we derive an O(kn) algorithm for the k-MSS problem by specifying it as a maximum marking problem and applying the theorem proposedin [SHT01].

5.9.4

Speciﬁcation

We specify this problem as a maximum marking problem: marking up theelements of a data structure with ﬁnite kinds of marks such that the marked
elements meet certain property p and has the maximum value with respect
to certain weight function w. First, we determine what kind of marks weuse. We use the marks True and False, and we attach the mark True to theelements that are selected as part of sublists and the mark False to the others.
Second, we describe property p. Property p checks whether the number ofsublists does not exceed the given k. This can be written as follows:

65

p xs
= p0 xs (False, k)0p [ ] (m, e)= True0p (x : xs) (m, e) = case m ofTrue → case kind x ofTrue → p0 xs (True, e)
False → p0 xs (False, e)
False → case kind x ofTrue → if e > 0 thenp0 xs (True, e − 1)else False
False → p0 xs (False, e).
The function kind is deﬁned as follows:
kind (x, m) = m.
Finally, we write the weight function w. The function w can be written
as follows:
w xs = sum (map f xs)
where
f x = case kind x ofTrue → w x
False → 0
The function w is deﬁned by w (y, m) = y.
Now we can describe the problem as a maximum marking problem asfollows:
mmp w p [True, False]
The function mmp generates all the possible 2n marked lists, and fromthose which satisfy the property p selects one that has the maximum value
with respect to w. For detail, refer to [SHT01].

5.9.5

Derivation

By Theorem 4, the derivation of a linear time algorithm is straight forward.
We omit the process of transforming p and w to the required form, but show

66

only the ﬁnal result.
optacc (f, +, 0) accept φ1 φ2 δ [True, False]
where
accept (c, e) = c ∧ e == (False, k)
f x = case kind x ofTrue → w x
False → 0
φ1 (m, e) = True
φ2 x (m, e) r =case m ofTrue → r
False → case kind x ofTrue → if e > 0 then relse False
False → r
δ x (m, e) =case m ofTrue → case kind x ofTrue → (True, e)
False → (False, e)
False → case kind x ofTrue → (True, e − 1)
False → (False, e)
The deﬁnition of the function optacc is given in Figure 4.3. The complexity
is O(kn) where n is the length of the list. Algorithm obtained by derivation
does not need veriﬁcation, which is an important beneﬁt of deriving eﬃcientalgorithm from speciﬁcation.

5.9.6

Comparison

Here we compare the algorithm above with the algorithm developed manually in [BRS99] (See Section 5.9.2). The derived algorithm is a dynamic
programming algorithm and recursive on the input list. In each step it generates 2k candidate solutions, where 2 corresponds to whether the current
head element is selected or not, and k corresponds to the number of sublists in the current list. So, the derived algorithm performs O(k) operations
67

n times. On the contrary, the algorithm in Section 5.9.2 is a greedy algorithm, which generates only one candidate in each step. But in each step,O(n) operations are performed. So, the algorithm in Section 5.9.2 performs
O(n) operations k times. So, though order of complexity is same, these twoalgorithms are essentially diﬀerent.

5.9.7

Dealing with Change of Speciﬁcation

Here, consider the modiﬁed k-MSS problem with the condition that thelength of each sublist must be between 5 and 10. It is not so easy to adapt
the algorithm in Section 5.9.2 to this modiﬁed problem. However, by our
method, the only thing we have to do is to change the property p as follows:p xs = p0 xs (2, k) ∧ q xs
The property q checks whether all the selected sublists have length between
5 and 10, which is deﬁned as follows:= q 0 xs (2, 0)= if m == 1 then5 ≤ e ∧ e ≤ 10
else Trueq 0 (x : xs) (m, e) = if kind x == 1 thenq 0 xs (1, e + 1)
else
if m == 1 then 5 ≤ e ∧ e ≤ 10
else True
q xs
q 0 [ ] (m, e)

Similarly to Section 5.9.5, we obtain an O(kn) algorithm for the modiﬁedproblem.

5.9.8

Remarks

In this section we show that a linear time algorithm for mining optimized
gain association rules is derived from simple speciﬁcation by reducing it to a
maximum marking problem. Although a smart O(kn) algorithm is presented
in [BRS99], its correctness is not easy to verify. Moreover, the algorithm isfragile to modiﬁcations of problems. On the contrary, by our method, we cansystematically derive an O(kn) algorithm, and its correctness is automatically guaranteed.
68By our previous method in [SHTO00], we can also derive a linear timealgorithm for the same problems. However, since its speciﬁcation does notallow accumulating parameters, the constant of the algorithm grows exponentially and the resulting complexity becomes O(2k n).

5.10

FeaturesIn this section we highlight several important features of our calculational approach for solving the maximum marking problems: its simplicity, generality,and ﬂexibility.

5.10.1

Simplicity

First, as seen in the derivation of a linear-time algorithm for solving the party
planning problem as well as seen in Section 1.7, our calculation is surprisingly simple. With the optimization theorem, all we need to do is derive amutumorphic form of the property description. Fortunately, there are a lotof handy calculation strategies for deriving mutumorphisms [HITT97], suchas generalization of subexpressions to functions and fusion transformation[Jeu93, BdM96].
In the following we shall further illustrate this simplicity by solving two
problems inspired by the party planning problem mentioned in the Introduction, whose derivation of linear algorithms are indeed not so straightforward
for even an experienced functional programmer.
Group Organizing Problem
The inputs in the group organizing problem are trees, and we use the samedata structure Org α that we used for the party planning problem. The
property p on the marked tree for this problem is that one of the ancestor
nodes of any two marked nodes must be marked. This can be described69

recursively by
p :: Org α∗ → Boolp (Leader v [ ]) = Truep (Leader v (t : ts)) =if marked v then Trueelse if nm t then p (Leader v ts)
else p t ∧ nm (Leader v ts).
The ﬁrst equation means that a single-node tree always satisﬁes p. The
second equation means that for a tree with the root v, if the root is marked,
then any way of marking the nodes of its subtrees is acceptable. Otherwise,
we have to check each of the subtrees to make sure that at most a single
subtree has marked nodes. The function nm t checks that the tree t has nomarked nodes; it is deﬁned as follows:
nm (Leader v [ ])= not (marked v)
nm (Leader v (t : ts)) = nm t ∧ nm (Leader v ts)
Using the calculational strategy described in Section 4.6, we can turn thesefunctions into the following mutumorphisms on Rtree α, which consist of
only property descriptions, and thus can obtain a linear-time algorithm forthe group organizing problem.
p0
p0 (Root v)
p0 (Join t1 t2 ):: RTree α∗ → Bool
= True= if lm0 t2 then Trueelse if nm0 t1 then p0 t2else p0 t1 ∧ nm0 t2

nm0 (Root v)= not (marked v)
0
nm (Join t1 t2 ) = nm0 t1 ∧ nm0 t2

70

Supervisor Chaining Problem
Similarly, for the supervisor chaining problem we can specify the property
that the marked nodes form a path chain as follows.
p :: Org α∗ → Boolp (Leader v [ ]) = Truep (Leader v (t : ts)) =if marked v then
if nm t then p (Leader v ts)
else marked (getLeader t) ∧ p t ∧ol (Leader v ts)
else if nm t then p (Leader v ts)
else p t ∧ nm (Leader v ts)
The function ol t checks that the leader of the tree t is marked and the othernodes of t are not marked.
ol (Leader v [ ])= marked vol (Leader v (t : ts)) = nm t ∧ ol (Leader v ts)
This property p can be expressed using the following mutumorphisms which
consist of only property descriptions.
p0
p0 (Root v)
p0 (Join t1 t2 ):: RTree α∗ → Bool
= True= if lm0 t2 then
if nm0 t1 then p0 t2else lm0 t1 ∧ p0 t1 ∧ ol0 t2else if nm0 t1 then p0 t2else p0 t1 ∧ nm0 t2

ol0 (Root v)= marked v
0ol (Join t1 t2) = nm0 t1 ∧ ol0 t2
Now we can use our optimization theorem, as we did for the partying planningproblem, to obtain a linear-time algorithm that solves the supervisor chaining
problem.

71

e1

e2
e1

e

u

w

w

u

u
v
Base graph

e1

e2
w

w

w
v

v

e2

e1
e3

e3
u

u

e2

v

v

u

v

Parallel operation

Series operation

Figure 5.1: Operations of series-parallel graphs.

5.10.2

Generality

Our approach is general (polytypic) enough to deal with maximum marking
problems on data structures that are not lists or trees. To illustrate this,we derive a linear-time algorithm solving the maximum two disjoint paths
problem on series-parallel graphs [TNS82].
The series-parallel graph is deﬁned as follows:
SPG ::= Base (Vert, Vert, Edge)|
Series SPG SPG|
Parallel SPG SPG
Here Vert represents the type of vertices and Edge represents the type ofedges. Every graph should have a single source and a single sink. The twodata constructors are Series and Parallel. Series g1 g2 makes sense only when
the sink of g1 is the source of g2 , and Parallel g1 g2 makes sense only when
g1 and g2 share a source and a sink.
Figure 5.1 shows the meaning of the constructors. For example, themiddle graph in Figure 5.1 is represented by
g = Series (Base (u, w, e1)) (Base (w, v, e2)).
The maximum two disjoint paths problem is deﬁned as follows: when given
two vertices s and t, ﬁnd two disjoint paths between the two vertices s, t suchthat the sum of the edge weights is maximum. Since the two disjoint paths
between the vertices s and t can be seen as a cycle containing the vertices sand t, we can specify the property p of the problem byp:: Vert → Vert → SPG → Boolp s t g = cycle g ∧ th s g ∧ th t g.
Here cycle judges whether the marked edges in the graph form a cycle, andth v judges whether there is a marked edge incident to the vertex v. These72

two functions can be deﬁned as follows:cycle (Base e)= not (marked e)
cycle (Series g1 g2 )= (cycle g1 ∧ nm g2 ) ∨(nm g1 ∧ cycle g2 )cycle (Parallel g1 g2 ) = (cycle g1 ∧ nm g2 ) ∨(nm g1 ∧ cycle g2 ) ∨(span g1 ∧ span g2 )th v g= anyMarked (inc v g)

The function span judges whether the marked edges in the graph span between the source and sink of the graph, nm judges whether or not there aremarked edges in the graph, anyMarked takes as its argument a list of edges es
and judges whether or not there is a marked edge in es, and inc v g gathers
all the edges of g which are incident to the vertex v.
span (Base e)
span (Series g1 g2 )span (Parallel g1 g2 )= marked e= span g1 ∧ span g2= (span g1 ∧ nm g2 ) ∨(nm g1 ∧ span g2 )nm (Base e)
nm (Series g1 g2 )nm (Parallel g1 g2 )= not (marked e)= nm g1 ∧ nm g2= nm g1 ∧ nm g2

inc v (Base e@(v1 , v2 , )) = if v == v1 ∨ v == v2
then [e] else [ ]inc v (Series g1 g2 )= inc v g1 ++ inc v g2
inc v (Parallel g1 g2 )= inc v g1 ++ inc v g2
By fusion calculation, we can get the following eﬃcient recursive deﬁnition
for th.
th v (Base e@(v1 , v2 , )) = if v == v1 ∨ v == v2
then marked e else Falseth v (Series g1 g2 )= th v g1 ∨ th v g2th v (Parallel g1 g2 )= th v g1 ∨ th v g2
Now the property description p s t is represented as mutumorphisms withproperty descriptions cycle, span, nm, th s, and th t. It follows from our
optimization theorem that a practical linear-time algorithm can be obtained.
73

5.10.3

Flexibility

Here we explain ﬂexibility of our derivation in coping with modiﬁcation of thespeciﬁcations of problems. We choose as our example the maximum segment
sum problem, which is to compute the maximum of the sums of all segments(contiguous sublist) of a list. This is a quite well-known problem in the
program calculation community [Bir89]. In the following we will not only givea new solution to it but will also demonstrate that we can straightforwardly
solve a set of related problems that would not be easily solved by using thepreviously available approaches.
The maximum segment sum problem is actually a maximum marking
problem where the property is that all marked elements in a list should be
adjacent (connected). This property can be speciﬁed as follows:conn [x]= Trueconn (x : xs) = if marked x then
nm xs ∨
(marked (hd xs) ∧ conn xs)
else conn xs
If the list contains only a single element, then the property is satisﬁed. Otherwise, if the head is marked, then either none of the other elements aremarked or all marked elements are connected to the head. If the head is notmarked, the remaining list is checked recursively. As before, the function nm
judges whether or not any of the elements are marked.
nm [x]= not (marked x)
nm (x : xs) = not (marked x) ∧ nm xs
To transform conn into mutumorphisms which consist only of property descriptions, we generalize the part marked (hd xs) and let it be mh xs.
mh xs = marked (hd xs)
By a simple fusion calculation, we can easily get the following deﬁnition ofmh.
mh [x]= marked x
mh (x : xs) = marked x

74

So we have obtained the following mutumorphisms which consist only of
property descriptions.
conn [x]= Trueconn (x : xs) = if marked x then
nm xs ∨ (mh xs ∧ conn xs)
else conn xs
Application of the optimization theorem gives us a linear-time algorithm.
Although our linear algorithm may use a few more operations than that
described by Bird [Bir89], it is much easier to derive.
Now consider an extension of the maximum segment sum problem where
we are interested only in those segments containing only even numbers. The
property for this extended problem isp xs = conn xs ∧ evens xs
where evens can be deﬁned byevens [x]= if marked x then even (weight x)
else True
evens (x : xs) = if marked x theneven (weight x) ∧ evens xs
else evens xs
It is easy to see that p can be deﬁned as mutumorphisms with property
descriptions conn, evens, nm, and mh, and thus that we obtain a linear
algorithm for solving this extended problem.
Following this line, we can consider many similar segment problems. We
can, for example, consider maximum sums of segments that have even numbers of elements by deﬁning the following property
p xs = conn xs ∧ even (mnum xs),
where mnum xs is the number of marked elements in xs. To get mutumorphisms which consist only of property descriptions, we generalize the parteven (mnum xs) and let it be em xs.
em xs = even (mnum xs)

75After deriving a recursive form for em by using calculations similar to thosedescribed above, we can apply the optimization theorem to get a lineartime algorithm. It should be noted that deriving a linear-time algorithm forthis problem requires some creativity when using the approach described in[Bir89, Jeu93] because the property p is not preﬁx-closed. This makes ﬁlter
promotion diﬃcult.
Finally, we mention that maximum segment sum problem can be generalized to trees: a segment in a list is simply generalized to a set of connected
nodes in a tree. It should be easy for reader to derive a linear-time algorithm
to solve this generalized problem.

76

Chapter 6
Automatic Generation ofEﬃcient Programs
In previous chapters, we show that by our proposing method eﬃcient linear
time algorithms for MMP can be derived mechanically. We have showedthat our method is quite general and powerful. In this chapter, we show that
our method can be implemented as a generation system to automaticallygenerate eﬃcient linear time algorithms for MMP from simple speciﬁcations.
It was known that generation of linear time algorithms for MMP (precisely
maximum weightsum problem) can be done by the method proposed by Borieet al., [BPT92]. Though his method is theoretically appealing, it generates aprohibitively large table (see Section 3.3 and Chapter 7 for details) and thus
cannot be put to practical use. For each individual problems, a practicallinear time algorithm can be derived by calculation. For example, for a
famous instance of MMP, the maximum segment sum problem, a practicallinear time algorithm derivation was known [Bir89]. But any method forautomatically deriving practical linear time algorithms has not been known
for MMP. Our method we propose in this thesis enables it. We implement our
proposing method and show that it generates practical linear time algorithms
by several examples [YSHT01].

6.1

MAG system

Before we show our implementation, we show that our method can be implemented using an existing transformation system called MAG [dMS98].
77

Though by using MAG system one can automatically generate eﬃcient algorithms for MMP, one cannot specify the transformation strategy, which israther inconvenient for describing transformation. So in the next section we
implement a ﬂexible system for MMP.

6.1.1

Implementation

Our generation rule can be implemented, so that eﬃcient programs can begenerated automatically. In this section, we highlight how we can do so using
MAG system [dMS98], a transformation system with a powerful higher orderpattern matching.
As seen in Figure 4.4, our obtained program can be divided into two parts:
the dynamic and static parts. The dynamic part changes from problems toproblems, while the static part remains the same. In Figure 4.4, the upper
part is dynamic and the lower is static. We show how to generate the dynamic
part from the speciﬁcation mmp w p ms.
Using MAG, we may code the generation of the dynamic part from speciﬁcation mmp w p ms as a rule called mmpRule and a rule called fusion as
follows:
mmpRule: mmp wfun p ms
= optacc (fun,oplus,e) (\(c,e) -> c && e==e0)
phi1 phi2 delta ms,
if {wfun = \xs -> foldr oplus e (map fun xs);p = \xs -> foldrh (phi1, phi2) delta xs e0};
fusion: f (foldr step e xs) = foldrh (phi1’, phi2’)
delta xs,
if {f e = phi1’;\ y ys acc -> f (step y ys) acc =\ y ys acc -> phi2’ y acc(f ys (delta y acc))}Now for the coloring problem, we can apply this rule to the following
speciﬁcation and obtain a linear time program like in Figure 4.4 automatically.
coloring: coloring = mmp wf indep [1,2,3];78

wf: wf xs = (foldr (+) 0 (map w xs));
w: w x = if kind x == 1 then weight x
else if kind x == 2 then (-1) * (weight x)
else 0;indep: indep xs = indep’ (foldr (:) [] xs) 0;
indep’1: indep’ [] color = True;
indep’2: indep’ (x:xs) color = kind x /= color &&indep’ xs (kind x);classlist: classlist = [False,True];
acclist: acclist = [0..3]With these, the MAG system can produce the linear time program asgiven in Figure 4.4. The above corresponds to Theorem 4. In the following,
we show the case for Theorem 3 using the maximum independent-sublist sum
problem. The rule that corresponds to Theorem 3 can be coded as follows:
mmpRule: mmp wfun p ms
= opt (fun, oplus, e) accept phi1 phi2 ms,
if {wfun = \ xs -> foldr oplus e (map fun xs);p = \ ys -> accept (foldr phi2 phi1 ys)};
split2: split2 f1 f2 x = (f1 x, f2 x);
uncurry2: uncurry2 e = \ x (a1, a2) -> e x a1 a2;tupling2: split2 f1 f2 (foldr (:) [] xs)= foldr (uncurry2 g) c xs,
if {split2 f1 f2 [] = c;
\ x xs -> split2 f1 f2 (x:xs) =\ x xs -> g x (f1 xs) (f2 xs)}
Now for the mis problem, we can apply this rule to the following speciﬁcation and obtain a linear time program like in Figure 1.1 automatically.
mis: mis = mmp w ind [True, False];
w: w = (foldr (+) 0) . map (\ (x,m) -> if m then x else 0);
ind: ind = (\(a1,a2) -> a1) .
split2 ind0 ind1 . foldr (:) [];ind01: ind0 [] = True;79ind02: ind0 (x:xs) = if marked x then ind1 xs
else ind0 xs;
ind11: ind1 [] = True;
ind12: ind1 (x:xs) = if marked x then False
else ind0 xs
As seen above, we can implement our proposing method using MAG,but the current version of the MAG system has several restrictions such as
not allowing case expression. Moreover, the ordering of rules aﬀects thederivation. So we make a system by extending the MAG system, which wename ”Yicho System”.

6.2

Yicho System

In this section we implement a system for generating eﬃcient linear timealgorithms for MMP, which enables ﬂexible description of transformation.
We would like to use a language for describing rules and strategy of generation. Generally speaking, ﬁrstly an eﬀective generation rule is a rule whichis general enough to be able to match many program pattern. Secondly aneﬀective generation rule is constructive and can be applied in practical time.
For example, the rule ”if there exist two natural numbers p, q that satisﬁes
n = p × q, then rewrite n into p × q” is not constructive. By using a languagefor describing transformation strategy, one can specify how to apply transformation rules [HT99, TH00, Vis01]．Though there exist systems which does
not have such language to describe strategy like MAG system [dMS98]，it
becomes diﬃcult to perform derivation as user intended. So a language fordescribing strategy is desired.
In the following, we propose a language for describing transformation
strategy for generating practical linear time algorithms for MMP and implement it. The system has the following features.
• Our transformation rule is general enough to be applied to MMP andthus it can be applied to many problems. It is constructive and can beeasily implemented.
• We use a meta language, called ”calculation carrying program (CCP
for short)” [TH00], for describing transformation strategy. Previously
available transformation description languages [Vis01] have only ﬁrst
80

order matching and thus restrict the rules which can be directly described. In constrast, CCP has higher order matching, it enlarge therules which can be directly described. Another feature of CCP is description about control of transformation. For example, it is possible
to apply rules when certain condition satisﬁed, to repeat application ofsome rule, or to use some strategy in another strategy. Description ofstrategy in intuitive form is one reason for CCP to be appropriate todescribe strategy.
• In our system, one can compile CCP to script, which is an intermediate language in our system. Environment to excute obtained script isavailable, which makes it easy to debug.

6.2.1

Structure of automatic generation system

In this section, we show a structure and implementration of the automatic
generation system for MMP, which is implemented using a functional programming language Haskell [PJH99, Bir98].
Structure of the system
The system consists of two layers. The above layer is for high level descriptionof transformation strategy, which is described by a language based on CCP[TH00] (Section 6.2.2). CCP has higher order matching, so it is possible
to describe a wide range of transformation rules. The lower layer is fordescription of transformation steps, which is described by a script language.
After checking the syntax and type of CCP, CCP is transformed into thescript language (Section 6.2.3).
CCP is approprite to describe high level transformation, so a stragegy
described in CCP can be reused for several programs by no chage or smallchange. Script is for low level transformation, so it can be reused for exactly
same structure programs.
Lower level provides an interactive environment, which is for step by step
excution, undo of a transfomation, showing bindings of variables, showing
rules that can be applied to the current expression, and so on (Section 6.2.2)．
CCP and script language is independent, so, it is possible to use a scriptthat is output of some other system.

816.2.2

Calculation Carrying Program (CCP)

CCP is a program accompanied by calculation rules [HT99]. Program calculation is transforming program to eﬃcient one by applying calculation rules.
Generally speaking, program calculation is done by hand and calculation
rules and how to apply them varies according to object program. Whencalculating programs on a computer, how to calculate should be written insome way. CCP gives one way for that. CCP is a program accompanied by
calculation rules and how to apply them, so programmer can specify how to
calculate eﬃcient programs. General rules such as fusion rule or tupling ruleare reusable once it is written. Furthermore, CCP has higher order matching,so it is possible to describe calculations directly.
An Example — sumsq
Here, we show what is CCP by using a problem to get sum of square of listof numbers. This problem can be solved by squaring each element and thensumming up. By letting the square function be sq and the sum function besum,
sumsq = sum ◦ map sq
gives one solution to this problem. This generates an intermediate list whichis the result of map sq, but it is possible to describe it not to generate thisintermediate list. We would like to transform the above function sumsq to
one which does not generate this intermediate list. This can be done by thefusion transformation.
Theorem 5 (Fusion Rule) If for any a, x
g a (f x) = f (step a x)
holds, thenf ◦ foldr step e = foldr g (f e)2holds.

The function foldr is a list folding function, which is deﬁned as follows:
foldr step e [ ] = efoldr step e (x : xs) = step x (foldr step e xs)
82In order to apply this fusion theorem, we change map sq into the form offoldr step e.
map sq = foldr step [ ]where step y ys = (sq y) : ys
Next, we should ﬁnd function g that satisﬁes the following equation:g y (sum ys) = sum (step y ys)
The following function g satisﬁes this equation.
g y s = sq y + s
Since sum [ ] = 0, by applying the fusion theorem, we getsum ◦ map sq = foldr g 0
This function foldr g 0 does not produce an intermediate list when computing
square sum, so eﬃciency is improved by this transformation.
When doing this kind of calculation on a computer, we should describe
how to calculate in some way. CCP gives one way of describing it. In CCP,
we accompany object program with calculation. For example, CCP for thesumsq problem is written as in Figure 6.1.
CCP can be divided into three parts. In Figure 6.1, the ﬁrst part isobject program, the second part is calculation rules, (fusion, applyFusion)，and the last part is to specify how an eﬃcient function sumsqOpt should beobtained from the object program sumsq.
The ﬁrst part is the speciﬁcation of the sumsq problem. Though thisspeciﬁcation generates an intermediate list when computing square sum, we
can transform it to eﬃcient one that does not generates the intermediate list.
The second part describe this transformation process. The rule <fusion> is
an implementation of the fusion theorem (Theorem 5). When applying thefusion rule, the right function g in the function composition f . g should
be described in the form foldr step e. For that purpose, we deﬁne thecalculation rule applyFusion.
In the rule applyFusion, the right most function in the given function
composition is rewrited into the form foldr step e by fusing with identity
function foldr (:) [] and then the fusion rule <fusion> is applied successively. By applying this calculation rule applyFusion to the expression
sum . map sq, we get the form that does not generate an intermediate list.
83

-------------- Object Program ----------------sumsq = sum . map sq;
sum [] = 0;sum (_x:_xs) = _x + sum _xs;
sq _x = _x * _x;
map _f [] = [];map _f (_x:_xs) = f _x : map _f _xs;
foldr _step _e [] = _e;foldr _step _e (_a:_x) = _step _a (foldr _step _e _x);(_f . _g) _x = _f (_g _x);-------------- Calculation Rules ----------------<fusion> _f (foldr _step _e _xs) =letm _g a (_f x) = _f (_step a x);_c = _f _e
in foldr _g _c _xs;
<applyFusion> (_f . _g) = <fusion> (_f . <applyFusion> _g);<applyFusion> _f = <fusion> (_f . foldr (:) []);-------------- Application of Calculation Rule ----------------sumsqOpt = <applyFusion> (<unfold> sumsq)

Figure 6.1: An Example of CCP — sumsq

84

The last part describes that. First the deﬁnition of sumsq is unfolded by therule <unfold> and then applyFusion is applied to that. As a result, thefunction sumsqOpt which does not generate an intermediate list is obtained.
The rule <unfold> is a built-in calculation rule that unfolds a deﬁnition offunction.
In CCP, one can describe function deﬁnitions and calculation rule deﬁnitions together. We distinguish function from rule by surrounding the nameof calculation rule. Furthermore, in a deﬁnition of calculation rule, anothercalculation rule or itself can be called. Allowing this kind of description enables it to describe complex calculation rule by combining basic calculation
rules as seen in the rule <applyFusion>.
In CCP, the name of pattern variables starts by _ in order to distinguishthem from local variables. For example, in the matching of letm expression_g a (_f x) = _f (_step a x)
a and x does not start with _, which means that these are not patternvariables but local variables. The locality means that the equation_g a (_f x) = _f (_step a x)
holds for any _a and _x with appropriate types.
The language for describing CCP
We deﬁne the language for describing CCP as in Figure 6.2.
In CCP, we can describe function deﬁnitions (funDef) and rule deﬁnitions (ruleDef) together. We can also use, in an expression, rule applications, meta lambda abstractions, meta let expressions, meta case expressions
where higher order pattern matching [dMS99] is performed. When patternmatching is performed, substitutions for pattern variables are obtained. We
deﬁne the meaning of expressions including higher order pattern matchingas follows:• Meta let Expression
letm ep1 = eb1 ; . . . ; epn = ebn in e
Obtain substitutions for pattern variables in expressions ep1 , ldots, epn
by a higher order pattern matching algorithm [dMS99], evaluate the expression e with the obtained substitutions, and ﬁnally let the obtained
value of e as the value of the whole meta let expression.
85

CCP:
ccp ::= def1 ; . . . ; defn Deﬁnitions
Deﬁnition:
def ::= funDef Function Deﬁnition|
ruleDef Rule Deﬁnition
Function Deﬁnition:
funDef ::= f pats = e Function Deﬁnition
Rule Deﬁnition:
ruleDef ::= hri ep = eb Rule Deﬁnition
Expression:e ::= haskellExp
Expression of Haskell|emExpression including higher order pattern matching
Expression including higher order pattern matching:em ::= letm ep1 = eb1 ; . . . ; epn = ebn in e
Meta let Expression|
casem e of ep1 → e1 ; . . . ; epn → en Meta case Expression|
hri eRule Application
Figure 6.2: Deﬁnition of CCP

86• Meta case Expression
casem e of ep1 → e1 ; . . . ; epn → en
Perform higher order pattern matching with respect to the expression ewith the expressions ep1 , . . . , epn using the higher order pattern matching algorithm [dMS99]. Obtain substitutions for the expression epi thatis the ﬁrst expression to succeed in matching, evaluate the expression
ei with the obtained substitutions, and ﬁnally let the obtained value ofei as the value of the whole meta case expression.
• Rule Application hri e
Apply the rule r to the expression e. When the rule r is deﬁned as
hri ep = eb
perform higher order pattern matching with respect to the expression
e with the expression ep using the higher order pattern matching algorithm [dMS99] to obtain substitutions for pattern variables in ep ,evaluate the expression eb with the obtained substitutions, and ﬁnally
let the obtained value of eb as the value of the whole rule application
expression.
In the deﬁnition of CCP, haskellExp represents expressions of the functional language Haskell [PJH99, Bir98], we implement part of them in thecurrent version of the system. We adopt that the name of a pattern variable
starts with underscore and the one of the other kind of variables does notstart with . This distinction is for distinguish local variables from patternvariables in letm expressions.
scriptWe deﬁne the syntax of script as in Figure 6.3. Script is a description oftransformation steps. By using script, we can execute transformation interactively for debugging. Script is divided into three parts, commands forsetting environment, commands for doing transformation, and commands fordebugging.
There are four kinds of commands for setting environment. Command
setPath is for specifying path for the ﬁle of CCP. Command loadTheory is forloading rules. Command setExp sets an expression as starting expression.

87

Script
Command ::= EnvComm
Command for setting environment|
IntCommCommand for doing transformation|
DebugComm Command for debugging
Command for setting environment
EnvComm ::= setPath PathName
Specifying path of ﬁle of ccp|
loadTheory TheoName Loading transformation rules|
setExp ExpName
Setting starting expression
Command for doing transformation
IntComm ::=
|
|
|
|
Path
::=
Loc
::=
|
|

step LawName Pathrule application
beginDerivation LawName Path starting local derivation
match
obtaining substitution by pattern matching
endDerivation
ending local derivation
createRule RuleNamecreating a new rule
Loc1 Loc2 · · ·path for subexpression
Bbody of a λ expression
Ffunction part of function application
A
argument part of function application

Command for debugging
DebugComm ::=
|
|
|
|
|
|
|

help
displaying help
showDerivation showing derivation up to the present
quit
quitting
showBindings showing bindings of local variables
showStack showing all the local derivations
undo undoing a transformation
showSubExpressions showing all the subexpressions
showTheory showing all the rules

Figure 6.3: The syntax of script

88Commands for doing transformation are divided into ﬁve kinds. Command step takes a rule and location of subexpression in the current expression and applies the rule to the subexpression indicated by the location.
Location of a subexpression is written by a sequence of B or F or A where B
represents body of lambda expression, F represents function part of function
application, and A represents argument part of function application.
Command beginDerivation takes a rule and location of subexpression
and starts sub-derivation. Command match match the pattern of conditionand current expression, and memorize the obtained substitution. Command
endDerivation ends the sub-derivation and substitute the pattern variablesin the right hand side of the rule using the obtained substitutions in the
sub-derivation, and substitute the subexpression with the right hand side of
the rule substituted.
Command createRule adds a rule that transforms the starting expression
to the current expression with a speciﬁed rule name.
Commands for debugging are used when debugging. Command help
displays commands currently executable. Command showDerivation displays the derivation up to the present. Command quit quits the session
even if there are commands not executed yet below the command. Command showBindings displays local variables in the current expression. Command showStack displays several informations before entering the current
sub-derivation and the current sub-derivation. Command undo undo one
step. Command showSubExpressions displays all the subexpressions of thecurrent expression. Command showTheory displays all the rules that can beapplied.
Here we show an example of script, which is for improving eﬃciency of afunction sumsq that computes sum of square of each elements. The script isshown in Figure 6.4. A number and a colon at the head of each line is notincluded in the script, only for explanation. In the ﬁrst line, #! represents
that this ﬁle is script. In the second line, the command setPath speciﬁes
directory of ﬁle in which CCP is written. In the third line, the commandloadTheory loads the ﬁle sumsq where calculation rules are described. In
the fourth line, the command setExp sets the expression sumsqOpt as thestarting expression. In the ﬁfth to eighth lines, the command step transforms
expression. For example, in the ﬁfth line, the rule sumsq is applied to thefunction part of function application in the body of lambda expression, whichis the current expression. Expressions are represented in the η-expanded formin the system, so the expression sumsq is represented as λxs . sumsq xs. The
89

1:

#!

2:
3:
4:

setPath "~/ysys/examples"
loadTheory "sumsq"
setExp "sumsqOpt"

5:
6:
7:
8:

step "sumsqOpt" "BF"
step "sumsq" "BF"
step "applyFusion1" "BF"
step "applyFusion2" "BFA"

9:
10:
11:
12:
13:
14:

beginDerivation "fusion" "BFABF"
step "map2" "BB"match
step "map1" ""match
endDerivation

15:
16:
17:
18:
19:
20:

beginDerivation "fusion" "BF"
step "sum2" "BB"match
step "sum1" ""match
endDerivation

21:
22:

showDerivation
quit

Figure 6.4: An example of script – sumsq.ys

90

body of the λ expression is sumsq xs and the function part of it is sumsq.
Since this expression sumsq matches with the left hand side of the rule sumsq
in the second line of 6.5, By applying the rule sumsq, we obtain the following
expression.
λxs . sum (map sq xs)
This expression is displayed in the η-contracted form as in the ﬁfth lineof Figure 6.6. In the ninth line, the command beginDerivation starts subderivation for the rule fusion. In the sub-derivation, by transforming left
hand side to right hand side in each conditional equation in the if clause, we
get substitution for pattern variables. By using the obtained substitutions,the rule fusion is applied. Here, by the command match substitutions are
obtained and by the command endDerivation the sub-derivation is ended. In
the 21th line, the command showDerivation displays the derivation up to thepresent, which is shown in Figure 6.6. In the 22th line, the command quitﬁnishes the session.
Transformation rules are written as in Figure 6.5. The part surroundedby ”{-” and ”-}” is comment. Rules are separated by a semicolon ”;”. In
each rule deﬁnition, rule name is written before colon ”:” and the remaining
part represents a rule where left hand side and right hand side are separated by equal ”=”. The if clause is used when describing conditional rule.
Conditional equations are separated by semicolon ”;”.
The result of execution of the above script is as in Figure 6.6.

6.2.3

Execution of CCP and transformation to script

In this section, we show how to execute CCP. Script is record of executionof CCP. So, executing CCP is also a transformation of CCP to script.
When executing CCP, as a preprocess, CCP is transformed into the form
that each rule does not call another rule. Each function deﬁnition is simply
transformed into rule to unfold the deﬁnition. Deﬁnition of calculation rule istransformed into the form where rule applications in the right hand side of it
are removed. These transformations are performed on expressions including
higher order pattern matching as follows:• Meta let expression
letm ep1 = eb1 ; . . . ; epn = ebn in e
This is transformed to a conditional expression as follows:91

{- sumsq.eq -}sumsq : sumsq = sum . map sq;
sum1: sum []= 0;sum2
: sum (x:xs) = x + sum xs;
sq: sq x = x * x;
map1
: map f []
= [];
map2
: map f (x:xs) = f x : map f xs;
foldr1 : foldr step e []= e;foldr2 : foldr step e (a:x) = step a (foldr step e x);
fusion : _f (foldr _step _e _x) = foldr _g _c _x,
if{ \ x a -> _f (_step a x) = \ x a -> _g a (_f x);_f _e = _c };applyFusion1: _f . _g = _f . _g;
applyFusion2: _f = _f . foldr (:) [];sumsqOpt: sumsqOpt = sumsq

Figure 6.5: Rule deﬁnitions – sumsq.eq

92sumsqOpt= { sumsqOpt }sumsq= { sumsq }sum . map sq= { applyFusion1 }sum . map sq= { applyFusion2 }sum . (map sq . foldr (:) [])= { fusion(\ a x -> map sq (a : x ))= { map2 }(\ b d -> sq b : map sq d)
map sq []= { map1 }[]}sum . foldr (\ g -> (:) (sq g)) []= { fusion(\ a x -> sum (sq a : x))= { sum2 }(\ b c -> sq b + sum c)sum []= { sum1 }0}foldr (\ f -> (+) (sq f)) 0

Figure 6.6: Result of derivation – sumsq.out
93

e, if {eb1 = ep1;
eb2 = ep2;...
ebn = epn}
In equations for matching, left hand side and right hand side areswapped, which is for writing pattern in the right hand side in a rewriting rule.
• Meta case expression
casem e of ep1 → e1 ; . . . ; epn → en
The following n rules are generated and the meta case expression istransformed into e.
ep1 = e1;
ep2 = e2;...
epn = en
CCP is executed by applying the obtained rewriting rules in the orderspeciﬁed in CCP. The record of applied rules and location to which rules areapplied is script. We show the process of execution of CCP by an example
in the following.
Here as an example, we transform CCP for the sumsq problem to script.
CCP for the sumsq problem is shown in Figure 6.1. We execute the CCP
according to the procedure given above, as a result of which script is obtained.
Firstly as a preprocess, each function deﬁnitions are transformed into the rule
which unfolds the deﬁnition itself. Each calculation rules are transformed into
the rule that is obtained by removing rule applications in the right hand sidemechanically. As a result, we obtain the rewriting rules as in Figure 6.7.
The rule applyFusion1 rewrite nothing since the original rule does not
do other than application of rules <fusion> and <applyfusion>.
Next, the obtained rewrite rules in Figure 6.7 are applied in the orderspeciﬁed in CCP in Figure 6.1. The calculation process is as in Figure
6.6. Firstly sumsqOpt is transformed to sumsq and then it is unfolded by<unfold>. The rule <applyFusion> is applied to it when sum . map sq
is tested for matching against _f . _g and the rule applyFusion1 is applied. Here nothing is changed since nothing other than rule application isdone. Later the rule applyFusion will be applied to map sq and then the94

sumsq: sumsq = sum . map sq;
sum1: sum [] = 0;
sum2: sum (x:xs) = x + sum xs;
sq: sq x = x * x;
map1: map f [] = [];map2: map f (x:xs) = f x : map f xs;
foldr1: foldr step e [] = e;foldr2: foldr step e (a:x) = step a (foldr step e x);compose: (_f . _g) _x = _f (_g _x);
fusion: _f (foldr _step _e _xs) = foldr _g _c _xs,
if{ _f (_step a x) = _g a (_f x);_f _e = _c}applyFusion1: _f . _g = _f . _g;
applyFusion2: _f = _f . foldr (:) [];sumsqOpt: sumsqOpt = sumsq;

Figure 6.7: Rewriting rules for sumsq

95rule <fusion> will be applied. Next the rule <applyFusion> is applied tomap sq, but map sq does not match with _f . _g, applyFusion2 is applied. As a result sum . (map sq . foldr (:) []) is obtained. Later therule <fusion> will be applied to (map sq . foldr (:) []). After that therule <fusion> will be applied twice and an eﬃcient program that does notproduce any intermediate list is obtained.
By recording the applied rules and locations they are applied as script
form, we get a script as in Figure 6.4.

6.2.4

Example of maximum marking problems

Here we automatically generate eﬃcient linear time algorithms for several
maximum marking problems by using the system described in Section 6.2.1.
Maximum segment sum problem
Here we automatically generate an eﬃcient linear time algorithm for solving
the maximum segment sum problem (mss for short). The mss problem canbe speciﬁed as a maximum marking problem.
mss = ↑w / ◦ ﬁlter conn0 ◦ gen(6.1)

Firstly 2n marked lists are generated by the generation function gen.
Then by ﬁlter conn0 only lists that satisﬁes the property conn0 is extracted.
Finally by ↑w / a marked list that maximizes the value of the weight functionw.
We would like to obtain an eﬃcient linear time algorithm for mss fromthis speciﬁcation. We describe CCP for that as in Figure 6.8. The equation(6.1) is written in the ﬁrst line in Figure 6.8. The function bmax w represents(↑w ) and the function reduce represents (/).
The rule mmpRule represents the optimization theorem (Theorem 3), thattransforms to the optimization function opt. If properties satisfy the condition in the optimization theorem, the property conn0 can be decomposed to
a composition of an accept function and a ﬁnite catamorphism by the rule
<tupling>. By compiling this CCP, we obtain a script similar to the one in
Figure 6.4.

96-------------- Program ----------------mss = reduce (bmax w) . filter conn0 . gen;reduce f [x] = x;
reduce f (x:xs) = f x (reduce f xs);
bmax f a b = if f a > f b then a else b;
w = reduce (+) . map fc
where fc (x,m) = if marked (x,m) then x
else 0;filter p [] = [];filter p (x:xs) = if p x then x : filter p xs
else filter p xs;
conn0 [] = True;
conn0 (x:xs) = if marked x then conn1 xs else conn0 xs;
conn1 [] = True;
conn1 (x:xs) = if marked x then conn1 xs else conn2 xs;
conn2 [] = True;
conn2 (x:xs) = if marked x then False else conn2 xs;
marked (x,b) = b;
gen [] = [[]];gen (x:xs) = [ x’:xs’ |x’ <- [mark x,unmark x],
xs’ <- gen xs ];mark x = (x,True);unmark x = (x,False);
foldr _step _e [] = _e;foldr _step _e (_a:_x) = _step _a (foldr _step _e _x);

Figure 6.8: CCP for the maximum segment sum problem (the ﬁrst half)97-------------- calculation rules ----------------<mmpRule> (reduce (bmax _w) . filter conn0 . gen) =letm _accept . _h = <tupling> conn0;
reduce _oplus . map _f = _w;
foldr _phi2 _phi1 = <applyFusion> _hin opt (_oplus,_f) _accept _phi1 _phi2;<tupling> conn0 =letm _h xs = (conn0 xs,conn1 xs,conn2 xs);
_accept (t0,t1,t2) = t0;
in _accept . _h;<fusion> _f (foldr _step _e _xs) =letm _g a (_f x) = _f (_step a x);_c = _f _e
in foldr _g _c _xs;
<applyFusion> (_f . _g) = <fusion> (_f . <applyFusion> _g);<applyFusion> _f = <fusion> (_f . foldr (:) []);--------- Application of calculation rule -------mssOpt = <mmpRule> (<unfold> mss)

Figure 6.9: CCP for the maximum segment sum problem (the second half)98-------------- Program --------------------------mss’ = reduce (bmax w) . filter p . gen;...
p xs = conn0 xs && even xs;
even [] = True;
even (x:xs) = if marked x then odd xs else even xs;
odd [] = False;
odd (x:xs) = if marked x then even xs else odd xs;
h xs = (p xs,even xs,odd xs,conn0 xs,conn1 xs,conn2 xs);...
accept (t0,t1,t2,t3,t4,t5) = t0;-------------- Calculation rules ----------------...
---------- Application of calculation rule ------mssOpt’ = <mmpRule> (<unfold> mss’)Figure 6.10: CCP for the extended version of mss
An extension of the mss problem
Here we consider a problem that is an extension of the mss problem, extended
with respect to the property a solution should satisfy. We require that the
number of selected elements in the input list should be even. By letting theadditional condition even, we can describe the property p for the extended
problem as follows:p xs = conn0 xs ∧ even xs
where the property conn0 is for the original mss problem.
The extended problem is also a maximum marking problem. CCP for theextended problem can be described as in Figure 6.10 where only diﬀerent partfrom Figure 6.8 is described. The calculation rule mmpRule is not changed at
all.

99

6.2.5

Summary

In this chapter, we show an implementation of the theorem we proposed, thatis, we design a system for automatically generating eﬃcient linear time algorithms for maximum marking problems based on our theory proposed in thisthesis. In concrete aspect, we propose a language for describing transformation, implement the theorem in the language, and show the system implementation. We showed eﬀectiveness of our method by automatically generatingeﬃcient linear time algorithms for several maximum marking problems using
the implemented system.

100

Chapter 7
Related Work
Since the mid-1980s there have been several powerful approaches by dynamic
programming, and many NP-complete problems have thus been reduced tolinear-time problems for families of recursively constructed graphs. The pioneering work in this ﬁeld was on series-parallel graphs [TNS82].
The backbone concept is a class of graphs with bounded tree-width [RS86],
which was independently developed as partial k-tree [Arn87] and is also discussed in terms of separators [Tho90a] and cliques [KT90]. The set of graphswith tree-width at most k is equal to the set of k-terminal graphs constructedby algebraic composition rules [ACPS93]. NP-complete problems on graphs,
such as the Hamilton path problem, are often linear in the size and beyond
exponential in the tree width by the divide-and-conquer strategy according
to this algebraic construction.
Much work has been done [Bod93, Arn95], but most of it is on individual graph problems. Courcelle showed that whether a (hyper) graph withbounded tree width satisﬁes a closed monadic second order (MSOL, for short)
formula (of graphs) is solvable in linear time [Cou90a]. Borie et al. further
showed that the recognition, enumeration, and optimization problems speciﬁed by an extension of MSOL formula can be solved in linear time [BPT92].
This graph variant of MSOL uses Inc (v, e), which means a vertex v is anincident of an edge e, instead of the use of a successor function in ordinary
MSOL [Tho90b].
Although appealing in theory, these methods are hardly useful in practicedue to a huge constant factor for space and time. This arises from the
manipulation of huge tables:101• The construction of tables reﬂects the decomposition of the property
description into primitive ones; previous methods adapt ﬁxed basic
predicates as primitives, whereas our method freely adapts new primitives if they are in the form of mutumorphisms.
• Their construction of tables causes the exponential blow-up at each occurrence of quantiﬁers. Our method replaces the occurrences of quantiﬁers with recursions, which are computationally more eﬃcient.
Aspvall et al. proposed a method to reduce the run-time memory storage
by reducing the number of simultaneously needed tables [APT00]. Our work
reduces the size of tables directly, complementing their work.
To investigate the relation between mutumorphisms and MSOL is a good
research topic, to which recently one solution seemed to be given by Kassios[Kas01]. He gave an algorithm which transforms logical formula in [BPT92]
to mutumorphisms which consist of small number of functions.
Bird calculated a linear-time algorithm for solving the maximum segment sum problem on lists [Bir89], which is a kind of maximum marking
problem. Bird and de Moor studied optimization problems, which include
maximum marking problems, in a more general way that uses relational calculus [BdM96]. For instance, a greedy linear functional program for the party
planning problem can be derived using relation calculus. Using relational calculus, they developed a very general framework to treat optimization problems. It is called thinning theory, and the thinning theorem plays the central
role. But when applying the thinning theorem, one has to ﬁnd two preorders
which meet prerequisites of the thinning theorem, which makes it diﬃcult
for the theorem to be used for mechanical program generation. And they
didn’t show the relation between the complexity of derived algorithms andspeciﬁcations, in return for discussing in a very general framework. We instead focus on a useful class of optimization problems, maximum marking
problems, propose a very simple way to derive eﬃcient algorithms, and assure the complexity of the derived algorithms. When the target problem is a
maximum marking problem, the two preorders for the thinning theorem canbe derived automatically by applying the optimization theorem. To apply
our optimization theorem, the only thing one has to do is to describe theproperty in the form of mutumorphisms. One signiﬁcant reason for achieving this simplicity in derivation is that we have recognized the importance of
the ﬁniteness of the range of a catamorphism as in the optimization lemma,
which received little attention in [BdM96].
102

De Moor considered a generic program for sequential decision processes[dM95] which are speciﬁed as follows:
listmin r . filter p . fold (choice fs) [c]The target problems are on lists and trees. They include maximum marking
problems by letting the list of functions fs, used in the above speciﬁcationof sequential decision processes, be a list of marking functions. But property
p is restricted to be suﬃx-closed. There are many examples whose property
is not suﬃx-closed.
Johan Jeuring proposed several fusion theorems, each of which deals witha class of optimization problems such as subsequence problems on lists, partition problems on lists, and so on [Jeu93]. In order to derive an eﬃcient
program for a problem by his method, one has to select a suitable fusion
theorem, which is not necessary in our method.
Recently, Bird showed that the maximum marking problems can betreated in the framework of thinning theory [Bir00]. He assured the derived
algorithm is a linear time algorithm, and showed the generic Haskell programfor solving the maximum marking problems on polynomial data types. His
method also requires that the property p should be suﬃx-closed. We show
his method later in detail and compare it with ours.
In graph algorithms, Borie et al. proposed a method which enables
the derivation of a linear time algorithm for solving the maximum marking problems on k-terminal graphs, a restricted class of graphs, from logicaldescription of properties by a graph variant of monadic second order formula[BPT92]. This graph variant of MSOL uses Inc (v, e), which means a vertex
v is an incident of an edge e, instead of the use of a successor function in
ordinary MSOL [Tho90b]. Although appealing in theory, these methods are
hardly useful in practice due to a huge constant factor for space and time.

Program Transformation System
There are several program transformation system. One of them is stratego[Vis01], which is a language for describing a program transformation. The
system we implemented in this thesis depends on a calculation describing
language called Calculation Carrying Program (CCP for short) [HT99]. The
words ”calculation carrying” represent that the code which speciﬁes how
to calculate an eﬃcient program is accompanied with the original program.
103

This method is useful for the user who use the program in the sense that hecan know the meaning of the program easily by the original program in CCP,
and at the same time he can obtain an eﬃcient program by calculating it.
Another possible approach for describing program transformation is to use
meta programming language such as Meta-ML, which is an extension of thelanguage ML.

Relational Calculus
Here we show the derivation of a linear time algorithm for MMP by relational
calculus. First, we show the Bird’s derivation [Bir00]. Second, we extend thespeciﬁcation to one which can express the same class as ours speciﬁcation
can do.

Speciﬁcation by Bird
Maximum marking problem can be speciﬁed by a relation as follows:
mmp = max (≤) ◦ Λ(w ◦ dom p ◦ mapT mark)This speciﬁcation is interpreted not as Haskell functions, but as multifunctions. A multifunction is a nondeterministic function, that is, a relation thatassociates zero or more results with each argument. Type of multifunction
is written as A ; B rather than A → B. For example,
mark:: α ; α∗mark n = (n, True) 2 (n, False)
The type of p is

p :: T α∗ −→| Class

For the mss problem, p can be deﬁned as follows:conn :: T α∗ −→| Classconn = foldFList f
where f (1, ()) = c1r == c1 ∧ b





 r == c1 ∧ ¬b

→ c2
→ c1
→ c2
f (2, ((x, b), r)) = r == c2 ∧ b



r
==
c
∧
¬b
→ c3

2


 r == c ∧ ¬b → c33104Here FList is deﬁned as follows:
FList (a, b) = 1 + a × b
The box 2 signiﬁes nondeterministic choice. The type α∗ is deﬁned asfollows:α∗ = α × Bool
The type of mapT is
mapT :: (a ; b) → (T a ; T b)
This is like the ordinary map function associated with a data type T exceptthat it can take a multifunction as argument and return a multifunction as
result. The combination mapT mark denotes the operation of marking anelement of T α in a completely nondeterministic way.
The function dom, which takes a multifunction as argument and returns
a partial function as result, is deﬁned as follows:dom:: (a ; b) → (a −→| a)dom p = fst ◦ hid, pi
The split operation hf, gi is deﬁned by hf, gi x = (f x, g x). The expression
hf, gi denotes a multifunction that returns a result on an argument x if andonly if both f and g do.
The weight function w is deﬁned as follows:w:: T α∗ → Weightw= sum ◦ mapT mw
mw (e, b) = if b then e else 0
The subsidiary function sum :: T Weight → Weight for summing a structureof weights will be deﬁned later.
The operation Λ turns a multifunction into the corresponding set-valued
function:Λ:: (a ; b) → (a → Set b)(Λf ) a = {b | b ← f a}
We write b ← f a to denote the fact that b is a possible value of f a. Thus(Λf ) a returns the set of all possible values b that can be returned as theresult of applying the multifunction f to a.
105

The multifunction max is deﬁned bymax:: (a → a → Bool) → (Set a ; a)a ← max () as ≡ a ∈ as ∧ (∀b ∈ as : b  a)
In words, max takes an ordering  and a set as as argument, and returns
some maximum element in as under . It is required that  should be aconnected preorder. A relation r is said to be preorder if r is a reﬂexive andtransitive relation. A relation r is said to be connected if for all x and y,either x  y or y  x. Then it is guaranteed that max () as produces
at least one result for all nonempty sets as. It is diﬀerent from functional
speciﬁcation that max () as does not specify which element of as should
be chosen.

Calculation
The speciﬁcation of mmp is as follows:
mmp = max (≤) ◦ Λ(w ◦ dom p ◦ mapT mark)First, rewrite the subexpression w ◦ dom p:w ◦ dom p={ definition of dom }w ◦ fst ◦ hid, pi={ claim }fst ◦ hw, pi={ definition of w }fst ◦ hfoldF plusF ◦ mapT mw, pi={ type functor fusion }fst ◦ hfoldF (plusF ◦ mapF (mw, id)), pi={ assume p = foldF partF }fst ◦ hfoldF (plusF ◦ mapF (mw, id)), foldF partF i={ banana split }fst ◦ hfoldF f i

Here, f is deﬁned as follows:
f :: F (α∗ , (Weight, Class)) −→| (Weight, Class)f = hplusF ◦ mapF (mw, fst), partF ◦ mapF (id, snd)i
106

The claim is a consequence of two laws:f ◦ fst= fst ◦ (f × id)(f × g) ◦ hh, ki = hf ◦ h, g ◦ ki
where (f × g)(x, y) = (f x, g y).
Now we can rewrite the subexpression w ◦ dom p ◦ mapT mark:w ◦ dom p ◦ mapT mark={ above }fst ◦ foldF f ◦ mapT mark={ type functor fusion }fst ◦ foldF g

where g :: F (α, (Weight, Class)) ; (Weight, Class) is deﬁned by g = f ◦mapF (mark, id). Using this result, we now obtainmax (≤) ◦ Λ(w ◦ dom p ◦ mapT mark)={ above }max (≤) ◦ Λ(fst ◦ foldF g)={ claim }fst ◦ max (≤1 ) ◦ Λ(foldF g)
where (≤1 ) :: (Weight, Class) → (Weight, Class) → Bool is deﬁned bydef(a1 , b1 ) ≤1 (a2 , b2 ) = (a1 ≤ a2 )The proof of the claim is in [BdM96].
Now we can apply the thinning theorem to the expression
max (≤1 ) ◦ Λ(foldF g).
Theorem 6 (Thinning)max (≤) ◦ Λ(foldF f ) ⊇ max (≤) ◦ foldF g
where

g :: F (a, Set b) ; Set b
g = thin () ◦ Λ(f ◦ mapF (id, choose))

provided that: (i) x  y ⇒ x ≤ y; and (ii) f is monotonic under .
1072Here thin is deﬁned as follows:thin:: (a → a → Bool) → (Set a ; Set a)bs ← thin () as ≡ bs ⊆ as ∧ (∀a ∈ as : ∃b ∈ bs : a  b)
To apply the thinning theorem, we have to ﬁnd an order  which satisﬁes
the condition (i) and (ii) in the theorem. In this case, the following order ≤2satisﬁes them.
def(a1 , b1 ) ≤2 (a2 , b2 ) = (a1 ≤ a2 ∧ b1 == b2 )Now the speciﬁcation is calculated to the following form:
mmp ⊇ fst ◦ max (≤1 ) ◦ foldF g
g= thin (≤2 ) ◦ Λ(f ◦ mapF (id, choose))f= hplusF ◦ mapF (mw, fst), partF ◦ mapF (id, snd)i ◦ mapF (mark, id)
The thinning theorem says that we can compute an optimum result by
maintaining a representative number of partial solutions at each stage ofthe folding process. If Class has size k, then we need keep only k partial
solutions at each stage. For the mss problem, |Class| = 3, so only threepartial solutions have to be kept.

Property by a relational fold
Properties are restricted to those which can be expressed using foldF :p = foldF partF
This restricts properties to “suﬃx-closed” properties. Originally the term
“suﬃx closed” is used for lists. If the property p doesn’t hold for the list xs,
then p doesn’t hold for the list ys ++ xs for all ys. We use the suﬃx-closed
for data type T , that is, if p doesn’t hold for the property p on the data x,
then p doesn’t hold for data which have x as its sub-data.

Extension of Property class
We extend properties to those which can be written as follows:p :: T α∗ −→| Classp = accept ◦ foldF partF
108

Here accept is a partial function which has following type:
accept :: Class −→| ClassThough we omit detail, the speciﬁcation mmp can be calculated to the following expression:
fst ◦ dom (accept ◦ snd) ◦ max (≤1 ) ◦ foldF g

Discussion
The derivation by relational calculus is clearer than that by functional calculus because by functional calculus, essentially nondeterministic part haveto be represented by a function. So, it may seem that it may be better toreplace the proof of the optimization function opt by one using a relational
calculus. It is true that the relational calculus is clear, but it is remained to
implement the obtained relation as a function. This step is slightly complicated and actually it takes about 4 pages to implement obtained result as afunction in [Bir00].

109

Chapter 8
Conclusion
In this thesis we present a new method for deriving practical linear-time algorithms for maximum marking problems on recursive data structures. From a
speciﬁcation represented as a functional program, our method obtains practical linear-time algorithms by deriving a catamorphism whose range size issmall. Though our method does not guarantee that the derived catamorphism has a range with the smallest number of elements, in many cases it
has range consisting of about 10 or 20 elements because the properties ofmany problems can be described in mutumorphisms which consist of threeor four property descriptions. This means our derived linear-time algorithms
are practical in many cases. Our method also enables linear time algorithms
to be derived in a simple, systematic, and natural way, and it can ﬂexibly
cope with modiﬁcation of the speciﬁcation.
Though our current focus is on well-used recursive data structures suchas lists and trees, our method should be able to deal with the graphs withbounded tree width because a class of the graphs with bounded tree width canbe represented as a recursive data structure like that described in Chapter 2.
Our next target problems are linear-time control ﬂow analyses for structured
procedural programs, for which the control ﬂow graphs are known to havebounded tree width [Tho98]. Though we currently restrict data types topolynomial data types, we think our optimization theorem can be extended
to regular data types. Although we concentrate on the maximizing problems,
our method is easily extended for the minimization, existence and enumeration problems in [BPT92].
Our method is mechanical, so it is appropriate for automatic generation. We have shown implementation of a system for automatically generat110

ing eﬃcient linear time algorithms for maximum marking problems. It was
known that generation of linear time algorithms for MMP (precisely maximum weightsum problem) can be done by the method proposed by Borie etal., [BPT92]. Though his method is theoretically appealing, it generates aprohibitively large table and thus cannot be put to practical use. We haveshown that our system generates practical linear time algorithms by using
several examples.
Our method of course has limitations, and the most fundamental isthat tree width is bounded. The two-dimensional maximum segment sum
problem, for example, cannot be dealt with by our method because a twodimensional matrix corresponds to a grid graph, which will have unbounded
tree width.

111

Bibliography[ACPS93]

Stefan Arnborg, Bruno Courcelle, Andrzej Proskurowski, andDetlef Seese. An algebraic theory of graph reduction. Journalof the ACM, 40(5):1134–1164, 1993.

[ADH+ 98]

Harold Abelson, R.K. Dybvig, C.T. Haynes, G.J. Rozas,
N.I. Adams IV, D.P. Friedman, E. Kohlbecker, G.L. Steele Jr.,
D.H. Bartley, R. Halstead, D. Oxley, G.J. Sussman, G. Brooks,
C. Hanson, K.M. Pitman, and M. Wand. Revised5 report on
the algorithmic language scheme. Higher-Order and Symbolic
Computation, 11(1):7–105, 1998.

[AP89]

Stefan Arnborg and Andrzej Proskurowski. Linear time algorithms for NP-hard problems on graphs embedded in k-trees.
Discrete Applied Mathematics, 23:11–24, 1989.

[APT00]

Bengt Aspvall, Andrzej Proskurowski, and Jan Arne Telle.
Memory requirements for table computations in partial k-tree
algorithms. Algorithmica, 27(3):382–394, 2000.

[Arn87]

Stefan Arnborg. Complexity of ﬁnding embeddings in a ktree. SIAM Journal Algebraic Discrete Mathematics, 8:277–287,
1987.

[Arn95]

Stefan Arnborg. Decomposable structures, Boolean function,
representations, and optimization. In J. Wiedermann and
P. Hájek, editors, Mathematical Foundations of Computer Science 1995, volume 969 of Lecture Notes in Computer Science,
pages 21–36. Springer-Verlag, 1995.

112

[AwJS96]

Harold Abelson and Gerald Jay Sussman with Julie Sussman.
Structure and Interpretation of Computer Programs (second
edition). MIT Press, 1996.

[BdM96]

Richard Bird and Oege de Moor. Algebra of Programming.
Prentice Hall, 1996.

[Ben84]

Jon Louis Bentley. Programming pearls: Algorithm design techniques. Communications of the ACM, 27(9):865–871, September 1984.

[Bir87]

Richard Bird. An introduction to the theory of lists. In Manfred Broy, editor, Logic of Programming and Calculi of Discrete
Design, volume F36 of NATO ASI Series, pages 5–42. SpringerVerlag, 1987.

[Bir89]Richard Bird. Algebraic identities for program calculation. The
Computer Journal, 32(2):122–126, 1989.

[Bir98]Richard Bird. Introduction to Functional Programming using
Haskell (second edition). Prentice Hall, 1998.

[Bir00]Richard Bird.
Maximum marking problems, 2000.
Availablefrom
http://www.comlab.ox.ac.uk/oucl/work/
richard.bird/publications/mmp.ps.

[BLW87]

Marshall W. Bern, Eugene L. Lawler, and A. L. Wong.
Linear-time computation of optimal subgraphs of decomposable graphs. Journal of Algorithms, 8:216–235, 1987.

[Bod93]

Hans L. Bodlaender. A tourist guide through treewidth. Acta
Cybernetica, 11:1–21, 1993.

[BPT92]

Richard B. Borie, R. Gary Parker, and Craig A. Tovey. Automatic generation of linear-time algorithms from predicate calculus descriptions of problems on recursively constructed graphfamilies. Algorithmica, 7:555–581, 1992.

[BRS99]Sergey Brin, Rajeev Rastogi, and Kyuseok Shim. Mining optimized gain rules for numeric attributes. In Proceedings of113

the ﬁfth ACM SIGKDD International Conference on Knowledge Discovery and Data Mining (KDD’99), pages 135–144, San
Diego, CA USA, August 1999. ACM Press.
[CLRS01]

Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest,
and Cliﬀord Stein. Introduction to Algorithms, Second Edition.
MIT Press, 2001.

[Cou90a]

Bruno Courcelle. Graph rewriting: An algebraic and logic approach. In Jan van Leeuwen, editor, Handbook of TheoreticalComputer Science, volume B, chapter 5, pages 194–242. Elsevier Science Publishers, 1990.

[Cou90b]

Bruno Courcelle. The monadic second-order logic of graphs. I.
Recognizable sets of ﬁnite graphs. Information and Computation, 85(1):12–75, March 1990.

[dM95]

Oege de Moor. A generic program for sequential decision processes. In Proceedings of the 7th International Symposium on
Programming Languages, Implementations, Logics, and Programs (PLILP’95), LNCS 982, pages 1–23, Utrecht, the Netherlands, September 1995.

[dMS98]Oege de Moor and Ganesh Sittampalam. Generic programtransformation. In Proceedings of the 3rd International Summer School on Advanced Functional Programming (AFP’98),
LNCS 1608, pages 116–149, Braga, Portugal, September 1998.
Springer-Verlag.

[dMS99]Oege de Moor and Ganesh Sittampalam. Higher-order matching for program transformation. Theoretical Computer Science,
to appear, 1999.

[ES00]

Thomas Erlebach and Frits Spieksma. Simple algorithms fora weighted interval selection problem. In Proceedings of the
11th International Symposium on Algorithms and Computation(ISAAC’00), LNCS 1969, pages 228–240, Taipei, Taiwan, December 2000. Springer-Verlag.

114

[FMMT96a] Takeshi Fukuda, Yasuhiko Morimoto, Shinichi Morishita, andTakeshi Tokuyama. Data mining using two-dimensional optimized association rules: Scheme, algorithms, and visualization.
In Proceedings of the 1996 ACM SIGMOD International Conference on Management of Data (SIGMOD’96), pages 13–23,
Montreal, Canada, June 1996. ACM Press.
[FMMT96b] Takeshi Fukuda, Yasuhiko Morimoto, Shinichi Morishita, andTakeshi Tokuyama. Mining optimized association rules for numeric attributes. In Proceedings of the ﬁfteenth ACM SIGACTSIGMOD-SIGART symposium on Principles of database systems (PODS’96), pages 182–191, Montreal, Canada, June 1996.
ACM Press.
[Fok89]Maarten M. Fokkinga. Tupling and mutumorphisms. Squiggolist, 1(4), 1989.

[Fok92]Maarten M. Fokkinga. Law and Order in Algorithmics. PhD
thesis, University of Twente, Dept INF, Enschede, The Netherlands, 1992.

[GLP93]

Andrew Gill, John Launchbury, and Simon Peyton Jones. A
short cut to deforestation. In Proceedings of the 6th International Conference on Functional Programming Languages
and Computer Architecture (FPCA’93), pages 223–232, Copenhagen, Denmark, June 1993. ACM Press.

[Gri90]D. Gries. The maximum-segment sum problem. In E. W. Dijkstra, editor, Formal Development of Programs and Proofs.
Addison-Wesley, 1990.

[HITT97]

Zhenjiang Hu, Hideya Iwasaki, Masato Takeichi, and Akihiko
Takano. Tupling calculation eliminates multiple data traversals.
In Proceedings of the 2nd ACM SIGPLAN International Conference on Functional Programming (ICFP’97), pages 164–175,
Amsterdam, The Netherlands, June 1997. ACM Press.

[HT99]

Zhenjiang Hu and Masato Takeichi. Calculation carrying programs. Technical Report METR 99-07, Department of Mathematical Engineering, University of Tokyo, Japan, 1999.
115

[Jeu93]

Johan Jeuring. Theories for Algorithm Calculation. Ph.D thesis, Faculty of Science, Utrecht University, 1993.

[Kas01]

Ioannins T. Kassios. Translating Borie-Parker-Tovey calculus
into mutumorphisms, 2001. submitted to Algorithmica.

[KT90]

Igor Křı́ž and Robin Thomas. Clique-sums, tree-decompositions
and compactness. Discrete Mathematics, 81:177–185, 1990.

[MFP91]Erik Meijer, Maarten Fokkinga, and Ross Paterson. Functional programming with bananas, lenses, envelopes and barbed
wire. In Proceedings of the 5th International Conference on
Functional Programming Languages and Computer Architecture(FPCA’91), volume 523 of Lecture Notes in Computer Science,
pages 124–144, Cambridge, Massachusetts, August 1991. ACM
Press.

[MT90]

Silvano Martello and Paolo Toth. Knapsack Problems : Algorithms and Computer Implementations. Wiley-Interscience
series in discrete mathematics and optimization. John Wiley &Sons Ltd., 1990.

[MTHM97] Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Deﬁnition of Standard ML - Revised. MIT Press,
1997.
[Pau96]

Lawrence C. Paulson. ML for the Working Programmer (second
edition). Cambridge University Press, 1996.

[PJH99]Simon Peyton Jones and John Hughes, editors.
The
Haskell 98 Report.
February 1999.
Available fromhttp://www.haskell.org/deﬁnition/.

[PP96]

Albert Pettrossi and Maurizio Proietti. Rules and strategies fortransforming functional and logic programs. ACM Computing
Surveys, 28(2):360–414, June 1996.

[RS86]

Neil Robertson and Paul D. Seymour. Graph minors. II. Algorithmic aspects of tree-width. Journal of Algorithms, 7(3):309–
322, September 1986.

116

[SF93]

Tim Sheard and Leonidas Fegaras. A fold for all seasons. In
Conference on Functional Programming Languages and Computer Architecture, pages 233–242, 1993.

[SHT01]

Isao Sasano, Zhenjiang Hu, and Masato Takeichi. Generationof eﬃcient programs for solving maximum multi-marking problems. In Walid Taha, editor, Semantics, Applications, and Implementation of Program Generation (SAIG’01), volume 2196
of Lecture Notes in Computer Science, pages 72–91, Firenze,
Italy, September 2001. Springer-Verlag.

[SHTO00]

Isao Sasano, Zhenjiang Hu, Masato Takeichi, and Mizuhito
Ogawa. Make it practical: A generic linear-time algorithm forsolving maximum-weightsum problems. In Proceedings of the
5th ACM SIGPLAN International Conference on Functional
Programming (ICFP’00), pages 137–149, Montreal, Canada,
September 2000. ACM Press.

[SHTO01a] Isao Sasano, Zhenjiang Hu, Masato Takeichi, and Mizuhito
Ogawa. Calculating linear time algorithms for solving maximum weightsum problems (in Japanese). Computer Software,
18(5):1–16, 2001.
[SHTO01b] Isao Sasano, Zhenjiang Hu, Masato Takeichi, and Mizuhito
Ogawa. Derivation of linear algorithm for mining optimized
gain association rules. In 18th Conference Proceedings Japan
Society for Software Science and Technology, 2001.
[SHTO01c] Isao Sasano, Zhenjiang Hu, Masato Takeichi, and Mizuhito
Ogawa. Solving a class of knapsack problems on recursive
data structures (in Japanese). Computer Software, 18(2):59–
63, 2001.
[TH00]

Masato Takeichi and Zhenjiang Hu. Calculation carrying programs: How to code program transformations (invited paper).
In International Sumposium on Principles of Software Evolution (ISPSE 2000), Kanazawa, Japan, November 2000. IEEE
Press.

117

[Tho90a]

Robin Thomas. A Menger-like property of tree-width: The
ﬁnite case. Journal of Combinatorial Theory, Series B, 48:67–
76, 1990.

[Tho90b]

Wolfgang Thomas. Automata on inﬁnite objects. In Jan van
Leeuwen, editor, Handbook of Theoretical Computer Science,
volume B, chapter 4, pages 133–192. Elsevier Science Publishers, 1990.

[Tho98]

Mikkel Thorup. All structured programs have small tree widthand good register allocation. Information and Computation,
142:159–181, 1998.

[TNS82]

Kazuhiko Takamizawa, Takao Nishizeki, and Nobuji Saito.
Linear-time computability of combinatorial problems on seriesparallel graphs. Journal of the Association for Computing Machinery, 29:623–641, 1982.

[Vis01]

Eelco Visser. Stratego: A language for program transformation
based on rewriting strategies. system description of stratego 0.5.
In Rewriting Techniques and Applications (RTA’01). SpringerVerlag, May 2001.

[Wim87]

Thomas V. Wimer. Linear Algorithms on k-Terminal Graphs.
PhD thesis, Clemson University, 1987. Report No. URI-030.

[YSHT01]

Tetsuo Yokoyama, Isao Sasano, Zhenjiang Hu, and Masato
Takeichi. Automatic generation of eﬃcient programs for maximum multi-marking problems (in Japanese), 2001. 36th IPSJ
Special Interest Group on Programming.

118