MATHEMATICAL ENGINEERINGTECHNICAL REPORTS

Generator-based GG Fortress Library—Collection of GGs and Theories—

Kento EMOTO, Zhenjiang HU, Kazuhiko KAKEHI,
Kiminori MATSUZAKI and Masato TAKEICHIMETR 2008–17

March 2008

DEPARTMENT OF MATHEMATICAL INFORMATICSGRADUATE SCHOOL OF INFORMATION SCIENCE AND TECHNOLOGYTHE UNIVERSITY OF TOKYOBUNKYO-KU, TOKYO 113-8656, JAPANWWW page: http://www.keisu.t.u-tokyo.ac.jp/research/techrep/index.html

The METR technical reports are published as a means to ensure timely dissemination ofscholarly and technical work on a non-commercial basis. Copyright and all rights therein
are maintained by the authors or by other copyright holders, notwithstanding that they
have offered their works here electronically. It is understood that all persons copying thisinformation will adhere to the terms and constraints invoked by each author’s copyright.
These works may not be reposted without the explicit permission of the copyright holder.

Generator-based GG Fortress Library—Collection of GGs and Theories—
Kento Emoto† , Zhenjiang Hu† , Kazuhiko Kakehi‡ ,Kiminori Matsuzaki† and Masato Takeichi†† Graduate School of Information Science and Technology, University of Tokyo‡ Division of University Corporate Relations (DUCR), University of Tokyo{emoto,kmatsu,kaz}@ipl.t.u-tokyo.ac.jp{hu,takeichi}@mist.i.u-tokyo.ac.jp

Abstract
We have proposed a novel library called “GG Library” on Fortress in the previous report.
The library supports easy development of correct and efficient parallel programs, allowing
users to write naive generate-and-test programs easily and uniformly with generator-ofgenerators that abstract generation of nested data structures. The library has an automatic
optimization mechanism by dispatching efficient implementation to a user program writtenwith generator-of-generators based on a collection of theories. To enrich the power of GG
library, we need to make collections of generator-of-generators and their theories for optimization. This report collects generator-of-generators and their theories for optimization
with formal discussion, as well as their implementations in GG library.

1Contents
1 Introduction

5

2 Overview of GG Library
2.1 Structure of GG Library . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.2 Behavior of GG Library . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

666

3 A Collection of GGenerators with Example Problems
3.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.1.1 Basic Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.1.2 GGenerators and Generate-and-test Specification . . . . . . . . . . . . . .
3.1.3 Predicates for Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.3 GGenerator inits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.3.1 Prefix Sums . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.3.2 Maximum Prefix Sum . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.3.3 Maximum p-Prefix Sum . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.4 GGenerator tails . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.4.1 Suffix Sums . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.4.2 Maximum Suffix Sum . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.4.3 Maximum p-Suffix Sum . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.5 GGenerator segs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.5.2 Maximum Segment Sum . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.5.3 Maximum p-Segment Sum . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.5.4 Longest-p Segment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.6 GGenerator subs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.6.1 Longest-p Subsequence . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.6.2 0-1 Knapsack Problem . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.7 GGenerator parts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.7.1 Smallest All Ascending Partition . . . . . . . . . . . . . . . . . . . . . . .
3.7.2 Paragraph Formatting . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.8 GGenerator perm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.8.1 Sorting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

9
9
9
10
10
11
11
11
12
12
12
13
13
14
14
14
15
16
16
16
17
17
17
18
18

4 A Collection of Theories
4.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.1.1 Homomorphism and Auxiliary Functions . . . . . . . . . . . . . . . . . . .
4.1.2 GGenerators and Generate-and-test Specification . . . . . . . . . . . . . .
4.2 Properties on Reduction Operators and Predicates . . . . . . . . . . . . . . . . .
4.2.1 Properties on Reduction Operators . . . . . . . . . . . . . . . . . . . . . .
4.2.2 Properties on Predicates . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.3 Theory of inits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.3.1 Formal Definition and Basic Lemmas . . . . . . . . . . . . . . . . . . . . .
4.3.2 Theorem for Reduction with Distributive Operators . . . . . . . . . . . .
4.3.3 Theorem for Filtering with Relational Predicates . . . . . . . . . . . . . .
4.4 Theory of tails . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.4.1 Formal Definition and Basic Lemmas . . . . . . . . . . . . . . . . . . . . .
4.4.2 Theorem for Reduction with Distributive Operators . . . . . . . . . . . .
4.4.3 Theorem for Filtering with Relational Predicates . . . . . . . . . . . . . .
4.5 Theory of segs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.5.1 Formal Definition and Basic Lemmas . . . . . . . . . . . . . . . . . . . . .
4.5.2 Theorem for Reduction with Distributive Operators . . . . . . . . . . . .

19
19
19
20
21
21
21
23
24
24
26
29
29
29
30
31
31
31

3

4.5.3 Theorem for Filtering with Relational Predicates . . . . . . . . . . . . . .
Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.6.1 Maximum Marking Problem . . . . . . . . . . . . . . . . . . . . . . . . . .
4.6.2 Longest Segment Problems . . . . . . . . . . . . . . . . . . . . . . . . . .

33
34
34
34

5 Implementation of GG Library
5.1 Core Implementation of GG Library . . . . . . . . . . . . . . . . . . . . . . . . .
5.1.1 Trait GGenerator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.1.2 Dispatching Table . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.1.3 Auxiliary Functions and Object . . . . . . . . . . . . . . . . . . . . . . . .
5.1.4 Desugaring of User Programs . . . . . . . . . . . . . . . . . . . . . . . . .
5.2 Traits for Describing Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.2.1 Properties on Reduction Operators . . . . . . . . . . . . . . . . . . . . . .
5.2.2 Properties on Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.2.3 Properties on Predicates . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.3 Implementation of GGenerator inits . . . . . . . . . . . . . . . . . . . . . . . . . .
5.3.1 Base Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.3.2 Implementation for Nested Reductions with Distributive Operators . . . .
5.3.3 Implementation for Filtering with Relational Predicates . . . . . . . . . .
5.4 Implementation of GGenerator tails . . . . . . . . . . . . . . . . . . . . . . . . . .
5.4.1 Base Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.4.2 Implementation for Nested Reductions with Distributive Operators . . . .
5.4.3 Implementation for Filtering with Relational Predicates . . . . . . . . . .
5.5 Implementation of GGenerator segs . . . . . . . . . . . . . . . . . . . . . . . . . .
5.5.1 Base Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.5.2 Implementation for Nested Reductions with Distributive Operators . . . .
5.5.3 Implementation for Filtering with Relational Predicates . . . . . . . . . .
5.6 Experimnt Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

37
37
37
38
40
40
42
42
43
43
46
46
47
47
49
49
49
50
52
52
52
53
55

6 Conclusion

57

4.6

4

1

Introduction

In the previous report [EHK+ 08], we have proposed a novel library called “GG Library” (GG
stands for Generator-of-Generators) for parallel computation on Fortress [ACH+ ]. The librarysupports easy development of correct and efficient parallel programs, and the library itself cangrow up to cover a wider range of problems and to achieve better optimization power. These
points match to the spirit of Fortress.
Features of the library are summarized as follows.
• Support for easy program development by generate-and-test specification
Users can write naive generate-and-test programs easily and uniformly with GGenerators (generator-of-generators) that abstract generation of nested data structures. This
generate-and-test specification covers wide range of problems, and users can make theirprograms by changing parameters of the specification, such as GGenerators, binary operators, functions and predicates to filter elements.
• Automatic optimization by dispatching correct and efficient implementation
The library automatically dispatches efficient implementation to a user program writtenwith GGenerators based on a collection of theories. Each GGenerator has its collection oftheories and accompanying efficient implementations. If the library detects that the given
user program satisfies conditions to apply some efficient implementation given by theories,
then the library dispatches the efficient implementation to the user program. Propertiesof user programs such as distributivity of operators should be explicitly given by users
when user-defined functions and operators are used in their programs.
• Growing Library
The library grows in two directions: expressiveness and optimization power. The expressiveness of the library easily grows by extending the specification supported by the library.
For example, adding a new GGenerator we can extend the specification to cover a wider
range of problems. The power of optimization of the library easily grows by adding new
knowledge of theories.
To enrich the power of GG library, we need to make collections of GGenerators and their
theories for optimization.
This report collects GGenerators and their theories for optimization with formal discussion,as well as their implementations in GG library. Section 2 shows an overview of GG library.
Section 3 shows a collection of GGenerators with some example problems. Section 4 formalizes
a collection of theories for optimization. Section 5 shows implementation of GGenerators andknowledge of their theories in GG library, as well as the core of GG library. Finally, Section 6
concludes this report. Note that, in Section 3, Section 4 and Section 5, subsections of thesame subsection-number correspond to the same target. For example, for GGenerator inits,
Section 3.3, Section 4.3 and Section 5.3 give example problems, theories, and implementationin GG library, respectively.

5

2

Overview of GG LibraryThis section briefly reviews our proposed GG library [EHK+ 08].

2.1

Structure of GG Library

Figure 1 illustrates the structure of GG Library. There are two kinds of collections in the library. One is a collection of GGeneratorsthat are used to describe specification of problems.
Each GGeneratorabstracts generation of a nested data structure. The collection of GGeneratorsprovides an interface for easy and uniform description of user programs. The collection of
GGeneratorswith their examples is shown in Section 3.
The other is a collection of theories and accompanying efficient implementations dispatched
to user programs. Basically, each GGenerator has its own collection of theories and efficient
implementations. Given a user program written with GGenerators, the library checks applicableconditions of theories against the given program, and then if the program satisfies the condition,
the library dispatches the accompanying efficient implementation. The collection of theories isshown in Section 4.
Besides those two specific collections, the library has a collection of traits to describe mathematical properties of user programs. Those traits are used to determine whether a given user
program satisfies applicable conditions of theories.
Figure 1 also illustrates how GG library grows in two directions: expressiveness and optimization power. The expressiveness of the library grows by adding new GGenerators to support
a wider range of problem specifications. The power of optimization grows by adding new knowledge of theories to dispatch more efficient implementation to more user programs.

2.2

Behavior of GG Library

Figure 2 shows the behavior of our GG Library with concrete examples for a program to solve“Maximum Prefix Sum Problem” (Section 3.3.2.) The objective of the program is to find the
maximum sum of a prefix of the input sequence. The behavior of GG Library for dispatching
implementation to a user program is separated into the following two phases.
Phase 1. Desugaring a user program into invocations of method generate2 of GGenerators
In the first phase, the library desugars a user program written with for-loops or comprehensions into invocations of method generate2 of GGenerators (Section 5.1.1) usedin the program. Method generate2 performs nested reductions on generated nested
data structures.
Figure 2-(a) shows an example of such user programs written with comprehensions.
This program uses GGenerator inits (Sections 3.3, 4.3, 5.3) to generate prefix segmentsof the input sequence x . The desugaring process transforms the user program into
the program shown in Figure 2-(b). Two reduction operators + and MAX are given
to method generate2 as its arguments enclosed in objects: SumReductionZZ32 andMaxReductionZZ32. The other arguments of method generate2 are default values
such as IdFunction (Section 5.2.2) and TrueListPredicate (Section 5.2.3).
Phase 2. Dispatching implementation within the invocation of method generate2
After the desugaring process, the library dispatches implementation within the invocation of generate2 . In this phase, the library checks whether properties of thegiven arguments of method generate2 satisfy the applicable condition of each theoryof the GGenerator. And then, if it is found that the applicable condition is satisfied,the library performs computation of the nested reductions by corresponding efficient
implementation.
6

Figure 1: Structure of GG library

BIG MAX [P[ a | a ← y] | y ← inits x ](a) User program of nested reductions with comprehensions
mis xs = inits(x).generate2 [[ MaxReductionZZ32, IdFunction[[Z32]],
SumReductionZZ32, IdFunction[[Z32]],
TrueListPredicate[[Z32]], Z32, Z32]](MaxReductionZZ32, IdFunction[[Z32]],
SumReductionZZ32, IdFunction[[Z32]],
TrueListPredicate[[Z32]])(b) Desugared program
opr MPS(a, b) = do
(m1 , s1 ) = a(m2 , s2 ) = b(m1 MAX (s1 + m2 ), s1 + s2 )end
object MPSReduction extends Reduction[[(Number, Number)]]
empty(): (Number, Number) = (−infinity, 0)join(a : (Number, Number), b : (Number, Number)): (Number, Number) = a MPS b
end
opr BIG MPS [[E]](g : (Reduction[[E]], E → E) → E): E = g(MPSReduction, fn a ⇒ a)(r1 , r2 ) = BIG MPS [ (a, a) | a ← x]r1(c) Efficient implementation for distributive operators
Figure 2: Two-phase behavior of GG library (with examples for “Maximum Prefix Sum”)
7

To tell properties of the arguments to the library, the operator/predicate/function
should extend a set of suitable traits when it has some mathematical properties. For
example, usual plus operator + has distributivity over the maximum operator MAX ,so SumReduction should extend trait LeftDistributiveOver[[MaxReduction]] to tell its
distributivity (Section 5.2.1). Since properties of the given arguments are specified bytraits, checking of applicable conditions of theories are performed by checking typesof the arguments (Section 5.1.2).
For example, for the desugared program shown in Figure 2-(b), the library checks
whether the reduction operator has distributivity. In this case, the library finds
SumReductionZZ32 (operator +) distributes over MaxReductionZZ32 (operator MAX),
since SumReductionZZ32 extends LeftDistributiveOver[[MaxReductionZZ32]]. Thus,
the library uses the efficient implementation shown in Figure 2-(c) to perform thenested reduction of the program. This efficient implementation is given by Theorem 15 in Section 4.

8

3

A Collection of GGenerators with Example Problems

This section gives a collection of GGenerators and their example applications. More examples
may be found in [Bir01, SHTO00, SHT01, Zha02, Zan92, Jeu93].
Notation in this section follows that of Haskell [Bir98].
Note that not all of GGenerators shown in this section are currently implemented in GG
library.

3.1

Preliminaries

In this section, some functions are defined to describe example problems, and a class of problem specifications called “generate-and-test” is introduced. Also, some predicates used in thefollowing examples are defined in this section.
3.1.1

Basic Functions

We use the following functions to define specification of problems.
map f [x1 , x2 , . . . , xn ]reduce (⊕) [x1 , x2 , . . . , xn ]hom (⊕, f ) [x1 , x2 , . . . , xn ]last [x1 , x2 , . . . , xn ]head [x1 , x2 , . . . , xn ]length [x1 , x2 , . . . , xn ]filter p [x1 , x2 , . . . , xn ]

=
=
=
=
=
=
=

[f x1 , f x2 , . . . , f xn ]x1 ⊕ x2 ⊕ · · · ⊕ xn
f x1 ⊕ f x2 ⊕ · · · ⊕ f xnxnx1
n[xi1 , xi2 , . . . , xim ] where p (xij ) = True

Function map f applies the given function f to every element of the input list. Function
reduce (⊕) performs ‘summation’ of the input list with the given associative binary operator⊕. Function hom (⊕, f ) performs reduce (⊕) after map f , i.e., hom (⊕, f ) = reduce (⊕) ◦ map f .
Function last takes the last element of the input, while function head takes the head. Function
length returns the length of the input. Function filter p removes every element that does notsatisfy the given predicate p.
Maximum and minimum are denoted by the following arrows.
a↑b =
=
a↓b =
=

a
b
a
b

if a ≥ botherwise
if a ≤ botherwise

For a function f , ↑f and ↓f are defined as follows.
a ↑f b ==a ↓f b =
=

a
b
a
b

if f a ≥ f botherwise
if f a ≤ f botherwise

For a tuple of any length, projection functions πi are defined as follows.
πi (a1 , . . . , ai , . . . , an ) = ai
For instance, π1 (a, b) = a and π2 (a, b) = b.
9

3.1.2

GGenerators and Generate-and-test Specification

A GGenerator is a function to generate a nested list. For example, inits shown in the next section
generates a nested list of which element is a prefix of an input list, as shown in Section 3.3 andSection 4.3.1.
Fortress’ generator abstracts generation of a flat data structure, i.e., a flat list, and reduction
on the flat structure. Our GGenerator extends the generator to abstract generation of a nested
data structure, i.e., a list of lists, and nested reductions on the nested data structure. Of course,
Fortress’ generator can perform nested reductions by nested use of Generators. The advantage
of our GGenerator’s nested reductions is that a GGenerator can use relationship between thepair of reductions to perform the reductions with specialized efficient implementation given bya collection of theories on GGenerators.
We focus on problems described with generate-and-test specification. The general form of
the generate-and-test specification with GGenerators is shown below.
hom (⊕, f ) ◦ map (hom (⊗, g)) ◦ filter p ◦gg
Here, gg is one instance of GGenerators, which generates a nested list, and the generated nested
list is consumed by the nested reductions, hom (⊕, f ) for the outer list and hom (⊗, g) for the
inner lists, after filtered with predicate p.
For example, simple nested reductions with two binary operators ⊕ and ⊗ for a GGenerator
gg can be described in the generate-and-test specification as follows.
reduce (⊕) ◦ map (reduce (⊗)) ◦gg = hom (⊕, id) ◦ map (hom (⊗, id)) ◦ filter true ◦gg
Here, true is the predicate returning always True. The equality of the left hand side (thesimple nested reductions) and the right hand side (the generate-and-test specification) is easily
shown. First, by the definition of reduce (⊕), we get hom (⊕, id) = reduce (⊕) and hom (⊗, id) =reduce (⊗). Next, by the definition of filter p, filter true = id since true returns always True.
Examples shown in the following sections are instances of the generate-and-test specification
with GGenerators.
3.1.3

Predicates for Examples

The following predicates on lists are used in examples shown in the following sections.
Predicate ascending returns True if the given list is ascending (i.e., each element is smaller
than the following element). For example, applying ascending to a sorted list [−2, 4, 5] we getascending([−2, 4, 5]) = True, while ascending([3, 6, 2]) = False since 6 is not smaller than 2.
Predicate descending returns True if the given list is descending (i.e., each element is bigger
than the following element). For example, applying descending to a descendingly sorted list
[5, 3, 0] we get descending([5, 3, 0]) = True, while ascending([1, 9, 7]) = False since 1 is not bigger
than 9.
Predicate smooth c returns True if a difference between any successive elements in the given
list is less than or equal to c. For example, smooth 2 ([6, 5, 7]) = True, since both of differences
1 = |6 − 5| and 2 = |5 − 7| are less than or equal to 2. But, smooth 2 ([6, 5, 8]) = False because
the difference 3 = |5 − 8| is greater than 2.
Predicate high returns True if the maximum element of the given list is greater than thelength of the list. For example, high([1, 4, 3]) = True, since the maximum element 4 is greaterthan the length of the list, i.e., 3. But, high([1, 4, 3, 2]) = False because the maximum element
4 is not greater than the length of the list 4.
10

3.3

GGenerator inits

GGenerator inits generates prefixes of an input list. For example, applying inits to [1, 3, 1, −7, 2, 4]
we get the following nested list.
inits [1, 3, 1, −7, 2, 4] = [[1], [1, 3], [1, 3, 1], [1, 3, 1, −7], [1, 3, 1, −7, 2], [1, 3, 1, −7, 2, 4]]Here, each element of the resulting list is a prefix of the given list.
3.3.1

Prefix Sums

The most famous application of inits is prefix sums, which has many applications [Ble90]. The
statement is as follows.
Example 1 (Prefix Sums). Given a list and an associative binary operator, find sums for all
prefixes of the given list.
For example, prefix sums of [1, 3, 1, −7, 2, 4] with operator ⊕ is [1, 1 ⊕ 3, 1 ⊕ 3 ⊕ 1, 1 ⊕ 3 ⊕1 ⊕ −7, 1 ⊕ 3 ⊕ 1 ⊕ −7 ⊕ 2, 1 ⊕ 3 ⊕ 1 ⊕ −7 ⊕ 2 ⊕ 4]. Using inits, prefix sums are easily obtainedby applying reduction with ⊕ to all prefixes generated by inits.
map (reduce (⊕)) (inits [1, 3, 1, −7, 2, 4])= map (reduce (⊕)) [[1], [1, 3], [1, 3, 1], [1, 3, 1, −7], [1, 3, 1, −7, 2], [1, 3, 1, −7, 2, 4]]= [1, 1 ⊕ 3, 1 ⊕ 3 ⊕ 1, 1 ⊕ 3 ⊕ 1 ⊕ −7, 1 ⊕ 3 ⊕ 1 ⊕ −7 ⊕ 2, 1 ⊕ 3 ⊕ 1 ⊕ −7 ⊕ 2 ⊕ 4]
Sample fortress code for prefix sums with the usual plus operator + is shown below.
x = h 1, 3, 1, −7, 2, 4 iPprefix sums = h y | y ← inits x i

A related theory is found in Section 4.3.1. Related implementation on GG library is found in
Section 5.3.1.
3.3.2

Maximum Prefix Sum

The maximum prefix sum problem is one of optimization problems on sequences. Its statement
is as follows.
Example 2 (Maximum Prefix Sum). Given a list, find the maximum sum of a prefix of thegiven list.
For example, the maximum prefix sum of [1, 3, 1, −7, 2, 4] is 5 since its prefix sums (with theusual plus operator +) are [1, 4, 5, −2, 0, 4]. So, using inits we can get the maximum prefix sum
easily by applying reduction with the maximum operator ↑ for the prefix sums.
reduce (↑) (map (reduce (+)) (inits [1, 3, 1, −7, 2, 4]))
= reduce (↑) (map (reduce (+)) [[1], [1, 3], [1, 3, 1], [1, 3, 1, −7], [1, 3, 1, −7, 2], [1, 3, 1, −7, 2, 4]])
= reduce (↑) ([1, 1 + 3, 1 + 3 + 1, 1 + 3 + 1 + −7, 1 + 3 + 1 + −7 + 2, 1 + 3 + 1 + −7 + 2 + 4])=5
Sample fortress code for the maximum prefix sum is shown below.
x = h 1, 3, 1, −7, 2, 4 i(∗ with complemension∗)P
mis = BIG MAX h y | y ← inits x i(∗ with for-loop ∗)m : Z32 = −infinity
for y P← inits x do
s= yatomic mMAX = s
end

11A related theory is found in Section 4.3.2. Related implementation on GG library is found in
Section 5.3.2.
3.3.3

Maximum p-Prefix Sum

This is a variant of the maximum prefix sum problem. The statement is as follows.
Example 3 (Maximum p-Prefix Sum). Given a list and a predicate p, find the maximum sumof its prefix satisfying the given predicate p.
For example, the maximum ascending-prefix sum of [1, 3, 1, −7, 2, 4] is 4 since its ascending
prefixes are [1] and [1, 3]. Using inits and filter , we can get the maximum ascending-prefix sum
easily as follows.
reduce (↑) (map (reduce (+)) (filter ascending (inits [1, 3, 1, −7, 2, 4])))= reduce (↑) (map (reduce (+)) (filter ascending [[1], [1, 3], [1, 3, 1], [1, 3, 1, −7],
[1, 3, 1, −7, 2], [1, 3, 1, −7, 2, 4]]))= reduce (↑) (map (reduce (+)) [[1], [1, 3]])= reduce (↑) [1, 1 + 3]
=4
Sample fortress code for the maximum ascending-prefix sum is shown below.
x = h 1, 3, 1, −7, 2,P
4i
mais = BIG MAX h y | y ← inits x, ascending(y) i

A related theory is found in Section 4.3.3. Related implementation on GG library is found in
Section 5.3.3.

3.4

GGenerator tails

GGenerator tails generates suffixes of an input list. For example, applying tails to [1, 3, 1, −7, 2, 4]
we get the following nested list.
tails [1, 3, 1, −7, 2, 4] = [[1, 3, 1, −7, 2, 4], [3, 1, −7, 2, 4], [1, −7, 2, 4], [−7, 2, 4], [2, 4], [4]]Here, each element of the resulting list is a suffix of the given list.
3.4.1

Suffix Sums

The most famous application of tails is suffix sums, which is converse computation of prefixsums shown in Section 3.3.1. The statement is as follows.
Example 4 (Suffix Sums). Given a list and an associative binary operator, find sums for all
suffixes of the given list.
For example, suffix sums of [1, 3, 1, −7, 2, 4] with operator ⊕ is [1 ⊕ 3 ⊕ 1 ⊕ −7 ⊕ 2 ⊕ 4, 3 ⊕1 ⊕ −7 ⊕ 2 ⊕ 4, 1 ⊕ −7 ⊕ 2 ⊕ 4, −7 ⊕ 2 ⊕ 4, 2 ⊕ 4, 4] . Using tails, we can get suffix sums easily
by applying reduction with ⊕ to all suffixes generated by tails.
map (reduce (⊕)) (tails [1, 3, 1, −7, 2, 4])= map (reduce (⊕)) [[1, 3, 1, −7, 2, 4], [3, 1, −7, 2, 4], [1, −7, 2, 4], [−7, 2, 4], [2, 4], [4]]= [1 ⊕ 3 ⊕ 1 ⊕ −7 ⊕ 2 ⊕ 4, 3 ⊕ 1 ⊕ −7 ⊕ 2 ⊕ 4, 1 ⊕ −7 ⊕ 2 ⊕ 4, −7 ⊕ 2 ⊕ 4, 2 ⊕ 4, 4]Sample fortress code for suffix sums with the usual plus operator + is shown below.
x = h 1, 3, 1, −7, 2, 4 iP
suffix sums = h y | y ← tails x i

A related theory is found in Section 4.4.1. Related implementation on GG library is found in
Section 5.4.1.
12

3.4.2

Maximum Suffix Sum

The maximum suffix sum problem is one of optimization problems on sequences. Its statement
is as follows.
Example 5 (Maximum Suffix Sum). Given a list, find the maximum sum of a suffix of thegiven list.
For example, the maximum suffix sum of [1, 3, 1, −7, 2, 4] is 6 since its suffix sums (with theusual plus operator +) are [4, 3, 0, −1, 6, 4]. So, using tails we can get the maximum suffix sum
easily by applying reduction with the maximum operator ↑ for suffix sums.
reduce (↑) (map (reduce (+)) (tails [1, 3, 1, −7, 2, 4]))
= reduce (↑) (map (reduce (+)) [[1, 3, 1, −7, 2, 4], [3, 1, −7, 2, 4], [1, −7, 2, 4], [−7, 2, 4], [2, 4], [4]]= reduce (↑) [1 + 3 + 1 + −7 + 2 + 4, 3 + 1 + −7 + 2 + 4, 1 + −7 + 2 + 4, −7 + 2 + 4, 2 + 4, 4]=6
Sample fortress code for the maximum suffix sum is shown below.
x = h 1, 3, 1, −7, 2, 4 i(∗ with complemension∗)P
mts = BIG MAX h y | y ← tails x i(∗ with for-loop ∗)m : Z32 = −infinity
for y P← tails x dos=yatomic mMAX = s
end

A related theory is found in Section 4.4.2. Related implementation on GG library is found in
Section 5.4.2.
3.4.3

Maximum p-Suffix Sum

This is a variant of the maximum suffix sum problem. The statement is as follows.
Example 6 (Maximum p-Suffix Sum). Given a list and a predicate p, find the maximum sumof its suffix satisfying the given predicate p.
For example, the maximum ascending-suffix sum of [1, 3, 1, −7, 2, 4] is 6 since its ascending
suffixes are [−7, 2, 4], [2, 4] and [4]. Using tails and filter , we can get the maximum ascendingsuffix sum easily as follows.
reduce (↑) (map (reduce (+)) (filter ascending (tails [1, 3, 1, −7, 2, 4])))= reduce (↑) (map (reduce (+)) (filter ascending [[1, 3, 1, −7, 2, 4], [3, 1, −7, 2, 4],[1, −7, 2, 4], [−7, 2, 4], [2, 4], [4]]))= reduce (↑) (map (reduce (+)) [[−7, 2, 4][2, 4], [4], ])= reduce (↑) [−7 + 2 + 4, 2 + 4, 4]=6
Sample fortress code for the maximum ascending-suffix sum is shown below.
x = h 1, 3, 1, −7, 2,P
4i
mats = BIG MAX h y | y ← tails x, ascending(y) i

A related theory is found in Section 4.4.3. Related implementation on GG library is found in
Section 5.4.3.
13

3.5

GGenerator segs

GGenerator segs generates segments (continuous subsequences) of an input list. The segments
are listed in the lexicographic order. For example, applying segs to [3, 2, −7, 4, 2] we get thefollowing nested list.
segs [3, 2, −7, 4, 2] = [[3], [3, 2], [3, 2, −7], [3, 2, −7, 4], [3, 2, −7, 4, 2], [2], [2, −7],
[2, −7, 4], [2, −7, 4, 2], [−7], [−7, 4], [−7, 4, 2], [4], [4, 2], [2]]3.5.2

Maximum Segment Sum

The most famous application of segs is maximum segment sum problem [Bir87,Jeu93,SHTO00],
which is one of optimization problems on sequences. The statement is as follows.
Example 7 (Maximum Segment Sum). Given a list, find the maximum sum of a segment of
the given list.
For example, the maximum segment sum of [3, 2, −7, 4, 2] is 6 that is the sum of its segment[4, 2]. We can get the maximum segment sum of the given list using segs as follows. First, we
generate all segments of the given list by segs. Then, we apply reduction with the usual plus
operator + to generated segments to get all segment sums. Finally, applying reduction withmaximum-operator to those segment sums, we get the maximum segment sum of the given list.
reduce (↑) (map (reduce (+)) (segs [3, 2, −7, 4, 2]))
= reduce (↑) (map (reduce (+)) [[3], [3, 2], [3, 2, −7], [3, 2, −7, 4], [3, 2, −7, 4, 2], [2], [2, −7],
[2, −7, 4], [2, −7, 4, 2], [−7], [−7, 4], [−7, 4, 2], [4], [4, 2], [2]])= reduce (↑) [3, 5, −2, 2, 4, 2, −5, −1, 1, −7, −3, −1, 4, 6, 2]=6
Sample fortress code for the maximum prefix sum is shown below.
x = h 3, 2, −7, 4, 2 i(∗ with complemension∗)P
mss = BIG MAX h y | y ← segs x i(∗ with for-loop ∗)m : Z32 = −infinity
for y P← segs x do
s= yatomic mMAX = s
end

A related theory is found in Section 4.5.2. Related implementation on GG library is foundin Section 5.5.2.
3.5.3

Maximum p-Segment Sum

This is a variant of the maximum segment sum problem. The statement is as follows.
Example 8 (Maximum p-Segment Sum). Given a list and a predicate p, find the maximum
sum of its segment satisfying the given predicate p.
For example, the maximum ascending-segment sum of [3, 2, −7, 4, 2] is 4 since its ascendingsegments are all singletons. The maximum descending-segment sum of [3, 2, −7, 4, 2] is 6 since14

its descending-segments are [3, 2], [3, 2, −7], [2, −7], [4, 2] and singletons. Using segs and filter ,we can get the maximum descending-segment sum easily as follows.
reduce (↑) (map (reduce (+)) (filter descending (segs [3, 2, −7, 4, 2])))= reduce (↑) (map (reduce (+)) (filter descending [[3], [3, 2], [3, 2, −7], [3, 2, −7, 4], [3, 2, −7, 4, 2],[2], [2, −7], [2, −7, 4], [2, −7, 4, 2], [−7], [−7, 4],[−7, 4, 2], [4], [4, 2], [2]]))= reduce (↑) (map (reduce (+)) [[3], [3, 2], [3, 2, −7], [2], [2, −7], [−7], [4], [4, 2], [2]])= reduce (↑) [3, 5, −2, 2, −5, −7, 4, 6, 2]=6
Sample fortress code for the maximum descending-segment sum is shown below.
x = h 3, 2, −7, 4, 2 iP
mdss = BIG MAX h y | y ← segs x, descending(y) i

A related theory is found in Section 4.5.3. Related implementation on GG library is found in
Section 5.5.3.
3.5.4

Longest-p Segment

Longest-p segment problem [Zan92] is also one of optimization problems on sequences. Its
statement is as follows.
Example 9 (Longest-p Segment). Given a list and a predicate, find the longest segment (continuous subsequence) of the list that satisfies the predicate.
For example, the longest-ascending segment of [3, 2, −7, 4, 2] is [−7, 4], while the longestdescending segment is [3, 2, −7]. There are many instances of longest-p segment for various
predicates. The longest segment satisfying a given predicate p is obtained by using segs andfiltering. Some instances are shown below.
The longest ascending segment of an input list is obtained by using the predicate ascending.
reduce (↑length ) (filter ascending (segs [3, 2, −7, 4, 2]))
= reduce (↑length ) (filter ascending (segs [[3], [3, 2], [3, 2, −7], [3, 2, −7, 4], [3, 2, −7, 4, 2],[2], [2, −7], [2, −7, 4], [2, −7, 4, 2], [−7], [−7, 4],[−7, 4, 2], [4], [4, 2], [2]]))= reduce (↑length ) [[3], [2], [−7], [−7, 4], [4], [2]]= [2, 5]The longest smooth segment of an input list is obtained by using the predicate smooth c .
reduce (↑length ) (filter smooth 4 (segs [3, 2, −7, 4, 2]))
= reduce (↑length ) (filter smooth 4 (segs [[3], [3, 2], [3, 2, −7], [3, 2, −7, 4], [3, 2, −7, 4, 2],[2], [2, −7], [2, −7, 4], [2, −7, 4, 2], [−7], [−7, 4],[−7, 4, 2], [4], [4, 2], [2]]))= reduce (↑length ) [[3], [3, 2], [2], [−7], [4], [4, 2], [2]]= [3, 2]The longest high segment of an input list is obtained by using predicate high.
reduce (↑length ) (filter high (segs [3, 2, −7, 4, 2]))
= reduce (↑length ) (filter high (segs [[3], [3, 2], [3, 2, −7], [3, 2, −7, 4], [3, 2, −7, 4, 2], [2], [2, −7],
[2, −7, 4], [2, −7, 4, 2], [−7], [−7, 4], [−7, 4, 2], [4], [4, 2], [2]]))= reduce (↑length ) [[3], [3, 2], [2], [4], [4, 2], [2]]= [3, 2]
Sample fortress code for the longest p-segment is shown below. The code computes thelongest p-segment with its length.
15x = h 3, 2, −7, 4, 2 i
las = BIG MAX h (length y, y) | y ← segs x, ascending(y) i
lss = BIG MAX h (length y, y) | y ← segs x, smooth(4, y) i
lhs = BIG MAX h (length y, y) | y ← segs x, high y i

3.6

GGenerator subs

GGenerator subs generates all subsequences (sub-lists) of an input list. Generated subsequences
are listed in the lexicographic order. For example, applying subs to [2, 5, −3, 4] we get thefollowing nested list.
subs [2, 3, −3, 4] = [[2], [2, 3], [2, 3, −3], [2, 3, −3, 4], [2, 3, 4], [2, −3], [2, −3, 4], [2, 4],[3], [3, −3], [3, −3, 4], [3, 4], [−3], [−3, 4], [4]]3.6.1

Longest-p Subsequence

Longest-p subsequence problem is one of optimization problems on sequences [Jeu93].
Example 10 (Longest-p Subsequence). Given a list and a predicate, find the longest subsequence of the list that satisfies the predicate.
For example, the longest-ascending subsequnce of [2, 3, −3, 4] is [2, 3, 4], while the longestdescending subsequnce is [2, −3]. There are many instances of longest-p subsequnce for various
predicates. The longest subsequnce satisfying a given predicate p is obtained by using subs andfilter . Some instances are shown blow.
The longest ascending subsequence of an input list is obtained by using subs and the predicate
ascending.
reduce (↑length ) (filter ascending (subs [2, 3, −3, 4]))
reduce (↑length ) (filter ascending [[2], [2, 3], [2, 3, −3], [2, 3, −3, 4], [2, 3, 4], [2, −3], [2, −3, 4], [2, 4],[3], [3, −3], [3, −3, 4], [3, 4], [−3], [−3, 4], [4]])= reduce (↑length ) [[2], [2, 3], [2, 3, 4], [2, 4], [3], [3, 4], [−3], [−3, 4], [4]]= [2, 3, 4]
The longest descending subsequence of an input list is obtained by using subs and the predicate
descending.
reduce (↑length ) (filter descending (subs [2, 3, −3, 4]))
reduce (↑length ) (filter descending [[2], [2, 3], [2, 3, −3], [2, 3, −3, 4], [2, 3, 4], [2, −3], [2, −3, 4],[2, 4], [3], [3, −3], [3, −3, 4], [3, 4], [−3], [−3, 4], [4]])= reduce (↑length ) [[2], [2, −3], [3], [3, −3], [−3], [4]]= [2, −3]
Sample fortress code for longest-ascending subsequence is shown below. The code computes
the longest p-subsequence with its length.
x = h2, 5, −3, 4 i
las = BIG MAX h (length y, y) | y ← subs x, ascending y i
lds = BIG MAX h (length y, y) | y ← subs x, descending y i

3.6.2

0-1 Knapsack Problem

Example 11 (0-1 Knapsack Problem). Given a list of items (pairs of value and weight) and aknapsack of fixed capacity, find a subset of items that has the maximum sum of values and its
sum of weight is less than or equals to the capacity.
16

For example, given four items [(2, 1), (5, 3), (1, 1), (4, 2)] (first element of a pair is value andthe second is weight) and a knapsack of capacity 4, the solution (a set of items to be put
into the knapsack) is [(2, 1), (5, 3)]. This solution is given as follows. First, we generate every
combination of items by subs. Then, using filtering, we throw away combinations of whichweight is greater than the capacity. Finally, we take the combination that have the maximum
sum of values.
reduce (↑reduce (+) ◦ map π1 ) (filter ((≤ 4)◦(reduce (+))◦(map π2 )) (subs [(2, 1), (5, 3), (1, 1), (4, 2)]))= reduce (↑reduce (+) ◦ map π1 ) [[(2, 1)], [(2, 1), (5, 3)], [(2, 1), (1, 1)], [(2, 1), (1, 1), (4, 2)],[(2, 1), (4, 2)], [(5, 3)], [(5, 3), (1, 1)], [(1, 1)], [(1, 1), (4, 2)], [(4, 2)]]= [(2, 1), (5, 3)]
Sample fortress code for 0-1 knapsack problem is shown below.
x = h(2, 1), (5, 3), (1, 1), (4, 2)i
capa = 4
PP
pf = BIG MAX h ( h first a | a ← yi, y) | y ← subs x, h second a | a ← yi ≤ capai

3.7

GGenerator parts

GGenerator parts generates all partitions of an input list. For example, applying parts to[2, 5, −3] we get the following nested list.
parts [2, 5, −3] = [[[2, 5, −3]], [[2, 5], [−3]], [[2], [5, −3]], [[2], [5], [−3]]]
3.7.1

Smallest All Ascending Partition

Example 12 (Smallest All Ascending Partition). Given a list, find the smallest partition inwhich each part is ascending.
For example, smallest all ascending partition of [2, 5, −3] is [[2, 5], [−3]]. This solution is
obtained by using parts and filter as shown below.
reduce (↓length ) (filter ((reduce (∧)) ◦ (map ascending)) (parts [2, 5, −3]))reduce (↓length ) (filter ((reduce (∧)) ◦ (map ascending)) [[[2, 5, −3]], [[2, 5], [−3]], [[2], [5, −3]],[[2], [5], [−3]]])= reduce (↓length ) [[[2, 5], [−3]], [[2], [5], [−3]]]= [[2, 5], [−3]]Sample fortress code for all ascending partition is shown below. The code computes shortestpartition with its length.
x = h2, 5, −3i
las = BIG MIN h (length y, y) | y ← parts x, BIG ∧ h ascending a | a ← y i i

3.7.2

Paragraph Formatting

Example 13 (Paragraph Formatting). Given a list of lengths of words and a length of a line,
find the minimum partition of the list so that a sum of each part is less or equals to the given
length of a line.
For example, lengths of words are [2, 5, 3, 4] and the length of the line is 7, the minimum
partition is [[2, 5], [3, 4]], where sum of each part is equal to 7. This solution is obtained by usingparts, filtering and reduction.
reduce (↓length ) (filter ((≤ 7) ◦ (reduce (+)) (parts [2, 5, 3, 4]))
= reduce (↓length ) [[[2, 5], [3, 4]], [[2, 5], [3], [4]], [[2], [5], [3, 4]], [[2], [5], [3], [4]]]= [[2, 5], [3, 4]]Sample fortress code for paragraph formatting is shown below.
17x = h2, 5, 3, 4iline width = 7
P
pf = BIG MIN h (length y, y) | y ← parts x, BIG ∧ h a ≤ line width | a ← y i i

3.8

GGenerator perm

GGenerator perm generates all permutations of an input list. For example, applying perm to[2, 5, −3] we get the following nested list.
perm [2, 5, −3] = [[2, 5, −3], [2, −3, 5], [5, 2, −3], [5, −3, 2], [−3, 2, 5], [−3, 5, 2]]
3.8.1

Sorting

Sorting can be performed by using perm as follows.
head (filter ascending (perm [2, 5, −3]))= head (filter ascending [[2, 5, −3], [2, −3, 5], [5, 2, −3], [5, −3, 2], [−3, 2, 5], [−3, 5, 2]])= head [[−3, 2, 5]]= [−3, 2, 5]
The program head ◦ filter ascending ◦perm describes clearly the specification of sorting, although
this program is, of course, extremely inefficient by naive execution.
Sample fortress code for the sorting is shown below.
x = h2, 5, −3isorted x = head h ys | ys ← perms x, ascending ys i18

4

A Collection of Theories

Theories given in this section are used to dispatch efficient implementation against user programsof the generate-and-test specification. Preliminaries for formal discussion of theories are shownat the beginning of this section. The collection of theories of GGeneratorsfollows it.
Notation in this section follows that of Haskell [Bir98] and BMF (Bird-Meertens formalism) [Bir87, Ski90].

4.1

Preliminaries

This section gives formal definitions and concise notations of functions for formal manipulationof specifications. Intuitive definitions of those functions are found in Section 3.1, in which someof them have more human-readable names.
We assume that binary operators in this section, such as ⊕ and ⊗, are associative, unlessotherwise noted. The identity of binary operator ⊕ is denoted by ı⊕ .
A list is a sequence of elements a1 , a2 , . . . , an denoted by [a1 , a2 , . . . , an ]. Function [·] takes
an element to make a singleton list, i.e., [·] a = [a]. Concatenation of two lists is denoted bybinary operator ++. An empty list, which is the identity of ++, is denoted by [ ].
Binary operators ≫ and ≪ used in the following sections are defined as follows.
a ≫ b = b, a ≪ b = a
4.1.1

Homomorphism and Auxiliary Functions

Homomorphisms are basic functions defined on lists as follows.
([⊕, f ]) (x ++ y) = ([⊕, f ]) x ⊕ ([⊕, f ]) y([⊕, f ]) [a]= f a
Homomorphism ([⊕, f ]) applies the given function f to every element of the input list, and then
combines the results using the given associative binary operator ⊕. Since a homomorphism
is completely specified by function f and associative binary operator ⊕, a homomorphism isdenoted by ([⊕, f ]). Homomorphism is the basis of parallel computation, since associativity ofthe operator ⊕ gives us correct balanced divide-and-conquer parallel computation of homomorphism.
Intuitive definition of homomorphism ([⊕, f ]) is shown below.
([⊕, f ]) [x1 , x2 , . . . , xn ] = f x1 ⊕ f x2 ⊕ · · · ⊕ f xn
Since ⊕ has associativity, the above result of the homomorphism can be obtained by the following
computation. First, the input list [x1 , x2 , . . . , xn ] is divided into two parts [x1 , x2 , . . . , xn/2 ] and[xn/2+1 , xn/2+2 , . . . , xn ]. Next, the homomorphism ([⊕, f ]) is applied to each of the parts tocompute in parallel the partial results f x1 ⊕ f x2 ⊕ · · · ⊕ f xn/2 and f xn/2+1 ⊕ f xn/2+2 ⊕· · · ⊕ f xn . Then, those partial results are combined by the operator ⊕ to get the result for thewhole input. Repeatedly applying the above division and combination to computation of thepartial results, we get balanced divide-and-conquer parallel computation of the homomorphism([⊕, f ]).
Two basic specializations of homomorphism are f ∗ and ⊕/ defined below.
f ∗ = ([++, [·] ◦ f ])⊕/ = ([⊕, id])
Function f ∗ applies the given function f to every element of the given list. Function ⊕/ performs‘summation’ of the given list with the given associative binary operator ⊕. One of the most19

important relations between these specializations and homomorphism is the following equation,
which shows that homomorphism ([⊕, f ]) can be decomposed into f ∗ and ⊕/.
([⊕, f ]) = ⊕/ ◦ f ∗Intuitive definitions of f ∗ and ⊕/ are shown below.
f ∗ [x1 , x2 , . . . , xn ] = [f x1 , f x2 , . . . , f xn ]⊕/ [x1 , x2 , . . . , xn ] = x1 ⊕ x2 ⊕ · · · ⊕ xn
Some functions are defined with homomorphism.
last = ([≫, id])head = ([≪, id])p⊳
= ([++, f ])

where f x = if p x then [x] else [ ]Function last takes the last element of the given list, while function head takes the head of thegiven list. Function p ⊳ filters the given list so that the resulting list contains only elements
satisfying the given predicate p. Intuitive definitions of the above function are given as follows.
last [x1 , x2 , . . . , xn ] = xn
head [x1 , x2 , . . . , xn ] = x1
p ⊳ [x1 , x2 , . . . , xn ]= [xi1 , xi2 , . . . , xim ] where p (xij ) = True
Correspondence between the above functions and those in Section 3.1 is shown below.
map f = f ∗, reduce (⊕) = ⊕/, hom (⊕, f ) = ([⊕, f ]), filter p = p ⊳For a tuple of any length, projection functions πn are defined as follows.
πi (a1 , . . . , ai , . . . , an ) = ai
For instance, π1 (a, b) = a and π2 (a, b) = b.
4.1.2

GGenerators and Generate-and-test Specification

A GGenerator is a function to generate a nested list. For example, inits generates a nested listof which element is a prefix of a given list, as shown in Section 3.3 and Section 4.3.1.
We focus on problems described with generate-and-test specification. The general form of
the generate-and-test specification is shown below.
([⊕, f ]) ◦ ([⊗, g])∗ ◦ p ⊳ ◦gg
Here, gg is one instance of GGenerators, which generates a nested list, and the generated nested
list is consumed by the nested reductions, ([⊕, f ]) for the outer list and ([⊗, g]) for the inner lists,
after filtered with predicate p.
For example, simple nested reductions ⊕/ ◦ ⊗/∗ for a GGenerator gg can be described in
the generate-and-test specification as follows.
⊕/ ◦ ⊗/∗ ◦ gg = ([⊕, id]) ◦ ([⊗, id])∗ ◦ true ⊳ ◦gg
Here, true is the predicate returning always True. The equality of the left hand side and the righthand side is easily shown. First, by the definition of ⊕/, we get ([⊕, id]) = ⊕/ and ([⊗, id]) = ⊗/.
Next, by the definition of p ⊳, true ⊳ = id since true returns always True.
Theories shown in the following sections give efficient implementations of subclasses of thegenerate-and-test specification.
Related implementation on GG library is found in Section 5.1.1.
20

4.2

Properties on Reduction Operators and Predicates

This section defines properties on operators and predicates for deriving efficient implementation.
4.2.1

Properties on Reduction Operators

Associativity is the basis of parallel computation of homomorphism since it guarantees correctness of balanced divide-and-conquer parallel computation of homomorphism.
Definition 1 (Associativity). Binary operator ⊕ is said to be associative if the following equation holds for all a, b and c.
a ⊕ (b ⊕ c) = (a ⊕ b) ⊕ cDistributivity plays an important role in deriving efficient implementation for nested reductions. Basically, distributivity guarantees efficient reuse of partial results.
Definition 2 (Left-Distributivity). Binary operator ⊗ is said to be left-distributive over ⊕ if
the following equation holds for all a, b and c.
a ⊗ (b ⊕ c) = (a ⊗ b) ⊕ (a ⊗ c)
Definition 3 (Right-Distributivity). Binary operator ⊗ is said to be right-distributive over ⊕if the following equation holds for all a, b and c.
(a ⊕ b) ⊗ c = (a ⊗ c) ⊕ (b ⊗ c)
Definition 4 (Distributivity). Binary operator ⊗ is said to be distributive over ⊕ if ⊗ is leftand right-distributive over ⊕, i.e. the following equations hold for all a, b and c.
a ⊗ (b ⊕ c) = (a ⊗ b) ⊕ (a ⊗ c)(a ⊕ b) ⊗ c = (a ⊗ c) ⊕ (b ⊗ c)Commutativity is used to change the order of computation to achieve good efficiency, as
well as distributivity.
Definition 5 (Commutativity). Binary operator ⊕ is said to be commutative if the following
equation holds for all a and b.
a⊕b=b⊕aFor example, well-known binary operators + (plus), × (times), ↑ (maximum), and ↓ (minimum) are all associative and commutative. Moreover, × distributes over +, and + distributes
over ↑ or ↓. Concatenation operator ++ is associative, but not commutative. Function f ∗ isleft-distributive over ++, since f ∗ (x ++ y) = (f ∗ x) ++ (f ∗ y). Distributivity of f ∗ is often usedin the following derivations of efficient implementations.
Related implementation on GG library is found in Section 5.2.1.
4.2.2

Properties on Predicates

The following closure properties are defined on predicates for deriving efficient implementation [Zan92, Jeu93].
Definition 6 (Prefix-Closed). Predicate p is said to be prefix-closed if the following equation
holds for all x and y.
p (x ++ y) ⇒ p (x)21Definition 7 (Suffix-Closed). Predicate p is said to be suffix-closed if the following equation
holds for all x and y.
p (x ++ y) ⇒ p (y)Definition 8 (Segment-Closed). Predicate p is said to be segment-closed if p is prefix- andsuffix closed, i.e. the following equation holds for all x, y and z.
p (x ++ y ++ z) ⇒ p (y)Definition 9 (Overlap-Closed). Predicate p is said to be overlap-closed if the following equation
holds for all x, y and z.
p (x ++ y) ∧ p (y ++ z) ∧ y 6= [ ] ⇒ p (x ++ y ++ z)
Prefix-closed property plays the most important role in derivation of efficient sequential implementation of segment problems [Zan92, Jeu93]. Other properties are used as auxiliary tools
to improve the derived implementation. However, in derivation of efficient parallel implementation, the pair of segment-closed property and overlap-closed property plays the most importantrole, as shown in the following sections.
A candidate of segment-closed and overlap-closed predicates is given by a relation [Zan92].
Definition 10 (Relational Predicate). Given a relation R, relational predicate pR is defined asfollows.
VpR (x) = {aRb | [a, b] ∈ segments x}

Here, segments x returns a set of segments (contiguous subsequences) of x, i.e., segments x ={ y | u ++ y ++ v = x }. Note that [a, b] ∈ segments x means that a and b are successive elements
in x, since segments x generates all contiguous subsequences of x and [a, b] ∈ segments x takes
such subsequences of length two. Relational predicate pR is true for the given list x, if all
successive elements a and b in x satisfy the relation R, i.e. aRb = True.
Zantema [Zan92] shows that a relational predicate pR is segment-closed and overlap-closed,
but we can also show the converse, i.e., a segment-closed and overlap-closed predicate is arelational predicate. The following lemma shows the relation between relational predicates andsegment-closed and overlap-closed predicates.

Lemma 11 (Relational Predicate). Given predicate p that is true for all singletons and empty
list, the following statements are equivalent.
1. p is segment-closed and overlap-closed.
2. p is relational.
Proof. 2 ⇒ 1) Since p is relational, there exists a relation R and the following equation holds.
^
p (x) = {aRb | [a, b] ∈ segments x}
First, we show that p is segment-closed.
p (x ++ y ++ z)V { unfolding p }{aRb | [a, b] ∈ segments (x ++ y ++ z)}⇒ V { segments y ⊆ segments (x ++y++ z) }{aRb | [a, b] ∈ segments y}={ folding p }
p (y)
=

22

Next, we show that p is overlap-closed.
p (x ++ y) ∧ p (y ++ z) ∧ y 6= [ ]{unfolding
p}
V
V
{aRb
|
[a,
b]
∈
segments
(x
+
+
y)}
∧
{aRb | [a, b] ∈ segments (y ++ z)} ∧ y 6=[ ] y 6= [ ] ⇒{[a, b] | [a, b] ∈ segments (x ++ y)} ∪ {[a, b] | [a, b] ∈ segments (y ++ z)}⇒= {[a, b] | [a, b] ∈ segments (x +
+y+
+ z)}
V
{aRb | [a, b] ∈ segments (x +
+y+
+ z)}
=
{ folding p }p (x ++y++ z)=

1 ⇒ 2) Letting R = {(a, b) | p ([a, b])}, we show p = pR by induction.
For base cases, we have p ([ ]) = p ([a]) = pR ([]) = pR ([a]) = True by assumption.
For induction case, we have p ([a] ++ x) = pR ([a] ++ x) by the following calculation.
p ([a] ++ x)={ segment-closed and overlap-closed }p (x) ∧ p ([a] ++ [head x])={ induction hypothesis and definition of R }pR (x) ∧ aR(head x)={ definition of pR }pR ([a] ++ x)
Thus, p = pR and p is relational.
In the above lemma, we assumed that the predicate p is true for all singletons and empty list
for simplicity. However, we can remove this assumption by letting values of relational predicate
pR in the proof be those of the given predicate p.
Examples of relational predicates are shown below.
ascending (x)descending (x)flat (x)smooth c (x)

=
=
=
=

p< (x)
p> (x)
p= (x)pRc (x) where aRc b = |a − b| ≤ cPredicate ascending is true when the given list is ascendingly sorted, while descending is true
for descendingly sorted lists. Predicate flat is true if the all elements in the given list are thesame. Predicate smooth c is true if the maximum of differences of successive elements is lessthan or equal to c. Especially, flat = smooth 0 .
It is worth mentioning about composition of predicates [Zan92]. Each closure property ofprefix-closed, suffix-closed, segment-closed and overlap-closed is closed under disjunction. Eachclosure property of prefix-closed, suffix-closed, and segment-closed is closed also under conjunction, but overlap-closed property is not closed under conjunction. For example, ascending anddescending are both overlap-closed, but ascending ∨ descending is not overlap-closed since we
can make a counterexample: ascending(x ++ y) ∧ descending(y ++ z) ∧ y 6= [ ] implies neither
ascending(x ++ y ++ z) nor descending(x +
+y+
+ z).
Related implementation on GG library is found in Section 5.2.3. Related examples are foundin Section 3.1.3.

4.3

Theory of inits

