Abstract interpretation of partial evaluation algorithms

Partial evaluation is an automatic program transformation technique that instantiates general programs to specialized programs, enabling removal of interpretive overhead and even automatic compiler generation. Partial evaluators are defined by an extensional correctness condition: running the partial evaluator on the source program and part of its input data and then running the specialized program on the remaining data must give the same result as running the source program on all the data (modulo termination). So the definition of partial evaluation guarantees that the specialized programs will be correct, that is, that they will compute the right function. Computer scientists, however, are not only interested in which function a program computes, but also in how it computes it: the intensional aspects. The definition of partial evaluation is purely extensional and does not give any guarantees about the intensional properties of the specialized programs. In order to fully exploit the potentials of partial evaluation, this aspect must also be explored, preferably with the same solid foundation in formal correctness as the extensional definition gives. In the general framework of partial evaluation of applicative programs based on polyvariant specialization, we study the family of specialized programs that can be generated from a given general program. We consider which intensional properties the programs in such a family will share and whether they can be pre-determined. We develop an analysis, based on abstract interpretation, that generates a grammar describing the family, based only on the partial evaluator and (parts of) the source program. We prove that the analysis is safe with respect to a standard semantics, in the sense that a concrete result is in the language generated by the abstract result. We use the analysis on several examples and show that various informal claims about the intensional properties of specialized programs can be justified formally. The analysis is also generally applicable to other program transformers and we show an example of this.