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 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. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 01, 1981
- Accession Number
- ADA107328
Entities
People
- Richard Waldinger
- Zohar Manna
Organizations
- Stanford University