Lambda-Calculus and Combinators

所需积分/C币:18 2019-04-13 19:26:23 251KB PDF
11
收藏 收藏
举报

Roger Hindley写的lambda演算经典书籍 Combinatory logic and lambda-calculus, originally devised in the 1920s, have since developed into linguistic tools, especially useful in programming languages. The authors' previous book served as the main reference for introductory courses on lambda-calculus for over 20 years: this version, first published in 2008, is thoroughly revised and offers an account of the subject with the same authoritative exposition. The grammar and basic properties of both combinatory logic and lambda-calculus are discussed, followed by an introduction to type-theory. Typed and untyped versions of the systems, and their differences, are covered. Lambda-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 at the end of the book.
CAMBRIDGE Cambridge University Press 978-0-521-89885-0- Lambda-Calculus and Combinators, an Introduction J. Roger Hindley and Jonathan P. Seldin Frontmatter More information Lambda-Calculus and Combinators an introduction L. ROGER HINDLEY Department mathematics Swansea university, Wales, UK JONATHAN P SELDIN Department of mathematics and Computer Science, University of lethbridge, Alberta, Canada CAMBRIDGE UNIVERSITY PRESS C Cambridge University Press www.cambridge.org CAMBRIDGE Cambridge University Press 978-0-521-89885-0- Lambda-Calculus and Combinators, an Introduction J. Roger Hindley and Jonathan P. Seldin Frontmatter More information CAMBRIDGE UNIVERSITY PRESS Cambridge, New York, Melbourne, Madrid, Cape Town, Singapore, Sao Paulo, Delhi Cambridge university pres The Edinburgh Building, Cambridge CB2 &RU, UK Published in the United States of America by Cambridge University Press, New York .cambridge.org Informationonthistitlewww.cambridgeorg/978052189880 Cambridge university press 2008 This publication is in copyright. Subject to statutory exception and to the provisions of relevant collective licensing agreements, no reproduction of any part may take place without the written permission of Cambridge University Press First published 2008 Printed in the united Kingdom at the university press, Cambridge a catalogue record for this publication is available from the British library Library of Congress Cataloguing in Publication data Hindley, J. Ro Lambda-calculus and combinators: an introduction/J. Roger Hindley, Jonathan p seld p Includes bibliographical references and index isbn9780-521-89885-0(hardback) 1. Lambda-calculus. 2. Combinatory logic. I Seldin..P. I. Title QA9.5H5652008 2008006276 Isbn 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 C Cambridge University Press www.cambridge.org CAMBRIDGE Cambridge University Press 978-0-521-89885-0- Lambda-Calculus and Combinators, an Introduction J. Roger Hindley and Jonathan P. Seldin Frontmatter More information To Carol. Goldie and Julie C Cambridge University Press www.cambridge.org CAMBRIDGE Cambridge University Press 978-0-521-89885-0- Lambda-Calculus and Combinators, an Introduction J. Roger Hindley and Jonathan P. Seldin Frontmatter More information Contents Preface page ix The入 calculus 1A Introduction 1B Term-structure and substitution 1C B-reduction 1D B-equality 16 Combinatory logic 2A Introduction to CL 21 2b Weak reduction 4 2C Abstraction in CL 26 2D Weak equality 29 3 The power of X and combinators 3a Introduction 33 3B The fixed-point theorem 3 c Boh’ s theore 36 3D The quasi-leftmost-reduction theorem 40 BE History and interpretation 43 Representing the computable functions 47 4a Introduction 47 4b Primitive recursive functions 50 4c Recursive functions 4d Abstract numerals and z 61 The undecidability theorem 63 6 The formal theories XB and Clw 6a The definitions of the theories 69 6b First-order theories 72 C Cambridge University Press www.cambridge.org CAMBRIDGE Cambridge University Press 978-0-521-89885-0- Lambda-Calculus and Combinators, an Introduction J. Roger Hindley and Jonathan P. Seldin Frontmatter More information Contents 6c Equivalence of theories 73 7 Extensionality in X-calculus 7a Extensional equality 76 7B Bn-reduction in A-calculus 79 8 Extensionality in combinatory logic 82 8a Extensional equality 82 8B Axioms for extensionality in CL 8c Strong reduction 89 Correspondence between X and cL 9A Introduction 92 9B The extensional equalities 9c New abstraction algorithms in CL 9D Combinatory B-equality 102 10 Simple typing, Church-style 107 10A Simple types 107 10 b Typed入 calculus 109 10C Typed CL 115 11 Simple typing, Curry-style in CL 119 11A Introduction 119 11B The system TAc 122 11c Subject-construction 126 11D Abstraction 127 11E Subject-reduction 130 11F Typable CL-terms 134 11G Link with Church's approach 137 11H Principal types 138 11i Adding new axioms 143 11J ProposilionIs-as-t y pes and normalizatioN 147 11k Thc cquality-rulc Ec 155 12 Simple typing, Curry-style in X 159 12 A The system TA入 159 12B Basic properties of TAx 165 12 c Typable入- terms 170 12D Propositions-as-types and normalization 173 12E The equality-rule Eq 176 13 Generalizations of typing 180 13a Introduction 180 13B Dependent function types, introduction 181 C Cambridge University Press www.cambridge.org CAMBRIDGE Cambridge University Press 978-0-521-89885-0- Lambda-Calculus and Combinators, an Introduction J. Roger Hindley and Jonathan P. Seldin Frontmatter More information Contents 13c Basic generalized typing, Curry-style in X 13D Deductive rules to define types 187 13E Church-style typing in X 191 13F Normalization in PTss 202 13G Propositions-as-types 209 13H PTSs with equality 217 14 Models of cl 220 14A Applicative structures 220 14B Combinatory algebras 3 15 Models of -calculus 229 15A The definition of A-lnlodel 229 15B Syntax-frcc dcfinitions 236 15C General properties of X-models 242 1 6 Scott's D and other modcls 247 16A Introduction: complete partial orders 247 16B Continuous functions 252 16c The construction of D 256 16d Basic properties of D 261 16E D is a A-model 267 16F Some other models 71 Appendi al bound variables and a-conversion 276 Appendi a2 Confluence proofs Appendix a3 Strong normalization proofs Appendix a4 Care of your pet combinator 305 Appendix a5 Answers to starred exercises 307 References 323 List of symbols 334 ndea 337 C Cambridge University Press www.cambridge.org CAMBRIDGE Cambridge University Press 978-0-521-89885-0- Lambda-Calculus and Combinators, an Introduction J. Roger Hindley and Jonathan P. Seldin Frontmatter More information Preface The X-calculus and combinatory logic are two systems of logic which can also serve as abstract programming languages. They both aim to describe some very general properties of programs that can modify other programs, in an abstract setting not cluttered by details. In some ways they are rivals, in others they support each other The A-calculus was invented around 1930 by an American logician Alonzo church, as part of a comprehensive logica. system which included higher-order operators(operators which act on other operators). In fact the language of X-calculus, or some other essentially equivalent notation is a key part of most higher-order languages, whether for logic or for computer programming. Indeed, the first uncomputable problems to be discovered were originally described, not in terms of idealized computers such as turing machines, but in A-calculus Combinatory logic has the same aims as X-calculus, and can express the same computational concepts, but its grammar is much simpler. Its basic idea is due to two people: Moses Schonfinkel, who first thought of it in 1920, and Haskell Curry, who independently re-discovered it seven years later and turned it into a workable technique The purpose of this book is to introduce the reader to the basic meth ods and results in both fields The reader is assumed to have no previous knowledge of these fields but to know a little about propositional and predicate logic and recursive functions, and to have some experience with mathematical induction Exercises are included, and answers to most of them(those marked *) are given in an appendix at the end of the book. In the early chapters there are also some extra exercises without answers, to give more routine practice if needed C Cambridge University Press www.cambridge.org CAMBRIDGE Cambridge University Press 978-0-521-89885-0- Lambda-Calculus and Combinators, an Introduction J. Roger Hindley and Jonathan P. Seldin Frontmatter More information Preface References for further reading are included at the ends of appropriat chapters, for the reader who wishes to go deeper ome chapters on special topics are included after the initial basic chapters. However, no attempt has been made to cover all aspects of A-calculus and combinatory logic; this book is only an introduction, not a complete survey This book is essentially an updated and re-written version of (HS86. It assumes less background knowledge. Those parts of HS86 which are still relevant have been retained here with only minor changes, but other parts have been re-written considerably. Many errors have been cor rected. More exercises have been added. with more detailed answers and the references have been brought up to date. Some technical details have been moved from the main text to a new appendix The three chapters on types in [HS86 have been extensively re-written here. Two of the more specialized chapters in [HS86, on higher-order logic and the consistency of arithmetic, have been dropped Acknowledgements The authors are very grateful to all those who have made comments on [HS86 which have been very useful in preparing the present book, especially Gerard Berry, Steven Blake, Naim Cagman Thierry Coquand, Clemens Grabmayer, Yexuan Gui, Benedetto Intrig- ila, Kenichi Noguchi, Hiroakira Ono, Gabriele ricci, Vincenzo Scianni John Shepherdson, Lewis Stiller, John Stone, Masako Takahashi, Peter Trigg and Pawel Urzyczyn Their comments have led to many improvements and the correction of several errors.(Any errors that remain are entirely the authors're sponsibility, however. On the production side, the authors wish to thank Larissa Kowbuz for her very accurate typing of an early draft, the designers of IATeX and its associated software for the actual type-setting, and M. Tatsuta for the usc of his macro proof sty. Wc are also vcry grateful to Chris Whylcy for technical help, and to Cambridge University Press, especially David Tranah, for their expert input On the financial side we thank the National Sciences and engineering Research Council of Canada for a grant which enabled a consultation visit by hindley to Seldin in 2006, and the Department of mathemat ics and Computer Science of the University of Lethbridge for helpful hospitality during that visit I Which itself was developed from [HLS72] which was written with Bruce Lercher C Cambridge University Press www.cambridge.org

...展开详情
试读 11P Lambda-Calculus and Combinators
立即下载 身份认证后 购VIP低至7折
一个资源只可评论一次,评论内容不能少于5个字
您会向同学/朋友/同事推荐我们的CSDN下载吗?
谢谢参与!您的真实评价是我们改进的动力~
关注 私信
上传资源赚钱or赚积分
最新推荐
Lambda-Calculus and Combinators 18积分/C币 立即下载
1/11
Lambda-Calculus and Combinators第1页
Lambda-Calculus and Combinators第2页
Lambda-Calculus and Combinators第3页

试读结束, 可继续读1页

18积分/C币 立即下载