Jones N.D.Partial evaluation and automatic program generation.1999
.pdfPartial Evaluation
and Automatic Program Generation
Neil D. Jones
DIKU, Department of Computer Science, University of Copenhagen Universitetsparken 1, DK-2100 Copenhagen , Denmark
Carsten K. Gomard
DIKU and Computer Resources International A/S
Bregner dvej 144, DK-3460 Birker d, Denmark
Peter Sestoft
Department of Computer Science, Technical University of Denmark Building 344, DK-2800 Lyngby, Denmark
with chapters by
Lars Ole Andersen and Torben Mogensen
DIKU, Department of Computer Science, University of Copenhagen Universitetsparken 1, DK-2100 Copenhagen , Denmark1
Originally published by Prentice Hall International 1993; ISBN 0-13-020249-5. In 1999, the copyright has been transferred back to the authors.
Copyright c 1999 Neil D. Jones, Carsten K. Gomard, and Peter Sestoft; the book homepage is http://www.dina.kvl.dk/~sestoft/pebook/pebook.html
Contents
Preface |
|
x |
|
1 |
Introduction |
1 |
|
|
1.1 |
Partial evaluation = program specialization |
1 |
|
1.2 |
Why do partial evaluation? |
5 |
|
1.3 |
Computation in one stage or more |
7 |
|
1.4 |
Partial evaluation and compilation |
11 |
|
1.5 |
Automatic program generation |
13 |
|
1.6 |
Critical assessment |
15 |
|
1.7 |
Overview of the book |
17 |
I |
Fundamental Concepts in Programming Languages |
21 |
|
2 |
Functions, Types, and Expressions |
23 |
|
|
2.1 |
Functions |
23 |
|
2.2 |
Types in programming languages |
26 |
|
2.3 |
Recursive data types |
32 |
|
2.4 |
Summary |
36 |
|
2.5 |
Exercises |
37 |
3 |
Programming Languages and Interpreters |
38 |
|
|
3.1 |
Interpreters, compilers, and running times |
38 |
|
3.2 |
The untyped lambda calculus: syntax and semantics |
43 |
|
3.3 |
Three mini-languages |
50 |
|
3.4 |
Compiling compilers |
58 |
|
3.5 |
The central problems of compilation |
60 |
|
3.6 |
Summary |
61 |
v
vi |
Contents |
|
|
|
3.7 |
Exercises |
62 |
II |
Principles of Partial Evaluation |
65 |
|
4 Partial Evaluation for a Flow Chart Language |
67 |
||
|
4.1 |
Introduction |
68 |
|
4.2 |
What is partial evaluation? |
69 |
|
4.3 |
Partial evaluation and compilation |
73 |
|
4.4 |
Program specialization techniques |
76 |
|
4.5 |
Algorithms used in mix |
85 |
|
4.6 |
The second Futamura projection: compiler generation |
86 |
|
4.7 |
Generating a compiler generator: mix3 |
91 |
|
4.8 |
The tricks under the carpet |
91 |
|
4.9 |
The granularity of binding-time analysis |
94 |
|
4.10 |
Overview of mix performance |
97 |
|
4.11 |
Summary and a more abstract perspective |
98 |
|
4.12 |
Exercises |
99 |
5 Partial Evaluation for a First-Order Functional Language |
101 |
||
|
5.1 |
From ow charts to functions |
101 |
|
5.2 |
Binding-time analysis by abstract interpretation |
106 |
|
5.3 |
Adding annotations |
110 |
|
5.4 |
Specialization algorithm for Scheme0 |
113 |
|
5.5 |
Call unfolding on the y |
118 |
|
5.6 |
Implementation |
122 |
|
5.7 |
Using type rules for binding-time checking |
123 |
|
5.8 |
Constructing the generating extension |
125 |
|
5.9 |
Exercises |
125 |
6 |
E ciency, Speedup, and Optimality |
127 |
|
|
6.1 |
De ning and measuring speedup |
127 |
|
6.2 |
Flow chart mix gives linear speedup |
130 |
|
6.3 |
Speedup analysis |
132 |
|
6.4 |
Optimality of mix |
138 |
|
6.5 |
Hierarchies of meta-languages |
139 |
|
6.6 |
Exercises |
141 |
7 Online, O ine, and Self-application |
144 |
||
|
7.1 |
Decision making as a prephase? |
145 |
|
7.2 |
Online and o ine expression reduction |
145 |
|
7.3 |
BTA and the taming of self-application |
153 |
|
7.4 |
A recipe for self-application |
157 |
|
7.5 |
Exercises |
159 |
|
|
Contents |
vii |
III |
Partial Evaluation for Stronger Languages |
161 |
|
8 |
Partial Evaluation for the Lambda Calculus |
163 |
|
|
8.1 |
The lambda calculus and self-interpretation |
164 |
|
8.2 |
Partial evaluation using a two-level lambda calculus |
166 |
|
8.3 |
Congruence and consistency of annotations |
169 |
|
8.4 |
Binding-time analysis |
172 |
|
8.5 |
Simplicity versus power in Lambdamix |
173 |
|
8.6 |
Binding-time analysis by type inference |
175 |
|
8.7 |
BTA by solving constraints |
175 |
|
8.8 |
Correctness of Lambdamix |
183 |
|
8.9 |
Exercises |
190 |
9 |
Partial Evaluation for Prolog |
192 |
|
|
9.1 |
An example |
195 |
|
9.2 |
The structure of Logimix |
196 |
|
9.3 |
Conclusion |
200 |
|
9.4 |
Exercises |
202 |
10 Aspects of Similix: A Partial Evaluator for a Subset of Scheme |
204 |
||
|
10.1 |
An overview of Similix |
204 |
|
10.2 |
Specialization with respect to functional values |
210 |
|
10.3 |
Avoiding duplication |
215 |
|
10.4 |
Call unfolding on the y |
217 |
|
10.5 |
Continuation-based reduction |
218 |
|
10.6 |
Handling partially static structures |
223 |
|
10.7 |
The Similix implementation |
225 |
|
10.8 |
Exercises |
225 |
11 Partial Evaluation for the C Language |
229 |
||
|
11.1 |
Introduction |
229 |
|
11.2 |
Specialization of control ow |
232 |
|
11.3 |
Function specialization |
234 |
|
11.4 |
Data structures and their binding-time separation |
239 |
|
11.5 |
Partial evaluation for C by two-level execution |
245 |
|
11.6 |
Separation of the binding times |
253 |
|
11.7 |
Self-application, types, and double encoding |
256 |
|
11.8 |
C-mix: a partial evaluator for C programs |
256 |
|
11.9 |
Towards partial evaluation for full Ansi C |
258 |
|
11.10 Exercises |
259 |
viii |
Contents |
|
|
IV |
Partial Evaluation in Practice |
261 |
|
12 Binding-Time Improvements |
263 |
||
|
12.1 |
A case study: Knuth, Morris, Pratt string matching |
264 |
|
12.2 |
Bounded static variation |
266 |
|
12.3 |
Conversion into continuation passing style |
270 |
|
12.4 |
Eta conversion |
273 |
|
12.5 |
Improvements derived from `free theorems' |
274 |
|
12.6 |
Exercises |
274 |
13 Applications of Partial Evaluation |
277 |
||
|
13.1 |
Types of problems susceptible to partial evaluation |
277 |
|
13.2 |
When can partial evaluation be of bene t? |
285 |
|
13.3 |
Exercises |
293 |
V |
Advanced Topics |
295 |
|
14 Termination of Partial Evaluation |
297 |
||
|
14.1 |
Termination of online partial evaluators |
297 |
|
14.2 |
Termination of o ine partial evaluators |
298 |
|
14.3 |
Binding-time analysis ensuring termination |
301 |
|
14.4 |
Safety of BTA algorithm |
305 |
|
14.5 |
Exercises |
307 |
15 Program Analysis |
309 |
||
|
15.1 |
Abstract interpretation |
309 |
|
15.2 |
Closure analysis |
314 |
|
15.3 |
Higher-order binding-time analysis |
319 |
|
15.4 |
Projections and partially static data |
323 |
|
15.5 |
Projection-based binding-time analysis |
328 |
|
15.6 |
Describing the dynamic data |
332 |
|
15.7 |
Summary |
333 |
|
15.8 |
Exercises |
333 |
16 Larger Perspectives |
335 |
||
|
16.1 |
Relations to recursive function theory |
335 |
|
16.2 |
Types for interpreters, compilers, and partial evaluators |
337 |
|
16.3 |
Some research problems |
346 |
17 Program Transformation |
347 |
17.1 |
A language with pattern matching |
347 |
17.2 |
Fold/unfold transformations |
350 |
17.3 |
Partial evaluation by fold/unfold |
355 |
|
Contents |
ix |
17.4 |
Supercompilation and deforestation |
358 |
17.5 |
Exercises |
364 |
18 Guide to the Literature |
366 |
|
18.1 |
A brief historical overview |
366 |
18.2 |
Partial evaluation literature by subject language |
368 |
18.3 |
Principles and techniques |
370 |
18.4 |
Applications |
372 |
18.5 |
Other topics related to partial evaluation |
374 |
A The Self-Applicable Scheme0 Specializer |
376 |
|
A.1 |
Using the Scheme0 specializer |
376 |
A.2 |
Data structures in the Scheme0 specializer |
378 |
A.3 |
The components of the Scheme0 specializer |
380 |
Bibliography |
389 |
|
Index |
|
406 |
Preface
This book is about partial evaluation, a program optimization technique also known as program specialization. It presents general principles for constructing partial evaluators for a variety of programming languages; and it gives examples, applications, and numerous references to the literature.
Partial evaluation
It is well known that a one-argument function can be obtained from a two-argument function by specialization, i.e. by xing one input to a particular value. In analysis this is called restriction or projection, and in logic it is called currying. Partial evaluation, however, works with program texts rather than mathematical functions.
A partial evaluator is an algorithm which, when given a program and some of its input data, produces a so-called residual or specialized program. Running the residual program on the remaining input data will yield the same result as running the original program on all of its input data.
The theoretical possibility of partial evaluation was established many years ago in recursive function theory as Kleene's `s-m-n theorem'. This book concerns its practical realization and application.
Partial evaluation sheds new light on techniques for program optimization, compilation, interpretation, and the generation of program generators. Further, it gives insight into the properties of the programming languages themselves.
Partial evaluation can be thought of as a special case of program transformation, but emphasizes full automation and generation of program generators as well as transformation of single programs.
x
Preface xi
Partial evaluation and compilation
Partial evaluation gives a remarkable approach to compilation and compiler generation. For example, partial evaluation of an interpreter with respect to a source program yields a target program. Thus compilation can be achieved without a compiler, and a target program can be thought of as a specialized interpreter.
Compiler generation
Moreover, provided the partial evaluator is self-applicable, compiler generation is possible: specializing the partial evaluator itself with respect to a xed interpreter yields a compiler. Thus a compiler can be thought of as a specialized partial evaluator: one which can specialize only an interpreter for a particular language.
Finally, specializing the partial evaluator with respect to itself yields a compiler generator. Thus a compiler generator can be thought of as a specialized partial evaluator: one which can specialize only itself.
Other applications
The application of partial evaluation is not restricted to compiling and compiler generation. If a program takes more than one input, and one of the inputs varies more slowly than the others, then specialization of the program with respect to that input gives a faster specialized program. Moreover, very many real-life programs exhibit interpretive behaviour. For instance they may be parametrized with con guration les, etc., which seldom vary, and therefore they may be pro tably specialized.
The range of potential applications is extremely large, as shown by the list of examples below. All have been implemented on the computer, by researchers from Copenhagen, MIT, Princeton, and Stanford universities; and INRIA (France) and ECRC (Germany). All have been seen to give signi cant speedups.
Pattern recognition
Computer graphics by `ray tracing'
Neural network training
Answering database queries
Spreadsheet computations
Scienti c computing
Discrete hardware simulation
xii Preface
This book
We give several examples of such applications, but the main emphasis of the book is on principles and methods for partial evaluation of a variety of programming languages: functional (the lambda calculus and Scheme), imperative (a owchart language and a subset of C), and logical (Prolog). We explain the techniques necessary for construction of partial evaluators, for instance program ow analysis, in su cient detail to allow their implementation. Many of these techniques are applicable also in other advanced programming tasks.
The book is structured as follows. The rst chapter gives an overview of partial evaluation and some applications. Then Part I introduces fundamental programming language concepts, de nes three mini-languages, and presents interpreters for them. Part II describes the principles of self-applicable partial evaluation, illustrated using two of the mini-languages: ow charts and rst-order recursion equations. Part III shows how these principles apply to stronger languages: the lambda calculus, and large subsets of the Prolog, Scheme, and C programming languages. Part IV discusses practical aspects of partial evaluation, and presents a wide range of applications. Part V presents more a theoretical view and a number of advanced techniques, and provides extensive references to other research.
The book should be accessible even to beginning graduate students, and thus useful for beginners and researchers in partial evaluation alike.
The perspective on partial evaluation and the selection of material re ect the experience of our group with construction of several partial evaluators. These include the rst non-trivial self-applicable partial evaluators for a functional language, an imperative language, the lambda calculus, a Prolog subset, and a subset of C. This work has been carried out at the University of Copenhagen.
Acknowledgements
Many have contributed to both the substance and the ideas appearing in this book. In particular we want to thank Lars Ole Andersen and Torben Mogensen who wrote two specialist chapters, and Olivier Danvy who provided numerous constructive comments and suggestions. More broadly we would like to express our thanks to: Peter Holst Andersen, Henk Barendregt, Job Baretta, Anders Bondorf, Hans Bruun, Mikhail Bulyonkov, Charles Consel, Robert Gl•uck, Chris Hankin, Reinhold Heckmann, Fritz Henglein, Carsten Kehler Holst, Paul Hudak, John Hughes, Kristian Damm Jensen, Jesper J rgensen, John Launchbury, Alan Mycroft, Hanne and Flemming Nielson, Patrick O'Keefe, Sergei Romanenko, Bill Scherlis, David A. Schmidt, Harald S ndergaard, Morten Heine S rensen, Carolyn Talcott, Valentin Turchin, Phil Wadler, Daniel Weise, and last but not least, Lisa Wiese.
Parts of the research reported here were supported by DIKU (the Department of Computer Science, University of Copenhagen) by the Danish Natural Sciences Research Council, and by ESPRIT Basic Research Action 3124, `Semantique'.