几乎每个简单类型的lambda项都有一个较长的β-还原序列
摘要：简单类型lambda术语的beta归约序列的长度可以非常大；在最坏情况下，它的大小可以达到lambda术语的指数级。我们考虑以下与数量特性相关的问题，而不是最坏情况：有多少简单类型lambda术语具有非常长的归约序列？我们通过显示几乎所有k阶简单类型lambda术语的归约序列长度在项大小上是(k-1)-fold指数级的部分回答了这个问题，假设函数的维数和可能出现在每个子项中的变量的数量上界是一个常数。为了证明这一点，我们将字符串的无穷猴定理扩展为参数化的正则树语言的定理，这可能具有独立的研究兴趣。该工作受到了高阶模型检查复杂度的定量分析的激励。
作者：Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada
论文ID：1801.03886
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22