Abstract A new program transformation method is presented. It is a further refinement of supercompilation where the supercompiler is not applied directly to the function to be transformed, but to a metafunction, namely an interpreter which computes this function using its definition and an abstract (i.e. including variables) input. It is shown that with this method such tranformations become possible which the direct application of the supercompiler cannot perform. Examples include the merging of iterative loops, function inversion, and transformation of deterministic into non-deterministic algorithms, and vice-versa .

We proved by construction an application considered theoretically by Turchin [7] that self-application of metacomputation will allow the automatic construction of inverse algorithms, in particular the algorithm of binary subtraction from the algorithm of binary addition. Further, we will present results concerning the algorithmic construction of an efficient pattern matcher, which leads to the Knuth, Morris and Pratt algorithm. These results were achieved with the first working model of a self-applicable supercompiler system, implementing the concept of metacomputation.

The interpretation of the ZF set theory reported in this paper is, actually, part of a wider effort, namely, a new approach to the foundation of mathematics, which is referred to as The Cybernetic Foundation. A detailed exposition of the Cybernetic Foundation will be published elsewhere. Our approach leads to a full acceptance of the formalism of the classical set theory, but interprets it using only the idea of potential, but not actual (completed) infinity, and dealing only with finite objects that can actually be constructed. Thus we have a finitist proof of the consistency of ZF. This becomes possible because we set forth a metatheory of mathematics which goes beyond the classical logic and set theory and, of course, cannot be formalized in ZF, yet yields proofs which are as convincing—at least, from the author's viewpoint—as any mathematical proof can be. Our metatheory is based on the following two ideas. Firstly, we define the semantics of the mathematical language using the cybernetical concept of knowledge. According to this concept, to say that a cybernetic system (a human being, in particular) has some knowledge is to say that it has some models of reality. In the Cybernetic Foundation we consider mathematics as the art of constructing linguistic models of reality.

A supercompiler is a program transformer of a certain type. It traces the possible generalized histories of computation by the original program, and compiles an equivalent program, reducing in the process the redundancy that could be present in the original program. The nature of the redundancy that can be eliminated by supercompilation may be various, e.g., some variables might have predefined values (as in partial evaluation), or the structure of control transfer could be made more efficient (as in lazy evaluation), or it could simply be the fact that the same variable is used more than once. The general principles of supercompilation are described and compared with the usual approach to program transformation as a stepwise application of a number of equivalence rules. It is argued that the language Refal serves the needs of supercompilation best. Refal is formally defined and compared with Prolog and other languages. Examples are given of the operation of a Refal supercompiler implemented at CCNY on an IBM/370.