Semantic unification for convergent systems
Subrata K. Mitra · 1994
Equation solving is the process of finding a substitution of terms for variables that makes two terms equal in a given theory, while semantic unification is the process that generates a basis set of such unifying substitutions. A simpler variant of the problem is semantic matching, where the substitution is made in only one of the terms. Semantic unification and matching constitute an important component of theorem proving and programming language interpreters. In this thesis we formulate a unification procedure based on a system of transformation rules that looks at goals in a lazy, top-down fashion, and prove its soundness and completeness for equational theories described by convergent rewrite systems (finite sets of equations that compute unique output values when applied from left-to-right to input values). We consider different variants of the system of transformation rules. We describe syntactic restrictions on the equations under which simpler sets of transformation rules are sufficient for generating a complete set of semantic matchings. We show that our first-order unification pro-cedure, with slight modifications, can be used to solve the satis ability problem in combinatory logic together with a convergent set of algebraic axioms, resulting in a complete higher-order unifi cation procedure for the given algebra. We also provide transformation rules to handle sit-