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.rnThe 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 su-percompilation notions as configuration, driving, generalization of a configuration, and a simple case of splitting a configuration.rnThe 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.