Lambda-Calculus and Combinators：An Introduction

Combinatorylogicandlambda-calculus,originallydevisedinthe1920s,havesincedevelopedintolinguistictools,especiallyusefulinprogramminglanguages.Theauthors'previousbookservedasthemainreferenceforintroductorycoursesonlambda-calculusforover20years:thislong-awaitednewversionisthoroughlyrevisedandoffersafullyup-to-dateaccountofthesubject,withthesameauthoritativeexposition.Thegrammarandbasicpropertiesofbothcombinatorylogicandlambda-calculusarediscussed,followedbyanintroductiontotype-theory.Typedanduntypedversionsofthesystems,andtheirdifferences,arecovered.Lambda-calculusmodels,whichliebehindmuchofthesemanticsofprogramminglanguages,arealsoexplainedindepth.Thetreatmentisasnon-technicalaspossible,withthemainideasemphasizedandillustratedbyexamples.Manyexercisesareincluded,fromroutinetoadvanced,withsolutionstomostattheendofthebook.