On the expressive power of simply typed and let-polymorphic lambda calculi
On the expressive power of simply typed and let-polymorphic lambda calculi
复制标题
论简单类型和 let 多态 lambda 演算的表达能力
DOI：
--
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
P. Kanellakis
中科院分区：
文献类型：
--
作者：
Gerd G. Hillebrand;P. Kanellakis
我们提出了一个用于描述性计算复杂性的功能框架，其中常规，一阶，Ptime，pspace，k-extime，k-expspace（k/spl ges/1）和基本集具有句法特征。在此框架中，键入的lambda项代表输入和输出以及程序。描述上述计算复杂性类别的lambda calculi是简单的，或者拼写为固定顺序的功能。它们包括：0阶原子常数，这些常数，变量，应用和抽象之间的1平等。这些语言的功能顺序增加一个，对应于通过一个交替增加计算复杂性。使用对每个固定顺序的语言的语义评估来建立这种确切的对应关系，这是本文的主要技术贡献。
We present a functional framework for descriptive computational complexity, in which the Regular, First-order, Ptime, Pspace, k-Exptime, k-Expspace (k/spl ges/1), and Elementary sets have syntactic characterizations. In this framework, typed lambda terms represent inputs and outputs as well as programs. The lambda calculi describing the above computational complexity classes are simply or let-polymorphically typed with functionalities of fixed order. They consist of: order 0 atomic constants, order 1 equality among these constants, variables, application, and abstraction. Increasing functionality order by one for these languages corresponds to increasing the computational complexity by one alternation. This exact correspondence is established using a semantic evaluation of languages for each fixed order, which is the primary technical contribution of this paper.