View Related Documents

Abstract

We present a fast algorithm for uniform semi-unification based on adapting the Huet unification closure method for standard unification. It solves the following decision problem in O(n 2 α(n) 2), where n is the size of the two terms, and α is the functional inverse of Ackermann's function: Given two terms s and t, do there exist two substitutions σ and ρ such that ρ(σ(s)) = σ(t)? In the affirmative case, a solution σ can be constructed within the same time bound. However, if a principal solution (analogous to an mgu) is required, some modifications to the algorithm must be made, and the upper bound increases to O(n 2 log 2(nα(n))α(n) 2).

Fulltext Preview

Image of the first page of the fulltext document