First-order unification in equational theories and its application to logic programming
Jia-Huai You · 1985
As an effective mechanism primarily used in theorem-proving, unification has been extensively studied by several researchers since the invention of the resolution principle. This thesis studies first-order unification in equational theories, called E-unification, paying particular attention to complete unification algorithms for classes of equational theories. It also investigates how results and notions of E-unification can be applied to logic programming systems that support equality handling and functional notation. First-order unification in equational theories is proved to be complete, i.e., it is shown that there exists an E-unification algorithm which is complete for all equational theories. This result is primarily of theoretical interest, since such an algorithm tends to be too inefficient to be of practical use. An E-unification algorithm using the narrowing process is then shown to be complete for the class of theories that can be described by a closed linear term rewriting system with the nonrepetition property. This result sets the stage for investigation of applications to logic programming. An extended equational programming paradigm, referred to as equational logic programming, is proposed, which uses narrowing and deletion upon successful unification as the inference rules, and enjoys the semantic simplicity of the classical theory of equality. It is shown that the kind of programming features that were initially possessed solely by Prolog can also be provided in this extended equational programming paradigm. Finally, a computational model integrating functional programming and logic programming is described. An important notion in the model is called semantic unification, which is a special case of E-unification for ground terms. The model supports computations with infinite data structures, and provides the user the flexibility of choosing between a backtracking free computation framework or a conventional logic computation framework, that is, a nondeterministic one involving backtracking. The model can be extended to include the notion of equality when complete E-unification algorithms are used. An interpreter for the proposed computational model is presented, written in DEC-20 Prolog.