 |
 |
|
|
|
|
|
|||
|
|
|||
|
July 2-5, 2008, Pereslavl-Zalessky (120 km to the north-east from Moscow), Russia |
|
|
|
|
|
|
|
|
|
|
|
A Program Specialization Relation Based on Supercompilation and its Properties
Andrei V. Klimov
|
Abstract |
Full text
|
An input-output relation for a wide class of program specializers for a simple functional language in the form of Natural Semantics inference rules is presented. It covers polygenetic specialization, which includes deforestation and supercompilation, and generalizes the author's previous paper on speci cation of monogenetic specialization like partial evaluation and restricted supercompilation.
The specialization relation expresses the idea of what is to be a specialized program, avoiding as much as possible the details of how a specializer builds it. The relation speci cation follows the principles of Turchin's supercompilation and captures its main notions: configuration, driving, generalization of a configuration, splitting a configuration, as well as collapsed-jungle driving. It is virtually a formal de nition of supercompilation abstracting away the most sophisticated parts of supercompilers| strategies of configuration analysis.
Main properties of the program specialization relation|idempotency, transitivity, soundness, completeness, correctness|are formulated and discussed.
Keywords:
specialization,
input-output relation,
partial evaluation,
supercompilation,
correctness.