4. Potential Applications and Problems
Supercompilation and partial evaluation belong to the same kind of program transformation, which we refer to as metacomputation. Supercompilation includes, but goes far beyond, partial evaluation. It may cause a deep transformation of a program, especially when combined with various metasystem transitions. Potential applications of driving, supercompilation, and other forms of metacomputation are numerous and include function inversion, program testing and theorem proving.
The boundaries of what is possible to do with metacomputation are not yet clear. Even though the principle of metacomputation is simple, its translation into working machines may be far from being simple. This is not unusual. The basic principles of flying are also simple, but a modern airplane consists of many thousands of details, and it has taken many years of work by many people, in order to develop air technology to the stage when the wonderful machines of today become possible. Metacomputation and, in particular, supercompilation are now at the technological stage of the brothers Wright. Let us hope that the process of technological improvement of supercompilers, which has just started, will produce software tools to be widely used in computer science and industry.
I want to finish by listing a few problems which could serve as milestones for the nearest stretch of the road towards reliable and widely used metacomputation technology.
1. The present supercompiler(s) must be rewritten so that its different parts be
more clearly separated and defined by more formal comments. The goal: to help other
authors to benefit from the existing experience.
2. To build and test a supercompiler with recursive restrictions on the configuration variables (it is partly done, but only non-recursive restrictions have been well tested). The second part of this problem is automatic computation of restrictions in the process of supercompilation.
3. To implement the generalization algorithm based on homeomorphic embedding relation (see Sec.2.2).
4. The present flat supercompiler in combination with a lazy interpreter works as a lazy supercompiler (see [25]). By making one more MST it should be possible to generate a compiled (and hence fast) lazy supercompiler.
5. To achieve the proof, in the computer, of commutativity of addition (see Sec.2.3 and 3.1) and similar theorems.
6. To use in the computer the method of theorem proving outlined in Sec.3.2. What kind of theorems can be proven using the existing SCP? How far can we go?
7. A theoretical analysis is needed of the theorem-proving method in Sec.3.2 in comparison with a formal logical proof.
8. To build a 'clever' interpreter of walk-sets as postulated in Sec.3.1 and test it in the combination with the flat supercompiler.
9. To use Abramov's neighborhood testing on some real-world problems.
10. We have done a few simple cases of automatic inversion of functions using SCP. The problem now is to determine the boundaries of this method and try it with more powerful supercompilers.
Acknowledgment. To avoid repetition of what I have said in the History section, let me simply express my deep gratitude to all those who worked with me or appreciated my work.