Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction Sequence
Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction Sequence
复制标题
几乎每个简单键入的 $$lambda $$-Term 都有一个很长的 $$eta $$-Reduction 序列
DOI：
10.1007/978-3-662-54458-7_4
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Kobayashi Naoki and Tsukada Takeshi
中科院分区：
文献类型：
--
作者：
Sin’ya Ryoma;Asada Kazuyuki;Kobayashi Naoki and Tsukada Takeshi
众所周知，一个阶的简单型项的a-约化序列的长度可以是很大的，在最坏的情况下，a-约化序列的长度可以是a-项大小的倍指数。我们考虑以下有关quantitativeproperties的问题，而不是最坏的情况：有多少simply typed-terms有很长的约简序列？我们提供了一个部分的答案，这个问题，通过显示，渐近几乎每一个简单的typed-term的orders有一个减少序列，只要倍指数的长期大小，假设的arity的功能和变量的数量，可能会出现在每个子项上有界的一个常数。这项工作的动机是定量分析高阶模型检测的复杂性。
It is well known that the length of a-reduction sequence of a simply typed-term of ordercan be huge; it is as large as-fold exponential in the size of the-term in theworstcase. We consider the following relevant question aboutquantitativeproperties, instead of the worst case:how manysimply 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 orderhas a reduction sequence as long as-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.