Skip to main content
SpringerLink
Log in
Book cover

International Conference on Mathematical Foundations of Programming Semantics

MFPS 1991: Mathematical Foundations of Programming Semantics pp 41–53Cite as

Call-by-value combinatory logic and the lambda-value calculus

  • Conference paper
  • First Online:

  • 161 Accesses

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

Abstract

Since it is unsound to reason about call-by-value languages using call-by name equational theories, we present two by-value combinatory logics and translations from the λ-value (λv) calculus to the logics. The first by-value logic is constructed in a manner similar to the λv-calculus: it is based on the byname combinatory logic, but the combinators are strict. The translation is non-standard to account for the strictness of the input program. The second by-value logic introduces laziness to K terms so that the translation can preserve the structure of functions that do not use their argument. Both logics include constants and delta rules, and we prove their equivalence with the λv-calculus.

Both authors were supported in part by NSF grant OCR 89-17022 and Darpa/NSF grant CCR 87-20277.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H. Barendregt. The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics 103. North-Holland, Amsterdam, revised edition, 1984.

    Google Scholar 

  2. W. Burge. Recursive Programming Techniques. Addison-Wesley, Reading, Mass., 1975.

    Google Scholar 

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

    Google Scholar 

  4. H. B. Curry. Grundlagen der kombinatorischen Logik. Amer. J. Math, 52:509–536; 789–834, 1930.

    Google Scholar 

  5. H. B. Curry and R. Feys. Combinatory Logic, volume 1. North Holland, 1958.

    Google Scholar 

  6. N. D. Goodman. A simplification of combinatory logic. Journal of Symbolic Logic, 37(2), 1972.

    Google Scholar 

  7. P. Hudak and B. Goldberg. Serial Combinators: “Optimal” Grains of Parallelism. In Proc of Conf. on Functional Prog. Langs. and Comp. Arch., 1985.

    Google Scholar 

  8. R. Hughes. Super-combinators: A new implementation method for applicative languages. In Sym. on Lisp and Functional Prog., pages 1–10. ACM, Aug 1982.

    Google Scholar 

  9. Kennaway, R. and R. Sleep. Director strings as combinators. ACM Trans. Prog. Lang. Syst., 10(4):602–626, 1988.

    Google Scholar 

  10. M. Schönfinkel. über die Bausteine der Mathematischen Logik. Math. Annalen, 92:305–316, 1924.

    Google Scholar 

  11. A. Meyer. What is a model of the lambda calculus? Information and Control, 52:87–122, 1982.

    Article  Google Scholar 

  12. G. Plotkin. Call-by-name, call-by-value, and the λ-calculus. Theoretical Computer Science, 1:125–159, 1975.

    Article  Google Scholar 

  13. R. Smullyan. To Mock a Mockingbird and Other Logic Puzzles. Alfred A. Knopf, Inc., New York, 1985.

    Google Scholar 

  14. D. A. Turner. A new implementation technique for applicative languages. Software—Practice and Experience, 9:31–49, 1979.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Rice University, USA

    John Gateley & Bruce F. Duba

Authors
  1. John Gateley
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bruce F. Duba
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Stephen Brookes Michael Main Austin Melton Michael Mislove David Schmidt

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gateley, J., Duba, B.F. (1992). Call-by-value combinatory logic and the lambda-value calculus. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds) Mathematical Foundations of Programming Semantics. MFPS 1991. Lecture Notes in Computer Science, vol 598. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55511-0_2

Download citation

  • DOI: https://doi.org/10.1007/3-540-55511-0_2

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55511-7

  • Online ISBN: 978-3-540-47194-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation