Asymptotically almost all \lambda-terms are strongly normalizing

TL;DR

This paper analyzes the asymptotic properties of random -terms and combinators, revealing that almost all -terms are strongly normalizing while most combinators are not, highlighting contrasting behaviors.

Contribution

It provides a quantitative analysis of the asymptotic properties of random -terms and combinators, showing contrasting normalization behaviors.

Findings

Almost all -terms are strongly normalizing asymptotically.

Any fixed closed -term almost never appears in a random -term.

Almost all combinators are not strongly normalizing due to the frequent appearance of fixed combinators.

Abstract

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.