A program specialization relation based on supercompilation and its properties

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 specification 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 specification 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 definition 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.