Abstract
The process of λ-lifting (or bracket abstraction) translates expressions in a typed λ-calculus into expressions in a typed combinator language. This is of interest because it shows that the λ-calculus and the combinator language are equally expressive (as the translation from combinators to λ-expressions is rather trivial). This paper studies the similar problems for 2-level λ-calculi and 2-level combinator languages. The 2-level nature of the type system enforces a formal distinction between binding times, e.g. between computations at compile-time and computations at run-time. In this setting the natural formulations of 2-level λ-calculi and 2-level combinator languages turn out not to be equally expressive. The translation into 2-level λ-calculus is straight-forward but the 2-level λ-calculus is too powerful for λ-lifting to succeed. We then develop a restriction of the 2-level λ-calculus for which λ-lifting succeeds and that is as expressive as the 2-level combinator language.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
P.-L. Curien: Categorical Combinators, Sequential Algorithms and Functional Programming, Pitman, London, 1986.
H.B. Curry, R. Feys: Combinatory Logic, vol. 1, North-Holland, Amsterdam, 1958.
R.J.M.Hughes: Super-combinators, a new implementation method for applicative languages, Conf. Record of the 1982 ACM Symposium on LISP and functional programming, 1982.
T.Johnson: Lambda lifting — transforming programs to recursive equations, Functional Programming Languages and Computer Architecture, Springer LNCS 201, 1985.
R.Milne, C.Strachey: A Theory of Programming Language Semantics, Halstead Press, 1976.
F.Nielson: Abstract interpretation of denotational definitions, STACS 1986, Springer LNCS 210, 1986.
H.R.Nielson, F.Nielson: Pragmatic aspects of two-level denotational meta-languages, ESOP 1986, Springer LNCS 213, 1986.
H.R.Nielson, F.Nielson: Semantics directed compiling for functional languages, Proceedings of the 1986 ACM Conf. on LISP and Functional Programming, 1986.
F.Nielson: Strictness analysis and denotational abstract interpretation (extended abstract), Proceedings from the 1987 ACM Conf. on Principles of Programming Languages, 1987. A full version is to appear in Information and Computation.
F.Nielson: A formal type system for comparing partial evaluators, The Technical University of Denmark, 1987. To appear in proceedings from Workshop on Partial Evaluation and Mixed Computation, North Holland, 1988.
H.R.Nielson, F.Nielson: Automatic binding time analysis for a typed λ-calculus, to appear in Proceedings from the 1988 ACM Conf. on Principles of Programming Languages, 1988.
D.Schmidt: Static properties of partial reduction, Kansas State University, 1987. To appear in proceedings from Workshop on Partial Evaluation and Mixed Computation, North Holland, 1988.
M.Schoenfinkel: Über die Bausteine der mathematischen Logik, Mathematische Annalen, vol.92, 1924.
R.D.Tennent: Principles of Programming Languages, Prentice Hall, 1981.
D.A.Turner: A new implementation technique for applicative languages, Software — Practice and Experience, vol.9, 1979.
D.A.Turner: Another algorithm for bracket abstraction, The Journal of Symbolic Logic, vol.44, 1979.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nielson, F., Nielson, H.R. (1988). 2-Level λ-lifting. In: Ganzinger, H. (eds) ESOP '88. ESOP 1988. Lecture Notes in Computer Science, vol 300. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-19027-9_22
Download citation
DOI: https://doi.org/10.1007/3-540-19027-9_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-19027-1
Online ISBN: 978-3-540-38941-5
eBook Packages: Springer Book Archive