Introduction to Lambda Calculus
美容大赏Henk Barendregt Erik Barendn
中小企业创新
Revid edition
黎明的反义词December1998,March2000
月落乌啼霜满天江枫渔火对愁眠
Contents
1Introduction5 2Conversion9 3The Power of Lambda17 4Reduction23 5Type Assignment33 6Extensions41 7Reduction Systems47 Bibliography51
3
Chapter1
Introduction
Some history
Leibniz had as ideal the following.
ipad手写键盘怎么设置(1)Create a‘universal language’in which all possible problems can be stated.
(2)Find a decision method to solve all the problems stated in the universal language.好看完结小说
If one restricts onelf to mathematical problems,point(1)of Leibniz’ideal is fulfilled by taking some form of t theory formulated in the language of first order predicate logic.This was the situation after Frege and Rusll(or Zermelo).
Point(2)of Leibniz’ideal became an important philosophical question.‘Can one solve all problems formulated in the universal language?’It ems not, but it is not clear how to prove that.This question became known as the Entscheidungsproblem.
In1936the Entscheidungsproblem was solved in the negative independently by Alonzo Church and Alan Turing.In order to do so,they needed a formali-sation of the intuitive notion of‘decidable’,or what is equivalent‘computable’. Church and Turing did this in two different ways by introducing two models of computation.
(1)Church(1936)invented a formal system called the lambda calculus and defined the notion of computable function via this system.
功利主义
(2)Turing(1936/7)invented a class of machines(later to be called Turing machines)and defined the notion of computable function via the machines.
f22猛禽Also in1936Turing proved that both models are equally strong in the n that they define the same class of computable functions(e Turing(1937)).
Bad on the concept of a Turing machine are the prent day Von Neu-mann computers.Conceptually the are Turing machines with random access registers.Imperative programming languages such as Fortran,Pascal etcetera as well as all the asmbler languages are bad on the way a Turing machine is instructed:by a quence of statements.
Functional programming languages,like Miranda,ML etcetera,are bad on the lambda calculus.An early(although somewhat hybrid)example of such a language is Lisp.Reduction machines are specifically designed for the execution of the functional languages.
5
