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