Skip to main content
SpringerLink
Log in

Linear second-order unification

  • Regular Papers
  • Conference paper
  • First Online:
Rewriting Techniques and Applications (RTA 1996)

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

Included in the following conference series:

Abstract

We present a new class of second-order unification problems, which we have called linear. We deal with completely general second-order typed unification problems, but we restrict the set of unifiers under consideration: they instantiate free variables by linear terms, i.e. terms where any λ-abstractions bind one and only one occurrence of a bound variable. Linear second-order unification properly extends context unification studied by Comon and Schmidt-Schauß. We describe a sound and complete procedure for this class of unification problems and we prove termination for three different subcases of them. One of these subcases is obtained requiring Comon's condition, another corresponds to Schmidt-Schauß's condition, (both studied previously for the case of context unification, and applied here to a larger class of problems), and the third one is original, namely that free variables occur at most twice.

This work was partially supported by the ESPRIT Basic Research Action CCL and the project DISCOR (TIC 94-0847-C02-01) funded by the CICYT

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.

References

  1. H. Comon. Completion of rewrite systems with membership constraints, part I: Deduction rules and part II: Constraint solving. Technical report, CNRS and LRI, Université de Paris Sud, 1993. (To appear in J. of Symbolic Computation).

    Google Scholar 

  2. J. H. Gallier and W. Snyder. Designing unification procedures using transformations: A survey. Bulletin of the EATCS, 40:273–326, 1990.

    Google Scholar 

  3. W. D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225–230, 1981.

    Article  Google Scholar 

  4. W. E. Gould. A Matching Procedure for ω-Order Logic. PhD thesis, Princeton Univ., 1966.

    Google Scholar 

  5. G. Huet. The undecidability of unification in third-order logic. Information and Control, 22(3):257–267, 1973.

    Article  Google Scholar 

  6. G. Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.

    Article  Google Scholar 

  7. D. C. Jensen and T. Pietrzykowski. Mechanizing ω-order type theory through unification. Theoretical Computer Science, 3:123–171, 1976.

    Article  Google Scholar 

  8. J. Levy and J. Agustí. Bi-rewriting, a term rewriting technique for monotonic order relations. In 4th Int. Conf. on Rewriting Techniques and Applications, RTA'93, volume 690 of LNCS, pages 17–31, Montreal, Canada, 1993.

    Google Scholar 

  9. J. Levy and J. Agustí. Bi-rewriting systems. J. of Symbolic Computation, 1995. (To be published).

    Google Scholar 

  10. C. Loría-Sáenz. A Theoretical Framework for Reasoning about Program Construction based on Extensions of Rewrite Systems. PhD thesis, Univ. Kaiserslautern, 1993.

    Google Scholar 

  11. C. L. Lucchesi. The undecidability of the unification problem for third-order languages. Technical Report CSRR 2059, Dept. of Applied Analysis and Computer Science, Univ. of Waterloo, 1972.

    Google Scholar 

  12. O. Lysne and J. Piris. A termination ordering for higher-order rewrite systems. In 6th Int. Conf on Rewriting Techniques and Applications, RTA'95, volume 914 of LNCS, Kaiserslautern, Germany, 1995.

    Google Scholar 

  13. D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. J. of Logic and Computation, 1:497–536, 1991.

    Google Scholar 

  14. T. Nipkow. Functional unification of higher-order patterns. In 8th IEEE Symp. on Logic in Computer Science, LICS'93, pages 64–74, Montreal, Canada, 1993.

    Google Scholar 

  15. T. Pietrzykowski. A complete mechanization of second-order logic. J. of the ACM, 20(2):333–364, 1973.

    Google Scholar 

  16. C. Prehofer. Solving Higher-Order Equations: From Logic to Programming. PhD thesis, Technische Universität München, 1995.

    Google Scholar 

  17. M. Schmidt-Schauß. Unification of stratified second-order terms. Technical Report 12/94, Johan Wolfgang-Goethe-Universität, Frankfurt, Germany, 1995.

    Google Scholar 

  18. K. U. Schulz. Makanin's algorithm, two improvements and a generalization. Technical Report CIS-Bericht-91-39, Centrum für Informations und Sprachverarbeitung, Universität München, 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Departament de Llenguatges i Sistemes Informátics, Universitat Politècnica de Catalunya, Spain

    Jordi Levy

Authors
  1. Jordi Levy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Harald Ganzinger

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Levy, J. (1996). Linear second-order unification. In: Ganzinger, H. (eds) Rewriting Techniques and Applications. RTA 1996. Lecture Notes in Computer Science, vol 1103. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61464-8_63

Download citation

  • DOI: https://doi.org/10.1007/3-540-61464-8_63

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61464-7

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation