A fast algorithm for uniform semi-unification

  • Alberto Oliart
  • Wayne Snyder
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)


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(n2α(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(n2log2(nα(n))α(n)2).


Fast Algorithm Decision Procedure Function Symbol Function Node Symbolic Operation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    A.V. Aho, J.E. Hopcroft, and J.D. Ullman. Data Structures and Algorithms. Addison-Wesley, Reading, MA, 1983.Google Scholar
  2. [2]
    F. Baader and W. Snyder. Unification theory. In Handbook on Automated Deduction. Springer. To be published.Google Scholar
  3. [3]
    Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.Google Scholar
  4. [4]
    J. Corbin and M. Bidoit. A rehabilitation of robinson's unification algorithm. Information Processing, 83:909–914, 1993.Google Scholar
  5. [5]
    F. Henglein. Type inference and semi-unification. In ACM Conference on Lisp and Functional Programming, pages 184–197. ACM, 1988.Google Scholar
  6. [6]
    Fritz Henglein. Polymorphic Type Inference and Semi-Unification. PhD thesis, Rutgers University, April 1989. Available as NYU Technical Report 443, May 1989, from New York University, Courant Institute of Mathematical Sciences, Department of Computer Science, 251 Mercer St., New York, N.Y. 10012, USA.Google Scholar
  7. [7]
    G. Huet. Résolution d'Equations dans les Langages d'Ordre 1,2,...,Ω. PhD thesis, Université de Paris VII, 1976.Google Scholar
  8. [8]
    D. Kapur, D. Musser, P. Narendran, and Stillman J. Semi-unification. Theoretical Computer Science, 81(2):169–188, April 1991.MathSciNetCrossRefGoogle Scholar
  9. [9]
    A.J. Kfoury, J. Tiuryn, and P. Urzyczyn. The undecidability of the semi-unification problem. Information and Computation, 102(1):83–101, January 1993.MathSciNetCrossRefGoogle Scholar
  10. [10]
    D.S. Lankford and D.R. Musser. A finite termination criterion. Unpublished Draft, USC Information Sciences Institute, 1978.Google Scholar
  11. [11]
    H. Leiss. Semi-unification and type inference for polymorphic recursion. Technical Report INF-2-ASE-5-89, Siemens, Munich, Germany, 1989.Google Scholar
  12. [12]
    A. Oliart and W. Snyder. Fast algorithms for semi-unification., 1998.Google Scholar
  13. [13]
    P. Pudlack. On a unification problem related to kreisel's conjecture. Commentationes Mathematicae Universitatis Carolinae, 1988. Praguec Czechoslovakia.Google Scholar
  14. [14]
    P.W. Purdom. Detecting looping simplifications. In Proc. 2nd Conference on Rewrite Rule Theory and Applications, volume 250 of Lecture Notes in Computer Science, pages 54–62. Springer, Berlin, May 1987.Google Scholar
  15. [15]
    P. Ruzicka. An efficient decision algorithm for the uniform semi-unification problem. In 16th International Symposium on Mathematical Foundations of Computer Science (MFCS). Springer, September 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Alberto Oliart
    • 1
  • Wayne Snyder
    • 1
  1. 1.Computer Science DepartmentBoston UniversityBoston

Personalised recommendations