Lambda Calculus

Lambda Calculus既是函数的数学理论，也是计算模型。因此，它是应用逻辑和理论计算机科学接口的一部分。 作为一个理论，简单类型的Lambda演算是教会的理论的一部分，功能的更高的类型。高等类型定理证明将句子的有效性问题简化为统一和转换，这是纯粹的Lambda演算的方程问题。Lambda演算也通过著名的Curry-Howard同构隐式地进入类型论的证明理论。作为一种形式化的计算模型，Lambda演算有助于理解更高类型和无类型的编程结构。 指称语义减少了程序合成和正确性的问题，以寻找和验证某些组合函数方程的解。Lambda演算也作为顺序计算的范例明确地进入应用程序编程语言的语法基础。简而言之，Lambda演算显式和隐式地进入了高阶定理证明理论和编程语言理论。 Lambda Calculus是对某些计算规则，程序或算法的研究。这项研究挑选出那些规则，其执行仅取决于这样一个事实，即一些数据本身就是同类的计算规则。 这并不是立即明显的，有任何非平凡的例子，这样的规则。λ演算丰富的深层结构必须由丘奇、伯奈斯、咖喱、克莱恩和他们的追随者来揭示。研究重点是纯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? ***