Skip to main content
SpringerLink
Log in

λ-Calculi with conditional rules

  • Conference paper
  • First Online:
Book cover Typed Lambda Calculi and Applications (TLCA 1993)

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

Included in the following conference series:

Abstract

A variety of typed/untyped λ-calculi and related reduction systems have been proposed in order to study various aspects of programs, some of which contain rules subject to side conditions. As a framework to study fundamental properties of such reduction systems, we first introduce the notion of conditional λ-calculus. Then we give a sufficient condition for them to be confluent (Church-Rosser) as well as to have a normalizing strategy à la Gross. The proof, being a generalization of Tait-Martin-Löf proof for the confluence of λβ, is inductive and simple.

I thank Roger Hindley and Jan Willem Klop for their valuable comments and stimuli which led me to the work.

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. Aczel: A General Church-Rosser Theorem, (Technical Report, University of Manchester, 1978).

    Google Scholar 

  2. H. P. Barendregt: The Lambda Calculus, second edition (North-Holland, 1984).

    Google Scholar 

  3. J. R. Hindley: Reduction of residuals are finite, Trans. A.M.S. 240 (1978) pp 345–361.

    Google Scholar 

  4. J. W. Klop: Combinatory Reduction Systems (Mathematisch Centrum, 1980).

    Google Scholar 

  5. F. van Raamsdonk: A Simple Proof of Confluence for Weakly Orthogonal Combinatory Reduction Systems, (Technical Report, CWI, 1992).

    Google Scholar 

  6. M. Takahashi: Parallel Reductions in λ-Calculus, J. Symbolic Computation 7 (1989) pp 113–123. Also Parallel Reductions in λ-Calculus, revised version (Research Report, Tokyo Institute of Technology, 1992).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Information Science, Tokyo Institute of Technology, 152, Tokyo, Japan

    Masako Takahashi

Authors
  1. Masako Takahashi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Marc Bezem Jan Friso Groote

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Takahashi, M. (1993). λ-Calculi with conditional rules. In: Bezem, M., Groote, J.F. (eds) Typed Lambda Calculi and Applications. TLCA 1993. Lecture Notes in Computer Science, vol 664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0037121

Download citation

  • DOI: https://doi.org/10.1007/BFb0037121

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-47586-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation