Almost every simply typed λ-term has a long β-reduction sequence

Ryoma Sin’ya, Kazuyuki Asada, Naoki Kobayashi, Takeshi Tsukada

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationFoundations 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
EditorsJavier Esparza, Andrzej S. Murawski
PublisherSpringer Verlag
Pages53-68
Number of pages16
ISBN (Print)9783662544570
DOIs
Publication statusPublished - 2017
Event20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017 - Uppsala, Sweden
Duration: 2017 Apr 222017 Apr 29

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10203 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017
CountrySweden
City Uppsala
Period17/4/2217/4/29

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Almost every simply typed λ-term has a long β-reduction sequence'. Together they form a unique fingerprint.

Cite this