文档介绍：The Lambda-Calculus:
connections to higher type Recursion Theory,
Proof-Theory, Category Theory1
Giuseppe Longo
Dipartimento di Informatica, Università di Pisa
Introduction
Church proposed his calculus of λ-conversion as "A set of postulates for the Foundation of Logic"
(Church[1932-3]). Church's ideas and program were part of the leading Hilbert's school, at the
time, whose aim was still a unified formalist approach to the foundation of Mathematics. In the
following years, though, the growth of Recursion Theory, which soon became an independent
mathematical discipline, led many authors to consider mostly putational power of λ-calculus,
. its expresiveness in terms of the definable class of number-theoretic functions. Church himself,
in view of the results of Kleene and Turing, proposed his welknown "Thesis", which is intended to
characterize putational power of finitistic systems (see Odifreddi[1986] for an updated
discussion). This lecture is not concerned with the issue of "computability" as focused by Church's
Thesis; however, the relevance of this claim on the expressiveness of formal systems must be
acknowledged. On one side it sets a limit to putations by finitistic methods, on the other
it suggests that there is no other reasonable understanding putability, besides the one
established within the Hilbert - Brouwer lively debate in the twenties and early thirties. Almost
everybody agrees nowadays that, as long as we do not have a counterexample, we may rely on
Church's Thesis, provided that its use is not mathematically misleading. Namely, the philosophical
point raised by the Thesis is surely crucial, but do we really need it when working out results ? In
case a new system for putations is proposed, it is then better to check carefully whether it
putes exactly the putable functions (what a discovery if it were not so ! ). If,
instead, one is using a well established formal system, such as λ-calculus or Turing Machines, "hand
wa