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

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

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. ***