Accession Number:

ADA107328

Title:

Deductive Synthesis of the Unification Algorithm,

Descriptive Note:

Corporate Author:

STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1981-06-01

Pagination or Media Count:

52.0

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

Subject Categories:

  • Theoretical Mathematics
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE