Deductive Synthesis Of The Unification Algorithm

Abstract

The deductive approach is a formal program construction method in which the derivation of a program from a given specification is regarded as a theorem-proving task. To construct a program whose output satisfies the conditions of the specification, we prove a theorem stating the existence of such an output. The proof is restricted to be sufficiently constructive so that a program computing the desired output can be extracted directly from the proof. The program we obtain is applicative and may consist of several mutually recursive procedures. The proof constitutes a demonstration of the correctness of this program.

To exhibit the full power of the deductive approach, we apply it to a nontrivial example–the synthesis of a unification algorithm. Unification is the process of finding a common instance of two expressions. Algorithms to perform unification have been central to many theorem-proving systems and to some programming-language processors.

The task of deriving a unification algorithm automatically is beyond the power of existing program synthesis systems. In this paper we use the deductive approach to derive an algorithm from a simple, high-level specification of the unification task. We will identify some of the capabilities required of a theorem-proving system to perform this derivation automatically.