文件名称：Lambda-Calculus and Combinators，an Introduction
文件大小：2.06MB
文件格式：PDF
更新时间：2014-11-08 15:23:22
Lambda-Calculus
The λ-calculus and combinatory logic are two systems of logic which can also serve as abstract programming languages. They both aim to describe some very general properties of programs that can modify other programs, in an abstract setting not cluttered by details. In some ways they are rivals, in others they support each other. The λ-calculus was invented around 1930 by an American logician Alonzo Church, as part of a comprehensive logical system which included higher-order operators (operators which act on other operators). In fact the language of λ-calculus, or some other essentially equivalent notation, is a key part of most higher-order languages, whether for logic or for computer programming. Indeed, the first uncomputable problems to be discovered were originally described, not in terms of idealized computers such as Turing machines, but in λ-calculus. Combinatory logic has the same aims as λ-calculus, and can express the same computational concepts, but its grammar is much simpler. Its basic idea is due to two people: Moses Sch¨onfinkel, who first thought of it in 1920, and Haskell Curry, who independently re-discovered it seven years later and turned it into a workable technique. The purpose of this book is to introduce the reader to the basic methods and results in both fields. The reader is assumed to have no previous knowledge of these fields, but to know a little about propositional and predicate logic and recursive functions, and to have some experience with mathematical induction. Exercises are included, and answers to most of them (those marked ∗) are given in an appendix at the end of the book. In the early chapters there are also some extra exercises without answers, to give more routine practice if needed.