%0 Conference Proceedings %F he90a %A Henglein, Fritz %T Fast Left-Linear Semi-Unification %B Proc. Int'l. Conf. on Computing and Information %P 82-91 %I Springer %X Semi-unification is a generalization of both unification and match- ing with applications in proof theory, term rewriting systems, poly- morphic type inference, and natural language processing. It is the problem of solving a set of term inequalities M1 ≤ N1 , . . . , Mk ≤ Nk , where ≤ is interpreted as the subsumption preordering on (first-order) terms. Whereas the general problem has recently been shown to be undecidable, several special cases are decidable. Kfoury, Tiuryn, and Urzyczyn proved that left-linear semi-unification (LLSU) is decidable by giving an exponential time decision procedure. We improve their result as follows. 1. We present a generic polynomial-time algorithm L1 for LLSU, which shows that LLSU is in P. 2. We show that L1 can be implemented in time O(n3 ) by using a fast dynamic transitive closure algorithm. 3. We prove that LLSU is P-complete under log-space reductions, thus giving evidence that there are no fast (NC-class) parallel algorithms for LLSU. As corollaries of the proof of P-completeness we obtain that both monadic semi-unification and LLSU with only 2 term inequalities are already P-complete. We conjecture that L1 can be implemented in time O(n2 ), which is the best that is possible for the solution method described by L1. The basic question as to whether another solution method may admit even faster algorithms is open. We conjecture also that LLSU with 1 inequality is P-complete %U http://www.diku.dk/hjemmesider/ansatte/henglein/papers/henglein1990.pdf %8 May %D 1990