Strategies and Analysis Techniques for Functional Program Optimization
PhD Thesis Abstract



Author: Santiago Escobar
Title: Strategies and Analysis Techniques for Functional Program Optimization
Language of presentation: English
Promotor: María Alpuente and Salvador Lucas
Date of defense: October 31, 2003
Institution granting degree: Universidad Politécnica de Valencia, Spain
Examiners: Hélène Kirchner, Francisco López-Fraguas, José Meseguer, Isidro Ramos, and Albert Rubio

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:

  1. 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:
    1. 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.
    2. 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.
  2. 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