Skip to main content
SpringerLink
Log in

Rewriting, and equational unification: the higher-order cases

  • Conference paper
  • First Online:
Rewriting Techniques and Applications (RTA 1991)

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

Included in the following conference series:

Abstract

We give here a general definition of term rewriting in the simply typed λ-calculus, and use it to define higher-order forms of term rewriting systems, and equational unification and their properties. This provides a basis for generalizing the first- and restricted higher-order results for these concepts. As examples, we generalize Plotkin's criteria for building-in equational theories, and show that pure third-order equational matching is undecidable. This approach simplifies computations in applications involving lexical scoping, and equations. We discuss open problems and summarize future research directions.

Extended abstract

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. P.B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Academic, Orlando, 1986.

    Google Scholar 

  2. G. Birkhoff, On the Structure of Abstract Algebras, Proceedings of the Cambridge Philosophical Society (1935) 31 433–454.

    Google Scholar 

  3. A. Bockmayr, A Note on a Canonical Theory with Undecidable Unification and Matching Problem, Journal of Automated Reasoning 3 (1987) 379–381.

    Google Scholar 

  4. A. Church, A Formulation of the Simple Theory of Types, Journal of Symbolic Logic 5 (1940) 56–68. D.C., 1988, 82–90.

    Google Scholar 

  5. M. Davis, Computability & Unsolvability, McGraw-Hill, New York, 1958.

    Google Scholar 

  6. N. Dershowitz, Computing with Rewrite Rules, Information and Control 65 (1985) 122–157.

    Google Scholar 

  7. S.J. Garland and J.V. Guttag, An Overview of LP: The Larch Prover, Proceedings of the Third International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 355, Springer, Berlin, 1989, 137–151.

    Google Scholar 

  8. J.A. Goguen, Higher Order Functions Considered Unnecessary for Higher Order Programming, in: (D.A. Turner, Ed.), Proceedings of the University of Texas Year of Programming Institute on Declarative Programming, Addison-Wesley, 1988.

    Google Scholar 

  9. J.A. Goguen and T. Winkler, Introducing OBJ3, Report SRI-CSL-88-9, SRI International, Menlo Park, 1988.

    Google Scholar 

  10. L. Henkin, Completeness in the Theory of Types, Journal of Symbolic Logic 15 (1950) 81–91.

    Google Scholar 

  11. D. Hilbert, Mathematische Probleme, Vortrag gehalten auf dem internationalen Mathematiker-Kongreß zu Paris, 1900. Nachr. Ges. Wiss. Göttingen, math.-phys. Kl., (1900) 253–297. English translation by H.W. Newsom in: Bulletin of the American Mathematical Society (1901–1902) 437–479.

    Google Scholar 

  12. G.P. Huet, A Unification Algorithm for Typed λ-Calculus, Theoretical Computer Science 1 (1975) 27–57.

    Google Scholar 

  13. G.P. Huet, Résolution d'équations dans des Langages d'Ordre 1,2, ...,ω, Thèse de Doctorat d'Etat, Université Paris VII, Paris, (1976).

    Google Scholar 

  14. G.P. Huet and F. Fages, Complete Sets of Unifiers and Matchers in Equational Theories, Theoretical Computer Science 43 2,3 (1986) 189–200.

    Google Scholar 

  15. G.P. Huet and B. Lang, Proving and Applying Program Transformations Expressed with Second-Order Patterns, Acta Informatica 11 (1978) 31–55.

    Google Scholar 

  16. G.P. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM 27, 4 (1980) 797–821.

    Google Scholar 

  17. G.P. Huet and D.C. Oppen, Equations and Rewrite Rules: A Survey, in: Formal Languages: Perspectives and Open Problems, R. Book, (Ed.), Academic, 1980, 349–405.

    Google Scholar 

  18. G. Huet and G. Plotkin, Eds., Proceedings of the First Workshop on Logical Frameworks, INRIA, 1990.

    Google Scholar 

  19. J.M. Hullot, Canonical Forms and Unification, Proceedings of the Fifth Conference on Automated Deduction, Lecture Notes in Computer Science 87, Springer, Berlin, 1980, 318–334.

    Google Scholar 

  20. S.C. Kleene, λ-definability and Recursiveness, Duke Math. J. 2 (1936) 340–353.

    Google Scholar 

  21. D. Knuth and P. Bendix, Simple Word Problems in Universal Algebra, in: Computational Problems in Abstract Algebra, (J. Leech, Ed.), Pergamon Press, 1970, 263–297.

    Google Scholar 

  22. P. Martin-Löf, Constructive Mathematics and Computer Programming, in: (C.A.R. Hoare and J.C. Shepherdson, Eds.), Mathematical Logic and Programming Languages, Prentice-Hall, 1985, 167–184.

    Google Scholar 

  23. Ju.V. Matiyasevič, Diophantine Representation of Enumerable Predicates, (In Russian), Izvestija Akademii Nauk SSSR, Serija Mathematika 35 (1971) 3–30. English translation in: Mathematics of the USSR — Izvestija 5 (1971) 1–28.

    Google Scholar 

  24. D. Miller, A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification. Extensions of Logic Programming, Lecture Notes in Computer Science, Springer, Berlin. To appear.

    Google Scholar 

  25. D. Miller, E.L. Cohen, and P.B. Andrews, A Look at TPS, Proceedings of the Sixth Conference on Automated Deduction, Lecture Notes in Computer Science 138, Springer, New York, 1982, 50–69.

    Google Scholar 

  26. T. Nipkow, A Critical Pair Lemma for Higher-Order Rewrite Systems and its Application to λ*, Draft version, in: [18]: (1990) 361–376.

    Google Scholar 

  27. M. O'Donnell, Equational Logic as a Programming Language, MIT Press, 1985.

    Google Scholar 

  28. L.C. Paulson, The Foundation of a Generic Theorem Prover, Journal of Automated Reasoning 5 (1989) 363–397.

    Google Scholar 

  29. G.D. Plotkin, Building-in Equational Theories, in: (B. Meltzer and D. Michie, Eds.), Machine Intelligence, 7, Edinburgh, 1972, 73–90.

    Google Scholar 

  30. J.H. Siekmann, Universal Unification, Proceedings of the Seventh Conference on Automated Deduction, Lecture Notes in Computer Science 170, Springer, New York, 1984, 1–42.

    Google Scholar 

  31. W. Snyder, Higher-Order E-Unification, Proceedings of the Tenth Conference on Automated Deduction, Lecture Notes in Computer Science, Springer, Berlin, 1990.

    Google Scholar 

  32. R. Statman, On the Existence of Closed Terms in the Typed λ-Calculus II: Transformations of Unification Problems, Theoretical Computer Science 15 (1981) 329–338.

    Google Scholar 

  33. D.A. Wolfram, The Clausal Theory of Types, Cambridge University Press. To appear.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Programming Research Group, Oxford University Computing Laboratory, 11 Keble Road, OX1 3QD, Oxford

    D. A. Wolfram

Authors
  1. D. A. Wolfram
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Ronald V. Book

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Wolfram, D.A. (1991). Rewriting, and equational unification: the higher-order cases. In: Book, R.V. (eds) Rewriting Techniques and Applications. RTA 1991. Lecture Notes in Computer Science, vol 488. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53904-2_83

Download citation

  • DOI: https://doi.org/10.1007/3-540-53904-2_83

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-46383-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation