Lambda-calculus, Combinators and Functional Programming

Description

Originally published in 1988, this book presents an introduction to lambda-calculus and combinators without getting lost in the details of mathematical aspects of their theory. Lambda-calculus is treated here as a functional language and its relevance to computer science is clearly demonstrated. The main purpose of the book is to provide computer science students and researchers with a firm background in lambda-calculus and combinators and show the applicabillity of these theories to functional programming. The presentation of the material is self-contained. It can be used as a primary text for a course on functional programming. It can also be used as a supplementary text for courses on the structure and implementation of programming languages, theory of computing, or semantics of programming languages. 1. Introduction 1.1 Variables and functions in mathematics and in programming languages 1.2 Domains, types, and higher-order functions 1.3 Polymorphic functions and Currying 2. Type-free lambda-calculus 2.1 Syntactic and semantic considerations 2.2 Renaming, a-congruence, and substitution 2.3 Beta-reduction and equality 2.4 The Church-Rosser theorem 2.5 Beta-reduction revisited 3. Combinators and constant symbols 3.1 Lambda-expressions without free variables 3.2 Arithmetic and other constants and combinators 3.3 Recursive definitions and the Y combinator 3.4 Elimination of bound variables: bracket abstraction 4. List manipulation in lambda-calculus 4.1 An extension of the syntax of lambda expressions 4.2 Additional axioms for list manipulation 4.3 List manipulating functions 4.4 Dealing with mutual recursion 4.5 Computing with infinite lists 5. Rule-based semantics of lambda expressions 5.1 Program transformation as a computation 5.2 Controlled reduction 5.3 The functional programming system FP 5.4 Translation of functional programs to lambda calculus 5.5 List comprehension in Miranda 6. Outlines of a reduction machine 6.1 Graph representation of lambda expressions 6.2 The instructions of a reduction machine 6.3 Implementation of primitive functions 6.4 Demand-driven evaluation 7. Towards a parallel graph-reduction 7.1 Harnessing the implicit parallelism 7.2 On-the-fly garbage collection 7.3 Control of parallelism Appendix A A proof of the Church-Rosser theorem Appendix B Introduction to typed lambda calculus Bibliographical notes References