Lambda Calculus

拉姆达演算

• 批准号: 9624681
• 负责人: Richard Statman
• 金额: $ 11.05万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1996
• 资助国家: 美国
• 起止时间: 1996-08-15 至 2000-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9624681&HistoricalAwards=false
• 关键词: Lambda; Calculus

Lambda Calculus is both a mathematical theory of functions and a model of computation. As such it is part of the interface of applied logic and theoretical computer science. As a theory, simply typed Lambda Calculus is part of Church's theory of functions of higher type. Higher type theorem proving reduces questions of validity of sentences to unification and conversion, which are purely equational questions of Lambda Calculus. Lambda Calculus also enters implicitly into the proof theory of type theory via the well known Curry-Howard isomorphism. As a formal model of computation Lambda Calculus contributes to understanding of higher-type and type-free programming constructs. Denotational semantics reduces questions of program synthesis and correctness to finding and verifying solutions to certain combinatory functional equations. Lambda Calculus also enters explicitly into the syntactic foundations of applicative programming languages as a paradigm of sequential computation. In short, Lambda Calculus enters both explicitly and implicitly into the theory of highertype theorem proving and the theory of programming languages. Lambda Calculus is the study of certain computation rules, programs, or algorithms. This research singles out those rules whose execution depends only on the fact that some of the data are themselves computation rules of the same sort. It is not immediately obvious that there are any non-trivial examples of such rules. The rich deep structure of the Lambda Calculus had to be diacovered by Church, Bernays, Curry, Kleene, and those who followed them. The research focuses on the deep structure of pure Lambda Calculus with at most algebraic types, to address a number of open questions in Lambda Calculus. These include: (1) Is it decidable whether a given finite set of proper combinators forms a basis? (2) Is there a recursive one-step Church Rosser strategy? (3) Is there a uniform universal generator? (4) Is the word problem for all proper com binators of order 3 decidable? (5) Is the matching problem for the pure simply typed lambda calculus decidable? ***

Lambda 演算既是函数的数学理论，也是计算模型。因此，它是应用逻辑和理论计算机科学接口的一部分。 作为一种理论，简单类型的 Lambda 演算是 Church 的高级类型函数理论的一部分。高类型定理证明将句子的有效性问题简化为统一和转换，这些问题纯粹是Lambda演算的方程问题。 Lambda 微积分还通过众所周知的 Curry-Howard 同构隐式地进入类型论的证明论。作为一种正式的计算模型，Lambda 演算有助于理解更高类型和无类型编程结构。 指称语义减少了程序综合以及查找和验证某些组合函数方程的解的正确性问题。 Lambda 演算还明确进入应用编程语言的语法基础作为顺序计算的范例。简而言之，Lambda 微积分显式地和隐式地进入了高级定理证明理论和编程语言理论。 Lambda 演算是对某些计算规则、程序或算法的研究。这项研究挑选出了那些其执行仅取决于某些数据本身就是同类计算规则这一事实的规则。 此类规则的重要示例并不是显而易见的。 Lambda 微积分丰富的深层结构必须由 Church、Bernays、Curry、Kleene 以及他们的追随者来发现。该研究重点关注最多代数类型的纯 Lambda 演算的深层结构，以解决 Lambda 演算中的一些悬而未决的问题。其中包括：（1）是否可以确定给定的有限集合的适当组合子是否构成基础？ (2)是否存在递归一步Church Rosser策略？ (3)是否有统一的通用生成器？ (4) 所有 3 阶真组合子的字问题都是可判定的吗？ (5) 纯简单类型 lambda 演算的匹配问题是否可判定？ ***