Offline Narrowing-Driven Partial Evaluation
|
Return to: main page.. |
|
|
||||||||||||||||||||||||||||||||||||||||||
|
|
We have extended the offline approach to narrowing-driven
partial evaluation presented in [1]. In particular, we analyzed the
quasi-termination of computations by means of so called size-change
graphs (rather than using a simpler syntactic characterization). The
resulting analysis is more expensive but also much more precise.
Moreover, in contrast to [1], we also integrate the
information from a standard binding-time analysis so that the number
of program annotations (i.e., the number of expressions that should
be generalized at partial evaluation time to ensure termination) is
further reduced. |
|
||||||||||||||||||||||||||||||||||||||||||
|
|
|
|
||||||||||||||||||||||||||||||||||||||||||
|
|
Given an inductively sequential TRS R, the first stage of the process consists in computing the annotated TRS: ann(R). In [1], annotations were added to those subterms that violate the non-increasingness condition, a simple syntactic characterization of programs that guarantees the quasi-termination of computations. Nevertheless, annotations can be based on other, more refined analysis as long as the annotated program still ensures the global termination.
The signature of a program is extended with a fresh symbol "ann". Given a TRS R, a term t is then annotated by replacing t by ann(t). Then, the second stage, the proper partial evaluation, takes the annotated TRS, ann(R), together with an initial term, t, and constructs the (finite) generalizing needed narrowing tree for t in ann(R) where, additionally, a test is included to check whether a variant of the current term has already been computed and, if so, stop the derivation; finally, a residual, partially evaluated, program is extracted from the generalizing needed narrowing tree. Informally, a generalizing needed narrowing derivation is composed of:
|
|
||||||||||||||||||||||||||||||||||||||||||
|
|
|
|
||||||||||||||||||||||||||||||||||||||||||
|
|
We implemented an annotating algorithm which takes a function definition and annotates those terms that break the quasi-terminating property. Essentially, in the annotation phase, we first compute the maximal multigraphs of the program. Then, for every function call we annotate those arguments which does not have an arc in some of its corresponding maximal multigraphs; finally, all repeated occurrences of dynamic variables but one are annotated. Main advantage: precision. The new schema is much more precise because:
|
|
||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||
|
|
We have conducted some experiments in order to compare both approaches (the one presented in [1] and the one based on Size-Change Graphs). Next table summarizes the results of both annotating algorithms:
Results show that even in the worst case of the SCHG annotating algorithm, when all the arguments are dynamic (and thus, no information from the BTAis profitable) the number of annotations is reduced w.r.t. the old schema. [1] J. Guadalupe Ramos, Josep Silva, Germán Vidal |
|
||||||||||||||||||||||||||||||||||||||||||
