Document Open Access Logo

Counting Environments and Closures

Authors Maciej Bendkowski, Pierre Lescanne

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2018.11.pdf
  • Filesize: 0.52 MB
  • 16 pages

Document Identifiers

Author Details

Maciej Bendkowski
  • Jagiellonian University, Faculty of Mathematics and Computer Science, Theoretical Computer Science Department, ul. Prof. Łojasiewicza 6, 30 - 348 Kraków, Poland
Pierre Lescanne
  • University of Lyon, École normale supérieure de Lyon, LIP (UMR 5668 CNRS ENS Lyon UCBL), 46 allée d'Italie, 69364 Lyon, France

Funding

  • Bendkowski, Maciej: Maciej Bendkowski was partially supported within the Polish National Science Center grant 2016/21/N/ST6/01032.

Cite AsGet BibTex

Maciej Bendkowski and Pierre Lescanne. Counting Environments and Closures. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSCD.2018.11

Abstract

Environments and closures are two of the main ingredients of evaluation in lambda-calculus. A closure is a pair consisting of a lambda-term and an environment, whereas an environment is a list of lambda-terms assigned to free variables. In this paper we investigate some dynamic aspects of evaluation in lambda-calculus considering the quantitative, combinatorial properties of environments and closures. Focusing on two classes of environments and closures, namely the so-called plain and closed ones, we consider the problem of their asymptotic counting and effective random generation. We provide an asymptotic approximation of the number of both plain environments and closures of size n. Using the associated generating functions, we construct effective samplers for both classes of combinatorial structures. Finally, we discuss the related problem of asymptotic counting and random generation of closed environments and closures.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Lambda calculus
  • Mathematics of computing → Generating functions
