We show that the power of supercompilation can be increased by constructing a hierarchy of supercompilers, in which a lowerlevel supercompiler is used by a higher-level one for proving improvement lemmas. The lemmas thus obtained are used to transform expressions labeling nodes in process trees,...

One of the applications of supercompilation is proving properties of programs. We focus in this paper on a specific task: proving term equivalence for a higher-order lazy functional language. The "classical" way to prove equivalence of two terms t1 and t2 is to write an equality...

The paper describes a simple supercompiler SPSC for a lazy first-order functional language. Each section of the paper starts by introducing an important aspect of supercompilation and then provides an implementation of the corresponding algorithms in Scala.

Суперкомпиляция является мощным, но довольно сложным методом анализа и оптимизации программ. В данной статье представлен полный текст простого, но реально...

This tutorial shows how to rewrite an interpreter written in a higher-order functional language, so that it will become more similar to a compiler, thereby eliminating the overhead due to interpretation.

Experiments on generating compilers by specializing specializers with respect to interpreters have shown that the compilers thus obtained have a natural structure only if the specializer does variable splitting. Variable splitting can result in a residual program using several variables to...

Most implementations of the language Refal represent ground expressions by doubly-linked lists, which results in low-cost concatenation. On the other hand, that representation necessitates the real copying of expressions in all cases where a variable's value has to be used two or more times....

This paper describes the structure of, and the ideas behind, a self-applicable specializer of programs, as well as the principles of operation of a compiler generator that has been produced automatically by specializing the specializer with respect to itself. It has been found that the structure...