E-Book Content
Introduction to Lambda Calculus Henk Barendregt
Erik Barendsen
Revised edition December 1998, March 2000
Contents
1 Introduction
5
2 Conversion
9
3 The Power of Lambda
17
4 Reduction
23
5 Type Assignment
33
6 Extensions
41
7 Reduction Systems
47
Bibliography
51
3
Chapter 1
Introduction Some history Leibniz 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 universal language. If one restricts oneself to mathematical problems, point (1) of Leibniz’ ideal is fulfilled by taking some form of set theory formulated in the language of first order predicate logic. This was the situation after Frege and Russell (or Zermelo). Point (2) of Leibniz’ ideal became an important philosophical question. ‘Can one 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 the Entscheidungsproblem. In 1936 the Entscheidungsproblem was solved in the negative independently by Alonzo Church and Alan Turing. In order to do so, they needed a formalisation 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 these machines. Also in 1936 Turing proved that both models are equally strong in the sense that they define the same class of computable functi