On the likelihood of normalisation in combinatory logic

TL;DR

This paper provides a quantitative, basis-independent analysis of combinatory logic, showing that most combinators are not strongly normalising or typeable, but a significant fraction are, with experimental evidence suggesting a high density of normalising combinators.

Contribution

It generalizes previous results to all Turing-complete bases, improves the lower bound of normalising combinator density, and introduces a constructive approach to identify significant fractions of normalising combinators.

Findings

Asymptotically almost no combinator is strongly normalising or typeable.

The density of normalising combinators is at least 34%.

Experimental results suggest the density is close to 85%.

Abstract

We present a quantitative basis-independent analysis of combinatory logic. Using a general argument regarding plane binary trees with labelled leaves, we generalise the results of David et al. and Bendkowski et al. to all Turing-complete combinator bases proving, inter alia, that asymptotically almost no combinator is strongly normalising nor typeable. We exploit the structure of recently discovered normal-order reduction grammars showing that for each positive $n$, the set of $\mathbf{S} \mathbf{K}$-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 normalising combinators. We show that the density of normalising combinators cannot be less than $34\%$, improving the previously best lower bound of approximately $3\%$. Finally, we present some super-computer experimental results, conjecturing that the density of normalising combinators is close to $85\%$.