CISE Postdoctoral Program: Computational Efficiency of Optimal Reduction in Lambda Calculus

9504288 Mairson这项研究的目标是调查为Lambda演算实现正确的、最佳的评估机制所需的计算资源。因为Lambda演算是设计和实现编程语言的基础，所以这样的研究有助于理解编程语言的实现。此外，它将整合强调语义问题和计算复杂性的计算方法。文中将分析Gonthier、Abadi和L提出的最优解。建立了该方案在初等、第一原理意义下的计算正确性，并分析了其计算复杂性。最后，在一个合理的Lambda演算代价模型中，将提出一个其复杂性为多项式的正确的赋值器的版本，即Lambda演算可以被视为不变性命题意义上的“第一类”形式主义，该不变性命题是丘奇-图灵命题的计算效率版本。作为懒惰环境模型的可能基础的静态语义也将被研究。***

9504288 Mairson The goal of this research is to investigate the computational resources required to implement correct, optimal evaluation mechanisms for the lambda calculus. Because lambda calculus is a foundation for the design and implementation of programming languages, such research could contribute to the understanding of programming language implementation. Moreover, it would integrate approaches to computation that emphasize semantic issues as well as those of computational complexity. The solution to optimality proposed by Gonthier, Abadi, and L vy will be analyzed. The computational correctness of this scheme in an elementary, first-principles sense will be established and its computational complexity will be analyzed. Ultimately, a version of a correct evaluator whose complexity is polynomial in a reasonable cost model for lambda calculus will be put forward that the lambda calculus may be regarded as a "first class" formalism in the sense of the invariance thesis, the computationally efficient version of the Church-Turing thesis. The static semantics as a possible foundation for a lazy environment model will also be investigated. ***