A general theory of semi-unification
Files
Main Report
Date
1993-12-20
DOI
Authors
Jahama, Said
Kfoury, A.J.
Version
OA Version
Citation
Jahama, Said; Kfoury, A.J.. "A General Theory of Semi-Unification", Technical Report BUCS-1993-018, Computer Science Department, Boston University, November 1993. [Available from: http://hdl.handle.net/2144/1476]
Abstract
Various restrictions on the terms allowed for substitution give rise to different cases of semi-unification. Semi-unification on finite and regular terms has already been considered in the literature. We introduce a general case of semi-unification where substitutions are allowed on non-regular terms, and we prove the equivalence of this general case to a well-known undecidable data base dependency problem, thus establishing the undecidability of general semi-unification. We present a unified way of looking at the various problems of semi-unification. We give some properties that are common to all the cases of semi-unification. We also the principality property and the solution set for those problems. We prove that semi-unification on general terms has the principality property. Finally, we present a recursive inseparability result between semi-unification on regular terms and semi-unification on general terms.