Abstract.
We present a name free λ-calculus with explicit substitutions, based on a generalised notion of director strings. Terms are annotated with information – directors – that indicate how substitutions should be propagated. We first present a calculus where we can simulate arbitrary β-reduction steps, and then simplify the rules to model the evaluation of functional programs (reduction to weak head normal form). We also show that we can define the closed reduction strategy. This is a weak strategy which, in contrast with standard weak strategies, allows certain reductions to take place inside λ-abstractions thus offering more sharing. Our experimental results confirm that, for large combinator-based terms, our weak evaluation strategies out-perform standard evaluators. Moreover, we derive two abstract machines for strong reduction which inherit the efficiency of the weak evaluators.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit substitutions. J. Funct. Prog. 1(4), 375–416 (1991)
Ariola, Z.M., Felleisen, M., Maraist, J., Odersky, M., Wadler, P.: A call-by-need lambda calculus. In: Proceedings of the 22nd ACM Symposium on Principles of Programming Languages (POPL’95), ACM Press, 1995, pp. 233–246
Asperti, A., Giovanetti, C., Naletto, A.: The Bologna optimal higher-order machine. J. Funct. Prog. 6(6), 763–810 (1996)
Asperti, A., Guerrini, S.: The Optimal Implementation of Functional Programming Languages. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998
Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. North-Holland, revised edition, 1984
Barendregt, H.P.: Lambda calculi with types. In: Handbook of Logic in Computer Science, S. Abramsky, D. Gabbay, T.S.E. Maibaum, (eds.), Oxford University Press, 1992
Benaissa, Z., Briaud, D., Lescanne, P., Rouyer-Degli., J.: Lambda-upsilon, a calculus of explicit substitutions which preserves strong normalisation. Journal of Functional Programming 6(5), 699–722 (1996)
Benaissa, Z., Rose, K.H., Lescanne, P.: Modeling sharing and recursion for weak reduction strategies using explicit substitution. In: 8th PLILP–-Symposium on Programming Language Implementation and Logic Programming, H. Kuchen, D. Swierstra, (eds.), Aachen, Germany, 1996, pp. 393–407
Bloo, R., Geuvers, H.: Explicit substitution: on the edge of strong normalization. Theor. Comp. Sci. 211(1), 375–395 (1999)
Crégut, P.: An abstract machine for lambda-terms normalization. In: Lisp and Functional Programming 1990, ACM Press, 1990, pp. 333–340
Curien, P.-L., Hardin, T., Lévy, J.-J.: Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM 43(2), 362–397 (1996)
David, R., Guillaume, B.: A λ-calculus with explicit weakening and explicit substitution. Mathematical Structures in Computer Science 11(1), 169–206 (2001)
de Bruijn, N.G.: Lambda calculus notation with nameless dummies. Indagationes Mathematicae, 34, 381–392 (1972)
de Bruijn, N.G.: A namefree lambda calculus with facilities for internal definition of expressions and segments. Technical Report T.H.-Report 78-WSK-03, Department of Mathematics, Eindhoven University of Technology, 1978
Dershowitz, N., Jouannaud, J.-P.: Rewrite Systems. In: Handbook of Theoretical Computer Science: Formal Methods and Semantics, J. van Leeuwen, (ed.), volume B. North-Holland, 1989
Ennals, R., Jones, S.P.: Optimistic evaluation: an adaptive evaluation strategy for non-strict programs. In: Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP-03), C. Norris, J. James, B. Fenwick (eds.), volume 38, 9 of ACM SIGPLAN Notices, ACM Press, 2003, pp. 287–298
Fernández, M., Mackie, I.: Closed reductions in the λ-calculus. In: Proceedings of Computer Science Logic (CSL’99), J. Flum, M. Rodríguez-Artalejo (eds.), number 1683 in Lecture Notes in Computer Sciences, Springer-Verlag, 1999, pp. 220–234
Fernández, M., Mackie, I.: Director strings and explicit substitutions. WESTAPP’01, Utrecht, 2001
Gonthier, G., Abadi, M., Lévy, J.-J.: The geometry of optimal lambda reduction. In: Proceedings of the 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Albequerque, New Mexico, 1992, pp. 15–26
Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: Proceedings of ICFP’02, Pittsburgh, Pennsylvania, USA, 2002
Hardin, T., Maranget, L., Pagano, B.: Functional runtime systems within the lambda-sigma calculus. J. Funct. Prog. 8(2), 131–176 (1998)
Kennaway, J., Sleep, M.: Director strings as combinators. ACM Transactions on Programming Languages and Systems 10(4), 602–626 (1988)
Lamping, J.: An algorithm for optimal lambda calculus reductions. In: Proceedings 17 th ACM Symposium on Principles of Programming Languages, 1990, pp. 16–30
Lang, F.: Modèles de la β-réduction pour les implantations. PhD thesis, École Normale Supérieure de Lyon, 1998
Lawall, J.L., Mairson, H.G.: Optimality and inefficiency: What isn’t a cost model of the lambda calculus? In: International Conference on Functional Programming, 1996, pp. 92–101
Lescanne, P.: From λσ to λν: a journey through calculi of explicit substitutions. In: Proceedings of the 21st ACM Symposium on Principles of Programming Languages (POPL’94). ACM Press, 1994
Lescanne, P., Rouyer-Degli, J.: The calculus of explicit substitutions lambda-upsilon. Technical Report RR-2222, INRIA, 1995
Lévy, J.-J.: Optimal reductions in the lambda-calculus. In: To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, J.P. Seldin, J.R. Hindley (eds.), Academic Press, 1980, pp. 159–191
Melliès, P.-A.: Typed lambda-calculi with explicit substitutions may not terminate. In: Proceedings of the 2nd International Conference on Typed Lambda Calculi and Applications, number 902 in Lecture Notes in Computer Science, Springer-Verlag, 1995, pp. 328–334
Nadathur, G.: A fine-grained notation for lambda terms and its use in intensional operations. Journal of Functional and Logic Programming, 1999(2), 1999
Nadathur, G.: The suspension notation for lambda terms and its use in metalanguage implementations. In: Electronic Notes in Theoretical Computer Science, R. de Queiroz, L.C. Pereira, E.H. Haeusler (eds.), volume 67. Elsevier, 2002
Newman, M.: On theories with a combinatorial definition of ‘‘equivalence’’. Annals of Mathematics 43(2), 223–243 (1942)
Rose, K.: Explicit substitution - tutorial and survey, 1996. Lecture Series LS-96-3, BRICS, Dept. of Computer Science, University of Aarhus, Denmark
Rosen, B.: Tree-manipulating systems and Church-Rosser theorems. Journal of the ACM 20(1), 160–187 (1973)
Sinot, F.-R., Fernández, M., Mackie, I.: Efficient reductions with director strings. In: Proceedings of Rewriting Techniques and Applications (RTA’03), R. Nieuwenhuis (ed), volume 2706 of Lecture Notes in Computer Science, Springer-Verlag, 2003, pp. 46–60
Yoshida, N.: Optimal reduction in weak lambda-calculus with shared environments. Journal of Computer Software, 11(6), 3–18 (1994)
Author information
Authors and Affiliations
Corresponding author
Additional information
Projet Logical, Pôle Commun de Recherche en Informatique du plateau de Saclay, CNRS, École Polytechnique, INRIA, Université Paris-Sud.
Rights and permissions
About this article
Cite this article
Fernández, M., Mackie, I. & Sinot, FR. Lambda-Calculus with Director Strings. AAECC 15, 393–437 (2005). https://doi.org/10.1007/s00200-005-0169-9
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00200-005-0169-9