TY - GEN
T1 - Almost every simply typed λ-term has a long β-reduction sequence
AU - Sin’ya, Ryoma
AU - Asada, Kazuyuki
AU - Kobayashi, Naoki
AU - Tsukada, Takeshi
N1 - Funding Information:
We would like to thank anonymous referees for useful comments. This work was supported by JSPS KAKENHI Grant Number JP15H05706.
Publisher Copyright:
© Springer-Verlag GmbH Germany 2017.
PY - 2017
Y1 - 2017
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 − 2)-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. 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 − 2)-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. 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=85015912902&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85015912902&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-54458-7_4
DO - 10.1007/978-3-662-54458-7_4
M3 - Conference contribution
AN - SCOPUS:85015912902
SN - 9783662544570
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 53
EP - 68
BT - Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings
A2 - Esparza, Javier
A2 - Murawski, Andrzej S.
PB - Springer Verlag
T2 - 20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017
Y2 - 22 April 2017 through 29 April 2017
ER -