Foundations for Programming Languages

所需积分/C币:10 2019-03-26 14:03:50 4.43MB PDF
收藏 收藏
举报

Foundations for Programming Languages
Foundations for Programming laiignagcis 2. PCF Roduction alld Syinbolic Interpret(u 2.4 oudeterninlist ic 1(dlulctioll 2.1.2 Reduction strato 2. 1,3 The loft -most and la duction 8 2. 1.1 Parallel reduction 1.卫a(rPCF 2. 5 PCF Programming Examples. Expressive Power and T: imitations 93 2.1R 93 2 Searching the nlatiltr'al tllllmibCr's 3 Iteration and tail roeulrsio1t 97 Total r( fulmictiors 2.5.5 Partia.I recursive functionis Definability of oelatIolls l(7 2.6 Variations and exte f pcf 2.6.1 Sulltlmlalv of (xt(sious 2. 6.2 Unit types 2.(.}R 117 12: 3 Universal Algebra and Algebraic Data Types 133 I Introduction 13 3.3 Algebras, Signatures alld terIns 3.}.1Agba5 2 Syntax of algebr 13G Algebras and the interpretation of terns 3.3. 1 TlLe substitution lemma B t Equation. So1uldlness and Coirplotcllcss 士 3.4.1 COllations 43 3.+.2 TorIn algebras andI subst itation 3.1.3 Semantic implication aldl al (qllationlal pr oof systeill 1.1 Forlls of coplteIIe'Ss 17 3. 1.6 NollcImpty sorts alld the least Ilodlel property lGO Hoinoimorphisilis alld iuitiality 1G1 3:. 1 HoinoimorphisTtis auld isoinorphisTtis G1 3. 5.2 Initial algebras 1 3 Data t 1(9 3.( 1 Specilicatioll and dat a abstraction 169 3. 6. 2 Initial algebra semantics alld datatype iilt 171 3.6i. 3 Examples and error values 3.6.+ Alternative approaches to (rl'or values 81 B7 Rewrit( l8, B fictitious 83 3.7.2 Colluencc and provable (qualit l86 3.7.3 Terlllinationl 3.7.1 (ritical pairs 192 Foundations for Progranming laiignagci 3. L: cft-liuIcar 11oul-overlapping rewrite systein 198 3.7.6 Local coufucuce, termination alld completion 7.7 Applications to algebraic datatypes 201 4 Simply-Typed Lambda Calculus 207 4.1 nt r odulctioll 2017 4. 2 Tpes 2018 4. 2. 1 Syntax 1.2.2 Iit(rprct ation of typ('S 20)90 1.}①1Ls 1.5.1 (ont cxt -sensitive synt a 210 1.3.2 Synt ax of tolima 1.3.3 Terms with product, sium and 1 elated tvpes 217 1.3. 1 Formulas-as-types correspond B5 Typing aIgorithuIn 士.士 Proor syster 225 collations and thicon 25 1.2 Reduct 1. 3 Rodulctioul with ade roof-thcoretic inlcthols for consistency alld ((uiservativity 7 Henkin Models dIne ss alld Coirplotenl('ss 6. 1 G(I1(ral Inodes andl the Itleaninlus of t(rlns 2.2 2 Applicative striletnires (xt(nsiouality and fr aliEs 3 1. 5. Environment molel condlition 5. 1 Type and equational solidness 1.5.3 Completeness for lInkin models without empty type s 52 1.5. Completeness with enpty types 21 1. i7 Combinator s alld t hc (oil minatory moll condit ion 2)6 +.0.8 Combinatory and lambda algebras t.3.9 Henkin models for othier types 5 Models of Typed Lambda Calculus 262 3.1 introduct 0.2 Domain-Theorctic models and fixcd points 5. 2.1 Recursive definitions and fixed point operator 5. 2. 2 Complete paltial orders. lifting and cartesian pr(diets 5.2.3 Continuous funct ions 5.2.+ Fixed points and thic lill continlLo1LS hicrarchy 272 5.2. 5 (P(Inode for PCF B F It tuld I COmputational Adequacy alld Fulll abstraction ). L 1 Appr oximation thcor'elnl and coinputational adequacy 5.1. 2 FiLll abstraction for PCF with parallel operations ). s RerursionI-thcorctic models 5∴.1 Introductio1l 5. 3.2 odest sots 5.3.3 Full recursive hierarchy 05 Foundations for Progranninr languages G Partial equivalence relatious and recursion 3() Partial equivalence rclation interpretation of tpes 3( 5. 6.2 Generalization to partial combinatory algebras G .3 Lifting, partial functions and recur sion 5. 6. 1 RcCllsicn and the intrinsic order 17 5.6.5 Lifting, pr( s anld fiullction spaces of effective cpo)s 2}21 6 Imperative programs 325 G 1 lntroduction (. 2 While programs 2}27 0.2.1 L-values and R-val1los 27 f.2.2 nta.x of while pr( 0.3 Operational Sclmlant ics f.3.1B boks 329 (.2工( cations and storo (1.3.3 EvallLation ol expressions 0: 1 Exccution of commands fi. Dell@tational soinanties L 1 Typed lambda calculus with stores 33f fi..L. 2 Scantic fiinctions (i 1.3 Equivaloueeof opeTational and denotational semantics 6. Before after Assertions About while proeraItIs |6i (js] First-order alld partial correctness asscrtio1ls |6i 0. .2 Proof illes .5 0. 5. 1 Rclativc completeness 0. 6 Semantics of Additional Program constricts 6. 6,1 Overview 6i. 6. 2 Blocks with local variable 6.6 Pro Gi. 6. 1 CoInbiuinlg blocks alld pror(dure declarations 3G7 7 Categories and Recursive Types 371 1 Introductio 371 7. 2 Cartesian Closed Categories 7. 2.1 Category thcory and typed la }72 72. 2 Categories. Lilnctors and natual transformations 7. 2. Dclinition ofcartosian closcd category 381 7. 2. Soundless alld the interpretation of t(rills 7. 2.s helkill nodels as cce's 7.2.6 Categorical characterizationi of IT(Alling fulllctioll 7. 3 Kripke Lainbrda odels alld FlllIctor Categoric 1017 74.1 Overview 士(7 7.3. 2 possib) 1017 7.3.3 Applicative strilcti1ro 107 7.3.1卫xt←1 signality、( mbinators and fiinetor catcsori 7. 3.5 Environments and meanings of tells 112 Foundations for Progranninr languages 7.3.6 Soundless alld couplet(11('S B 7 Kripke lainhda inodes as cartesian closed categorics 1 Domain models of recursive types 7.1.1 A motivating cxapl 7.1.2 Diagrams. cones and limit s 122 7 1s F-alecbras 121 7 ++ w-Chains and it itial f-alecfras 26 4. 6 Colitnits and (-colirnits 43 7. 4.7 T ocally cont iltu1011s functors 436 7.8 Examples of thic ganeral mcthod 8 Logical relations 442 8.1 Introduction to Logical relations 112 8.2 Logical Relatiolls Ove] Applicative strllctill'cs 8.2.1 Dclinition of Logical eclat ion 士士 8.2.2 The Basic Lontra 8.2.3 Partial functions and thories of inodes vale 2.3Quoticnits alk extensionality 3 proof-ThIo I(OT(T1 8.3.1 ((loss for H(nkin inodes rnializatioTl 3. 3 Confluence and other reduction properties 8.3. 1 Rediction with fir and additional operations 8.1 Partial sirjcctions and Specific lodels S lI Partial surjections and the full classical hierarchy 2 Fllll recursive hierarch 8. 4.3 Full continious bicrarchIv 476 8.3 Representation independence 8. .1 lotivatioll 8..2卫 8.5.3 G(neal represcltatiol illdepclldlellco S G GenEralizations of logical iclatioils 183 8 6.1 1trodulctioTu 8. 6. 2 Motivating(xanplcs: couple partial orders alld Kripke irlodlcls 8. 6s Coning and 8.6.1 Comparison with logical relations 8.6.5 Gencral casc and applications to specilic categorics 士9 9 Polymorphism and Modularity 499 9. 1 lntroduction 0.11 Overview 士99 9.12T as filllctiol r1lllClItS (( neral products aldt siils O.l. 1 Types as specifications 9.2 Prclicativc Polymorphic calculus Foundations for Progranming laiignagci 9. yntax of types and tells 9.2.2 Comparison with othier formis of polyniorphiisirt 9.2.3 Equational proof system and 1'cdliction 16 9. 2. 1 Models of predicative polymorphisim 9.2.5 ML-style polymorphic declarations 21 b Impredicative Polyimiorphisin 21 升.3.]ⅡtP(<tct1 9.3.2 Fxpressivrll@ss an< properties ol thicortcs 93.3 TerMination ofr ion 38 3. 4 SiNnai of semantic Models d.3.3 Models based onl llmliversal doiriails 9. . Partia I (quivalcnco 1 elation tn(dIcIs 9. 1 Data Abstraction and existential TypeS 0. 5 Gon(Ia.I Products. Surnis and prograln \odules )(( 0.5.1T( NL Module、I 9.5.2 Predicative calcilliis with products and sums 9.5.3 Representing MOdulo s With Products alld Sins )(8 0.0.1 Prcdicativity and the rclationship betwe(1l (universes 10 Subtyping and related concepts 573 10. 1 Introduction 10).2 Simply Typ(d L: alnlda calculus with Sub pIg 10.3 Records 10.3.1 General properties of rccord suBtyping 581 10.3.2 Typed calculis with records andl subtyping 10. 1 Semantic Mordels of Subtyping 8 10. 1.1 Overview 10.1.2 Co1vers1ol interprctation of subtyping 10.4.3 Subsct interpretation ol typos 93 10.+. Partial cquivalence 1 cations as trpcs 10.5 Recursive Types alld a Rocord Mo(lol of objects 603 10.i PolyinorphisIll with Subtype constraints 1 Type Inference 621 11.1 IntroductiOn to Type iilorcnce 21 11.2 Type Inlerenlcc forX7 with Type variables )2士 11.2.1 The language Xi 21 11.22 Subst it iition. instances and luilicationl 11.2.3 An algorithin for principal curry typiulgs 6:0 11.2.1 Inplicit typing 11.2.5 Equivalence of typing alld unification 11.3 Type Infer@uce with Polymorphic Declarations 11.3.1 IL type illlerenee and poly morphic variables 士1 11.3.2 Two sots of iMplicit typing rules 11.3.3 Type inference algorit hms 11.3. 1 Equivalence of ml 60 11.35(mp plexity of l type inference Foul1clation for P1ograinniny languages Bibliography 661 Index 676 List of figures 1.1 Binary trcc 40 3. 1 A locally confu@lit bllt 11oll-coniflulent r(duction 2 Disjoint reductions 19士 8.3 Trivial(verla 3.1 Crit ical pair .19 5. 1 Ordering of continious fiinctions k 7( f 1 Morphism of concs 12 F. 2 F-aulgobras and unique morphisms of coconc 128 7. 3 Unique morphism fion u(e) into limit (onc H Over. 11 lllllcat1oll (ll (xp)I'('SS1o11 graphis 27 List of ables ().1 Introductory (ol1ls ollt lin ().2 Mat hematical colr sc on typed lainbxda calc11l1is ( CoURse on type theory 1,1 Well-loiulldedl l cations iorcoininol forins of induction 2.1 Equational proof system for PCF 2.2 Reduction axioms for PCF 2.s Left-most 1((lilction for PCF 2. Lay reduction for PCF 2.3 Fagor pcf reduction 2. 6 Evaluationt PCF reduction l(}8 3. 1 Aleck 3. 2 Algebraic specification of multi- scts. n/ and boo/ B 3 Algcbraic specification of trees B+ A specification for sc/.?(/alld bo l70 or list. alc a tool l了 3. G Naive tr(atireuit of (IroT valules for list. atom alld bool 3.7A ification for list. ato annd boo with lules 4.1 TypC-rhiecking algorit hIml Smythi-Plotkin mcthod for finding fixedl-ppoints of functors 138 llI R(Cirsii rithin unifi 11.2 Algorithiin PT lor pr'inicipal A+(city)typing 63] 11.3 AlgorithIn reducing At'(Curry) typing to unification 637 11. AlgorithIn PTL Cor principal typing with let 48

...展开详情
试读 127P Foundations for Programming Languages
立即下载 低至0.43元/次 身份认证VIP会员低至7折
抢沙发
一个资源只可评论一次,评论内容不能少于5个字
  • 签到新秀

    累计签到获取,不积跬步,无以至千里,继续坚持!
关注 私信 TA的资源
上传资源赚积分,得勋章
最新推荐
Foundations for Programming Languages 10积分/C币 立即下载
1/127
Foundations for Programming Languages第1页
Foundations for Programming Languages第2页
Foundations for Programming Languages第3页
Foundations for Programming Languages第4页
Foundations for Programming Languages第5页
Foundations for Programming Languages第6页
Foundations for Programming Languages第7页
Foundations for Programming Languages第8页
Foundations for Programming Languages第9页
Foundations for Programming Languages第10页
Foundations for Programming Languages第11页
Foundations for Programming Languages第12页
Foundations for Programming Languages第13页
Foundations for Programming Languages第14页
Foundations for Programming Languages第15页
Foundations for Programming Languages第16页
Foundations for Programming Languages第17页
Foundations for Programming Languages第18页
Foundations for Programming Languages第19页
Foundations for Programming Languages第20页

试读结束, 可继续阅读

10积分/C币 立即下载 >