一句话：证明在函数元数与变量数有界时，渐近几乎所有 k 阶简单类型 λ 项都有长达 (k-1) 重指数的 β-归约序列。
简单类型 λ 项的 β-归约序列长度在最坏情况下可随阶 k 达到 k 重指数级。本文转向定量问题：有多少简单类型 λ 项具有很长的归约序列？作者证明，在函数元数以及每个子项中可出现的变量数均有常数上界的假设下，阶 k 的简单类型 λ 项中渐近几乎每一个都具有长度为项大小 (k-1) 重指数的 β-归约序列。证明的关键是将字符串上的无限猴子定理推广为面向正则树语言的参数化版本，该结果可能具有独立价值。研究动机来自高阶模型检测复杂度的定量分析。
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.
@article{paperbot825,
title = {Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence},
author = {Kazuyuki Asada and Naoki Kobayashi and Ryoma Sin'ya and Takeshi Tsukada},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 1},
year = {2019},
doi = {10.23638/lmcs-15(1:16)2019}
}