文档介绍：The Bulletin of Symbolic Logic
Volume 3, Number 2, June 1997
THE IMPACT OF THE LAMBDA CALCULUS
IN LOGIC PUTER SCIENCE
HENK BARENDREGT
Abstract. One of the most important contributions of A. Church to logic is his invention
of the lambda calculus. We present the genesis of this theory and its two major areas of
application: the representation putations and the resulting functional programming
languages on the one hand and the representation of reasoning and the resulting systems of
computer mathematics on the other hand.
Acknowledgment. The following persons provided help in various ways.
Erik Barendsen, Jon Barwise, Johan van Benthem, Andreas Blass, Olivier
Danvy, Wil Dekkers, Marko van Eekelen, Sol Feferman, Andrzej Filinski,
Twan Laan, Jan Kuper, Pierre Lescanne, Hans Mooij, Robert Maron, Rinus
Plasmeijer, Randy Pollack, Kristoffer Rose, Richard Shore, Rick Statman
and Simon Thompson.
§1. Introduction. This paper is written to honor Church’s great invention:
the lambda calculus. The best way to do this—I think—is to give a descrip-
tion of its genesis (§2) and its impact on two areas of mathematical logic:
the representation putations (§3) and of reasoning (§4). In both cases
technological applications have emerged.
The very notion putability was first formalized in terms of defin-
ability on numerals represented in the lambda calculus. Church’s Thesis,
stating that this is the correct formalization of the notion putability,
has for more than 60 years never seriously been challenged. One of the recent
advances in lambda calculus is putations on other data types, like
trees and syntactic structures (., for parsing), can be done by representing
these data types directly as lambda terms and not via a coding as Godel¨
numbers that are then represented as numerals. This resulted in a much
more efficient representation of functions defined on these data types.
Received September 12, 1996; revised February 28, 1997.
Partial suppor