Ph.D. Thesis, Departamento de Sistemas Informáticos y
Computación, Universidad Politécnica de Valencia, Sep 1996.
In Spanish
Published by Ed. UPV, ISBN 84-699-5066-5, 2001
The integration of functional and logic programming languages is one of the most interesting research problems in the area of declarative programming. In order to develop useful and practical integrated languages, it is essential to succeed in shrinking the efficiency gap with respect to imperative languages, as is already being done for Prolog. To this goal, formally based, practical tools for the analysis and transformation of functional logic programs which are able to improve the current implementations are a pressing need. There is common agreement for substituting ad-hoc proposals for more systematic approaches to program manipulation. Since functional logic languages have been widely investigated from the point of view of the semantics, it becomes of natural concern to study formal manipulation techniques based on the semantics, which are able to improve program performances without changing the computational meaning. This thesis explores the development of such techniques, adopting a formal approach based on the (operational) semantics of the integrated language to formulate and evaluate the proposed optimizations within a unified setting.
In the first part of the thesis, a semantic framework for the static analysis of functional logic programs, based on the idea of correctly approximating the operational semantics of the program, is developed. We formalize a simple, uniform and flexible program analysis scheme, which allows us to reason correctly about different program properties (concerning computed answers), and which is easily implementable. The scheme is parameterized by the narrowing strategy which is used in the formulation of the operational principles of the language, thus enhancing its genericity. We also include a methodological study of the (AND-)compositional properties of the narrowing relation, which we extensively exploit to develop incremental (and parallel) optimizations.
We start with a compositional characterization of the operational semantics of functional logic programs. Then we compositionally characterize the success set of a goal, i.e., the set of the computed answer substitutions corresponding to all successfull narrowing derivations. In other words, we prove that the meaning of a composite goal can be obtained by composing the meanings of its conjuncts, when considering the success set as observable. Next, we show that this semantics and the standard operational semantics for ascertained kinds of narrowing, coincide. We define an abstract narrower mimicking this semantics, and show how it can be used as a basis for efficient AND-compositional program analysis. As an application of our framework, we present a compositional analysis to detect the unsatisfiability of an equation set with respect to a given program. We also show that our method allows us to perform computations and analysis incrementally in a constraint equational setting and that the tests of unsatisfiability in this setting can be done in parallel.
Program transformation aims to derive better semantically equivalent programs. Of the great amount of literature on program transformation, partial evaluation (PE) work has been the most intensively pursued over the last two decades. It has been extensively applied both in functional and in logic programming. In the second part of this thesis, we show how specialization can be based on the unification-based computational mechanism of narrowing in the context of languages that integrate functional and logic programming. Because of the two-way parameter propagation due to unification, the resulting method can produce significant specializations. Moreover, we show that several optimizations are possible which are unique to the execution mechanism of functional logic programs (as it is the inclusion of a deterministic simplification process). The effectiveness of the method is illustrated by various representative examples dealing with the specialization and the elimination of intermediate data structures.
We present a PE scheme for functional logic languages based on an automatic unfolding algorithm which builds narrowing trees. A generic algorithm is provided that does not depend on the eager or lazy nature of the narrower being used. We study the semantic properties of the transformation as well as the conditions under which the technique terminates, is sound and complete, and is also generally applicable to a wide class of programs. Such conditions depend on the semantics we associate to the program. We consider the semantics of answer substitutions computed by conditional narrowing, and identify sufficient conditions that prove the (strong) computational equivalence of the original and the partially evaluated programs for the intended queries. To the best of our knowledge, this is the first formal approach to PE of functional logic programs .
Available: PS BibTeX-Entry