Lambda Calculus

Lambda演算既是函数的数学理论，又是计算的模型。因此，它是应用逻辑和理论计算机科学接口的一部分。作为一种理论，简单类型Lambda演算是丘奇高型函数理论的一部分。高阶类型定理证明将句子的有效性问题归结为统一和转换问题，它们纯粹是Lambda演算的方程问题。Lambda演算也通过著名的Curry-Howard同构隐含地进入类型理论的证明理论。作为计算的正式模型，Lambda演算有助于理解更高类型和无类型的编程结构。指称语义学将程序综合和正确性问题归结为寻找和验证某些组合函数方程的解。Lambda演算也明确地进入了应用编程语言的语法基础，作为顺序计算的范例。简而言之，Lambda演算显式和隐式地进入了高阶类型定理证明理论和程序设计语言理论。Lambda演算是对某些计算规则、程序或算法的研究。这项研究挑出了那些规则，它们的执行只取决于这样一个事实，即一些数据本身就是相同类型的计算规则。目前还不清楚是否存在此类规则的任何不寻常的例子。兰姆达微积分丰富的深层结构必须由丘奇、伯奈斯、库里、克莱恩和他们的追随者分割。本文主要研究纯Lambda演算的深层结构，以解决Lambda演算中一些尚未解决的问题。这些问题包括：(1)给定有限的真组合子集合是否构成基是可判定的？(2)是否存在递归的一步Church Rosser策略？(3)是否存在统一的通用生成器？(4)所有3阶真组合子的字问题是可判定的吗？(5)纯单型Lambda演算的匹配问题是可判定的吗？*

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