[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