Skip to main content
SpringerLink
Log in

Adding algebraic rewriting to the untyped lambda calculus (extended abstract)

  • Conference paper
  • First Online:
Book cover 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 investigate the system obtained by adding an algebraic rewriting system R to the untyped lambda calculus. On certain classes of terms, called here “stable”, we prove that the resulting calculus is confluent if R is confluent, and terminating if R is terminating. The termination result has the corresponding theorems for several typed calculi as corollaries. The proof of the confluence result yields a general method for proving confluence of typed β reduction plus rewriting; we sketch the application to the polymorphic calculus F ω.

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. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam. 1981, revised 1984.

    Google Scholar 

  2. F. Barbanera. Adding Algebraic Rewriting to the Calculus of Constructions: Strong Normalization Preserved. In Proceedings of the Second International Workshop on Conditional and Typed Rewriting Systems, Concordia University, 1990.

    Google Scholar 

  3. V. Breazu-Tannen. Conservative extensions of type theories. dissertation, Massachusetts Institute of Technology 1987.

    Google Scholar 

  4. V. Breazu-Tannen. Combining algebra and higher-order types. In Proceedings of the Third Annual Symposium on Logic in Computer Science, pp. 82–90. 1988.

    Google Scholar 

  5. V. Breazu-Tannen and J. Gallier. Polymorphic rewriting conserves algebraic strong normalization. Theoretical Computer Science, to appear.

    Google Scholar 

  6. V. Breazu-Tannen and J. Gallier. Polymorphic rewriting conserves algebraic confluence. Information and Computation, to appear.

    Google Scholar 

  7. V. Breazu-Tannen and A. R. Meyer. Computable values can be classical. In Proceedings of the Fourteenth Symposium on Principles of Programming Languages pp. 238–245, ACM, 1987.

    Google Scholar 

  8. T. Coquand and G. Huet. The Calculus of Constructions. Information and Control, v.76, no.2/3, pp. 95–120, 1988.

    Google Scholar 

  9. N. Dershowitz. Termination of rewriting. J. Symbolic Computation 3, pp. 69–116, 1987.

    Google Scholar 

  10. J-Y. Girard. Une extension de l'interprétation de Gödel à l'analyse, et son application à l'elimination des coupures dans l'analyse et la théorie des types. In Proc. Second Scandinavian Logic Symposium, ed. J.E. Fenstad. North-Holland, Amsterdam, 1971.

    Google Scholar 

  11. J-Y. Girard. Interprétation functionelle et élimination des coupures de l'arithmétique d'ordre supérieur. These D'Etat, Universite Paris VII, 1972.

    Google Scholar 

  12. G. Huet, J.J. Lévy. Call by need computations in non-ambiguous linear term rewriting systems. Rapport Laboria 359, INRIA, 1979

    Google Scholar 

  13. G. Huet, D. Oppen. Equations and rewrite rules: a survey. In Formal Languages: Perspectives and Open Problems, ed. R. Book. Academic Press, New York 1980.

    Google Scholar 

  14. J. W. Klop. Combinatory Reduction Systems. Mathematical Center Tracts 127, Amsterdam, 1980.

    Google Scholar 

  15. D. B. MacQueen. Using dependent types to express modular structure. In Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, pp. 277–286, 1986.

    Google Scholar 

  16. A. Middeldorp. Modular aspects of properties of term rewriting systems related to normal forms. In Proc. Third International Conference on Rewriting Techniques and Applications, Springer-Verlag LNCS 355, pp. 263–277, 1989.

    Google Scholar 

  17. G. Pottinger. The Church-Rosser theorem for the typed λ calculus with surjective pairing. Notre Dame Journal of Formal Logic, v.22, no. 3, pp. 264–268, 1981.

    Google Scholar 

  18. J. C. Reynolds. Towards a theory of type structure. In Proc. Colloque sur la Programmation, Springer-Verlag LNCS 19, pp. 408–425, 1974.

    Google Scholar 

  19. M. Rusinowitch. On termination of the direct sum of term rewriting systems. Information Processing Letters 26 pp.65–70, 1987.

    Google Scholar 

  20. Y. Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. Journal of the ACM, v.34, no.1, pp.128–143, 1987.

    Google Scholar 

  21. Y. Toyama, J. W. Klop and H. Barendregt. Termination for the direct sum of left-linear term rewriting systems. In Proc. Third International Conference on Rewriting Techniques and Applications, Springer-Verlag LNCS 355, pp. 477–491, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Wesleyan University, 06457, Middletown, CT

    Daniel J. Dougherty

Authors
  1. Daniel J. Dougherty
    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

Dougherty, D.J. (1991). Adding algebraic rewriting to the untyped lambda calculus (extended abstract). 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_84

Download citation

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

  • 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