Keywords
  • lambda-calculus
  • combinatorics
  • functional programming
  • mathematical analysis
  • complexity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Beniamino Accattoli and Ugo Dal Lago. (leftmost-outermost) beta reduction is invariant, indeed. Logical Methods in Computer Science, 12(1), 2016. URL: http://dx.doi.org/10.2168/LMCS-12(1:4)2016.
  2. Martin Avanzini, Ugo Dal Lago, and Georg Moser. Analysing the complexity of functional programs: higher-order meets first-order. In Kathleen Fisher and John H. Reppy, editors, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada., pages 152-164. ACM, 2015. URL: http://dx.doi.org/10.1145/2784731.2784753.
  3. Martin Avanzini and Georg Moser. Closing the gap between runtime complexity and polytime computability. In Christopher Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, July 11-13, 2010, Edinburgh, Scottland, UK, volume 6 of LIPIcs, pages 33-48. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2010. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2010.33.
  4. Maciej Bendkowski. Normal-order reduction grammars. Journal of Functional Programming, 27, 2017. URL: http://dx.doi.org/10.1017/S0956796816000332.
  5. Maciej Bendkowski, Olivier Bodini, and Sergey Dovgal. Polynomial tuning of multiparametric combinatorial samplers, pages 92-106. SIAM, 2018. URL: http://dx.doi.org/10.1137/1.9781611975062.9.
  6. Maciej Bendkowski, Katarzyna Grygiel, Pierre Lescanne, and Marek Zaionc. Combinatorics of λ-terms: a natural approach. Journal of Logic and Computation, 27(8):2611-2630, 2017. URL: http://dx.doi.org/10.1093/logcom/exx018.
  7. Maciej Bendkowski, Katarzyna Grygiel, and Marek Zaionc. On the likelihood of normalization in combinatory logic. Journal of Logic and Computation, 2017. URL: http://dx.doi.org/10.1093/logcom/exx005.
  8. Olivier Bodini, Danièle Gardy, and Bernhard Gittenberger. Lambda-terms of bounded unary height. In Philippe Flajolet and Daniel Panario, editors, Proceedings of the Eighth Workshop on Analytic Algorithmics and Combinatorics, ANALCO 2011, San Francisco, California, USA, January 22, 2011, pages 23-32. SIAM, 2011. URL: http://dx.doi.org/10.1137/1.9781611973013.3.
  9. Olivier Bodini, Bernhard Gittenberger, and Zbigniew Gołębiewski. Enumerating lambda terms by weighted length of their de bruijn representation. CoRR, abs/1707.02101, 2017. URL: https://arxiv.org/abs/1707.02101.
  10. Christine Choppy, Stéphane Kaplan, and Michèle Soria. Algorithmic complexity of term rewriting systems. In Pierre Lescanne, editor, Rewriting Techniques and Applications, 2nd International Conference, RTA-87, Bordeaux, France, May 25-27, 1987, Proceedings, volume 256 of Lecture Notes in Computer Science, pages 256-273. Springer, 1987. URL: http://dx.doi.org/10.1007/3-540-17220-3_22.
  11. Christine Choppy, Stéphane Kaplan, and Michèle Soria. Complexity analysis of term-rewriting systems. Theor. Comput. Sci., 67(2&3):261-282, 1989. URL: http://dx.doi.org/10.1016/0304-3975(89)90005-4.
  12. Koen Claessen and John Hughes. Quickcheck: A lightweight tool for random testing of haskell programs. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, pages 268-279. ACM, 2000. Google Scholar
  13. Pierre-Louis Curien. Categorical Combinators, Sequential Algorithms, and Functional Programming (2nd Ed.). Birkhauser Boston Inc., Cambridge, MA, USA, 1994. Google Scholar
  14. Pierre-Louis Curien, Thérèse Hardin, and Jean-Jacques Lévy. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43(2):362-397, March 1996. URL: http://dx.doi.org/10.1145/226643.226675.
  15. René David, Katarzyna Grygiel, Jakub Kozik, Christophe Raffalli, Guillaume Theyssier, and Marek Zaionc. Asymptotically almost all λ-terms are strongly normalizing. Logical Methods in Computer Science, 9:1-30, 2013. Google Scholar
  16. Nicolaas G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381-392, 1972. Google Scholar
  17. Philippe Duchon, Philippe Flajolet, Guy Louchard, and Gilles Schaeffer. Boltzmann samplers for the random generation of combinatorial structures. Combinatorics, Probability and Computing, 13(4-5):577-625, 2004. Google Scholar
  18. Philippe Flajolet and Andrew M. Odlyzko. Singularity analysis of generating functions. SIAM Journal on Discrete Mathematics, 3(2):216-240, 1990. Google Scholar
  19. Philippe Flajolet and Robert Sedgewick. Analytic Combinatorics. Cambridge University Press, 1 edition, 2009. Google Scholar
  20. Philippe Flajolet, Paul Zimmermann, and Bernard Van Cutsem. A calculus for the random generation of labelled combinatorial structures. Theoretical Computer Science, 132(1):1-35, 1994. Google Scholar
  21. Étienne Ghys. A singular mathematical promenade. Ecole Normale Supérieure, 2017. URL: http://perso.ens-lyon.fr/ghys/promenade/.
  22. Bernhard Gittenberger and Zbigniew Gołębiewski. On the number of lambda terms with prescribed size of their de Bruijn representation. In 33rd Symposium on Theoretical Aspects of Computer Science, STACS, pages 40:1-40:13, 2016. Google Scholar
  23. Katarzyna Grygiel and Pierre Lescanne. Counting and generating terms in the binary lambda calculus. Journal of Functional Programming, 25, 2015. URL: http://dx.doi.org/10.1017/S0956796815000271.
  24. Donald E. Knuth. Mathematical Analysis of Algorithms, 2000. First chapter of [25]. Google Scholar
  25. Donald E. Knuth. Selected Papers on Analysis of Algorithms, volume 102 of CSLI Lecture Notes. Stanford, California: Center for the Study of Language and Information, 2000. Google Scholar
  26. Ugo Dal Lago and Simone Martini. On constructor rewrite systems and the lambda calculus. Logical Methods in Computer Science, 8(3), 2012. URL: http://dx.doi.org/10.2168/LMCS-8(3:12)2012.
  27. Peter J. Landin. The mechanical evaluation of expressions. The Computer Journal, 6(4):308-320, 1964. URL: http://dx.doi.org/10.1093/comjnl/6.4.308.
  28. Pierre Lescanne. From λσ to λ υ: A journey through calculi of explicit substitutions. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 60-69. ACM, 1994. Google Scholar
  29. Michel Mauny and Ascánder Suárez. Implementing functional languages in the categorical abstract machine. In LISP and Functional Programming, pages 266-278, 1986. Google Scholar
  30. John C. Mitchell. Concepts in Programming Language (1st Ed.). Cambridge University Press, New York, NY, USA, 2002. Google Scholar
  31. Albert Nijenhuis and Herbert S. Wilf. Combinatorial Algorithms. Academic Press, 2 edition, 1978. Google Scholar
  32. Michał H. Pałka. Random Structured Test Data Generation for Black-Box Testing. PhD thesis, Chalmers University of Technology, 2012. Google Scholar
  33. Gordon David Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1(2):125-159, 1975. URL: http://dx.doi.org/10.1016/0304-3975(75)90017-1.
  34. Bruno Salvy and Paul Zimmermann. Gfun: a Maple package for the manipulation of generating and holonomic functions in one variable. ACM Transactions on Mathematical Software, 20(2):163-177, 1994. Google Scholar
  35. Robert Sedgewick and Philippe Flajolet. An Introduction to the Analysis of Algorithms (2nd Edition). Createspace Independent Pub, 2014. Google Scholar
  36. Daniel A. Spielman and Shang-Hua Teng. Smoothed analysis of algorithms: Why the simplex algorithm usually takes polynomial time. J. ACM, 51(3):385-463, 2004. URL: http://dx.doi.org/10.1145/990308.990310.
  37. Herbert S. Wilf. Generatingfunctionology. A. K. Peters, Ltd., 2006. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact