TY - JOUR

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

AU - Asada, Kazuyuki

AU - Kobayashi, Naoki

AU - Sin’ya, Ryoma

AU - Tsukada, Takeshi

N1 - Funding Information:
Acknowledgment. We would like to thank anonymous referees for useful comments. This work was supported by JSPS KAKENHI Grant Number JP15H05706.
Publisher Copyright:
© 2019 K. Asada, N. Kobayashi, R. Sin’ya, and T. Tsukada. All rights reserved.

PY - 2019

Y1 - 2019

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85070361003&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85070361003&partnerID=8YFLogxK

U2 - 10.23638/LMCS-15(1:16)2019

DO - 10.23638/LMCS-15(1:16)2019

M3 - Article

AN - SCOPUS:85070361003

VL - 15

SP - 16:1-16:57

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 1

ER -