Introduction to Lambda Calculus

Introduction to Lambda CalculusHenk Barendregt Erik BarendsenRevised editionDecember 1998, March 2000aaaaaaaContents1 Introduction 52 Conversion 93 The Power of Lambda 174 Reduction 235 Type Assignment 336 Extensions 417 Reduction Systems 47Bibliography 513Chapter 1IntroductionSome historyLeibniz had as ideal the following.(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 universallanguage.If one restricts oneself to mathematical problems, point (1) of Leibniz’ idealis ful lled by taking some form of set theory formulated in the language of rst order predicate logic. This was the situation after Frege and Russell (orZermelo).Point (2) of Leibniz’ ideal became an important philosophical question. ‘Canone solve all problems formulated in the universal language?’ It seems not,but it is not clear how to prove that. This question became known as theEntscheidungsproblem.In 1936 the Entscheidungsproblem was solved in the negative independentlyby 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 di eren t ways by introducing two models ofcomputation.(1) Church (1936) invented a formal system called the lambda calculus andde ned the notion of computable function via this system.(2) Turing (1936/7) invented a ...