Specifying Monogenetic Specializers by Means of a Relation Between Source and Residual Programs

A specification of a class of specializers for a tiny functional language in form of natural semantics inference rules is presented. The specification defines a relation between source and residual programs with respect to an initial configuration (a set of input data). The specification expresses the idea of

what

is to be a specialized program, avoiding where possible the details of

how

a specializer builds it. In particular, it abstracts from the difference between on-line and off-line specialization.

The class of specializers specified here is limited to

monogenetic

specializers, which includes specializers based upon partial evaluation as well as restricted supercompilation. The specification captures such supercompilation notions as

configuration

,

driving

,

generalization of a configuration

, and a simple case of

splitting a configuration

.

The proposed specification is an

intensional

definition of equivalence between source and residual programs. It provides a shorter cut for proving the correctness and other properties of specializers than usual reduction to the

extensional

equivalence of programs does.