Abstract
In light of the usual definition of values [18] as terms in weak head normal form (WHNF), a λ-abstraction is regarded as a value, and therefore no expressions under λ-abstraction can get evaluated and the sharing of computation under λ has to be achieved through program transformations such as λ-lifting and supercombinators. In this paper we generalise the notion of head normal form (HNF) and introduce the definition of generalised head normal form (GHNF). We then define values as terms in GHNF with flexible heads, and study a call-by-value λ-calculus λ v hd corresponding to this new notion of values. After establishing a version of the normalisation theorem in λ v hd , we construct an evaluation function evalhd for λ v hd which evaluates under λ-abstraction. We prove that a program can be evaluated in λ v hd to a term in GHNF if and only if it can be evaluated in the usual λ-calculus to a term in HNF. We also present an operational semantics for λ v hd via a SECD machine. We argue that lazy functional programming languages can be implemented through λ v hd and an implementation of λ v hd can significantly enhance the degree of sharing in evaluation. This establishes a solid foundation for implementing run-time code generation through λ v hd
Keywords
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi, L. Cardelli, P.-L. Curien, and I.-I. Lévy (1991), Explicit substitutions, Journal of Functional Programming, 4(1), pp. 375–416.
S. Abramsky (1990), The lazy lambda calculus. In D. Turner, editor, Declarative Programming, Addison-Wesley Publishing Company.
Z.M. Ariola, M. Felleisen, J. Maraist, M. Odersky and P. Wadler (1996), A Callby-Need Lambda Calculus, Proceedings of the 22 nd ACM Symposium on Principles of Programming Languages, San Francisco, pp. 233–246
H.P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, North-Holland, Amsterdam, 1984.
R. Bloo, F. Kamareddine and R. Nederpelt (1996), The Barendregt cube with definitions and generalised reduction, Information and Computation, vol 126(2), pp. 123–143. A useful lambda-notation, Theoretical Computer Science, vol. 155(1), pp 85–109.
R. Davies and F. Pfenning (1996), A Modal Analysis of Staged Computation, In Proceedings of the 23 rd ACM Symposium on Principles of Programming Languages, pp. 206–209
A.J. Field and P.G. Harrison (1988), Functional Programming, Addison-Wesley Publishing Company.
J.R. Hindley (1978), Reductions of residuals are finite, Trans. Amer. Math. Soc. 240, pp. 345–361.
G. Huét (1994), Residual Theory in λ-Calculus: A Formal Development, Journal of Functional Programming Vol. 4, pp. 371–394.
R.J.M. Hughes (1984), The design and implementation of programming languages, Ph.D. thesis, University of Oxford.
C.K. Holst and C.K. Gomard (1991), Partial Evaluation is Fuller Laziness, in Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 223–233.
R. Glück and J. Jørgensen (1995), Efficient multi-level generating extensions for program specialisation. In S.D. Swierstra and M. Hermenegildo, editors, Programming Languages, Implementations Logics and Programs, Springer-Verlag LNCS 982, pp. 259–278.
T. Johnsson (1985), Lambda lifting: transforming programs to recursive equations, In Proceedings of the Conference on Functional programming Languages and Computer Architecture, Nancy, pp. 190–203.
F. Kamareddine and R. Nederpelt (1996), A useful lambda-notation, Theoretical Computer Science, vol. 155(1), pp 85–109.
J. Lamping (1990), An Algorithm for Optimal Lambda Calculus Reduction, In Seventeenth ACM Symposium on Principles of Programming Languages, pp 16–30.
P.J. Landin (1964), The mechanical evaluation of expressions, BCS Computing Journal 6(4), pp. 308–320.
S.L. Peyton Jones (1991), A fully-lazy λ-lifter in Haskell, Software practice and experience 21.
G.D. Plotkin (1975), Call-by-name, call-by-value and the lambda-calculus, Theoretical Computer Science 1, pp. 125–159.
C. Reade (1989), Elements of Functional Programming, Addison-Wesley Publishing Company.
H. Xi (1996), Separating developments in λ-calculus http://www.cs.cmu.edu/-hwxi/papers/SepDev.ps
H. Xi (1996), Evaluation under lambda abstraction: http://www.cs.cmu.edu/-hwxi/papers/EvUdLam.ps
H. Xi (1997), Generalized Lambda-Calculi: http://www.cs.cmu.edu/-hwxi/papers/GLam.ps
N. Yoshida (1993), Optimal reduction in weak λ-calculus with shared environments. In Proc. ACM conference on Functional Programming Languages and Computer Architecture, Copenhagen.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Xi, H. (1997). Evaluation under lambda abstraction. In: Glaser, H., Hartel, P., Kuchen, H. (eds) Programming Languages: Implementations, Logics, and Programs. PLILP 1997. Lecture Notes in Computer Science, vol 1292. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0033849
Download citation
DOI: https://doi.org/10.1007/BFb0033849
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63398-3
Online ISBN: 978-3-540-69537-0
eBook Packages: Springer Book Archive