This section gives formal definition and theory of GGenerator inits.
23

4.3.1

Formal Definition and Basic Lemmas

First of all, we give a formal definition of inits.
Definition 12 (GGenerator Inits). GGenerator inits is defined with homomorphism as follows.
inits = ([⊕, [·] ◦ [·]]) where x ⊕ y = x ++ ((last x)++)∗ y
The operator ⊕ in the above definition makes a list of initial segments of a list u ++ v fromlists (x and y in the above equation) of initial segments of u and v. Since each initial segmentof u is also an initial segment of u ++ v, x remains in the result. Since each initial segment ofv need to be concatenated with u to become an initial segment of u ++ v, the operator maps((last x)++) (u is the last element of x) to y.
The following two lemmas are well-known lemmas of inits [Bir87].
Lemma 13 (Scan). For any associative binary operator ⊕, the following equation holds.
scan (⊕) = ⊕/∗ ◦ inits
Lemma 14 (Inits-Map Promotion). For function f , the following equation holds.
f ∗∗ ◦ inits = inits ◦ f ∗First lemma gives us a way to compute prefix sums by inits. The second lemma gives us a way
to promote the application of function f through inits. The number of applications of function
f on the left hand side is n(n + 1)/2, while that on the right hand side is n. So, transformationfrom the left hand side to the right hand side improves the efficiency. Also, the lemma enables
us to ignore a function g in the generate-and-test specification ([⊕, f ]) ◦ ([⊗, g])∗ ◦ p ⊳ ◦inits, since
we can replace g with the identity function id and apply g to the input of inits beforehand (ofcourse, we need some tricks to through p ⊳).
A related example problem is found in Section 3.3.1. Related implementation on GG libraryis found in Section 5.3.1.
4.3.2

Theorem for Reduction with Distributive Operators

The following theorem gives efficient parallel implementation of nested reductions for inits when
two reductions have distributivity. One of the most famous problems for which this theorem
is applicable is maximum initial-segment sum problem (also known as maximum prefix sum
problem), which is an instance of maximum marking problems [SHTO00, Bir01]. A related
example problem is found in Section 3.3.2. Related implementation on GG library is found in
Section 5.3.2.
Theorem 15 (Maximum Initial-segment Sum). Provided that ⊕ is associative, and ⊗ is associative and left-distributive over ⊕, the following equation holds.
⊕/ ◦ ⊗/∗ ◦ inits = π1 ◦ ([⊙, pair ])where (i1 , s1 ) ⊙ (i2 , s2 ) = (i1 ⊕ (s1 ⊗ i2 ), s1 ⊗ s2 )pair a = (a, a)

Proof. We show the theorem by induction.
For base case, we have LHS [a] = RHS [a] by the following calculation.
LHS [a]{ LHS }(⊕/ ◦ ⊗/∗ ◦ inits) [a]={ definition of inits, ∗, / }a={ definition of π1 , ([, ]), pair }(π1 ◦ ([⊙, pair ])) [a]={ RHS }RHS [a]=24

For induction case, we have LHS (x ++ y) = RHS (x ++ y) by the following calculation.

=
=
=
=
=
=
=
=
=

LHS (x ++ y){ LHS }(⊕/ ◦ ⊗/∗ ◦ inits) (x ++ y){ definition of function composition, unfolding inits, last (inits x) = x }(⊕/ ◦ ⊗/∗) (inits x ++ (x++)∗ (inits y)){ definition of function composition, ∗ and / }⊕/ (⊗/∗ (inits x)) ⊕ ⊕/ ((⊗/ x⊗)∗(⊗/∗ (inits y))){ distributivity of ⊗ }⊕/ (⊗/∗ (inits x)) ⊕ (⊗/ x ⊗ ⊕/ (⊗/∗ (inits y))){ induction hypothesis }(π1 ◦ ([⊙, pair ])) x ⊕ (⊗/ x ⊗ (π1 ◦ ([⊙, pair ])) y){ ⊗/ x = π2 (([⊙, pair ]) x) (shown below) }(π1 ◦ ([⊙, pair ])) x ⊕ ((π2 (([⊙, pair ]) x)) ⊗ (π1 ◦ ([⊙, pair ])) y){ definition of ⊙ }π1 (([⊙, pair ]) x ⊙ ([⊙, pair ]) y){ definition of ([, ]), function composition }(π1 ◦ ([⊙, pair ])) (x ++ y){ RHS }RHS (x ++ y)Finally, we show that ⊗/ x = π2 (([⊙, pair ]) x). For base case, we have
LHS [a]{ LHS }⊗/[a]={ definition of / }a={ definition of π2 , ([, ]), pair }π2 (([⊙, pair ]) [a])={ RHS }RHS [a]=For induction case, we have

=
=
=
=
=
=

LHS (x ++ y){ LHS }⊗/ (x ++ y){ definition of / }⊗/ x ⊗ ⊗/ y
{ induction hypothesis }π2 (([⊙, pair ]) x) ⊗ π2 (([⊙, pair ]) y){ definition of ⊙ }π2 (([⊙, pair ]) x ⊙ ([⊙, pair ]) y){ definition of ([, ]) }π2 (([⊙, pair ]) (x ++ y)){ RHS }RHS (x ++ y)

Similar proof is also shown in [Gor97].
25

The resulting program (the right hand side) of the theorem uses only one reduction with
the new operator ⊙, while the original program (the left hand side) uses two nested reductions
with inits. The cost of the new operator is proportional to the cost of operators in the original
reductions. So, the resulting program is more efficient than the original program.
The new operator ⊙ is applied to tuples. The first element of a tuple is equal to the resultof the original program. The second element of the tuple is equal to the reduction of the same
input with operator ⊗, which is used to improve efficiency of the program by reusing the partial
results effectively.
4.3.3

Theorem for Filtering with Relational Predicates

The following theorem extends Theorem 15 by allowing filtering with the given predicate. It
gives efficient parallel implementation of nested reductions for inits when two reductions have
distributivity and the predicate is relational. Derivation of efficient sequential implementations
for those programs with filtering is shown in [Zan92,Jeu93]. A related example problem is foundin Section 3.3.3. Related implementation on GG library is found in Section 5.3.3.
Theorem 16 (Maximum p-Initial-segment Sum). Provided that ⊕ is associative, ⊗ is associative and left-distributive over ⊕, and predicate p is relational, the following equation holds.
⊕/ ◦ ⊗/∗ ◦ p ⊳ ◦ inits = π1 ◦ ([⊡, pentuple])where(i1 , s1 , h1 , l1 , p1 ) ⊡ (i2 , s2 , h2 , l2 , p2 ) = (i, s1 ⊗ s2 , h1 ≪ h2 , l1 ≫ l2 , p1 ∧ p2 ∧ p ([l1 , h2 ]))where i = i1 ⊕ if p1 ∧ p ([l1 , h2 ]) then s1 ⊗ i2 else ı⊕
pentuple a = (a, a, a, a, T )Proof. We show the theorem by induction.
For base case, we have
LHS [a]{ LHS }(⊕/ ◦ ⊗/∗ ◦ p ⊳ ◦ inits) [a]={ definition of inits, ∗, / and ⊳, p is true for singleton }a={ definition of π1 , ([, ]), and pentuple }(π1 ◦ ([⊡, pentuple])) [a]={ RHS }RHS [a]=For induction case, we have the following calculation.
LHS (x ++ y){ LHS }(⊕/ ◦ ⊗/∗ ◦ p ⊳ ◦ inits) (x ++ y)={ definition of inits }(⊕/ ◦ ⊗/∗ ◦ p ⊳) (inits x ++ ((x++)∗ (inits y)))={ definition of ⊳, /, and ∗ }(⊕/ ◦ ⊗/∗ ◦ p ⊳ ◦ inits) x ⊕ (⊕/ ◦ ⊗/∗ ◦ p ⊳) ((x++)∗ (inits y))=

To proceed more, we calculate a part of the above equation p ⊳ ((x++)∗ (inits y)) as follows.
p ⊳ ((x++)∗ (inits y))={ p is relational: p (x ++ y) ⇒ p (y) }p ⊳ ((x++)∗ (p ⊳ (inits y)))={ p is relational: p (x ++ y) = p (y) ∧ p (x) ∧ p ([last x, head y]) }if p (x) ∧ p ([last x, head y]) then (x++)∗ (p ⊳ (inits y)) else [ ]26Using this result, we proceed a wider part of the above equation (⊕/ ◦ ⊗/∗ ◦ p ⊳) ((x++)∗ (inits y))
as follows.
(⊕/ ◦ ⊗/∗ ◦ p ⊳) ((x++)∗ (inits y)){ above calculation }(⊕/ ◦ ⊗/∗) (if p (x) ∧ p ([last x, head y]) then (x++)∗ (p ⊳ (inits y)) else [ ])={ distributivity of if-then-else, definition of ∗ and / }if p (x) ∧ p ([last x, head y]) then ⊕/ ((⊗/ x⊗)∗ (⊗/∗ (p ⊳ (inits y))))) else ı⊕={ distributivity of ⊗ }if p (x) ∧ p ([last x, head y]) then ⊗/ x ⊗ ⊕/ (⊗/∗ (p ⊳ (inits y))) else ı⊕=

Now, we resume the suspended calculation for induction case.
LHS (x ++ y){ resume }(⊕/ ◦ ⊗/∗ ◦ p ⊳ ◦ inits) x ⊕ (⊕/ ◦ ⊗/∗ ◦ p ⊳) ((x++)∗ (inits y))= { above calculation }(⊕/ ◦ ⊗/∗ ◦ p ⊳ ◦ inits) x⊗ if p (x) ∧ p ([last x, head y]) then ⊗/ x ⊗ ⊕/ (⊗/∗ (p ⊳ (inits y))) else ı⊕= { induction hypothesis }(π1 ◦ ([⊡, pentuple])) x⊗ if p (x) ∧ p ([last x, head y]) then ⊗/ x ⊗ (π1 ◦ ([⊡, pentuple])) y else ı⊕= { ( , ⊗/ x, head x, last x, p (x)) = ([⊡, pentuple]) x (shown below) }(π1 ◦ ([⊡, pentuple])) x⊗ if (π5 ◦ ([⊡, pentuple])) x ∧ p ([(π4 ◦ ([⊡, pentuple])) x, (π3 ◦ ([⊡, pentuple])) y])then (π2 ◦ ([⊡, pentuple])) x ⊗ (π1 ◦ ([⊡, pentuple])) y else ı⊕= { definition of ⊡ }(π1 ◦ ([⊡, pentuple])) (x ++ y)= { RHS }RHS (x ++ y)=Finally, we show ( , ⊗/ x, head x, last x, p (x)) = ([⊡, pentuple]) x. For base case, we have( , ⊗/ [a], head [a], last [a], p ([a]))={ definition of each function, p is relational }( , a, a, a, T )={ definition of ([, ]) and pentuple }([⊡, pentuple]) [a]For induction case, we have( , ⊗/ (x ++ y), head (x ++ y), last (x ++ y), p (x ++ y))={ definition of each function, p is relational }( , ⊗/ x ⊗ ⊗/ y, head x ≪ head y, last x ≫ head y, p x ∧ p y ∧ p ([head x, last y]))={ definition of ⊡ }( , ⊗/ x, head x, last x, p x) ⊡ ( , ⊗/ y, head y, last y, p y)=

{ induction hypothesis }([⊡, pentuple]) x ⊡ ([⊡, pentuple]) y={ definition of ([, ]) }([⊡, pentuple]) (x ++ y)Thus, we have ( , ⊗/ x, head x, last x, p (x)) = ([⊡, pentuple]) x.
27

The resulting program (the right hand side) of the theorem uses only one reduction with
the new operator ⊡, while the original program (the left hand side) uses two nested reductions
with inits. The cost of the new operator is proportional to the cost of operators in the original
reductions and the application of p. So, the resulting program is more efficient than the original
program.
The new operator ⊡ is applied to pentuples. The first element of a pentuple is equal to theresult of the original program. The second element of the pentuple is equal to the reduction of
the same input with operator ⊗, which is used to improve efficiency of the program by reusing
the partial results effectively. The third and forth elements are the edge elements of the input.
Those edge elements are used to check whether results from two recursions in divide-and-conquer
computation can be connected to make a better solution. Since the predicate p is relational, we
can check the connectability by using only elements on the edge. The fifth element is a Boolean
value that is the result of p applied to the input.
Here, we want to reduce the size of pentuples by eliminating the fifth element (it corresponds
to p (x)) for simplicity. To do so, we use an assumption that ı⊗ is the zero of ⊗, i.e. ı⊕ ⊗ a = ı⊕ .
Corollary 17 (Maximum p-Initial-segment Sum (Simplified)). Provided that ⊕ is associative,⊗ is associative and left-distributive over ⊕, the identity ı⊕ is the zero of ⊗, and predicate p isrelational, the following equation holds.
⊕/ ◦ ⊗/∗ ◦ p ⊳ ◦ inits = π1 ◦ ([⊠, quadruple])where(i1 , s1 , h1 , l1 ) ⊠ (i2 , s2 , h2 , l2 ) = (i1 ⊕ (s1 ⊗ i2 )l1 ,h2 , (s1 ⊗ s2 )l1 ,h2 , h1 ≪ h2 , l1 ≫ l2 )
quadruple a = (a, a, a, a)(a)l,h = if p ([l, h]) then a else ı⊕
Proof. To simplify the result of the theorem, we add an invariant to the result of Theorem 16.
The invariant added to the pentuple (i, s, h, t, p) is ¬p ⇒ s = ı⊕ . In the following calculation,
we derive a operator slightly changed from that of Theorem 16.
i
=
=
=
=
=

{ definition }i1 ⊕ if p1 ∧ p ([l1 , h2 ]) then s1 ⊗ i2 else ı⊕{ splitting condition }i1 ⊕ if p ([l1 , h2 ]) then (if p1 then (s1 ⊗ i2 ) else ı⊕ ) else ı⊕{ assumption: ı⊕ is the zero }i1 ⊕ if p ([l1 , h2 ]) then ((if p1 then s1 else ı⊕ ) ⊗ i2 ) else ı⊕{ s′1 = if p1 then s1 else ı⊕ }i1 ⊕ if p ([l1 , h2 ]) then (s′1 ⊗ i2 ) else ı⊕{ definition of (a)t,h }i1 ⊕ (s′1 ⊗ i2 )l1 ,h2Computation of s′ = if p then s else ı⊕ is as follows.
s′
=
=
=
=
=

{ definition }if p then s else ı⊕{ computation of s and p }if p1 ∧ p2 ∧ p ([l1 , h2 ]) then s1 ⊗ s2 else ı⊕{ splitting condition }if p ([l1 , h2 ]) then (if p1 then s1 else ı⊕ ) ⊗ (if p1 then s2 else ı⊕ ) else ı⊕{ definition of s’ }if p ([l1 , h2 ]) then s′1 ⊗ s′2 else ı⊕{ definition of (a)t,h }(s′1 ⊗ s′2 )l1 ,h228

Now, we can use s′ instead of s and p in the pentuple (i, s, h, t, p), since p and s are not usedby computation of other parts. Thus, replacing s and p in the pentuple with s′ and rename s′
as s, we get the reduced operator ⊠.
The resulting program (the right hand side) uses the new reduction operator ⊠ that is
applied on quadruples. The difference from the result of Theorem 16 is that the second element
becomes the identity ı⊕ of ⊕ when the input does not satisfy the predicate p.
A sufficient condition of the assumption that ı⊕ is the zero of ⊗ is that ⊗ distributes over⊕. So, we will use this condition in implementation of the library.

4.4

Theory of tails

This section gives formal definition and theory of GGenerator tails.
4.4.1

Formal Definition and Basic Lemmas

First of all, we give a formal definition of tails.
Definition 18 (GGenerator Tails). GGenerator tails is defined with homomorphism as follows.
tails = ([⊕, [·] ◦ [·]]) where x ⊕ y = (++(head y))∗ x ++ y
The operator ⊕ in the above definition makes a list of tail segments of a list u ++ v fromlists (x and y in the above equation) of tail segments of u and v. Since each tail segment of v
is also a tail segment of u ++ v, y remains in the result. Since each tail segment of u need to beconcatenated with v to become a tail segment of u ++ v, the operator maps (++(head y)) (v isthe head element of y) to x.
The following two lemmas are well-known lemmas of tails [Bir87].
Lemma 19 (Scanr). For any associative binary operator ⊕, the following equation holds.
scanr (⊕) = ⊕/∗ ◦ tails
Lemma 20 (Tails-Map Promotion). For function f , the following equation holds.
f ∗∗ ◦ tails = tails ◦ f ∗First lemma gives us a way to compute suffix sums by tails. The second lemma gives us a way
to promote the application of function f through tails. The number of applications of function
f on the left hand side is n(n + 1)/2, while that on the right hand side is n. So, transformationfrom the left hand side to the right hand side improves the efficiency. Also, the lemma enables
us to ignore a function g in the generate-and-test specification ([⊕, f ]) ◦ ([⊗, g])∗ ◦ p ⊳ ◦tails, since
we can replace g with the identity function id and apply g to the input of tails beforehand (ofcourse, we need some tricks to through p ⊳).
A related example problem is found in Section 3.4.1. Related implementation on GG libraryis found in Section 5.4.1.
4.4.2

Theorem for Reduction with Distributive Operators

The following theorem gives efficient parallel implementation of nested reductions for tails when
two reductions have distributivity. One of the most famous problems for which this theorem is applicable is maximum tail-segment sum problem (also known as maximum suffix sum
problem), which is an instance of maximum marking problems [SHTO00, Bir01]. A related
example problem is found in Section 3.4.2. Related implementation on GG library is found in
Section 5.4.2.
29

Theorem 21 (Maximum Tail-segment Sum). Provided that ⊕ is associative, and ⊗ is associative and right-distributive over ⊕, the following equation holds.
⊕/ ◦ ⊗/∗ ◦ tails = π1 ◦ ([⊛, pair ])where (t1 , s1 ) ⊛ (t2 , s2 ) = ((t1 ⊗ s2 ) ⊕ t2 , s1 ⊗ s2 )pair a = (a, a)

Proof. Similar to the proof of Theorem 15 in Section 4.3.2.
The resulting program (the right hand side) of the theorem uses only one reduction with
the new operator ⊛, while the original program (the left hand side) uses two nested reductions
with tails. The cost of the new operator is proportional to the cost of operators in the original
reductions. So, the resulting program is more efficient than the original program.
The new operator ⊛ is applied to tuples. The first element of a tuple is equal to the resultof the original program. The second element of the tuple is equal to the reduction of the same
input with operator ⊗, which is used to improve efficiency of the program by reusing the partial
results effectively.
4.4.3

