English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

It is well known that the length of a beta-reduction sequence of a simplytyped lambda-term of order k can be huge; it is as large as k-fold exponentialin the size of the lambda-term in the worst case. We consider the followingrelevant question about quantitative properties, instead of the worst case: howmany simply typed lambda-terms have very long reduction sequences? We provide apartial answer to this question, by showing that asymptotically almost everysimply 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 offunctions and the number of variables that may occur in every subterm arebounded above by a constant. To prove it, we have extended the infinite monkeytheorem for strings to a parametrized one for regular tree languages, which maybe of independent interest. The work has been motivated by quantitativeanalysis of the complexity of higher-order model checking.

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