有界查询修订的类型2迭代
Type-two Iteration with Bounded Query Revision
摘要:
受Kapron和Steinberg(LICS 2018)的最新结果的启发,我们在更高类型的多时间可计算性的应用代数演算的设置中引入了新的长度迭代形式。特别是,在第二类设置中,我们考虑捕获输入长度上的迭代的泛函,该输入长度约束与第一类输入参数的交互,通过将函数参数可以返回增加大小的值的次数或函数参数可以应用于增加大小的参数的次数限制为常数。我们证明,对于任何常数的限制,得到的迭代器是等价的,相对于在类型1多时间函数的可定义性,递归的库克和厄克特捕获科巴姆的概念,有限的递归符号在此设置。
英文摘要:
Motivated by recent results of Kapron and Steinberg (LICS 2018) we introduce new forms of iteration on length in the setting of applied lambda-calculi for higher-type poly-time computability. In particular, in a type-two setting, we consider functionals which capture iteration on input length which bound interaction with the type-one input parameter, by restricting to a constant either the number of times the function parameter may return a value of increasing size, or the number of times the function parameter may be applied to an argument of increasing size. We prove that for any constant bound, the iterators obtained are equivalent, with respect to lambda-definability over type-one poly-time functions, to the recursor of Cook and Urquhart which captures Cobham's notion of limited recursion on notation in this setting.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。