Theorem for Filtering with Relational Predicates

The following theorem extends Theorem 21 by allowing filtering with the given predicate. It
gives efficient parallel implementation of nested reductions for tails when two reductions have
distributivity and the predicate is relational. Derivation of efficient sequential implementations
for those programs with filtering is shown in [Zan92,Jeu93]. A related example problem is foundin Section 3.4.3. Related implementation on GG library is found in Section 5.4.3.
Theorem 22 (Maximum p-Tail-segment Sum). Provided that ⊕ is associative, ⊗ is associativeand right-distributive over ⊕, and predicate p is relational, the following equation holds.
∗ , pentuple])⊕/ ◦ ⊗/∗ ◦ p ⊳ ◦ tails = π1 ◦ ([⊡where∗ (t2 , s2 , h2 , l2 , p2 ) = (t, s1 ⊗ s2 , h1 ≪ h2 , l1 ≫ l2 , p1 ∧ p2 ∧ p ([l1 , h2 ]))(t1 , s1 , h1 , l1 , p1 ) ⊡where i = (if p1 ∧ p ([l1 , h2 ]) then t1 ⊗ s2 else ı⊕ ) ⊕ t2
pentuple a = (a, a, a, a, T )Proof. Similar to the proof of Theorem 16 in Section 4.3.3.
The resulting program (the right hand side) of the theorem uses only one reduction with∗ , while the original program (the left hand side) uses two nested reductions
the new operator ⊡with tails. The cost of the new operator is proportional to the cost of operators in the original
reductions and the application of p. So, the resulting program is more efficient than the original
program.
∗ is applied to pentuples. The first element of a pentuple is equal to the
The new operator ⊡result of the original program. The second element of the pentuple is equal to the reduction of
the same input with operator ⊗, which is used to improve efficiency of the program by reusing
the partial results effectively. The third and forth elements are the edge elements of the input.
Those edge elements are used to check whether results from two recursions in divide-and-conquer
computation can be connected to make a better solution. Since the predicate p is relational, we
can check the connectability by using only elements on the edge. The fifth element is a Boolean
value that is the result of p applied to the input.
Here, we want to reduce the size of pentuples by eliminating the fifth element (it corresponds
to p (x)) for simplicity. To do so, we use an assumption that ı⊗ is the zero of ⊗, i.e. a ⊗ ı⊕ = ı⊕ .

30

Corollary 23 (Maximum p-Tail-segment Sum (Simplified)). Provided that ⊕ is associative, ⊗is associative and right-distributive over ⊕, the identity ı⊕ is the zero of ⊗, and predicate p isrelational, the following equation holds.
⊕/ ◦ ⊗/∗ ◦ p ⊳ ◦ tails = π1 ◦ ([⊠⊞, quadruple])where(t1 , s1 , h1 , l1 ) ⊠⊞ (t2 , s2 , h2 , l2 ) = ((t1 ⊗ s2 )l1 ,h2 ⊕ t2 , (s1 ⊗ s2 )l1 ,h2 , h1 ≪ h2 , l1 ≫ l2 )
quadruple a = (a, a, a, a)(a)l,h = if p ([l, h]) then a else ı⊕
Proof. Similar to the proof of Corollary 17 in Section 4.3.3.
The resulting program (the right hand side) uses the new reduction operator ⊠⊞ that isapplied on quadruples. The difference from the result of Theorem 22 is that the second element
becomes the identity ı⊕ of ⊕ when the input does not satisfy the predicate p.
A sufficient condition of the assumption that ı⊕ is the zero of ⊗ is that ⊗ distributes over⊕. So, we will use this condition in implementation of the library.

4.5

Theory of segs

This section gives formal definition and theory of GGenerator segs.
4.5.1

Formal Definition and Basic Lemmas

First of all, we give a formal definition of segs using inits and tails.
Definition 24 (GGenerator Segs). GGenerator segs is defined with homomorphism as follows.
segs = ++/ ◦ inits∗ ◦ tails
This definition is based on the fact that a segment of a list is a prefix of a suffix of the list.
The following lemma is well-known lemma of segs [Bir87].
Lemma 25 (Segs-Map Promotion). For function f , the following equation holds.
f ∗∗ ◦ segs = segs ◦ f ∗The lemma gives us a way to promote the application of function f through segs. The
number of applications of function f on the left hand side is O(n3 ), while that on the righthand side is n. So, transformation from the left hand side to the right hand side improves
the efficiency. Also, the lemma enables us to ignore a function g in the generate-and-test
specification ([⊕, f ]) ◦ ([⊗, g])∗ ◦ p ⊳ ◦segs, since we can replace g with the identity function id andapply g to the input of segs beforehand (of course, we need some tricks to through p ⊳).
A related example problem is found in Section 3.5. Related implementation on GG libraryis found in Section 5.5.1.
4.5.2

Theorem for Reduction with Distributive Operators

The following theorem gives efficient parallel implementation of nested reductions for segs when
two reductions have distributivity. One of the most famous problems for which this theorem
is applicable is maximum segment sum problem [Bir87], which is an instance of maximum
marking problems [SHTO00, Bir01]. A related example problem is found in Section 3.5.2.
Related implementation on GG library is found in Section 5.5.2.
31

Theorem 26 (Maximum Segment Sum). Provided that ⊕ is associative and commutative, and⊗ is associative and distributive over ⊕, the following equation holds.
⊕/ ◦ ⊗/∗ ◦ segs = π1 ◦ ([⊚, quadruple])where(m1 , t1 , i1 , s1 ) ⊚ (m2 , t2 , i2 , s2 ) = (m1 ⊕ m2 ⊕ (t1 ⊗ i2 ), (t1 ⊗ s2 ) ⊕ t2 , i1 ⊕ (s1 ⊗ i2 ), s1 ⊗ s2 )quadruple a = (a, a, a, a)
Proof. We can prove the theorem by the following calculation.
=
=
=
=
=
=
=
=
=
=

LHS
{ LHS }⊕/ ◦ ⊗/∗ ◦ segs
{ definition of segs }⊕/ ◦ ⊗/∗ ◦ ++/ ◦ inits∗ ◦ tails{ promotion of ∗ }⊕/ ◦ ++/ ◦ ⊗/∗∗ ◦ inits∗ ◦ tails{ promotion of / }⊕/ ◦ ⊕/∗ ◦ ⊗/∗∗ ◦ inits∗ ◦ tails{ distributivity of ∗ }⊕/ ◦ (⊕/ ◦⊗/∗ ◦ inits)∗ ◦ tails{ Theorem 15 }⊕/ ◦ (π1 ◦ ([⊙, pair ]))∗ ◦ tails{ making ⊕′ so that (a1 , b1 ) ⊕′ (a2 , b2 ) = (a1 ⊕ a2 , b1 ⊕ b2 ), Lemma 20 }π1 ◦ ⊕′ / ◦ ⊙/∗ ◦ tails ◦ pair ∗{ Theorem 21 (commutativity of ⊕ guarantees distributivity of ⊙ over ⊕′ ) }π1 ◦ π1 ◦ ([⊛, pair ]) ◦pair ∗{ fusing two π1 s, and two pair s }π1 ◦ ([⊚, quadruple]){ RHS }
RHS

Definition of ⊛ in the above calculation is given as follows.
((m1 , t1 ), (i1 , s1 )) ⊛ ((m2 , t2 ), (i2 , s2 ))={ definition of ⊛ in Theorem 21 }(((m1 , t1 ) ⊙ (i2 , s2 )) ⊕′ (m2 , t2 ), (i1 , s1 ) ⊙ (i2 , s2 ))={ definition of ⊙ in Theorem 15 }((m1 ⊕ (t1 ⊗ i2 ), t1 ⊗ s2 ) ⊕′ (m2 , t2 ), (i1 ⊕ (s1 ⊗ i − 2), s1 ⊗ s2 ))={ definition of ⊕′ shown above }((m1 ⊕ (t1 ⊗ i2 ) ⊕ m2 , (t1 ⊗ s2 ) ⊕ t2 ), (i1 ⊕ (s1 ⊗ i − 2), s1 ⊗ s2 ))Flattening the nested pair into quadruple, we get the definition of ⊚.
The resulting program (the right hand side) of the theorem uses only one reduction with
the new operator ⊚, while the original program (the left hand side) uses two nested reductions
with segs. The cost of the new operator is proportional to the cost of operators in the original
reductions. So, the resulting program is more efficient than the original program.
The new operator ⊚ is applied to quadruples. The first element of a tuple is equal to theresult of the original program. The second and the third elements are results of the original
nested reductions with tails and inits. The last element is equal to the reduction of the same
input with operator ⊗. These extra elements are used to improve efficiency of the program byreusing the partial results effectively.
32

4.5.3

Theorem for Filtering with Relational Predicates

The following theorem extends Theorem 26 by allowing filtering with the given predicate. It
gives efficient parallel implementation of nested reductions for segs when two reductions have
distributivity and the predicate is relational. Derivation of efficient sequential implementations
for those programs with filtering is shown in [Zan92,Jeu93]. A related example problem is foundin Section 3.5.3. Related implementation on GG library is found in Section 5.5.3.

Theorem 27 (Maximum p-Segment Sum). Provided that ⊕ is associative and commutative, ⊗is associative and distributive over ⊕, and predicate p is relational, the following equation holds.
⊕/ ◦ ⊗/∗ ◦ p ⊳ ◦ segs = π1 ◦ ([◦ , hextuple])where (m1 , t1 , i1 , s1 , h1 , l1 ) ◦ (m2 , t2 , i2 , s2 , h2 , l2 )= ( m1 ⊕ m2 ⊕ (t1 ⊗ i2 )l1 ,h2 ,(t1 ⊗ s2 )l1 ,h2 ⊕ t2 ,i1 ⊕ (s1 ⊗ i2 )l1 ,h2 ,(s1 ⊗ s2 )l1 ,h2 ,h1 ≪ h2 , l1 ≫ l2 )hextuple a = (a, a, a, a, a, a)(a)l,h = if p ([l, h]) then a else ı⊕

Proof. We can prove the theorem by the following calculation.

=
=
=
=
=
=
=
=
=

LHS
{ LHS }⊕/ ◦ ⊗/∗ ◦ p ⊳ ◦ segs
{ definition of segs }⊕/ ◦ ⊗/∗ ◦ p ⊳ ◦ ++/ ◦ inits∗ ◦ tails{ promotion of ⊳, ∗ and / }⊕/ ◦ ⊕/∗ ◦ ⊗/∗ ◦ p ⊳∗ ◦ inits∗ ◦ tails{ ∗ distributivity }⊕/ ◦ (⊕/ ◦ ⊗/ ◦ p ⊳ ◦ inits)∗ ◦ tails{ Theorem 17 }⊕/◦ (π1 ◦ ([⊠, quadruple]))∗ ◦ tails
making ⊕′ such that
(i1 , s1 , h1 , l1 ) ⊕′ (i2 , s2 , h2 , l2 ) = (i1 ⊕ i2 , s1 ⊕ s2 , h1 ≪ h2 , l1 ≫ l2 )π1 ◦ ⊕′ / ◦ ⊠/∗ ◦ tails ◦ quadruple∗{ Theorem 21 (⊠ distributes over ⊕′ ) }π1 ◦ π1 ◦ ([⊛, pair ]) ◦quadruple∗{ fusing two π1 s, fusing pair and quadruple, removing duplicated parts }π1 ◦ ([◦ , hextuple]){ RHS }
RHS

Note that distributivity of ⊠ over ⊕′ is guaranteed for quadruples (i1 , s1 , h1 , l1 ) and (i2 , s2 , h2 , l2 )of operands of ⊕′ when l1 = l2 . Condition l1 = l2 holds in the above calculation since l1 and l2
are the last element of tail-segments of the same list.
33

Definition of ⊛ in the above calculation is given as follows.
((m1 , t1 , h1 , l1 ), (i1 , s1 , k1 , n1 )) ⊛ ((m2 , t2 , h2 , l2 ), (i2 , s2 , k2 , n2 ))={ definition of ⊛ in Theorem 21 }(((m1 , t1 , h1 , l1 ) ⊠ (i2 , s2 , k2 , n2 )) ⊕′ (m2 , t2 , h2 , l2 ), (i1 , s1 , k1 , n1 ) ⊠ (i2 , s2 , k2 , n2 ))={ definition of ⊠ in Theorem 17 }((m1 ⊕ (t1 ⊗ i2 )l1 ,k2 , (t1 ⊗ s2 )l1 ,k2 , h1 ≪ k2 , l1 ≫ n2 ) ⊕′ (m2 , t2 , h2 , l2 ),(i1 ⊕ (s1 ⊗ i2 )n1 ,k2 , (s1 ⊗ s2 )n1 ,k2 , k1 ≪ k2 , n1 ≫ n2 )={ definition of ⊕′ shown above }((m1 ⊕ m2 ⊕ (t1 ⊗ i2 )l1 ,k2 , (t1 ⊗ s2 )l1 ,k2 ⊕ t2 , h1 ≪ k2 ≪ h2 , l1 ≫ n2 ≫ l2 ),(i1 ⊕ (s1 ⊗ i2 )n1 ,k2 , (s1 ⊗ s2 )n1 ,k2 , k1 ≪ k2 , n1 ≫ n2 )If h1 = k1 , l1 = n1 , h2 = k2 and l2 = n2 , then we have h1 ≪ k2 ≪ h2 = k1 ≪ k2 andl1 ≫ n2 ≫ l2 = n1 ≫ n2 . So, for octuple ((m, t, h, l), (i, s, k, n)), we have invariant h = k andl = n. Using this invariant, we can eliminate k and n from octuples and we get computation
using hextuples. Finally, flattening the hextuples, we get the definition of ⊚.
The resulting program (the right hand side) of the theorem uses only one reduction with
the new operator ◦ , while the original program (the left hand side) uses two nested reductions
with segs. The cost of the new operator is proportional to the cost of operators in the original
reductions. So, the resulting program is more efficient than the original program.
The new operator ◦ is applied to hextuples. The first element of a tuple is equal to the resultof the original program. The second and the third elements are results of the original programin which segs is replaced with tails and inits. The fourth element is equal to the reduction of
the same input with operator ⊗. The fifth and the sixth elements are the edge elements of the
input. Those edge elements are used to check whether results from two recursions in divideand-conquer computation can be connected to make a better solution. Since the predicate p
is relational, we can check the connectability by using only elements on the edge. These extra
elements are used to improve efficiency of the program by reusing the partial results effectively.

4.6
4.6.1

Related Work
Maximum Marking Problem

Maximum marking problem is one of optimization problems on sequences. The objective of
maximum marking problem is to find a marking of the input sequence that gives the maximum weight sum. We can produce many instances of maximum marking problem by changing
the rule of marking on the input sequence. For example, maximum prefix sum problem (Section 3.3.2), maximum suffix sum problem (Section 3.4.2), and maximum segment sum problem(Section 3.5.2) are instances of maximum marking problem.
Derivation of efficient sequential programs for maximum marking problem was studied by
Sasano et al. [SHTO00, SHT01] and Bird [Bir01]. They showed systematic construction of efficient sequential programs when rules of marking are given as recursive functions of a certainclass. Since marking of a prefix/suffix/segment is given as a recursive function of the class, anefficient sequential program for maximum prefix/suffix/segment problem is obtained systematically by their results.
4.6.2

Longest Segment Problems

The objective of longest segment problems is to find the longest segment that satisfies a given
predicate. Derivation of efficient sequential programs for longest segment problems were stud34

ied by Zatema [Zan92], Jeuring [Jeu93] and Zhao [Zha02]. Zatema [Zan92] and Jeuring [Jeu93]
showed derivation of efficient sequential programs for various predicates. Zhao [Zha02] studied derivation of efficient sequential programs for predicates constructed as a combination ofprimitive predicates. She applied it for data mining to make a querying system that supports
efficient querying of combined predicates.

35

trait GGenerator[[E]] extends List[[ List[[ E ]] ]]getter list() : List[[ E ]]getter defaultImplementation() : List[[ E ]] → List[[ List[[ E ]] ]]generate2 [[ R, F, M, N, P, Z, Y ]](r : R, f : F, mr : M, mf : N, p : P ) : Z= defaultgeneration[[ R, F, M, N, P, Z, Y ]](r, f, mr , mf , p)defaultgeneration[[ R, F, M, N, P, Z, Y ]](r : R, f : F, mr : M, mf : N, p : P ) : Z =actualList().filter (fn (e : List[[E]]) : Boolean ⇒ p.judge(e)).generate[[Z]](r, (fn a ⇒ f.apply(a))◦(fn (x) ⇒ x.generate[[Y ]](mr , (fn a ⇒ mf .apply(a)))))
actualList() : List[[ List[[ E ]] ]] = defaultImplementation()(list())
end

Figure 3: Base trait of GGenerators

5

Implementation of GG LibraryThis section gives implementation of GG library. First, implementation of the core of GG
library is given in Section 5.1. Then, a collection of traits to describe properties is given in
Section 5.2. After that, a collection of implementations for various GGenerators follows.

5.1

Core Implementation of GG Library

The core of GG Library is trait GGenerator (Section 5.1.1), which is the base of all GGenerators, and function dispatching (Section 5.1.2), which acts as a dispatching table of efficient
implementations. Intuitive interpretation of GGenerators is found in Section 3.1.2. Formal
discussion of GGenerators is found in Section 4.1.2
Besides the above two constructs, auxiliary functions and object to define GGenerators
are shown in Section 5.1.3, and desugaring of user programs for GG library is discussed in
Section 5.1.4.
5.1.1

Trait GGenerator

Trait GGenerator is the base trait of all GGenerators. Figure 3 shows the definition of trait
GGenerator (the figure contains only essential fields).
Currently, GGenerator[[E ]] is defined as a subtrait of trait List[[List[[E ]]]], which is a subtrait ofFortress’s Generator. The core of trait Generator is method generate that generates elements oftype E , passes each of them to the function body , and combines the results using the reductionr.
Trait GGenerator extends the existing Generator as follows. First, GGenerator itself canwork as Generator to generate elements of type List[[E ]], since GGenerator is a subtrait ofGenerator. Next, method generate2 of GGenerator is an extension of method generate ofGenerator. Method generate2 takes two pairs of operators and body functions, namely thepair (r , f ) and the pair (mr , mf ), for nested reductions so that it can use relationship between
the given pairs to perform the reductions efficiently, while generate takes a pair of an operator
and a function to perform a single reduction, performing nested reductions individually. Of
course, if the nested reductions use the same operator for each reduction, both generate2 andnested use of generate result in the same computation.
The rest of this section explains methods of trait GGenerator.
Getter list () returns the original list given to the GGenerator. Basically, values in thegenerated nested lists are taken from this original list.
37

Getter defaultImplementation () returns implementation to generate the actual nested data
structures. Basically, an efficient implementation does not generate such actual nested data
structures. Implementation given by defaultImplementation is used to perform the nested
reductions naively as the default of dispatching.
Method generate2 is the most important method of trait GGenerator that is an interface of dispatching implementation to the nested reductions. Meaning of an invocation ofgenerate2 (r , f , mr , mf , p) of GGenerator gg is the same as the following nested comprehension
with nested reductions.
r [ f ( mr [ mf y | y ← ys ] ) | ys ← gg xs, p ys ]GGenerator gg generates a nested data structure, and its element (basically a subsequence of
the input xs ) is bound to variable ys . Predicate p is used to filter the generated element ys .
Function mf is applied to each element of ys passed the filtering, and a reduction with mr istaken on the result. And then, function f is applied for each result of the inner reduction with
mr , and finally reduction with r is taken on those results. Straightforward implementation of
the computation explained above is seen in method defaultgeneration explained below.
Method defaultgeneration performs the default naive nested reductions on the actual nested
data structure. Arguments are the same as method generate2 explained above. The actual
nested data structure is generated by actualList () explained later. Against the generated nested
data structure, it performs filtering with the given predicate p by method filter of List. Judgment by the predicate p is denoted by p.judge(e). After that, it performs the nested reductions
with two invocations of method generate of Generators. The inner reduction is performed
with the given reduction mr and function mf . Application of the function mf is denotedby mf .apply(a). The outer reduction is performed with the given reduction r and function fcomposed with the inner reduction. The computation by method defaultgeneration is the sameas a program of nested comprehensions desugared by the usual desugaring process of Fortress.
Method acutalList () generates the actual nested data structure by the implementation given
by defaultImplementation (). This actual list is used in some methods, such as taking the headof the generated nested data structure, as well as the default naive nested reductions.
It is worth mentioning about type variables used in method generate2 . There are many
type variables in the method and they have no restrictions. The reason of a number of typevariables is as follows. Method generate2 wants to know complete types of the arguments andbind those types to variables, since the dispatching process needs to check properties of thearguments by their types to dispatch efficient implementation. The reason of no restriction on
types is basically the limitation of the current interpreter, which does not completely support
where-clause. When where-clause is supported in the future, we can add restriction on typevariables like shown below.
generate2 [[ R, F, M, N, P, Z, Y ]](r : R, f : F, mr : M, mf : N, p : P ) : Z
where { R extends Reduction[[Z]], F extends Function[[Y, Z]],
M extends Reduction[[Y ]], N extends Function[[E, Y ]],P extends ListPredicate[[E]]}= defaultgeneration[[ R, F, M, N, P, Z, Y ]](r, f, mr , mf , p)

5.1.2

Dispatching Table

The dispatching process dispatches efficient implementation given by a theorem to an invocationof generate2 of a GGenerator (a desugared user program) when the arguments satisfy theapplicable condition of the theorem. Basically, checking of applicable conditions of theorems
against the arguments is performed by checking types of the arguments, since properties of thearguments should be specified by traits shown in Section 5.2.
The dispatching table shown in Figure 4 is the core of dispatching process. The dispatchingtable is defined as function dispatching that checks types of the given arguments and selects
38dispatching[[ G, R, F, M, N, P, Z, Y, E ]](g : G, r : R, f : F, mr : M, mf : N, p : P ) = do
typecase (g, r, f, mr , mf , p) of(InitsGenerator[[E]], R, IdFunction[[Y ]], LeftDistributiveOver[[R]], N, TrueListPredicate[[E]])⇒ g.efficientImplTrueDistributive[[R, F, M, N, P, Z, Y ]](r, f, mr , mf , p)(InitsGenerator[[E]], R, IdFunction[[Y ]], LeftDistributiveOver[[R]], N, RelationalPredicate[[E]])⇒ g.efficientImplRelationalDistributive[[R, F, M, N, P, Z, Y ]](r, f, mr , mf , p)
(TailsGenerator[[E]], R, IdFunction[[Y ]], RightDistributiveOver[[R]], N, TrueListPredicate[[E]])⇒ g.efficientImplTrueDistributive[[R, F, M, N, P, Z, Y ]](r, f, mr , mf , p)
(TailsGenerator[[E]], R, IdFunction[[Y ]], RightDistributiveOver[[R]], N, RelationalPredicate[[E]])⇒ g.efficientImplRelationalDistributive[[R, F, M, N, P, Z, Y ]](r, f, mr , mf , p)
(SegsGenerator[[E]], Commutative, IdFunction[[Y ]], DistributiveOver[[R]], N, TrueListPredicate[[E]])⇒ g.efficientImplTrueDistributive[[R, F, M, N, P, Z, Y ]](r, f, mr , mf , p)
(SegsGenerator[[E]], Commutative, IdFunction[[Y ]], DistributiveOver[[R]], N, RelationalPredicate[[E]])⇒ g.efficientImplRelationalCommutativeDistributive[[R, F, M, N, P, Z, Y ]](r, f, mr , mf , p)else
⇒ g.defaultgeneration[[R, F, M, N, P, Z, Y ]](r, f, mr , mf , p)
end
end

Figure 4: Dispatching table
suitable implementation according to the arguments. Function dispatching receives a GGenerator and arguments given to generate2 of the GGenerator. Each GGenerator should invoke
function dispatching to perform dispatching in generate2 (see implementation of GGenerators
shown in the following sections).
Function dispatching checks types of arguments by typecase of Fortress to dispatch suitable
implementation. Basically, one case of typecase corresponds to one theorem, and the default( else ) case corresponds to naive implementation of nested reductions. Figure 4 contains cases
for theorems given in Section 4 and the default case. For the default case ( else case), thedispatching table invokes method defaultgeneration of GGenerator g . In the other cases, it
checks whether properties of the arguments satisfy applicable conditions by checking types of
the arguments, to dispatch the corresponding efficient implementation.
For example, the first case of the table shown in Figure 4 corresponds to Theorem 15 in Section 4.3.2. The theorem requires that the inner reduction (mr ) has distributivity over the outerreduction (r ). So, function dispatching checks whether mr extends LeftDistributiveOver[[R]](see Section 5.2.1). Also, function dispatching checks that f is the identity function (see Section 5.2.2) and p is the true-predicate (see Section 5.2.3), since the theorem cannot deal withother functions and predicates. If those conditions on types are satisfied, function dispatching
confirms that the applicable condition of the theorem is satisfied, and it invokes the efficient
implementation efficientImplTrueDistributive of InitsGenerator (see Section 5.3.2) to performthe nested reductions of a user program efficiently by the implementation.
Summary of dispatching is as follows. Method generate2 of each GGenerator invokes function dispatching with the GGenerator and its arguments. The typecase in function dispatching
checks whether the given arguments satisfy applicable condition of each theorem by checking
their types. If it confirms that the arguments satisfy the condition, it invokes the corresponding
efficient implementation of the theorem. If no condition is satisfied, the default implementation
is used in the default case of the typecase .
To exploit knowledge of a theorem, an implementer has to do two things. One is to implement
the optimization given by the theorem in its corresponding GGenerator. The other is to modify
the typecase in function dispatching by adding a new case of type conditions corresponding to39

takeleft[[T ]](a : Nothing[[T ]], b : Any) = b
takeleft(a : Any, b : Any) = a
takeright[[T ]](a : Any, b : Nothing[[T ]]) = a
takeright(a : Any, b : Any) = b
object MapReduceReduction[[R]](j : (R, R) → R, z : R) extends Reduction[[R]]empty() = z
join(a : R, b : R): R = (j)(a, b)
end

Figure 5: Auxiliary functions and object
the applicable condition of the theorem, and a code to invoke the efficient implementation of the
GGenerator in the case. Then, nested reductions of a user program can be executed with theefficient implementation given by the theorem, if the nested reduction satisfies the applicablecondition of the theorem.
5.1.3

Auxiliary Functions and Object

Figure 5 gives implemetation of auxiliary functions and object for defining GGenerators.
Functions takeleft and takeright provides function of operators ≪ and ≫ (used in Section 4)
with identities. Their identities are represented by a special value Nothing.
Object MapReduceReduction makes a reduction object from an associative binary operator
and its identity, and is used in invocations of method generate of Generator. This object isborrowed from the Fortress Standard Library.
5.1.4

Desugaring of User Programs

Currently, desugaring of a user program into invocations of method generate2 of GGenerators
does not completely work. It is very difficult to desugar any expression into generate2 , since itneeds to split an expression into a function and a reduction. Thus, we are planning to desugar
restricted nested comprehensions that can be transformed into a form below.
L N[[ f y | y ← ys ] | ys ← gg xs, p ys ](1)Here, gg is one of GGenerators, p is a predicate, f is a function, and ⊕ and ⊗ are associative
operators. This form is the same computation as the following invocation of generate2 .
gg(x).generate2 (BinReduction[[ ⊕ ]], IdFunction, BinReduction[[ ⊗ ]], f, p)

Here, BinReduction makes a reduction object from an associative binary operator.
We show, with an example, that quite a lot of nested comprehensions can be systematicallydesugared into the above form. Consider the next nested comprehension as our example.

↑[ +[ f (y, b, w) | y ← ys, even y ] | ys ← inits xs, ascending ys, b ← bs ]This example computes a variant of the maximum prefix sum, in which the maximum is considered only on ascending prefixes, the summation is taken only on even numbers, and the value
is replaced with f (y, b, w) instead of the number itself (y) at the summation.
Transformation steps with the example program are shown below.
Step. 1 Remove guards p x by fusing it with generators x ← g xs
There are two occurrences of guards in the example: even y and ascending ys. Fusing
these guards, we can get the following program.

↑[ +[ f (y, b, w) | y ← filter even ys ] | ys ← filter ascending (inits xs), b ← bs ]40

This transformation is applicable, when each predicate depends only on a variable in
the left hand side of generators in the same comprehension.
Step. 2 Move depending generations to the edges
If there is depending generations in generators of two comprehensions, move thosedepending generation to the edges of comprehensions as follows.

⊕[ ⊗[ e | gs 1 ] | gs 2 ] ⇒ ⊕[ ⊗[ e | y ← fg ys, gs ′1 ] | gs ′2 , ys ← fgg xs ]Here, fgg is one of GGenerators with filter, and fg is the identity function or filter. Thistransformation is valid if each operator of reductions is commutative and there is nodependency of gs ′2 to ys.
The example program has a pair of depending generations y ← filter even ys and ys ←filter ascending (inits xs). Since operators used in our example are both commutative,
we can perform this transformation to get the following program.

↑[ +[ f (y, b, w) | y ← filter even ys ] | b ← bs, ys ← filter ascending (inits xs) ]Here, ys ← filter ascending (inits xs) is moved to the edge using commutativity of ↑.
Step. 3 Restructure comprehensions to extract the form
The following is a rule used in this step.

⊕[ ⊗[ e | y ← fg ys, gs ′1 ] | gs ′2 , ys ← fgg xs ]⇒ ⊕[ ⊕[ ⊗[ ⊗[ e | gs ′1 ] | y ← fg ys ] | ys ← fgg xs ] | gs ′2 ]This transformation is always valid, since it is a combination of steps used in the usual
desugaring process in Fortress. For readability, the result of this transformation can be
written as the following form.
h(⊕[ ⊗[ f ′ (y) | y ← fg ys ] | ys ← fgg xs ])where h(z) = ⊕[ z | gs ′2 ]f ′ (y) = ⊗[ e | gs ′1 ]Here, the argument of h is almost the same as the form (1). The difference can beeliminated in the following way. If fg is filter q, we introduce another function f ′′ (x) =if q(x) then x else ı⊗ , in which ı⊗ is the identity of ⊗. Otherwise, let f ′′ = f ′ . If fgg
does not includes filter, we introduce p = true that always returns true. Otherwise, let
p be the predicate of the filter, i.e., fgg xs = filter p (gg xs). Using these f ′′ and p, theargument of h is now the same as the form (1).

⊕[ ⊗[ f ′′ (y) | y ← ys ] | ys ← gg xs, p ys ])If there is no direct dependency of f ′′ to ys, we can replace this part by an invocationof method generate2 of gg.
Applying the above transformation, we get the following result for the example.

↑[ +[ f (y, b, w) | y ← filter even ys ] | b ← bs, ys ← filter ascending (inits xs) ]⇒ h(↑[ +[ f (y, b, w) | y ← filter even ys ] | ys ← filter ascending (inits xs) ])where h(z) = ⊕[ z | b ← bs ]⇒ h(↑[ +[ f ′′ y | y ← ys ] | ys ← inits xs, ascending ys ])where h(z) = ⊕[ z | b ← bs ]f ′′ (z) = if even x then x else 0Here, the argument of h is the same as the form (1). Since there is no direct dependencyof f ′′ to ys, the part can be replaced with invocation of generate2 of GGenerator inits .
41

mis = BIG MAX hPy | y ← inits x iPmais = BIG MAX h y | y ← inits x, ascending(y) i(a) User program

mis = inits(x).generate2 [[ MaxReductionZZ32, IdFunction[[Z32]],
SumReductionZZ32, IdFunction[[Z32]],
TrueListPredicate[[Z32]], Z32, Z32]](MaxReductionZZ32, IdFunction[[Z32]],
SumReductionZZ32, IdFunction[[Z32]],
TrueListPredicate[[Z32]])
mais = inits(x).generate2 [[ MaxReductionZZ32, IdFunction[[Z32]],
SumReductionZZ32, IdFunction[[Z32]],
Ascending[[Z32]], Z32, Z32]](MaxReductionZZ32, IdFunction[[Z32]],
SumReductionZZ32, IdFunction[[Z32]],
Ascending[[Z32]])(b) Desugared program
Figure 6: Examples of desugaring user programs
The desugaring transformation shown above has some restrictions on target comprehensions.
For example, Step. 1 requires that each predicate should depend only on a variable in theleft hand side of generators in the same comprehension, Step. 2 requires that the operators
should be commutative and there is no dependency of outer generators to generation of the
GGenerator, and replacement of comprehension with generate2 in Step. 3 requires that there isno direct dependency of the inner function to generation of the GGenerator. One easy sufficient
restriction for dependencies of generators is that a variable on the left hand side of arrows in
generators is used at most once in the right hand side of arrows in the generators and the bodyfunction. This restriction is often satisfied.
Some examples of desugaring is shown in Figure 6. Please refer to Section 5.2 for objects
used in the desugared program.

5.2
5.2.1

Traits for Describing Properties
Properties on Reduction Operators

Figure 7 gives definitions of traits for describing properties on reduction operators, which aredefined in Section 4.2.1.
Trait LeftDistributiveOver[[X ]] is used to indicate that a reduction object extending the trait
is left distributive over the reduction object X . Similarly, trait RightDistributiveOver[[X ]] isused to indicate right-distributivity. Trait DistributiveOver[[X ]] indicates the reduction object
extending the trait is distributive, i.e., left-distributive and right-distributive, over the reduction
object X . Thus, trait DistributiveOver extends both trait LeftDistributiveOver and trait
RightDistributiveOver. Trait Commutative indicates commutativity.
Example use of those traits is also shown in Figure 7. Object MaxReductionZZ32 is a reduction object of the maximum operator ↑ defined in Section 3.1. Since the maximum operator iscommutative, MaxReductionZZ32 extends the trait Commutative. Object SumReductionZZ32
is a reduction object of the usual plus operator +. Since the plus distributes over the maximum
operator, SumReductionZZ32 extends trait DistributiveOver[[MaxReductionZZ32]], as well as
trait Commutative. Similarly, object ProdReductionZZ32 for the usual product operator ×
extends DistributiveOver[[SumReductionZZ32]] and Commutative.
42

trait LeftDistributiveOver[[X]] end
trait RightDistributiveOver[[X]] end
trait DistributiveOver[[X]] extends {LeftDistributiveOver[[X]], RightDistributiveOver[[X]]} end
trait Commutative end
object MaxReductionZZ32
extends { Reduction[[Z32]], Commutative }empty(): Z32 = −infinity
join(a: Z32, b: Z32): Z32 = a MAX b
end
object SumReductionZZ32
extends { Reduction[[Z32]], DistributiveOver[[MaxReductionZZ32]], Commutative }empty(): Z32 = 0
join(a: Z32, b: Z32): Z32 = a + b
end
object ProdReductionZZ32
extends { Reduction[[Z32]], DistributiveOver[[SumReductionZZ32]], Commutative }empty(): Z32 = 1
join(a: Z32, b: Z32): Z32 = a ∗ b
end

Figure 7: Traits for describing properties on reductions and example reductions
5.2.2

Properties on Functions

Figure 8 gives definitions of traits for describing properties on functions.
Trait Function[[X ,Y ]] is the base trait of functions that take a value of type X and return
a value of type Y . Every function given to dispatching and generate2 should extend trait
Function to make the library check properties of the function. Basically, a function does notnecessarily need to be a trait or an object in Fortress, since Fortress can handle functions
directly. However, to describe properties of functions by themselves, we require a function to
be a trait or an object. Otherwise, we need an extra argument in generate2 to tell propertiesof functions.
Object IdFunction is the identity function that returns the given argument as its return
value. Object IdFunction is used to cancel functions in the generate-and-test specification. If
the user program does not need mapping of a function to elements, the object IdFunction mustbe given to method generate2 of GGenerator (and function dispatching ) to let the library know
there is no function to map. Note that when a function object other than IdFunction is given
to method generate2 , the library determines that there is a function to map that can return avalue different form the input value, even if the function actually returns always the input value
itself.
5.2.3

Properties on Predicates

Figure 9 gives definitions of traits for describing properties on predicates, which are defined in
Section 4.2.2.
Trait Predicate is the base of all predicates. It has method judge that returns a Boolean
value (true or false) of the given argument x .
Trait ListPredicate is a predicate on lists. Every predicate given to method generate2 of
GGenerators or the dispatching table dispatching should extend trait ListPredicate.
Object TrueListPredicate is a predicate returning true for any input. This predicate isused to cancel the filtering in the generate-and-test specification, since filtering with the pred43

trait Function[[X, Y ]]apply(x : X) : Y
end
object IdFunction[[X]] extends Function[[X, X]]
apply(x : X) : X = x
endobject SingletonFunction[[X]] extends Function[[X, List[[X]]]]
apply(x : X) : List[[X]] = singleton[[X]](x)endobject FunctionWrapper[[X, Y ]](f : X → Y ) extends Function[[X, Y ]]apply(x : X) : Y = f x
end

Figure 8: Traits for function objects
icate is equals to the identity function. If the user program does not need filtering, theobject TrueListPredicate must be given to method generate2 of GGenerator (and function
dispatching ) to let the library know there is no filtering. Note that when a predicate object
other than TrueListPredicate is given to method generate2 , the library determines that there
is a filtering with a predicate that can return false, even if the predicate actually returns always
true.
Trait SuffixClosedPredicate indicates that a predicate extending SuffixClosedPredicate issuffix-closed. Similarly, trait PrefixClosedPredicate indicates prefix-closedness of a predicate.
Since a segment-closed predicate is both suffix-closed and prefix-closed, SegmentClosedPredicate
extends both SuffixClosedPredicate and PrefixClosedPredicate. Trait OverlapClosedPredicate
indicates a predicate is overlap-closed.
Trait RelationalPredicate is the base trait of all relational predicates. Since a relational
predicate is segment-closed and overlap-closed (Lemma 11 in Section 4.2.2), RelationalPredicate
extends SuffixClosedPredicate and OverlapClosedPredicate. Method related corresponds to
the relation that determines the predicate, and it returns true when the given arguments are
related by the relation. Method judge uses related to check all pairs of consecutive elements
are related by the relation.
Operator AND and object AndRelationalPredicate composes two relational predicates tomake another relational predicate that returns true when both of the two predicates return
true.
Example instances of RelationalPredicate are specified by comparison operators. Object
Ascending is specified by <, and returns true when the given list is sorted in ascending order.
Similarly, we can define objects Descending, WeaklyAscending, WeaklyDescending and Flatby >, ≤, ≥ and =. Object Smooth makes a relational predicate to check that the difference
between any pair of consecutive elements is less than or equal to the given threshold c .

44

trait Predicate[[ E ]]judge(x : E) : Boolean
end
trait ListPredicate[[ E ]] extends Predicate[[ List[[ E ]] ]] end
object TrueListPredicate[[ E ]] extends ListPredicate[[ E ]]judge(x : List[[ E ]]) : Boolean = trueend
trait SuffixClosedPredicate[[ E ]] extends ListPredicate[[ E ]] end
trait PrefixClosedPredicate[[ E ]] extends ListPredicate[[ E ]] end
trait SegmentClosedPredicate[[ E ]]extends { PrefixClosedPredicate[[ E ]], SuffixClosedPredicate[[ E ]] }end
trait OverlapClosedPredicate[[ E ]] extends ListPredicate[[ E ]] end
trait RelationalPredicate[[ E ]]extends { SegmentClosedPredicate[[ E ]], OverlapClosedPredicate[[ E ]] }related (a : E, b : E) : Boolean
judge(x : List[[ E ]]) : Boolean = doif x.size() ≤ 1 then
true
else
sz = x.size() − 1(0 # sz ).generate[[Boolean]](AndReduction, fn i ⇒ related (xi , xi+1 ))
end
end
end
opr ∧[[E]](p1 : RelationalPredicate[[ E ]], p2 : RelationalPredicate[[ E ]]): RelationalPredicate[[ E ]]= AndRelationalPredicate[[ E ]](p1 , p2 )object AndRelationalPredicate[[ E ]](p1 : RelationalPredicate[[ E ]], p2 : RelationalPredicate[[ E ]])extends RelationalPredicate[[ E ]]related (a : E, b : E) : Boolean = p1 .related (a, b) ∧ p2 .related (a, b)
end
object Ascending[[E]] extends RelationalPredicate[[E]]related (a : E, b : E) : Boolean = a < bend
object Descending[[E]] extends RelationalPredicate[[E]]related (a : E, b : E) : Boolean = a > bend
object WeaklyAscending[[E]] extends RelationalPredicate[[E]]related (a : E, b : E) : Boolean = a ≤ bend
object WeaklyDescending[[E]] extends RelationalPredicate[[E]]related (a : E, b : E) : Boolean = a ≥ bend
object Flat[[E]] extends RelationalPredicate[[E]]related (a : E, b : E) : Boolean = a = b
end
object Smooth[[E]](c : E) extends RelationalPredicate[[E]]related (a : E, b : E) : Boolean = |a − b| ≤ cend

Figure 9: Traits for describing properties on predicates and example predicates45

object InitsGenerator[[E]](arglist : List[[ E ]]) extends GGenerator[[ E ]]getter list() : List[[ E ]] = arglist
getter defaultImplementation() : List[[ E ]] → List[[ List[[ E ]] ]] = initsImpl [[ E ]]generate2 [[ R, F, M, N, P, Z, Y ]](r : R, f : F, mr : M, mf : N, p : P ) : Z= dodispatching[[ InitsGenerator[[E]], R, F, M, N, P, Z, Y, E ]](self, r, f, mr , mf , p)
end
endinitsImpl [[ E ]](x : List[[ E ]]) : List[[ List[[ E ]] ]] = dox.generate[[ List[[ List[[ E ]]]] ]](InitsReduction[[ E ]], fn (a) ⇒ singleton[[ List[[ E ]] ]](singleton[[ E ]](a)))
endobject InitsReduction[[ E ]] extends Reduction[[ List[[ List[[ E ]] ]] ]]empty(): List[[ List[[ E ]] ]] = emptyList[[ List[[ E ]] ]]()
join(a : List[[ List[[ E ]] ]], b : List[[ List[[ E ]] ]]): List[[ List[[ E ]] ]] = dol = a.right().generate[[ List[[ E ]]]](Concat[[ E ]], fn (x) ⇒ x);a.append (b.map[[ List[[ E ]] ]](fn (x) ⇒ l.append (x)));end
end
inits[[ E ]](x : List[[ E ]]) : GGenerator[[E]] = InitsGenerator[[E]](x)Figure 10: Base definition of GGenerator inits

5.3

Implementation of GGenerator inits

This section gives implementations for GGenerator inits: an object for base implementationof inits and methods for efficient implementations of nested reductions given by theorems in
Section 4.3.

5.3.1

Base Implementation

The base implementation of GGenerator inits is object InitsGenerator given in Figure 10. A
related example problem is found in Section 3.3.1. A related theory is found in Section 4.3.1.
Object InitsGenerator takes the original list as its argument, and getter list() returns
the given original list. Default implementation of GGenerator inits is defined outside the object InitsGenerator as function initsImpl shown below. Method generate2 invokes function
dispatching (Section 5.1.2) to dispatch suitable implementation to a user program specified by
the given arguments.
Function initsImpl generates a list of prefix (initial) segments using method generate of thegiven list with reduction object InitsReduction shown below.
InitsReduction takes two lists of initial segments (a and b in the code), and returns a listof initial segments of the concatenated list. Suppose a is a list of initial segments of a list x ,and b is that of a list y . InitsReduction makes a list of initial segments of the concatenatedlist x .append (y) from a and b as follows. Initial segments of x are also initial segments ofthe concatenated list. So, all elements in a remain in the result. Each initial segment of yneeds to be concatenated with x to become an initial segment of the concatenated list. So,
InitsReduction maps a function to concatenate the last (rightmost) element of a (x is the lastelement of a ) to each element of b so that it can become an initial segment of the concatenated
list.
46

efficientImplTrueDistributive[[ R, F, M, N, P, Z, Y ]](r : R, f : IdFunction[[Y ]], mr : LeftDistributiveOver[[R]], mf : N, p : TrueListPredicate[[E]])= dojoin(x, y) = do
(i1 , s1 ) = x(i2 , s2 ) = y(r.join(i1 , mr .join(s1 , i2 )), mr .join(s1 , s2 ))endzero = (r.empty(), mr .empty())(r1 , r2 ) = list().generate[[(Z, Z)]](MapReduceReduction[[(Z, Z)]](join, zero),(fn a ⇒ do b = mf .apply(a); (b, b) end))
r1
end

Figure 11: Efficient implementation of nested reductions with distributive operators for GGenerator inits
5.3.2

Implementation for Nested Reductions with Distributive Operators

Figure 11 shows the efficient implementation efficientImplTrueDistributive for Theorem 15 inSection 4.3.2, which should be implemented in object InitsGenerator to be used in dispatching.
A related example problem is found in Section 3.3.2.
The signature of efficientImplTrueDistributive is almost the same as method generate2 oftrait GGenerator. The types of some arguments are restricted to guarantee that the applicablecondition of the theorem is satisfied by the arguments. Basically, restriction on types here is
not necessary because the checking of types are performed before an invocation of this method.
The type restriction in the code is added for safety.
Function join defined in efficientImplTrueDistributive is straightforward implementation of
the new operator ⊙ given in the theorem. Function join is applied to tuples. The first elementof a tuple is the result of the nested reductions. The second element of the tuple is the resultof a reduction with mr , which is used to improve efficiency by reuse of partial results. Value
zero is the identity of the new operator, constructed from identities of the operators used in
the original nested reductions. The reduction with the new operator is performed by generateof the original list (list () in the code). The body function given to generate is extended toapply a function mf before the reduction. The correctness of this extension is guaranteed by
Theorem 14
To dispatch this implementation to a user program, we have to add an entry to typecaseof the dispatching table (Section 5.1.2). The entry is shown below.
(InitsGenerator[[E]], R, IdFunction[[Y ]], LeftDistributiveOver[[R]], N, TrueListPredicate[[E]])⇒ g.efficientImplTrueDistributive[[R, F, M, N, P, Z, Y ]](r, f, mr , mf , p)

Since the condition for the theorem is that the inner reduction (mr ) has left-distributivity over
the outer reduction (r ), the entry checks whether mr extends trait LeftDistributiveOver[[R]].
Also, it checks that f is the identity function and p is the true-predicate, since the theorem
cannot deal with other functions and predicates.
5.3.3

Implementation for Filtering with Relational Predicates

Figure 12 shows the efficient implementation efficientImplRelationalDistributive for Corollary 17(Theorem 16) in Section 4.3.3, which should be implemented in object InitsGenerator to be
used in dispatching. A related example problem is found in Section 3.3.3.
47

efficientImplRelationalDistributive[[ R, F, M, N, P, Z, Y ]](r : R, f : IdFunction[[Y ]], mr : LeftDistributiveOver[[R]], mf : N, p : RelationalPredicate[[E]])= dojoin(x, y) = do
(i1 , s1 , h1 , l1 ) = x(i2 , s2 , h2 , l2 ) = y
px = typecase (l1 , h2 ) of
(Just[[E]], Just[[E]]) ⇒ p.related (l1 .unJust(), h2 .unJust())
else⇒ trueend
if px then(r.join(i1 , mr .join(s1 , i2 )), mr .join(s1 , s2 ), takeleft(h1 , h2 ), takeright(l1 , l2 ))
else(i1 , r.empty(), takeleft(h1 , h2 ), takeright(l1 , l2 ))end
end
zero = (r.empty(), mr .empty(), Nothing[[E]], Nothing[[E]])(r1 , r2 , r3 , r4 ) = list().generate[[(Z, Z, Maybe[[E]], Maybe[[E]])]](MapReduceReduction[[(Z, Z, Maybe[[E]], Maybe[[E]])]](join, zero),(fn a ⇒ do b = mf .apply(a); (b, b, Just[[E]](a), Just[[E]](a)) end))
r1
end

Figure 12: Efficient implementation of nested reductions with distributive operators and filtering
by relational predicate for GGenerator inits
The signature of efficientImplRelationalDistributive is almost the same as method generate2
of trait GGenerator. The types of some arguments are restricted to guarantee that the applicable condition of the theorem is satisfied by the arguments. Basically, restriction on types here is
not necessary because the checking of types are performed before an invocation of this method.
The type restriction in the code is added for safety.
Function join defined in efficientImplRelationalDistributive is straightforward implementation of the new operator ⊠ given in the theorem. Function join is applied to quadruples. The
first element of a quadruple is the result of the nested reductions. The second element of thequadruple is the result of a reduction with mr after filtering with p, which is used to improve
efficiency by reuse of partial results. The third and the fourth elements are the edge elementsof the input, which are used to check whether results from two recursions in divide-and-conquer
computation can be combined to make a better solution. Value zero is the identity of the new
operator, constructed from identities of the operators used in the original nested reductions.
The reduction with the new operator is performed by generate of the original list (list () inthe code). The body function given to generate is extended to apply a function mf before thereduction. The correctness of this extension is guaranteed by Theorem 14
To dispatch this implementation to a user program, we have to add an entry to typecaseof the dispatching table (Section 5.1.2). The entry is shown below.
(InitsGenerator[[E]], R, IdFunction[[Y ]], LeftDistributiveOver[[R]], N, RelationalPredicate[[E]])⇒ g.efficientImplRelationalDistributive[[R, F, M, N, P, Z, Y ]](r, f, mr , mf , p)

Since the condition for the theorem is that the inner reduction (mr ) has left-distributivity over
the outer reduction (r ) and the predicate (p ) is relational, the entry checks whether mr extends
trait LeftDistributiveOver[[R]] and p extends trait RelationalPredicate. Also, it checks that f
is the identity function, since the theorem cannot deal with other functions.

48

object TailsGenerator[[E]](arglist : List[[ E ]]) extends GGenerator[[ E ]]getter list() : List[[ E ]] = arglist
getter defaultImplementation() : List[[ E ]] → List[[ List[[ E ]] ]] = tailsImpl [[ E ]]generate2 [[ R, F, M, N, P, Z, Y ]](r : R, f : F, mr : M, mf : N, p : P ) : Z= dodispatching[[ TailsGenerator[[E]], R, F, M, N, P, Z, Y, E ]](self, r, f, mr , mf , p)
end
end
tailsImpl [[ E ]](x : List[[ E ]]) : List[[ List[[ E ]] ]] = dox.generate[[ List[[ List[[ E ]]]] ]](TailsReduction[[ E ]], fn (a) ⇒ singleton[[ List[[ E ]] ]](singleton[[ E ]](a)))
endobject TailsReduction[[ E ]] extends Reduction[[ List[[ List[[ E ]] ]] ]]empty(): List[[ List[[ E ]] ]] = emptyList[[ List[[ E ]] ]]()
join(a : List[[ List[[ E ]] ]], b : List[[ List[[ E ]] ]]): List[[ List[[ E ]] ]] = doh = b.left().generate[[ List[[ E ]]]](Concat[[ E ]], fn (x) ⇒ x);a.map[[ List[[ E ]] ]](fn (x) ⇒ x.append (h)).append (b);endendtails[[ E ]](x : List[[ E ]]) : GGenerator[[E]] = TailsGenerator[[E]](x)Figure 13: Base definition of GGenerator tails

5.4

Implementation of GGenerator tails

This section gives implementations for GGenerator tails: an object for base implementationof tails and methods for efficient implementations of nested reductions given by theorems in
Section 4.4.
5.4.1

Base Implementation

The base implementation of GGenerator tails is object TailsGenerator given in Figure 13. A
related example problem is found in Section 3.4.1. A related theory is found in Section 4.4.1.
Object TailsGenerator takes the original list as its argument, and getter list() returns
the given original list. Default implementation of GGenerator tails is defined outside the object TailsGenerator as function tailsImpl shown below. Method generate2 invokes function
dispatching (Section 5.1.2) to dispatch suitable implementation to a user program specified by
the given arguments.
Function tailsImpl generates a list of suffix (tail) segments using method generate of thegiven list with reduction object TailsReduction shown below.
TailsReduction takes two lists of tail segments (a and b in the code), and returns a list of tailsegments of the concatenated list. Suppose a is a list of tail segments of a list x , and b is thatof a list y . TailsReduction makes a list of tail segments of the concatenated list x .append (y)from a and b as follows. Tail segments of y are also tail segments of the concatenated list. So,
all elements in b remain in the result. Each tail segment of x needs to be concatenated withy to become a tail segment of the concatenated list. So, TailsReduction maps a function to
concatenate the first (leftmost) element of b (y is the first element of b ) to each element of aso that it can become an tail segment of the concatenated list.
5.4.2

Implementation for Nested Reductions with Distributive Operators

Figure 14 shows the efficient implementation efficientImplTrueDistributive for Theorem 15 inSection 4.4.2, which should be implemented in object TailsGenerator to be used in dispatching.
49

efficientImplTrueDistributive[[ R, F, M, N, P, Z, Y ]](r : R, f : IdFunction[[Y ]], mr : RightDistributiveOver[[R]], mf : N, p : TrueListPredicate[[E]])= dojoin(x, y) = do
(t1 , s1 ) = x(t2 , s2 ) = y(r.join(mr .join(t1 , s2 ), t2 ), mr .join(s1 , s2 ))endzero = (r.empty(), mr .empty())(r1 , r2 ) = list().generate[[(Z, Z)]](MapReduceReduction[[(Z, Z)]](join, zero),(fn a ⇒ do b = mf .apply(a); (b, b) end))
r1
end

Figure 14: Efficient implementation of nested reductions with distributive operators for GGenerator tails
A related example problem is found in Section 3.4.2.
The signature of efficientImplTrueDistributive is almost the same as method generate2 oftrait GGenerator. The types of some arguments are restricted to guarantee that the applicablecondition of the theorem is satisfied by the arguments. Basically, restriction on types here is
not necessary because the checking of types are performed before an invocation of this method.
The type restriction in the code is added for safety.
Function join defined in efficientImplTrueDistributive is straightforward implementation of
the new operator ⊛ given in the theorem. Function join is applied to tuples. The first elementof a tuple is the result of the nested reductions. The second element of the tuple is the resultof a reduction with mr , which is used to improve efficiency by reuse of partial results. Value
zero is the identity of the new operator, constructed from identities of the operators used in
the original nested reductions. The reduction with the new operator is performed by generateof the original list (list () in the code). The body function given to generate is extended toapply a function mf before the reduction. The correctness of this extension is guaranteed by
Theorem 20.
To dispatch this implementation to a user program, we have to add an entry to typecaseof the dispatching table (Section 5.1.2). The entry is shown below.
(TailsGenerator[[E]], R, IdFunction[[Y ]], RightDistributiveOver[[R]], N, TrueListPredicate[[E]])⇒ g.efficientImplTrueDistributive[[R, F, M, N, P, Z, Y ]](r, f, mr , mf , p)

Since the condition for the theorem is that the inner reduction (mr ) has right-distributivity over
the outer reduction (r ), the entry checks whether mr extends trait RightDistributiveOver[[R]].
Also, it checks that f is the identity function and p is the true-predicate, since the theorem
cannot deal with other functions and predicates.
5.4.3

Implementation for Filtering with Relational Predicates

Figure 15 shows the efficient implementation efficientImplRelationalDistributive for Corollary 23(Theorem 22) in Section 4.4.3, which should be implemented in object TailsGenerator to be
used in dispatching. A related example problem is found in Section 3.4.3.
The signature of efficientImplRelationalDistributive is almost the same as method generate2
of trait GGenerator. The types of some arguments are restricted to guarantee that the applicable condition of the theorem is satisfied by the arguments. Basically, restriction on types here is
not necessary because the checking of types are performed before an invocation of this method.
The type restriction in the code is added for safety.
50

efficientImplRelationalDistributive[[ R, F, M, N, P, Z, Y ]](r : R, f : IdFunction[[Y ]], mr : RightDistributiveOver[[R]], mf : N, p : RelationalPredicate[[E]])= dojoin(x, y) = do
(t1 , s1 , h1 , l1 ) = x(t2 , s2 , h2 , l2 ) = y
px = typecase (l1 , h2 ) of
(Just[[E]], Just[[E]]) ⇒ p.related (l1 .unJust(), h2 .unJust())
else⇒ trueend
if px then(r.join(mr .join(t1 , s2 ), t2 ), mr .join(s1 , s2 ), takeleft(h1 , h2 ), takeright(l1 , l2 ))else(t2 , r.empty(), takeleft(h1 , h2 ), takeright(l1 , l2 ))end
end
zero = (r.empty(), mr .empty(), Nothing[[E]], Nothing[[E]])(r1 , r2 , r3 , r4 ) = list().generate[[(Z, Z, Maybe[[E]], Maybe[[E]])]](MapReduceReduction[[(Z, Z, Maybe[[E]], Maybe[[E]])]](join, zero),(fn a ⇒ do b = mf .apply(a); (b, b, Just[[E]](a), Just[[E]](a)) end))
r1
end

Figure 15: Efficient implementation of nested reductions with distributive operators and filtering
by relational predicate for GGenerator tails
Function join defined in efficientImplRelationalDistributive is straightforward implementation of the new operator ⊠⊞ given in the theorem. Function join is applied to quadruples. The
first element of a quadruple is the result of the nested reductions. The second element of thequadruple is the result of a reduction with mr after filtering with p, which is used to improve
efficiency by reuse of partial results. The third and the fourth elements are the edge elementsof the input, which are used to check whether results from two recursions in divide-and-conquer
computation can be combined to make a better solution. Value zero is the identity of the new
operator, constructed from identities of the operators used in the original nested reductions.
The reduction with the new operator is performed by generate of the original list (list () inthe code). The body function given to generate is extended to apply a function mf before thereduction. The correctness of this extension is guaranteed by Theorem 20.
To dispatch this implementation to a user program, we have to add an entry to typecaseof the dispatching table (Section 5.1.2). The entry is shown below.
(TailsGenerator[[E]], R, IdFunction[[Y ]], RightDistributiveOver[[R]], N, RelationalPredicate[[E]])⇒ g.efficientImplRelationalDistributive[[R, F, M, N, P, Z, Y ]](r, f, mr , mf , p)

Since the condition for the theorem is that the inner reduction (mr ) has right-distributivity over
the outer reduction (r ) and the predicate (p ) is relational, the entry checks whether mr extends
trait RightDistributiveOver[[R]] and p extends trait RelationalPredicate. Also, it checks thatf is the identity function, since the theorem cannot deal with other functions.

51

object SegsGenerator[[E]](arglist : List[[ E ]]) extends GGenerator[[ E ]]getter list() : List[[ E ]] = arglist
getter defaultImplementation() : List[[ E ]] → List[[ List[[ E ]] ]] = segsImpl [[ E ]]generate2 [[ R, F, M, N, P, Z, Y ]](r : R, f : F, mr : M, mf : N, p : P ) : Z= dodispatching[[ SegsGenerator[[E]], R, F, M, N, P, Z, Y, E ]](self, r, f, mr , mf , p)
end
end
segsImpl [[ E ]](x : List[[ E ]]) : List[[ List[[ E ]] ]] = doconcat(tailsImpl (x).map[[ List[[ List[[ E ]]]]]](initsImpl [[E]]))end
segs[[ E ]](x : List[[ E ]]) : GGenerator[[E]] = SegsGenerator[[E]](x)Figure 16: Base definition of GGenerator segs

5.5

Implementation of GGenerator segs

This section gives implementations for GGenerator segs: an object for base implementationof segs and methods for efficient implementations of nested reductions given by theorems in
Section 4.5.
5.5.1

Base Implementation

The base implementation of GGenerator segs is object SegsGenerator given in Figure 16. A
related example problem is found in Section 3.5. A related theory is found in Section 4.5.1.
Object SegsGenerator takes the original list as its argument, and getter list() returns
the given original list. Default implementation of segs generator is defined outside the object SegsGenerator as function segsImpl shown below. Method generate2 invokes function
dispatching (Section 5.1.2) to dispatch suitable implementation to a user program specified by
the given arguments.
Function segsImpl generates a list of all segments (continuous subsequences) using naive
implementation initsImpl (Section 5.3.1) and tailsImpl (Section 5.4.1).
5.5.2

Implementation for Nested Reductions with Distributive Operators

Figure 17 shows the efficient implementation efficientImplTrueDistributive for Theorem 26 in
Section 4.5.2, which should be implemented in object SegsGenerator to be used in dispatching.
A related example problem is found in Section 3.5.2.
The signature of efficientImplTrueDistributive is almost the same as method generate2 oftrait GGenerator. The types of some arguments are restricted to guarantee that the applicablecondition of the theorem is satisfied by the arguments. Basically, restriction on types here is
not necessary because the checking of types are performed before an invocation of this method.
The type restriction in the code is added for safety.
Function join defined in efficientImplTrueDistributive is straightforward implementationof the new operator ⊚ given in the theorem. Function join is applied to quadruples. The
first element of a quadruple is the result of the nested reductions. The second and the third
elements of the quadruple are the results of the nested reductions on suffixes only and prefixes
only, which are used to improve efficiency by reuse of partial results. The fourth element is theresult of a reduction with mr . Value zero is the identity of the new operator, constructed fromidentities of the operators used in the original nested reductions. The reduction with the new
operator is performed by generate of the original list (list () in the code). The body function52efficientImplTrueDistributive[[ R, F, M, N, P, Z, Y ]](r : Commutative, f : IdFunction[[Y ]],mr : DistributiveOver[[R]], mf : N, p : TrueListPredicate[[E]])= dojoin(x, y) = do
(m1 , i1 , t1 , s1 ) = x(m2 , i2 , t2 , s2 ) = yt = r.join(mr .join(t1 , s2 ), t2 )i = r.join(i1 , mr .join(s1 , i2 ))(r.join(r.join(m1 , m2 ), r.join(t, i)), i, t, mr .join(s1 , s2 ))endzero = (r.empty(), r.empty(), r.empty(), mr .empty())(r1 , r2 , r3 , r4 ) = list().generate[[(Z, Z, Z, Z)]](MapReduceReduction[[(Z, Z, Z, Z)]](join, zero),(fn a ⇒ do b = mf .apply(a); (b, b, b, b) end))
r1
end

Figure 17: Efficient implementation of nested reductions with distributive operators for GGenerator segs
given to generate is extended to apply a function mf before the reduction. The correctness of
this extension is guaranteed by Theorem 25.
To dispatch this implementation to a user program, we have to add an entry to typecaseof the dispatching table (Section 5.1.2). The entry is shown below.
(SegsGenerator[[E]], R, IdFunction[[Y ]], DistributiveOver[[R]], N, TrueListPredicate[[E]])⇒ g.efficientImplTrueDistributive[[R, F, M, N, P, Z, Y ]](r, f, mr , mf , p)

Since the condition for the theorem is that the inner reduction (mr ) has distributivity over
the outer reduction (r ) and the outer reduction is commutative, the entry checks whether mrextends trait DistributiveOver[[R]] and r extends trait Commutative. Also, it checks that f
is the identity function and p is the true-predicate, since the theorem cannot deal with otherfunctions and predicates.
5.5.3

Implementation for Filtering with Relational Predicates

Figure 18 shows the efficient implementation efficientImplRelationalCommutativeDistributive
for Theorem 27 in Section 4.5.3, which should be implemented in object SegsGenerator to be
used in dispatching. A related example problem is found in Section 3.5.3.
The signature of efficientImplRelationalCommutativeDistributive is almost the same as
method generate2 of trait GGenerator. The types of some arguments are restricted to guarantee that the applicable condition of the theorem is satisfied by the arguments. Basically,
restriction on types here is not necessary because the checking of types are performed before an
invocation of this method. The type restriction in the code is added for safety.
Function join defined in efficientImplRelationalCommutativeDistributive is straightforward
implementation of the new operator ◦ given in the theorem. Function join is applied to
hextuples. The first element of a hextuple is the result of the nested reductions. The second
and the third elements of the hextuple are the results of the nested reductions on suffixes only
and prefixes only, which are used to improve efficiency by reuse of partial results. The fourth
element is the result of a reduction with mr after filtering with p. The fifth and the sixth
elements are the edge elements of the input, which are used to check whether results from tworecursions in divide-and-conquer computation can be combined to make a better solution. Value
zero is the identity of the new operator, constructed from identities of the operators used in53efficientImplRelationalCommutativeDistributive[[ R, F, M, N, P, Z, Y ]](r : Commutative, f : IdFunction[[Y ]],mr : DistributiveOver[[R]], mf : N, p : RelationalPredicate[[E]])= dojoin(x, y) = do
(m1 , t1 , i1 , s1 , h1 , l1 ) = x(m2 , t2 , i2 , s2 , h2 , l2 ) = y
px = typecase (l1 , h2 ) of
(Just[[E]], Just[[E]]) ⇒ p.related (l1 .unJust(), h2 .unJust())
else⇒ trueend
if px then(r.join(r.join(m1 , m2 ), mr .join(t1 , i2 )), r.join(mr .join(t1 , s2 ), t2 ),r.join(i1 , mr .join(s1 , i2 )), mr .join(s1 , s2 ),takeleft(h1 , h2 ), takeright(l1 , l2 ))
else(r.join(m1 , m2 ), t2 , i1 , r.empty(), takeleft(h1 , h2 ), takeright(l1 , l2 ))end
end
zero = (r.empty(), r.empty(), r.empty(), mr .empty(), Nothing[[E]], Nothing[[E]])(r1 , r2 , r3 , r4 , r5 , r6 ) = list().generate[[(Z, Z, Z, Z, Maybe[[E]], Maybe[[E]])]](MapReduceReduction[[(Z, Z, Z, Z, Maybe[[E]], Maybe[[E]])]](join, zero),(fn a ⇒ do b = mf .apply(a); (b, b, b, b, Just[[E]](a), Just[[E]](a)) end))
r1
end

Figure 18: Efficient implementation of nested reductions with distributive operators and filtering
by relational predicate for GGenerator segs
the naive nested reductions. The reduction with the new operator is performed by generateof the original list (list () in the code). The body function given to generate is extended toapply a function mf before the reduction. The correctness of this extension is guaranteed by
Theorem 25.
To dispatch this implementation to a user program, we have to add an entry to typecaseof the dispatching table (Section 5.1.2). The entry is shown below.
(SegsGenerator[[E]], Commutative, IdFunction[[Y ]], DistributiveOver[[R]], N, RelationalPredicate[[E]])⇒ g.efficientImplRelationalCommutativeDistributive[[R, F, M, N, P, Z, Y ]](r, f, mr , mf , p)

Since the condition for the theorem is that the inner reduction (mr ) has distributivity over theouter reduction (r ), the outer reduction is commutative, and the predicate (p ) is relational,
the entry checks whether mr extends trait DistributiveOver[[R]], r extends trait Commutativeand p extends trait RelationalPredicate. Also, it checks that f is the identity function, since
the theorem cannot deal with other functions.

54

(MIS)(MAIS)(MTS)(MATS)(MSS)(MDSS)

mis = BIG MAX hPy | y ← inits x iPmais = BIG MAX h y | y ← inits x, ascending(y) iP
mts = BIG MAX h y | y ← tails x iPmats = BIG MAX h y | y ← tails x, ascending(y) iP
mss = BIG MAX h y | y ← segs x iPmdss = BIG MAX h y | y ← segs x, descending(y) iFigure 19: Programs for experiment

5.6

Experimnt Results

This section shows the power of automatic optimization with dispatching implementation. Figure 19 shows the target programs of the experiment. Since the desugaring process does notwork well, we desugared comprehensions by hand.
Execution time of each program is measured on the current Fortress interpreter [For] in twocases. In the first case (case “naive”), the library does not know any theorems and dispatches
naive implementations to programs. In the second case (case “efficient”), the library knows
theorems and dispatches accompanying efficient implementations to programs.
Measured execution time (an average of eight executions) is shown in Table 1. The measurement is performed on a PC with two quadcore CPUs (Intel R Xeon R E5430, total 8 cores), 8GB
memory, and Linux 2.6.22. The execution time contains startup time of a Fortress program, as
well as the execution time of the program code.
The ratio of execution time of two cases shows the power of the optimization by dispatching,although the absolute speed is not meaningful because the interpreter is still under active
development. Dispatching the efficient implementation, the library succeeded in improving theefficiency of the user program to achieve ten times faster execution time. So, a user program
naively written with our GG library can run efficiently.

55

Table 1: Execution time and relative speed of dispatched naive/efficient implementation
problem
MIS

case
naive
efficient

MAIS

naive
efficient

MTS

naive
efficient

MATS

naive
efficient

MSS

naive
efficient

MDSS

naive
efficient

input size
1000
2000
1000
2000
1000
2000
1000
2000
1000
2000
1000
2000
1000
2000
1000
2000
100
200
100
200
100
200
100
200

execution time (s)
19.72
71.49
0.40
0.46
31.53
117.86
0.50
0.61
20.88
76.54
0.40
0.51
32.92
127.47
0.49
0.63
17.51
92.00
0.35
0.35
22.02
125.37
0.35
0.35

56

relative speed (naive / x)
1.00
1.00
49.30
155.41
1.00
1.00
63.06
193.21
1.00
1.00
52.20
150.07
1.00
1.00
67.18
202.33
1.00
1.00
50.02
262.85
1.00
1.00
62.91
358.206Conclusion

This report provides collections for enriching the power of “GG library.” It provides a collectionof GGenerators with example problems, a collection of theories on GGenerators for efficient
implementations with formal discussion, and a collection of their actual implementation in GG
library on Fortress.
The library will grow with further collections of GGenerators and theories.

Acknowledgments
This report is a partial result of a joint research project “Development of a library based onskeletal parallel programming in Fortress” with Sun Microsystems. We would like to thank themembers of Project Fortress, especially, Guy L. Steele Jr. and Jan-Willem Maessen for fruitful
discussions on this research.

References[ACH+ ]

Eric Allen, David Chase, Joe Hallett, Victor Luchangco, Jan-Willem Maessen, Sukyoung Ryu, Guy L. Steele Jr., and Sam Tobin-Hochstadt. The Fortress language
specification version 1.0 β. available on web:
http://research.sun.com/projects/plrg/Publications/fortress1.0beta.pdf.

[Bir87]

Richard S. Bird. An introduction to the theory of lists. In Proceedings of the NATO
Advanced Study Institute on Logic of programming and calculi of discrete design,
pages 5–42, New York, NY, USA, 1987. Springer-Verlag New York, Inc.

[Bir98]Richard S. Bird. Introduction to Functional Programming using Haskell. PrenticeHall Series in Computer Science. Prentice Hall, 2nd edition, April 1998.

[Bir01]

Richard S. Bird. Functional pearls maximum marking problems. Journal of Functional Programming, 11(4):411–424, 2001.

[Ble90]Guy E. Blelloch. Prefix sums and their applications. Technical Report CMU-CS-90190, School of Computer Science, Carnegie Mellon University, November 1990.

[EHK+ 08] Kento Emoto, Zhenjiang Hu, Kazuhiko Kakehi, Kiminori Matsuzaki, and Masato
Takeichi. Generator-based GG Fortress library. Technical Report METR2008–16,
Department of Mathematical Informatics, Graduate School of Information Scienceand Technology, University of Tokyo, 2008.
available on web: http://www.keisu.t.u-tokyo.ac.jp/research/techrep/.
[For]

Project Fortress. The reference interpreter for the Fortress language.
available on web: http://projectfortress.sun.com/Projects/Community.

[Gor97]Sergei Gorlatch. Optimizing compositions of scans and reductions in parallel program
derivation. Technical Report MPI–9711, Universität Passau, 1997.

[Jeu93]

Johan Theodoor Jeuring. Theories for Algorithm Calculation. PhD thesis, Facultyof Science, Utrecht University, 1993.

[SHT01]

Isao Sasano, Zhenjiang Hu, and Masato Takeichi. Generation of efficient programsfor solving maximum multi-marking problems. In SAIG 2001: Proceedings of theSecond International Workshop on Semantics, Applications, and Implementation of
Program Generation, pages 72–91, London, UK, 2001. Springer-Verlag.
57

[SHTO00] Isao Sasano, Zhenjiang Hu, Masato Takeichi, and Mizuhito Ogawa. Make it practical:
a generic linear-time algorithm for solving maximum-weightsum problems. In ICFP
’00: Proceedings of the fifth ACM SIGPLAN international conference on Functional
programming, pages 137–149, New York, NY, USA, 2000. ACM.
[Ski90]David B. Skillicorn. Architecture-independent parallel computation. Computer,23(12):38–50, 1990.

[Zan92]

Hans Zantema. Longest segment problems. Science of Computer Programming,
18(1):39–66, 1992.

[Zha02]

Haiyan Zhao. A Compositional Approach to Mining Optimal Ranges. PhD thesis,
Department of Information Engineering, University of Tokyo, 2002.

58