On the likelihood of normalization in combinatory logic

摘要

We present a quantitative basis-independent analysis of combinatory logic. Using a general argument regarding plane binary trees with labelled leaves, we generalize the results of David et al. (see [11]) and Bendkowski et al. (see [6]) to all Turingcomplete combinator bases proving, inter alia, that asymptotically almost no combinator is strongly normalizing nor typeable. We exploit the structure of recently discovered normal-order reduction grammars (see [3]) showing that for each positive n, the set of SK-combinators reducing in n normal-order reduction steps has positive asymptotic density in the set of all combinators. Our approach is constructive, allowing us to systematically find new asymptotically significant fractions of the set of normalizing combinators. We show that the density of normalizing combinators cannot be less than 34%, improving the previously best lower bound of approximately 3% (see [6]). Finally, we present some super-computer experimental results, conjecturing that the density of the set of normalizing combinators is close to 85%.