Lambda-Calculus and Combinators，an Introduction.pdf

发布时间：2022-06-14 发布人：admin 分类：说明书资料大小：2.06M 资料格式：pdf 举报版权申诉

b037de49-21f7-4b4b-a8df-63965ac796d5.pdf-第1页.png

第1页 / 共359页

b037de49-21f7-4b4b-a8df-63965ac796d5.pdf-第2页.png

第2页 / 共359页

b037de49-21f7-4b4b-a8df-63965ac796d5.pdf-第3页.png

第3页 / 共359页

b037de49-21f7-4b4b-a8df-63965ac796d5.pdf-第4页.png

第4页 / 共359页

b037de49-21f7-4b4b-a8df-63965ac796d5.pdf-第5页.png

第5页 / 共359页

b037de49-21f7-4b4b-a8df-63965ac796d5.pdf-第6页.png

第6页 / 共359页

b037de49-21f7-4b4b-a8df-63965ac796d5.pdf-第7页.png

第7页 / 共359页

b037de49-21f7-4b4b-a8df-63965ac796d5.pdf-第8页.png

第8页 / 共359页

Cover

Half-title

Title

Contents

Preface

1 The lambda-calculus

1A Introduction

1B Term-structure and substitution

1C beta-reduction

1D beta-equality

Further reading

2 Combinatory logic

2A Introduction to CL

2B Weak reduction

2C Abstraction in CL

2D Weak equality

Further reading

3 The power of lambda and combinators

3A Introduction

3B The fixed-point theorem

3C Bohm’s theorem

3D The quasi-leftmost-reduction theorem

3E History and interpretation

4 Representing the computable functions

4A Introduction

4B Primitive recursive functions

4C Recursive functions

4D Abstract numerals and Z

5 The undecidability theorem

6 The formal theories lamnda beta and CLw

6A The definitions of the theories

6B First-order theories

6C Equivalence of theories

7 Extensionality in lambda-calculus

7A Extensional equality

7B lambdaeta-reduction in lambda-calculus

8 Extensionality in combinatory logic

8A Extensional equality

8B Axioms for extensionality in CL

8C Strong reduction

9 Correspondence between lambda and CL

9A Introduction

9B The extensional equalities

9C New abstraction algorithms in CL

9D Combinatory beta-equality

10 Simple typing, Church-style

10A Simple types

10B Typed lambda-calculus

10C Typed CL

11 Simple typing, Curry-style in CL

11A Introduction

11B The system TA→C

11C Subject-construction

11D Abstraction

11E Subject-reduction

11F Typable CL-terms

11G Link with Church’s approach

11H Principal types

11I Adding new axioms

11J Propositions-as-types and normalization

12 Simple typing, Curry-style in lambda

12A The system TA→lambda

12B Basic properties of TA→lambda

12C Typable lambda-terms

12D Propositions-as-types and normalization

12E The equality-rule Eq

Further reading

13 Generalizations of typing

13A Introduction

13B Dependent function types, introduction

13C Basic generalized typing, Curry-style in lambda

13D Deductive rules to define types

13E Church-style typing in lambda

13F Normalization in PTSs

13G Propositions-as-types

13H PTSs with equality

14 Models of CL

14A Applicative structures

14B Combinatory algebras

15 Models of lambda-calculus

15A The definition of lambda-model

15B Syntax-free definitions

15C General properties of lambda-models

16 Scott's D∞ and other models

16A Introduction: complete partial orders

16B Continuous functions

16C The construction of D∞

16E D∞ is a lambda-model

16F Some other models

Further reading

Appendix A1 Bound variables and alpha-conversion

Appendix A2 Confluence proofs

A2A Confluence of beta-reduction

A2B Confluence of other reductions

Appendix A3 Strong normalization proofs

A3A Simply typed lambda-calculus

A3B Simply typed CL

A3C Arithmetical system

Appendix A4 Care of your pet combinator

Appendix A5 Answers to starred exercises

References

List of symbols

Index

This page intentionally left blank

Lambda-Calculus and Combinators, an Introduction Combinatory logic and λ-calculus were originally devised in the 1920s for investigating the foundations of mathematics using the basic concept of ‘operation’ instead of ‘set’. They have since evolved into important tools for the development and study of programming languages. The authors’ previous book Introduction to Combinators and λ-Calculus served as the main reference for introductory courses on λ-calculus for over twenty years: this long-awaited new version offers the same authoritative exposition and has been thoroughly revised to give a fully up-to-date account of the subject. The grammar and basic properties of both combinatory logic and λ-calculus are discussed, followed by an introduction to type-theory. Typed and untyped versions of the systems, and their differences, are covered. λ-calculus models, which lie behind much of the semantics of programming languages, are also explained in depth. The treatment is as non-technical as possible, with the main ideas emphasized and illustrated by examples. Many exercises are included, from routine to advanced, with solutions to most of them at the end of the book. Review of Introduction to Combinators and λ-Calculus: ‘This book is very interesting and well written, and is highly recommended to everyone who wants to approach combinatory logic and λ-calculus (logicians or computer scientists).’ Journal of Symbolic Logic ‘The best general book on λ-calculus (typed or untyped) and the theory of combinators.’ G´erard Huet, INRIA

Lambda-Calculus and Combinators, an Introduction J. ROGER HINDLEY Department of Mathematics, Swansea University, Wales, UK JONATHAN P. SELDIN Department of Mathematics and Computer Science, University of Lethbridge, Alberta, Canada

CAMBRIDGE UNIVERSITY PRESS Cambridge, New York, Melbourne, Madrid, Cape Town, Singapore, São Paulo Cambridge University Press The Edinburgh Building, Cambridge CB2 8RU, UK Published in the United States of America by Cambridge University Press, New York www.cambridge.org Information on this title: www.cambridge.org/9780521898850 © Cambridge University Press 2008 This publication is in copyright. Subject to statutory exception and to the provision of relevant collective licensing agreements, no reproduction of any part may take place without the written permission of Cambridge University Press. First published in print format 2008 ISBN-13 978-0-511-41423-7 eBook (EBL) ISBN-13 978-0-521-89885-0 hardback Cambridge University Press has no responsibility for the persistence or accuracy of urls for external or third-party internet websites referred to in this publication, and does not guarantee that any content on such websites is, or will remain, accurate or appropriate.

To Carol, Goldie and Julie

Contents 1 2 3 4 5 6 Introduction to CL Abstraction in CL Introduction Term-structure and substitution β-reduction β-equality Preface The λ-calculus 1A 1B 1C 1D Combinatory logic 2A 2B Weak reduction 2C 2D Weak equality The power of λ and combinators 3A 3B 3C 3D 3E Representing the computable functions Introduction 4A Primitive recursive functions 4B Recursive functions 4C 4D Abstract numerals and Z The undecidability theorem The formal theories λβ and CLw 6A 6B Introduction The ﬁxed-point theorem B¨ohm’s theorem The quasi-leftmost-reduction theorem History and interpretation The deﬁnitions of the theories First-order theories vi page ix 1 1 5 11 16 21 21 24 26 29 33 33 34 36 40 43 47 47 50 56 61 63 69 69 72

分享到：

赞收藏

资料库

Lambda-Calculus and Combinators，an Introduction.pdf

相关推荐

开发技术

热门标签

最新资料