Fast algorithms for uniform semi-unification

Uniform semi-unification is a simple combination of matching and unification defined as follows: given two terms s and t, do there exist substitutions σ and ρ such that sσρ=tσ? We present two algorithms for this problem based on Huet’s unification closure method, one producing (possibly) non-principal solutions, and one producing principal solutions. For both we provide a precise analysis of correctness and asymptotic complexity. Under the uniform cost RAM model (counting assignment, comparison, and arithmetic operations as primitive) our first algorithm is asymptotically as fast as Huet’s method, O(nα(n)), where α is the functional inverse of Ackermann’s function. Under a model which counts assignments and comparisons of pointers, and arithmetic operations on bits, the cost is O(n2α(n)2). Producing principal solutions is more complex, however, and our second algorithm runs in O(n2α(n)2) and O(n2log2(nα(n))log log(nα(n))α(n)2) under these two models.