Uniform semi-unification
Alberto Oliart, Wayne Snyder · 1999
Semi-unification can be thought as a combination of unification and matching on first-order terms, defined as follows: Given a set of pairs of terms $\Gamma = \{s\sb{1}, t\sb{1}),\... ,(s\sb{n},t\sb{n})\},$ do there exist mappings $\sigma$ and $\rho\sb1,\... ,\rho\sb{n}$ from variables to terms, such that $\rho\sb1(\sigma(t\sb1))$ = $\sigma (s\sb1),\...,\rho\sb{n}(\sigma(t\sb{n}))$ = $\sigma(s\sb{n})$? This problem has applications in many areas of computer science, such as automated deduction, programming language theory, proof theory, data bases and computational linguistics. Even though it can be defined simply, semi-unification has proved to be remarkably difficult to analyze precisely. In this general form it is undecidable, with an exceedingly difficult proof. In this thesis we study the problem of uniform semi-unification, which is a simpler problem where $\Gamma$ is a singleton, i.e. $ n = 1.$ This problem is decidable, and although it has been studied for some time, an efficient algorithm and a proof of its correctness has not been developed. We present two algorithms that solve, in an efficient way, the uniform semi-unification problem. The first is a decision procedure with time complexity in $O(n\sp2\alpha(n)\sp2),$ where $\alpha(n)$ is the inverse of Ackermann's function. This algorithm is based on the Huet unification algorithm, using a graph representation of the terms. It call generate solutions, although they may not be principal. A second algorithm that can find principal solutions in $O(n\sp2 \log\sp2(n \alpha(n)) \log \log(n \alpha(n))\alpha(n)\sp2)$ is also presented. Both algorithms are proved correct with respect to an underlying equational semantics.