Almost every simply typed λ-Term has a long β-Reduction sequence

Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin’ya, Takeshi Tsukada

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)


It is well known that the length of a β-reduction sequence of a simply typed λ-term of order k can be huge; it is as large as k-fold exponential in the size of the λ-term in the worst case. We consider the following relevant question about quantitative properties, instead of the worst case: how many simply typed λ-terms have very long reduction sequences? We provide a partial answer to this question, by showing that asymptotically almost every simply typed λ-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 inβnite monkey theorem for words to a parameterized 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.

Original languageEnglish
Pages (from-to)16:1-16:57
JournalLogical Methods in Computer Science
Issue number1
Publication statusPublished - 2019


Dive into the research topics of 'Almost every simply typed λ-Term has a long β-Reduction sequence'. Together they form a unique fingerprint.

Cite this