On positive occur-checks in unification

Abstract

We address the problem of structuring the so-called positive occur-checks preventing unifiability. We introduce the notions of elementary and derived occur-checks. There exists a finite basis of elementary occur-checks for a given unification problem, obtained by a linearization process. Linearization gives unification problems that possess a single positive occur-check, necessarily elementary. We prove soundness and completeness of an equational deduction system well-suited for cyclic equations (= positive occur-checks), or, more generally, for reasoning about unification. Finally, up to permutation, there exists a minimum equational deduction associated to a given elementary positive occur-check. We give a deterministic algorithm computing this deduction, thus exhibiting the sequential nature of these occur-checks. This classification problem was encountered while dealing with higher-order unification. Besides insights in the nature of unification and its complexity, this technical analysis should also be of interest in symbolic debugging for systems where unification is involved. The minimum deduction appears to be a fundamental tool in the study of higher-order unification.

Part of this research was supported by the Office of Naval Research under contract N00014-84-K-0415 and by the Defense Advanced Research Projects Agency (DOD), ARPA Order No. 5404, monitored by the Office of Naval Research under the same contract. The views and conclusions contained in this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of DARPA or the U.S. Government.