Asymptotically almost all \lambda-terms are strongly normalizing

René David; Katarzyna Grygiel; Jakub Kozik; Christophe Raffalli; Guillaume Theyssier; Marek Zaionc

doi:10.2168/LMCS-9(1:2)2013

René David ; Katarzyna Grygiel ; Jakub Kozik ; Christophe Raffalli ; Guillaume Theyssier et al. - Asymptotically almost all \lambda-terms are strongly normalizing

lmcs:848 - Logical Methods in Computer Science, February 15, 2013, Volume 9, Issue 1 - https://doi.org/10.2168/LMCS-9(1:2)2013

Asymptotically almost all \lambda-terms are strongly normalizingArticle

Authors: René David ; Katarzyna Grygiel ; Jakub Kozik ; Christophe Raffalli ; Guillaume Theyssier ; Marek Zaionc

We present quantitative analysis of various (syntactic and behavioral) properties of random \lambda-terms. Our main results are that asymptotically all the terms are strongly normalizing and that any fixed closed term almost never appears in a random term. Surprisingly, in combinatory logic (the translation of the \lambda-calculus into combinators), the result is exactly opposite. We show that almost all terms are not strongly normalizing. This is due to the fact that any fixed combinator almost always appears in a random combinator.

https://doi.org/10.2168/LMCS-9(1:2)2013

Source: arXiv.org:0903.5505

Volume: Volume 9, Issue 1

Published on: February 15, 2013

Imported on: September 27, 2010

Keywords: Mathematics - Logic,Computer Science - Discrete Mathematics,Computer Science - Logic in Computer Science,Mathematics - Combinatorics,G.2.1

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Publications

Has review

Review available on zbMATH Open, by Martin W. Bunder (Wollongong) (English)

1 zbMATH Open

Bibliographic References

12 Documents citing this article

Samuele Giraudo, 2022, The combinator M and the Mockingbird lattice, 32, 3, pp. 271-299, 10.1017/s0960129522000354, https://hal.science/hal-03669017.

Yoshiki Nakamura;Kazuyuki Asada;Naoki Kobayashi;Ryoma Sin'ya;et al., 2020, On Average-Case Hardness of Higher-Order Model Checking., pp. 23-, 10.4230/lipics.fscd.2020.21.

Olivier Bodini;Bernhard Gittenberger;Zbigniew Gołębiewski, 2018, Enumerating lambda terms by weighted length of their De Bruijn representation, arXiv (Cornell University), 239, pp. 45-61, 10.1016/j.dam.2017.12.042, https://arxiv.org/abs/1707.02101.

Olivier Bodini;Danièle Gardy;Bernhard Gittenberger;Zbigniew Gołębiewski, 2018, On the Number of Unary-Binary Tree-Like Structures with Restrictions on the Unary Height, Annals of Combinatorics, 22, 1, pp. 45-91, 10.1007/s00026-018-0371-7, https://doi.org/10.1007/s00026-018-0371-7.

Pierre Lescanne, 2018, Quantitative Aspects of Linear and Affine Closed Lambda Terms, 19, 2, pp. 1-18, 10.1145/3173547, https://hal-ens-lyon.archives-ouvertes.fr/ensl-01464047v5/document.

MACIEJ BENDKOWSKI, 2017, Normal-order reduction grammars, arXiv (Cornell University), 27, 10.1017/s0956796816000332, http://arxiv.org/abs/1603.01758.

MACIEJ BENDKOWSKI;KATARZYNA GRYGIEL;PAUL TARAU, 2017, Random generation of closed simply typed λ-terms: A synergy between logic programming and Boltzmann samplers, Theory and Practice of Logic Programming, 18, 1, pp. 97-119, 10.1017/s147106841700045x.

Maciej Bendkowski;Katarzyna Grygiel;Pierre Lescanne;Marek Zaionc, 2017, Combinatorics of $\lambda$-terms: a natural approach, arXiv (Cornell University), 27, 8, pp. 2611-2630, 10.1093/logcom/exx018, http://arxiv.org/abs/1609.07593.

Ryoma Sin’ya;Kazuyuki Asada;Naoki Kobayashi;Takeshi Tsukada, arXiv (Cornell University), Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction Sequence, pp. 53-68, 2017, 10.1007/978-3-662-54458-7_4, http://arxiv.org/abs/1801.03886.

KATARZYNA GRYGIEL;PIERRE LESCANNE, 2015, Counting and generating terms in the binary lambda calculus, Journal of Functional Programming, 25, 10.1017/s0956796815000271, https://doi.org/10.1017/s0956796815000271.

Maciej Bendkowski;Katarzyna Grygiel;Marek Zaionc, Lecture notes in computer science, Asymptotic Properties of Combinatory Logic, pp. 62-72, 2015, 10.1007/978-3-319-17142-5_7.

KATARZYNA GRYGIEL;PIERRE LESCANNE, 2013, Counting and generating lambda terms, Journal of Functional Programming, 23, 5, pp. 594-628, 10.1017/s0956796813000178, https://doi.org/10.1017/s0956796813000178.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1665 times.

This article's PDF has been downloaded 393 times.