Name
Abstract | ||
|---|---|---|
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 arc bounded above by a constant. To prove it, we have extended the infinite 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. |
Year | DOI | Venue |
|---|---|---|
2019 | 10.23638/LMCS-15(1:16)2019 | LOGICAL METHODS IN COMPUTER SCIENCE |
DocType | Volume | Issue |
Journal | 15 | 1 |
ISSN | Citations | PageRank |
1860-5974 | 0 | 0.34 |
References | Authors | |
0 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Kazuyuki Asada | 1 | 8 | 3.83 |
| Naoki Kobayashi | 2 | 0 | 3.38 |
| Ryoma Sin'ya | 3 | 8 | 2.13 |
| Takeshi Tsukada | 4 | 59 | 11.61 |