From computation to foundations via functions and application:: The λ-calculus and its webbed models

Church's lambda-calculus is an enthralling object of mathematical and logical study, born in 1930 as the mathematical theory of functions as rules, and invented for foundational purposes. lambda-calculus gave rise to the first (and the most elegant) mathematical definition of computable functions and inspired the main theorems of recursion theory. It came back on the scene in the 1960s with the development of programming theory. A capital contribution of lambda-calculus to this subject is that it allows the mathematical expression and development of the Curry-Howard correspondence between proofs and programs, which generates deep and active research. The first aim of this paper is to introduce lambda-calculus to a mathematical audience with no previous knowledge of it. After giving a brief insight to the conceptual and practical importance of typed calculi we will concentrate on untyped lambda-calculus, which is logic free, has the most powerful expressive power and can be more easily described. In the second and main part of the paper we give an elementary, algebraic, and bottom-up presentation of its useful classes of models, which are powersets built from adequate "webs". We focus on two methods: completion of partial webs (for building models) and reducibility (for studying them). In the third part we try to give evidence that the study of models is interesting per se. We survey or raise a lot of natural questions which arise when one tries to develop a model theory for untyped lambda-calculus, in the sense of a general study of the relations between its models and its equational extensions, and we illustrate them with many recent results. Finally, we give a sketchy presentation of Grue's map theory, which is a common foundation for Mathematics, Logic and Computer Science, based on lambda-calculus and, hence, on the notion of function and application (instead of sets and membership). MT fulfills Church's original aim and its consistency can be proved by exhibiting webbed models for it. (C) 2000 Elsevier Science B.V. All rights reserved.