Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence

TL;DR

This paper demonstrates that almost all simply typed lambda-terms of order k have extremely long beta-reduction sequences, with lengths reaching (k-1)-fold exponential in size, under certain boundedness conditions.

Contribution

It extends the infinite monkey theorem to regular tree languages and provides a probabilistic analysis of the length of reduction sequences in simply typed lambda-terms.

Findings

Almost all simply typed lambda-terms of order k have very long reduction sequences.

The length of these sequences can reach (k-1)-fold exponential in the size of the term.

The results are conditioned on bounded arity of functions and variables in subterms.

Abstract

It is well known that the length of a beta-reduction sequence of a simply typed lambda-term of order k can be huge; it is as large as k-fold exponential in the size of the lambda-term in the worst case. We consider the following relevant question about quantitative properties, instead of the worst case: how many simply typed lambda-terms have very long reduction sequences? We provide a partial answer to this question, by showing that asymptotically almost every simply typed lambda-term of order k has a reduction sequence as long as (k-1)-fold exponential in the term size, under the assumption that the arity of functions and the number of variables that may occur in every subterm are bounded above by a constant. To prove it, we have extended the infinite monkey theorem for strings to a parametrized one for regular tree languages, which may be of independent interest. The work has been motivated by quantitative analysis of the complexity of higher-order model checking.