高阶递归和线性概念在理论计算机科学中的应用

理论计算机科学www.elsevier.com/locate/entcs用高阶递归卡尔-海因茨·尼格尔摘要众所周知，通过一个单一的使用更高类型的递归记法，可以定义适当的卡尔马初等函数。这是由于在递归的步骤项中使用了“前一个函数”的某种非线性它显示了如何限制递归符号在所有有限类型，以消除多项式时间可计算函数。通过丰富类型结构获得限制 一起！s，并通过将线性概念添加到lambda演算中为此，本文提出了哥德尔T中的一个抽象的系统RNA，其中RNA指出了对术语构成的基本限制：相关性、必然性和可解释性。RNA术语是由变量和在S4对N的解释中，通过消除'！'，通过对A的有限lambda抽象，以及通过在所有有限安全类型中引入情况分析和递归的规则。 安全是指那些不能让人相信的东西！“. 类似于哥德尔的 T 项在集合论函数空间上得到了重新解释。一个可解释性形式化的线性的基本概念，这是整个系统的核心它被设计成可以判定给定的通用项是否在RNA中结果表明，RNA在还原条件下是封闭的。RNA的强标准化和唯一性然后是正常的形式。 特别是，每个封闭的RNA术语的基础类型减少到一个数字表示的价值的术语。因此，RNA可以被认为是一种简单的函数式编程语言，其中计算是标准化的。至于RNA的表达能力，一种在RNA内部实现的共享概念，证明了每一个计算数论函数的RNA程序都可以在给定输入的长度上以时间多项式进行评估。所有多项式时间可计算函数都可以在RNA中定义，只需嵌入BC函数即可。（与S.Bellantoni和H.Schwichtenberg的联合工作）。15 71-0661- 2 - 3 - 4 - 5 - 6 - 7 - 5 - 7 - 8 -10 V. 操作访问和C CB Y-NC-ND许可证。10.1016/S1571-0661（05）80736-4