René David ; Katarzyna Grygiel ; Jakub Kozik ; Christophe Raffalli ; Guillaume Theyssier et al.
-
Asymptotically almost all \lambda-terms are strongly normalizing
Asymptotically almost all \lambda-terms are strongly normalizingArticle
Authors: René David ; Katarzyna Grygiel ; Jakub Kozik ; Christophe Raffalli ; Guillaume Theyssier ; Marek Zaionc
NULL##NULL##0000-0002-1362-7780##NULL##NULL##NULL
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.
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.
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, https://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.