Introduction to Lambda Calculus

Por • 30 may, 2017 • Sección: Leyes

Henk Barendregt Erik Barendsen

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.

Revised edition December 1998, March 2000

http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf

Post to Twitter

Escribe un comentario