Unification in pseudo-linear sort theories is decidable

Abstract

In this paper the decidability of unification in pseudo-linear sort theories is shown. In contrast to standard unification, variables range over subsets of the domain described by sorts. The denotations of sorts are fixed by declarations in a sort theory. Then two terms are unifiable, if they are unifiable in the standard sense and the assignments of the unifier satisfy the restrictions on the domain variables with respect to the sort theory. This problem is known to be undecidable in general, but is known to be decidable for elementary, weak-elementary, linear and semi-linear sort theories. So-called pseudo-linear sort theories properly include all these sort theories. We show that the problem of whether two terms are unifiable with respect to a pseudo-linear sort theory is decidable and of unification type infinitary.