Strategies and Analysis Techniques for Functional Program Optimization
PhD Thesis Abstract
Abstract
Computer systems play an important role in the modern information society.
However, the low quality of software and its low level of abstraction,
inhibit the necessary confidence of final users and system developers in
software engineering.
Correctness of computer programs by a mathematical theory of computation
is the fundamental concern of the theory of programming and
of its application in large-scale software engineering.
Formal methods provide software engineering with the suitable
scientific and technological framework to become a real engineering,
as predictable
as civil or electrical engineering are.
Indeed, the use of
declarative rule-based programming languages
during all program development stages
ensures that
correct and certified formal methodologies are followed during the whole software production
process.
Programs in declarative rule-based programming languages
are usually described as
term rewriting systems.
Program execution consists of reducing (or rewriting) input terms to output terms
by applying a sequence of rules.
Narrowing is an extension of rewriting for term rewriting systems which
permits the instantiation of variables in
input terms in order to enable rewriting steps on the instantiated expression.
Rewriting (as well as narrowing) is generally undecidable,
i.e. it is not possible to determine if a term rewrites (narrows) to another one.
The reduction space associated to a given input term is huge
due to the different possibilities for selecting subterms to reduce and the rules applicable to those subterms.
This situation is even worse in the case of narrowing due to the instantiation process.
In fact, the reduction (or narrowing) space usually contains
useless (no interesting output expression is achievable),
dangerous (no interesting output expression is guaranteed),
and
inefficient reduction sequences (an alternative more efficient sequence exists which delivers an equivalent outcome).
This thesis faces the problem of how to define efficient methods to
improve the
computational behavior of term rewriting systems,
i.e.
to shrink
the reduction space associated to an input term
by selecting which subterms and/or rules should be used for rewriting (or narrowing).
We consider the following different approaches to optimize programs:
-
By
dynamically selecting
the allowed reductions in execution time due to the definition
of appropriate reduction or narrowing strategies.
We refine this case into two parts:
- Whether the allowed reductions are automatically calculated from the program,
i.e. the appropriate reduction strategy is inferred from the program.
Here, we study the definition of optimal rewriting and narrowing strategies.
Roughly speaking,
we provide an incremental definition of the outermost-needed narrowing strategy
(the best narrowing strategy for term rewriting systems)
and
we improve it,
obtaining the natural narrowing strategy.
- Whether the allowed reductions are provided by assertions of the programmer
included into the program,
i.e. the appropriate reduction strategy is induced by the programmer.
Here, we study different aspects of
the inclusion of syntactic strategy annotations into term rewriting systems.
First, we reformulate (and improve) the computational
model associated in the literature to on-demand strategy annotations by
handling
demandedness in a different way.
Also,
we
provide two program transformations:
one for solving the incompleteness problem w.r.t. the absence of some annotations;
and the other to
encode on-demand strategy annotations into standard annotations
in order to introduce a
flavour of laziness into languages which only consider standard strategy annotations.
-
By statically analyzing the program in compilation time
in order to discard (and remove) some parts. We use
program analysis and transformation techniques.
Here, we study
a different semantics-based problem which is orthogonal to the definition
of reduction or narrowing strategies.
Roughly speaking,
we analyze and remove the irrelevant data appearing in the program in the form of redundant arguments of functions,
which produce inefficient reduction steps which cannot be avoided by a
reduction strategy.
On the other hand,
the proposed techniques are semantically correct,
i.e.
they are strong enough
to avoid undesired sequences
but not too much restrictive in order to preserve
the sequences of interest.
All these research lines lie
on
the common intuitive
idea of optimizing
term rewriting systems at the most simple but flexible and powerful level:
symbol arguments.
Available
Gzipped Postcript (289 pages - 800Kb) -
PDF (289 pages - 1.8Mb) -
BibTex entry