Skip to main content
SpringerLink
Log in

Rule-based semantics for an extended lambda-calculus

  • Part I Categorical And Algebraic Methods
  • Conference paper
  • First Online:
Mathematical Foundations of Programming Language Semantics (MFPS 1987)

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

  • 186 Accesses

Abstract

Many implementation techniques proposed for functional languages in the literature are based on lambda-calculus and the theory of combinators [5, 12, 14]. The main advantage of functional languages over the more conventional programming languages is their lack of side-effects which makes their semantics much simpler [2].

This paper presents a λ-calculus dialect with list-handling extensions that can be used for defining an operational semantics for functional programs. This semantics is based on a set of elementary α-rules and β-rules which collectively implement the substitution operation without explicitly using it [10]. Two extra reduction rules, called γ-rules, have been added to the system for list manipulations [11]. Combining λ-calculus with list-handling capabilities makes an efficient vectorization of λ-calculus possible. This way we obtain a very elegant treatment of mutual recursion in our system.

The reduction rules described in this paper represent, in fact, an operational semantics for our extended λ-notation. An interpreter program for this extended λ-calculus has been developed by a direct implementation of the reduction rules which makes the correctness proof of the interpreter very easy. The notion of controlled reduction is introduced here to guarantee the existence of a normal form for λ-expressions representing recursively defined functions using the Y combinator.

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. Arvind, Kathail, V., and Pingali, K., Sharing Computation in Functional Language Implementations, Proc. Internat. Workshop on High-level Computer Architecture, Los Angeles, May 21–25, 1985, pp. 5.1–5.12.

    Google Scholar 

  2. Backus, J., The algebra of functional programs: Function level reasoning, linear equations, and extended definitions, Proc. International Colloquium on the Formalization of Programming Concepts, Lecture Notes in Computer Science, No. 107, Springer-Verlag 1981, pp. 1–43.

    Google Scholar 

  3. Barendregt, H.P., The Lambda Calculus — Its Sytax and Semantics (revised edition), Studies in Logic and the Foundation of Mathematics, Vol.103, North-Holland 1984.

    Google Scholar 

  4. Burton, F. W., A linear space translation of functional programs to Turner combinators, Information Processing Letters, Vol.14, No.5, 1982, pp. 201–204.

    Article  Google Scholar 

  5. Clarke, T. J. W., Gladstone, P. J. S, MacLean, C. D., and Norman, A. C., SKIM — The S, K, I reduction macine, LISP Conference Records, Stanford Univ., Stanford, CA 1980, pp. 128–135.

    Google Scholar 

  6. Friedman, D. P. and Wise, D. S., Cons should not evaluate its arguments, in Automata, Languages, and Programming (Michaelson S. and Milner, R. eds) pp. 257–284. Edinburgh University Press, Edinburgh (1976).

    Google Scholar 

  7. Hindley, J. R., and Seldin, J. P., Introduction to Combinators and λ-calculus, London Mathematical Society Student Text 1, Cambridge University Press 1986.

    Google Scholar 

  8. Johnsson, T., Lambda lifting: Transforming programs to recursive equations, IFIP Conf. on Functional Programming Languages and Computer Architecture, Sept. 16–19, 1985, Nancy, France, Lecture Notes in Computer Science, Vol.201, Springer Verlag 1985, pp. 190–203.

    Google Scholar 

  9. Noshita, K., and Hikita, T., The BC-chain method for representing combinators in linear space, New Generation Computing, Vol.3, No.2, (1985), pp. 131–144.

    Google Scholar 

  10. Revesz, G., Axioms for the theory of lambda-conversion, SIAM Journal on Computing, Vol.14, No.2, (1985) pp. 373–382.

    Article  Google Scholar 

  11. Revesz, G., An extension of lambda-calculus for functional programming, The Journal of Logic Programming, Vol.1, No.3, (1984) pp. 241–251.

    Article  Google Scholar 

  12. Scheevel, M., NORMA: A graph reduction processor, Proc. of the 1986 ACM Conference on LISP and Functional Programming, Cambridge, Mass. (Aug. 1986), pp. 212–219.

    Google Scholar 

  13. Turner, D. A., Another algorithm for bracket abstraction, Journal of Symbolic Logic, Vol.44, No.2, (June 1979), pp. 267–270.

    Google Scholar 

  14. Turner, D. A., A new implementation technique for applicative languages, Software — Practice and Experience, Vol.9, No.1, (1979) pp. 31–49.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IBM T. J. Watson Research Center, Yorktown Heights, N.Y.

    György E. Révész

Authors
  1. György E. Révész
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

M. Main A. Melton M. Mislove D. Schmidt

Rights and permissions

Reprints and permissions

Copyright information

© 1988 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Révész, G.E. (1988). Rule-based semantics for an extended lambda-calculus. In: Main, M., Melton, A., Mislove, M., Schmidt, D. (eds) Mathematical Foundations of Programming Language Semantics. MFPS 1987. Lecture Notes in Computer Science, vol 298. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-19020-1_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-19020-1_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-19020-2

  • Online ISBN: 978-3-540-38920-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation