Skip to main content
SpringerLink
Log in

An efficient decision algorithm for the uniform semi-unification problem extended abstract

  • Contributions
  • Conference paper
  • First Online:
Mathematical Foundations of Computer Science 1991 (MFCS 1991)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 520))

Abstract

An algorithm to decide whether a pair of terms is semi-unifiable is presented. It is based on compact graph representation of terms and on efficient implementation of variable replacements. The time complexity of the decision algorithm is O(n2) in the worst case, where n is the size of the input terms.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

6. References

  1. Dershowitz, N.: Termination of Rewriting. Journal of Symbolic Computation 3, No 1,2 1987, pp. 69–116

    Google Scholar 

  2. Henglein,F.: Polymorphic Type Inference and Semi-Unification. Technical Report 443, Department of Computer Science, Courant Institute of Mathematical Sciences, New York University, 1989, p. 109

    Google Scholar 

  3. Kapur,D.-Musser,D.-Narendran,P.-Stillman,J.: Semi-unification. In: Proceedings of the 8th Conference on Foundations of Software Technology and Theoretical Computer Science, LNCS 338, Springer-Verlag, 1988, pp. 435–454

    Google Scholar 

  4. Kfoury,A.J.-Tiuryn,J.-Urzyczyn,P.: The undecidability of the semi-unification. In: Proceedings of the 22nd ACM Symposium on Theory of Computing, 1990, pp. 468–476

    Google Scholar 

  5. Lankford, D.S.-Musser, D.R.: A finite termination criterion. Unpublished draft. USC Information Sciences Institute, Marina Del Rey, California, 1978

    Google Scholar 

  6. Leiss,H.: Semi-unification and type inference for polymorphic recursion. Bericht INF2-ASE-5-89, Siemens AG, München, 1989, p. 46

    Google Scholar 

  7. Pudlák, P.: On a unification problem related to Kreisel's conjecture. Commentationes Mathematicae Universitatis Caroline 29, No 3, 1988, pp.551–556

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. VUSEI-AR, Dúbravská 3, 842 21, Bratislava, Czecho-Slovakia

    Peter Ružička

Authors
  1. Peter Ružička
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Andrzej Tarlecki

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ružička, P. (1991). An efficient decision algorithm for the uniform semi-unification problem extended abstract. In: Tarlecki, A. (eds) Mathematical Foundations of Computer Science 1991. MFCS 1991. Lecture Notes in Computer Science, vol 520. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54345-7_85

Download citation

  • DOI: https://doi.org/10.1007/3-540-54345-7_85

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54345-9

  • Online ISBN: 978-3-540-47579-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation