分支结构递归与上递归
Ramified Structural Recursion and Corecursion
摘要：
我们调查可行的计算在一个相当一般的概念的数据和codata。具体来说，我们提出了一个直接Bellantoni库克风格的正常/安全类型的编程形式主义，RS 1，表示可行的结构递归和corerursions的数据和codata指定的多项式函子。（列表、流、有限树、无限树等都是可以直接定义的。RS 1的一个新颖之处在于它像标准函数式编程实现一样包含了结构共享。由于我们的数据表示使用共享，我们的结构递归的实现是memoized，以避免可能的指数，许多重复的子计算一个天真的实现可能执行。我们引入的概念表示的数据（占共享）和codata（使用的想法类型2计算复杂性）的大小，并建立类型级别1 RS 1函数具有多项式有界的运行时，并满足多项式时间的完整性条件。此外，将RS 1项限制为特定类型会产生一些标准复杂度类的特征（例如，Ω-正则语言，线性空间函数）和一些不太标准的类（例如，日志空间流）。
英文摘要：
We investigate feasible computation over a fairly general notion of data and codata. Specifically, we present a direct Bellantoni-Cook-style normal/safe typed programming formalism, RS1, that expresses feasible structural recursions and corecursions over data and codata specified by polynomial functors. (Lists, streams, finite trees, infinite trees, etc. are all directly definable.) A novel aspect of RS1 is that it embraces structure-sharing as in standard functional-programming implementations. As our data representations use sharing, our implementation of structural recursions are memoized to avoid the possibly exponentially-many repeated subcomputations a naive implementation might perform. We introduce notions of size for representations of data (accounting for sharing) and codata (using ideas from type-2 computational complexity) and establish that type-level 1 RS1-functions have polynomial-bounded runtimes and satisfy a polynomial-time completeness condition. Also, restricting RS1 terms to particular types produces characterizations of some standard complexity classes (e.g., omega-regular languages, linear-space functions) and some less-standard classes (e.g., log-space streams).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
