Skip to main content
SpringerLink
Log in

Meaningless terms in rewriting

  • Lambda-Calculus and Rewriting
  • Conference paper
  • First Online:
Algebraic and Logic Programming (ALP 1996)

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

Included in the following conference series:

Abstract

We present an axiomatic approach to meaninglessness in finite and transfinite term rewriting and lambda calculus. We justify our axioms in two ways. First, they are shown to imply important properties of meaninglessness: genericity of the class of meaningless terms, the consistency of equating all meaningless terms, and the construction of Böhm trees. Second we show that they can be easily verified for existing notions of meaninglessness.

Richard Kennaway was supported by an EPSRC Advanced Fellowship, and by EPSRC Grant no. GR/F 91582. Vincent van Oostrom's work was partially performed at the Vrije Universiteit, Amsterdam and with an HCM grant at the Technische Universität München.

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. S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors. Handbook of Logic in Computer Science, volume 2, Background: Computational Structures. Oxford University Press, New York, 1992.

    Google Scholar 

  2. Z. M. Ariola, J. R. Kennaway, J. W. Klop, M. R. Sleep, and F. J. de Vries. Syntactic definitions of undefined: On defining the undefined. In Int. Symp. on Theoretical Aspects of Computer Software, Sendai, pages 543–554, 1994. Lecture Notes in Computer Science, vol. 789.

    Google Scholar 

  3. H. P. Barendregt. The Lambda Calculus, Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. Elsevier Science Publishers B.V., Amsterdam, revised edition, 1984.

    Google Scholar 

  4. H. P. Barendregt. Representing ‘undefined’ in lambda calculus. Journal of Functional Programming, 2(3):367–374, July 1992.

    Google Scholar 

  5. A. Berarducci. Infinite λ-calculus and non-sensible models. Presented to the conference in honour of Roberto Magari, Siena 1994.

    Google Scholar 

  6. A. Church. The Calculi of Lambda Conversion. Princeton University Press, 1941.

    Google Scholar 

  7. N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In[Lee90 Ch.6 pp. 243–320], 1990.

    Google Scholar 

  8. J. R. Hindley and J. P. Seldin. Introduction to Combinators and λ-Calculus, volume 1 of London Mathematical Society Students Texts. Cambridge University Press, 1986.

    Google Scholar 

  9. J. G. Jacopini and M. Venturini Zilli. Easy terms in the lambda calculus. Fundamenta Informaticae, VIII, 1985.

    Google Scholar 

  10. J. R. Kennaway, J. W. Klop, M. R. Sleep, and F. J. de Vries. Infinitary lambda calculus and Böhm models. In Proc. Conference on Rewriting Techniques and Applications, pages 257–270, 1995. Lecture Notes in Computer Science, vol. 914.

    Google Scholar 

  11. J. R. Kennaway, J. W. Klop, M. R. Sleep, and F. J. de Vries. Transfinite reductions in orthogonal term rewriting systems. Information and Computation, 119:18–38, 1995.

    Google Scholar 

  12. J. R. Kennaway, J. W. Klop, M. R. Sleep, and F. J. de Vries. Infinitary lambda calculus. Th. Comp. Sci., 1996. to appear.

    Google Scholar 

  13. J. W. Klop. Term rewriting systems. In [AGM92116] pp. 1–116, 1992.

    Google Scholar 

  14. J. Kuper. Partiality in Logic and Computation, Aspects of Undefinedness. PhD thesis, Universiteit Twente, February 1994.

    Google Scholar 

  15. J. Kuper. Proving the Genericity Lemma by leftmost reduction is simple. In Proc. Conference on Rewriting Techniques and Applications, pages 271–278, 1995. Lecture Notes in Computer Science, vol. 914.

    Google Scholar 

  16. J. R. Kennaway, V. van Oostrom, and F. J. de Vries. abc-active terms in transfinite lambda calculus. Available by ftp from ftp://ftp.sys.uea.ac.uk/ pub/kennaway/publications/abcactive. dvi, 1996.

    Google Scholar 

  17. J. van Leeuwen, editor. Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics. Elsevier Science Publishers B.V., Amsterdam, 1990.

    Google Scholar 

  18. C.-H. L. Ong. The Lazy Lambda Calculus: An Investigation into the Foundations of Functional Programming. PhD thesis, Imperial College of Science and Technology, University of London, May 1988.

    Google Scholar 

Download references

Author information

Author notes

  1. Fer-Jan de Vries

    Present address: ETL, 1-1-4 Umezono, Tsukuba, 305, Ibaraki, Japan

Authors and Affiliations

  1. School of Information Systems, University of East Anglia, NR4 7TJ, Norwich, UK

    Richard Kennaway

  2. Information Processing Principles Research Group, NTT BRL, 3-1 Wakamiya Morinosato Atsugi-shi, 243-01, Kanagawa, Japan

    Vincent van Oostrom

  3. Hitachi Advanced Research Laboratory, Hatoyama, 350-03, Saitama, Japan

    Fer-Jan de Vries

Authors
  1. Richard Kennaway
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vincent van Oostrom
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Fer-Jan de Vries
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Fer-Jan de Vries .

Editor information

Michael Hanus Mario Rodríguez-Artalejo

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kennaway, R., van Oostrom, V., de Vries, FJ. (1996). Meaningless terms in rewriting. In: Hanus, M., Rodríguez-Artalejo, M. (eds) Algebraic and Logic Programming. ALP 1996. Lecture Notes in Computer Science, vol 1139. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61735-3_17

Download citation

  • DOI: https://doi.org/10.1007/3-540-61735-3_17

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61735-8

  • Online ISBN: 978-3-540-70672-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation