Jump to : Download | Abstract | See also | Contact | BibTex reference | EndNote reference |


Fritz Henglein. Fast Left-Linear Semi-Unification. In Proc. Int'l. Conf. on Computing and Information, Lecture Notes of Computer Science, Vol. 468, Pages 82-91, May 1990.


Download paper: Adobe portable document (pdf) pdf

Copyright notice:This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.


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

See also

[ icci90 ]


Fritz Henglein

BibTex Reference

   Author = {Henglein, Fritz},
   Title = {Fast Left-Linear Semi-Unification},
   BookTitle = {Proc. Int'l. Conf. on Computing and Information},
   Pages = {82--91},
   Publisher = {Springer},
   Month = {May},
   Year = {1990}

EndNote Reference [help]

Get EndNote Reference (.ref)