New Generation Computing

, Volume 2, Issue 3, pp 207–219 | Cite as

Efficient unification over infinite terms

  • Joxan Jaffar
Regular Papers


We address the unification problem for expressions over infinite first-order terms. An algorithm which is practically linear in time and space is presented. It is argued that this algorithm is better than some recent algorithms with respect to performance in practice and simplicity in nature. It is further argued that this superiority also holds in comparison with some of the best known algorithms for the more conventional unification problem over finite terms.


Unification First-Order Terms Infinite Terms 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1).
    Aho, A. V., Hopcroft, J. E. and Ullman, J. D.: “Data Structures and Algorithms” (Addison-Wesley) (1983).Google Scholar
  2. 2).
    Baxter, L. D.: “A Practically Linear Unification Algorithm,” Report,CS-76-13 (Department of Computer Science, University of Waterloo) (February, 1976).Google Scholar
  3. 3).
    Corbin, J. and Bidoit, M.: “A Rehabilitation of Robinson’s Unification Algorithm,” Information Processing 83, R. E. A. Mason (ed.) (Elsevier Science Publishers) (September, 1983) 909–914.Google Scholar
  4. 4).
    Colmerauer, A.: “Prolog and Infinite Trees,” in Logic Programming, K. L. Clark and S-Å. Tärnlund (eds.) (Academic Press) (1982) 231–251.Google Scholar
  5. 5).
    Courcelle, B.: “Fundamental Properties of Infinite Trees,” Theoretical Computer Science,25(1983) 95–169.MATHCrossRefMathSciNetGoogle Scholar
  6. 6).
    Martelli, A. and Montanari, U.: “An Efficient Unification Algorithm,” ACM TOPLAS,4(2) (April, 1982) 239–257.CrossRefGoogle Scholar
  7. 7).
    Mukai, K.: “A Unification Algorithm for Infinite Trees,” Proceedings IJCAI-83 (Karlsruhe) (August, 1983) 547–549.Google Scholar
  8. 8).
    Paterson, M. S. and Wegman, M. N.: “Linear Unification,” Journal of Computer and System Sciences,16 (1978) 158–167.MATHCrossRefMathSciNetGoogle Scholar
  9. 9).
    Tarjan, R. E.: “On the Efficiency of a Good but Not Linear Set Merging Algorithm,” Journal of the ACM,22(2) (April, 1975) 215–225.MATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Ohmsha, Ltd. and Springer 1984

Authors and Affiliations

  • Joxan Jaffar
    • 1
  1. 1.Department of Computer ScienceMonash UniversityClaytonAustralia

Personalised recommendations