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

Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya +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-t…