Towards the Average-Case Analysis of Substitution Resolution in Lambda-Calculus

Author Maciej Bendkowski



PDF
Thumbnail PDF

File

LIPIcs.FSCD.2019.7.pdf
  • Filesize: 0.6 MB
  • 21 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

Cite As Get BibTex

Maciej Bendkowski. Towards the Average-Case Analysis of Substitution Resolution in Lambda-Calculus. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 7:1-7:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSCD.2019.7

Abstract

Substitution resolution supports the computational character of beta-reduction, complementing its execution with a capture-avoiding exchange of terms for bound variables. Alas, the meta-level definition of substitution, masking a non-trivial computation, turns beta-reduction into an atomic rewriting rule, despite its varying operational complexity. In the current paper we propose a somewhat indirect average-case analysis of substitution resolution in the classic lambda-calculus, based on the quantitative analysis of substitution in lambda-upsilon, an extension of lambda-calculus internalising the upsilon-calculus of explicit substitutions. Within this framework, we show that for any fixed n >= 0, the probability that a uniformly random, conditioned on size, lambda-upsilon-term upsilon-normalises in n normal-order (i.e. leftmost-outermost) reduction steps tends to a computable limit as the term size tends to infinity. For that purpose, we establish an effective hierarchy (G_n)_n of regular tree grammars partitioning upsilon-normalisable terms into classes of terms normalising in n normal-order rewriting steps. The main technical ingredient in our construction is an inductive approach to the construction of G_{n+1} out of G_n based, in turn, on the algorithmic construction of finite intersection partitions, inspired by Robinson’s unification algorithm. Finally, we briefly discuss applications of our approach to other term rewriting systems, focusing on two closely related formalisms, i.e. the full lambda-upsilon-calculus and combinatory logic.

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Mathematics of computing → Generating functions
Keywords
  • lambda calculus
  • explicit substitutions
  • complexity
  • combinatorics

Metrics

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

References

  1. M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, 1991. URL: http://dx.doi.org/10.1017/S0956796800000186.
  2. B. Accattoli and U. 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.
  3. Z.-E.-A. Benaissa, D. Briaud, P. Lescanne, and J. Rouyer-Degli. λ υ, a calculus of explicit substitutions which preserves strong normalisation. Journal of Functional Programming, 6(5):699–722, 1996. URL: http://dx.doi.org/10.1017/S0956796800001945.
  4. M. Bendkowski. Normal-order reduction grammars. Journal of Functional Programming, 27, 2017. URL: http://dx.doi.org/10.1017/S0956796816000332.
  5. M. Bendkowski, K. Grygiel, P. Lescanne, and M. 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.
  6. M. Bendkowski, K. Grygiel, and M. Zaionc. On the likelihood of normalization in combinatory logic. Journal of Logic and Computation, 2017. URL: http://dx.doi.org/10.1093/logcom/exx005.
  7. M. Bendkowski and P. Lescanne. Combinatorics of Explicit Substitutions. In Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP '18, pages 7:1-7:12. ACM, 2018. URL: http://dx.doi.org/10.1145/3236950.3236951.
  8. C. Choppy, S. Kaplan, and M. Soria. Complexity Analysis of Term-Rewriting Systems. Theoretical Computer Science, 67(2&3):261-282, 1989. URL: http://dx.doi.org/10.1016/0304-3975(89)90005-4.
  9. A. Cichon and P. Lescanne. Polynomial interpretations and the complexity of algorithms. In Automated Deduction - CADE-11, pages 139-147. Springer Berlin Heidelberg, 1992. Google Scholar
  10. H. Comon, M. Dauchet, R. Gilleron, Ch. Löding, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree Automata Techniques and Applications, 2007. Release October, 12th 2007. URL: http://www.grappa.univ-lille3.fr/tata.
  11. N. 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
  12. Ph. Flajolet and A. M. Odlyzko. Singularity Analysis of Generating Functions. SIAM Journal on Discrete Mathematics, 3(2):216-240, 1990. Google Scholar
  13. Ph. Flajolet and R. Sedgewick. Analytic Combinatorics. Cambridge University Press, 1 edition, 2009. Google Scholar
  14. J. L. Lawall and H. G. Mairson. Optimality and Inefficiency: What Isn't a Cost Model of the Lambda Calculus? In Proceedings of the 1st ACM SIGPLAN International Conference on Functional Programming, ICFP '96, pages 92-101. ACM, 1996. URL: http://dx.doi.org/10.1145/232627.232639.
  15. P. 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
  16. P. Lescanne. The lambda calculus as an abstract data type. In M. Haveraaen, O. Owe, and O.-J. Dahl, editors, Recent Trends in Data Type Specification, pages 74-80. Springer Berlin Heidelberg, 1996. Google Scholar
  17. J. A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. J. ACM, 12(1):23-41, January 1965. URL: http://dx.doi.org/10.1145/321250.321253.
  18. R. Sin'Ya, K. Asada, N. Kobayashi, and T. Tsukada. Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence. In Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures, volume 10203, pages 53-68. Springer-Verlag New York, Inc., 2017. URL: http://dx.doi.org/10.1007/978-3-662-54458-7_4.
  19. Ch. Walther. Many-sorted Unification. J. ACM, 35(1):1-17, January 1988. URL: http://dx.doi.org/10.1145/42267.45071.
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