[Some citations for Lambda Calculus books from MathSciNet --djr]
88j:03009 03B40 (03-01 68Q55)
Hindley, J. Roger(4-WALS); Seldin, Jonathan P.(3-CONC)
Introduction to combinators and $\lambda$-calculus.
London Mathematical Society Student Texts, 1.
Cambridge University Press, Cambridge-New York, 1986. vi+360 pp.
$49.50; \$16.95 paperbound. ISBN 0-521-26896-6; 0-521-31839-4
In December 1920, the Soviet mathematician M. Schonfinkel opened, by
his report "Uber die Bausteine der mathematischen Logik" to the
Mathematical Society in Gottingen [Math. Ann. 92 (1924), 305--316;
Jbuch 50, 23], a new trend in the foundations of mathematics, which is
based on the concept of a generalized function, the argument of which
is also a function (without any restrictions). This mathematical
discipline, named "combinatory logic" by Curry and the "theory
(calculus) of $\lambda$-conversion" or "$\lambda$-calculus" by A.
Church, during the past fifteen years has changed its appearance. Its
connections with algebra, topology and category theory were revealed
and became an important part of informatics. In particular,
$\lambda$-calculi have turned out today to be convenient models,
revealing fundamental aspects of the construction and operation of
programs in algorithmic languages.
While the classical methods of research were purely syntactical, the
discovery of models enabled us to apply semantic methods, which have
turned out to be very effective, for example, in problems of extension
and application of classical $\lambda$-calculi.
The authors of the book under review are outstanding specialists in
this domain; in particular, they wrote, together with H. B. Curry, the
second volume of Combinatory logic [North-Holland, Amsterdam, 1972;
Zbl 242:02029] and, together with B. Lercher, the book Introduction to
combinatory logic [Cambridge Univ. Press, London, 1972; MR 49 #25].
The book under review is divided into eighteen chapters: (1)
$\lambda$-calculus; (2) Combinatory logic; (3) The power of $\lambda$
and combinators; (4) Representing the recursive functions; (5) The
undecidability theorem; (6) The formal theories $\lambda\beta$ and
CLw; (7) Extensionality in $\lambda$-calculus; (8) Extensionality in
combinatory logic; (9) The correspondence between $\lambda$ and CL;
(10) Models of CLw; (11) Models of $\lambda\beta$; (12) $D\sb \infty$
and other models; (13) Typed terms; (14) Type assignment to CL-terms;
(15) Type assignment to $\lambda$-terms; (16) Generalized type
assignment; (17) Logic based on combinators; (18) Godel's consistency
proof for arithmetic.
The titles of the chapters characterize the book, on the one hand, as
an introduction to this subject and, on the other hand, as a complete
exposition of almost all the new (especially, model-theoretic)
results.
We may note in particular the logical constructions, introduced as
type-free sequential extensions (with unrestricted abstraction
(comprehension), but with restricted cut rule) of the theory of
combinators of Schonfinkel and Curry or the $\lambda$-calculi of
Church [see the reviewer, Z. Math. Logik Grundlag. Math. 29 (1983),
no. 5, 385--416; MR 85d:03026; and the references cited therein].
These systems are worth noticing in such a book, since their use makes
it possible to prove the consistency of the well-known calculi ZF, NBG
and FA (without presuming the consistency of any other calculi, i.e.\
in the absolute sense) by the method of reduction of one
logico-mathematical system to another, elaborated by Kolmogorov,
Bernays and Godel. The provable syntactical completeness (according to
Godel) of such logical constructions, and the provable consistency (in
the classical sense) of some subclasses of the classes of all their
derivations, are essentially used.
Reviewed by A. S. Kuzichev
_________________________________________________________________
86k:03007 03B40 (03-02 68Q55)
Barendregt, H. P.(NL-UTRE)
Introduction to lambda calculus.
Nieuw Arch. Wisk. (4) 2 (1984), no. 3, 337--372.
From the introduction: "This paper is an introduction to the type-free
lambda calculus. Section 1 gives some intuition about the basic
operations of the $\lambda$-calculus and some examples of inductive
definitions and proofs. In Section 2, $\lambda$-terms and conversion
(provable equality) are introduced and it is proved that all recursive
functions are represented in the $\lambda$-calculus. In Section 3, the
notion of $\lambda$-model in the category of complete lattices is
introduced and the construction of a particular such model $D\sb A$ is
given. Section 4 is about reduction and gives a dynamical and
proof-theoretical analysis of conversion. In the concluding Section 5,
the notion of the Bohm tree of a $\lambda$-term is introduced. It is
proved that terms with the same Bohm tree are equal in the model $D\sb
A$, giving an interesting consistent extension of the
$\lambda$-calculus.
"The methods in Section 2 and Section 4 are algebraic, that is,
finitary in character. In Section 3 limits play a role, so it has an
infinitary character. In Section 5 an interaction of the algebraic and
limit aspects plays an important role. The sections end with some
exercises; the more difficult ones have one or more stars."
_________________________________________________________________
86f:01030 01A60 (03-03 03B40 68-03)
Rosser, J. Barkley(1-WI-R)
Highlights of the history of the lambda-calculus.
Ann. Hist. Comput. 6 (1984), no. 4, 337--349.
This paper is a short history of the lambda calculus and combinatory
logic by a participant in that history. After a brief introduction to
both systems and their early history, the author takes up the
inconsistency originally discovered by himself and S. C. Kleene [Ann.
of Math. (2) 36 (1935), 630--636; Zbl 12, 146] and later simplified by
H. B. Curry [J. Symbolic Logic 7 (1942), 115--117; MR 4, 125] and the
effect of this inconsistency on the further development of the
subject. He then gives the simplest known proof of the Church-Rosser
theorem, which shows the consistency of both systems. Next follows a
discussion of completeness, which is taken here to mean the
representability of all partial recursive functions; instead of giving
a proof, which is easily available in many other places, the author
discusses the history of this representation and of Church's thesis,
the original form of which was that all effectively computable
functions are lambda representable. The author includes some personal
recollections of his early work with Church and Kleene on this
subject. This is followed by a discussion of models, including a
simple presentation of a simple model due to G. D. Plotkin ["A
set-theoretical definition of application", Memorandum MIP-R-95,
School of Artificial Intelligence, Univ. Edinburgh, Edinburgh, 1972;
per bibl.] and E. Engeler [Algebra Universalis 13 (1981), no. 3,
389--392; MR 83f:03012]. The paper closes with a discussion of the
connection with computers, especially the early development of
functional programming. There is an extensive list of references.
\{Reviewer's remarks: 1. The paper is very well written and is a
pleasure to read. 2. The reference to Engeler (1979) might be replaced
with a reference to the published version cited above.\}
Reviewed by J. P. Seldin
© Copyright American Mathematical Society 1986, 2000
==============================================================================
From: forkosh@panix.com (John Forkosh)
Subject: Re: Good textbook for lambda calculus?
Date: 29 Apr 1999 12:13:49 -0400
Newsgroups: sci.math,comp.theory
Gerhard Niklasch (nikl@mathematik.tu-muenchen.de) wrote:
: Erik Max Francis wrote:
: >I got a copy of _Lambda calculi: A guide for computer scientists_
: >(Chris Hankin), and although it certainly covers everything, it is
: >clearly intended to be accompanied by a lecture to fill in the details
: >and skipped steps in the proof. [...]
: >
: >Can anyone suggest a good self-teaching textbook on lambda calculus?
: _The_ classic textbook is H.P.Barendregt, The Lambda Calculus,
: Its Syntax and Semantics. (Reaches into shelf) Revised Edition,
: North Holland 1984; ISBN 0-444-87508-5 (ppb).
: (Studies in logic and the foundations of mathematics ; v.103)
: (This may not be the latest edition.)
Latest as far as I know (someone should tell North-Holland to
stop using acid-rich paper that turns yellow, and cheap bindings
from which pages fall out after a little use)
: It has an introductory chapter striding through a large area, before
: going into depth and details. Also: lots of exercises, and thumbnail
: pictures of many of the chief characters.
A simpler read is (the almost equally old)
Introduction to Combinators and lambda-Calculus
J. Roger Hindley and Jonathan P. Seldin
Cambridge U.P. 1986, ISBN 0-521-31839-4 (paperback)
Graduate level is
Lambda-Calculus, Types and Models
J.L. Krivine
Masson, Paris, 1993 (English xlation) ISBN 0-13-062407-1
They all omit some steps (to my mind), but perhaps
one may help you where another fails.
John (forkosh@panix.com)
==============================================================================
From: David Eader
Subject: Re: Good textbook for lambda calculus?
Date: Mon, 03 May 1999 20:17:15 -0700
Newsgroups: sci.math,comp.theory
Another book is "Lambda-Calculus Combinators and Functional Programming"
by G.Revesz. (Cambridge Tracts in Theoretical Comp Sci)
ISBN# 0-521-34589-8
I haven't read the books suggested by others, so can't compare, but this
book is pretty cool. Some topics it covers:
Currying
Renaming, alpha-congruence, and substitution
beta reduction
Church-Rosser theorem.
Recursive definitions and the lambda-combinator.
mutual recursion
infinite lists.
deader
Erik Max Francis wrote:
> I got a copy of _Lambda calculi: A guide for computer scientists_
> (Chris Hankin), and although it certainly covers everything, it is
> clearly intended to be accompanied by a lecture to fill in the details
> and skipped steps in the proof. I can follow it, but I need to stop and
> work out everything every ten seconds (since no motivation for their
> statements is given; a lecture is implied, since it's a small book).
>
> Can anyone suggest a good self-teaching textbook on lambda calculus?
> High-level mathematics wasn't the problem, it was the skipped steps and
> clear intention of having secondary material to help explain the text
> that has me thinking there's probably a better book out there.
>
> Thanks.
>
> --
> Erik Max Francis / email max@alcyone.com / whois mf303 / icq 16063900
> Alcyone Systems / irc maxxon (efnet) / finger max@members.alcyone.com
> San Jose, CA / languages En, Eo / web http://www.alcyone.com/max/
> USA / icbm 37 20 07 N 121 53 38 W / &tSftDotIotE
> \
> / Men live by forgetting -- women live on memories.
> / T.S. Eliot