Formal specifications of supercompilers by Natural Semantics

Andrei Klimov

Supercompilation is a program transformation method aimed at such problems as program specialization, program composition ("fusion"), inversion etc. The method was conceived in 1970s and 1980s by Valentin Turchin and originally developed for the functional programming language Refal. Related methods -- Partial Evaluation by the group led by Neil Jones and Mixed Computation by Andrei Ershov.

A supercompiler, Scp: p -> q, given a source program p in some programming language builds a equivalent residual program q in the same (or another) language. As a rule, program q is more efficient than p due to specialization of code with respect to known information inherent in the code, and/or constraint of the domain D of the source program p.

Now the area of supercompilation lacks supercompilation theory that allows for formulating and proving general properties of supercompilers independently of particular algorithms implemented in supercompilers, and at least briefly and formally defines what is a supercompiler.

As foundation of such supercompilation theory, we suggest to use supercompiler specifications that define a relation R(p,q,D) between source and residual programs p and q such that the programs are equivalent on domain D. A specification tells what is a possible result of supercompilation, saying nothing about how a supercompiler builds a residual program, what algorithms and strategies are used to take particular decisions.

The specifications are given by deduction rules of Natural Semantics (based on Plotkin's operational semantics) for a simple functional language. The supercompiler specifications are presented as extension of operational semantics of the language interpreter. The main notions of supercompilation such as configuration, driving, generalization, configuration cutting are formalized. Based on the specifications, the correctness and other properties of supercompilers that meet the specifications, can be proved.

Prerequisites: Informal acquaintance with the ideas of supercompilation as it was presented at this seminar on April 28, 2004 ("Supercompilation and Partial Evaluation: introduction and the state of affairs") is desirable.