Kazuyuki Asada ; Naoki Kobayashi ; Ryoma Sin'ya ; Takeshi Tsukada - Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence

lmcs:4203 - Logical Methods in Computer Science, February 22, 2019, Volume 15, Issue 1 - https://doi.org/10.23638/LMCS-15(1:16)2019
Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction SequenceArticle

Authors: Kazuyuki Asada ; Naoki Kobayashi ORCID; Ryoma Sin'ya ORCID; Takeshi Tsukada

    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.


    Volume: Volume 15, Issue 1
    Published on: February 22, 2019
    Accepted on: January 12, 2019
    Submitted on: January 14, 2018
    Keywords: Computer Science - Logic in Computer Science,F.4.3

    1 Document citing this article

    Consultation statistics

    This page has been seen 2134 times.
    This article's PDF has been downloaded 450 times.