The Challenge of Optimality in Program Specialisation
There is a ubiquitous trade-off in software design between generality and efficiency -- should we write general software, which can be used to solve a wide variety of problems, or specialised software optimised to solve a particular case fast? Automatic program specialisation offers a way to have our cake and eat it too: a program specialiser is a tool which can transform a general program into an efficient specialised one, thus enabling us to enjoy both the labour savings of writing a single general purpose program for a whole class of problems, and the speed gained from using an efficient specialised program to solve each individual case.
If we think of a general purpose program as interpreting a problem description to determine which particular problem it should solve, then we can think of a program specialiser as removing a layer of interpretation. Some program specialisers succeed in removing more interpretation than others, and thus generate more efficient specialised programs. We can even define a notion of optimal program specialisation -- an optimal specialiser can remove a complete layer of interpretation, in the sense that it can completely eliminate a "universal interpreter" for the programming language itself. An optimal specialiser can generate any program that can be written by hand, thus reducing the inherent extra cost of using a specialiser to zero.
During the eighties and early nineties optimal specialisers were developed for wider and wider classes of programming languages -- with dynamic typing. But languages with static typing proved a tough nut to crack. An optimal specialiser for a typed language must be able to specialise types as well as programs, and this is not easy to do. The problem was recognised in the mid eighties, but remained open for almost a decade.
In my lecture, I will explain how I solved this problem very simply, by adopting a fundamentally different approach to program specialisation, which moreover offers many other benefits also.