第1页 / 共191页
第2页 / 共191页
第3页 / 共191页
第4页 / 共191页
第5页 / 共191页
第6页 / 共191页
第7页 / 共191页
第8页 / 共191页
Programming Languages and Lambda Calculi.pdf
I Models of Languages
Chapter 1: Computing with Text
1.1 Defining Sets
1.2 Relations
1.3 Relations as Evaluation
1.4 Directed Evaluation
1.5 Evaluation in Context
1.6 Evaluation Function
1.7 Notation Summary
Chapter 2: Consistency of Evaluation
Chapter 3: The -Calculus
3.1 Functions in the -Calculus
3.2 -Calculus Grammar and Reductions
3.3 Encoding Booleans
3.4 Encoding Pairs
3.5 Encoding Numbers
3.6 Recursion
3.6.1 Recursion via Self-Application
3.6.2 Lifting Out Self-Application
3.6.3 Fixed Points and the Y Combinator
3.7 Reduction Strategy and Normal Form
3.8 History
II Models of Realistic Languages
Chapter 4: ISWIM
4.1 ISWIM Expressions
4.2 ISWIM Reductions
4.3 The Yv Combinator
4.4 Evaluation
4.5 Consistency
4.6 Observational Equivalence
4.7 History
Chapter 5: Standard Reduction
5.1 Standard Reductions
5.2 Proving the Standard Reduction Theorem
5.3 Observational Equivalence
5.4 Uniform Evaluation
Chapter 6: Machines
6.1 CC Machine
6.2 SCC Machine
6.3 CK Machine
6.4 CEK Machine
6.5 Machine Summary
Chapter 7: SECD, Tail Calls, and Safe for Space
7.1 SECD machine
7.2 Context Space
7.3 Environment Space
7.4 History
Chapter 8: Continuations
8.1 Saving Contexts
8.2 Revised Texual Machine
8.3 Revised CEK Machine
Chapter 9: Errors and Exceptions
9.1 Errors
9.1.1 Calculating with Error ISWIM
9.1.2 Consistency for Error ISWIM
9.1.3 Standard Reduction for Error ISWIM
9.1.4 Relating ISWIM and Error ISWIM
9.2 Exceptions and Handlers
9.2.1 Calculating with Handler ISWIM
9.2.2 Consistency for Handler ISWIM
9.2.3 Standard Reduction for Handler ISWIM
9.2.4 Observational Equivalence of Handler ISWIM
9.3 Machines for Exceptions
9.3.1 The Handler-Extended CC Machine
9.3.2 The CCH Machine
Chapter 10: Imperative Assignment
10.1 Evaluation with State
10.2 Garbage Collection
10.3 CEKS Machine
10.4 Implementing Garbage Collection
10.5 History
III Models of Typed Languages
Chapter 11: Types
11.1 Numbers and Booleans
11.2 Soundness
Chapter 12: Simply Typed ISWIM
12.1 Function Types
12.2 Type Rules for Simply Typed ISWIM
12.3 Soundness
12.4 Normalization
Chapter 13: Variations on Simply Typed ISWIM
13.1 Conditionals
13.2 Pairs
13.3 Variants
13.4 Recursion
Chapter 14: Polymorphism
14.1 Polymorphic ISWIM
Chapter 15: Type Inference
15.1 Type-Inferred ISWIM
15.1.1 Constraint Generation
15.1.2 Unification
15.2 Inferring Polymorphism
Chapter 16: Recursive Types
16.1 Fixed-points of Type Abstractions
16.2 Equality Between Recursive Types
16.3 Isomorphisms Between Recursive Types
16.4 Using Iso-Recursive Types
Chapter 17: Data Abstraction and Existential Types
17.1 Data Abstraction in Clients
17.2 Libraries that Enforce Abstraction
17.3 Existential ISWIM
17.4 Modules and Existential Types
Chapter 18: Subtyping
18.1 Records and Subtypes
18.2 Subtypes and Functions
18.3 Subtypes and Fields
18.4 From Records to Objects
Chapter 19: Objects and Classes
19.1 MiniJava Syntax
19.2 MiniJava Evaluation
19.3 MiniJava Type Checking
19.4 MiniJava Soundness
19.5 MiniJava Summary
IV Appendices
Appendix 20: Structural Induction
20.1 Detecting the Need for Structural Induction
20.2 Definitions with Ellipses
20.3 Induction on Proof Trees
20.4 Multiple Structures
20.5 More Definitions and More Proofs
Programming Languages and Lambda Calculi
(Summer 2006 Revised Version)
Matthias Felleisen Matthew Flatt
Draft: July 12, 2006
Copyright c1989, 2003, 2006 Felleisen, Flatt
2
Contents
I Models of Languages
9
Chapter 1: Computing with Text
11
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.1 Defining Sets
1.2 Relations
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.3 Relations as Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
1.4 Directed Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
1.5 Evaluation in Context . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.6 Evaluation Function . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
1.7 Notation Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
Chapter 2: Consistency of Evaluation
17
Chapter 3: The λ-Calculus
21
3.1 Functions in the λ-Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
3.2 λ-Calculus Grammar and Reductions . . . . . . . . . . . . . . . . . . . . . . . . . 22
3.3 Encoding Booleans . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
3.4 Encoding Pairs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
3.5 Encoding Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
3.6 Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3.6.1 Recursion via Self-Application . . . . . . . . . . . . . . . . . . . . . . . . 28
3.6.2 Lifting Out Self-Application . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3.6.3 Fixed Points and the Y Combinator
. . . . . . . . . . . . . . . . . . . . . 30
3.7 Reduction Strategy and Normal Form . . . . . . . . . . . . . . . . . . . . . . . . 31
3.8 History . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
II Models of Realistic Languages
35
Chapter 4: ISWIM
37
ISWIM Expressions
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4.1
ISWIM Reductions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
4.2
4.3 The Yv Combinator
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
4.4 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
4.5 Consistency . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
4.6 Observational Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
4.7 History . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
Chapter 5: Standard Reduction
49
5.1 Standard Reductions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
5.2 Proving the Standard Reduction Theorem . . . . . . . . . . . . . . . . . . . . . . 52
5.3 Observational Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
3
4
5.4 Uniform Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
Chapter 6: Machines
65
6.1 CC Machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
6.2 SCC Machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
6.3 CK Machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
6.4 CEK Machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
6.5 Machine Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
Chapter 7: SECD, Tail Calls, and Safe for Space
79
7.1 SECD machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
7.2 Context Space
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
7.3 Environment Space . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
7.4 History . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
Chapter 8: Continuations
85
8.1 Saving Contexts
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
8.2 Revised Texual Machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
8.3 Revised CEK Machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
Chapter 9: Errors and Exceptions
89
9.1 Errors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
9.1.1 Calculating with Error ISWIM . . . . . . . . . . . . . . . . . . . . . . . . 89
9.1.2 Consistency for Error ISWIM . . . . . . . . . . . . . . . . . . . . . . . . . 91
9.1.3
Standard Reduction for Error ISWIM . . . . . . . . . . . . . . . . . . . . 94
9.1.4 Relating ISWIM and Error ISWIM . . . . . . . . . . . . . . . . . . . . . . 95
9.2 Exceptions and Handlers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
9.2.1 Calculating with Handler ISWIM . . . . . . . . . . . . . . . . . . . . . . . 99
9.2.2 Consistency for Handler ISWIM . . . . . . . . . . . . . . . . . . . . . . . 100
9.2.3
Standard Reduction for Handler ISWIM . . . . . . . . . . . . . . . . . . . 101
9.2.4 Observational Equivalence of Handler ISWIM . . . . . . . . . . . . . . . . 102
9.3 Machines for Exceptions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
9.3.1 The Handler-Extended CC Machine . . . . . . . . . . . . . . . . . . . . . 103
9.3.2 The CCH Machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104
Chapter 10: Imperative Assignment
107
10.1 Evaluation with State . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
10.2 Garbage Collection . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110
10.3 CEKS Machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112
10.4 Implementing Garbage Collection . . . . . . . . . . . . . . . . . . . . . . . . . . . 113
10.5 History . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
III Models of Typed Languages
115
Chapter 11: Types
117
11.1 Numbers and Booleans . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118
11.2 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120
5
Chapter 12: Simply Typed ISWIM
123
12.1 Function Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123
12.2 Type Rules for Simply Typed ISWIM . . . . . . . . . . . . . . . . . . . . . . . . 124
12.3 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126
12.4 Normalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127
Chapter 13: Variations on Simply Typed ISWIM
131
13.1 Conditionals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131
13.2 Pairs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132
13.3 Variants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133
13.4 Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134
Chapter 14: Polymorphism
137
14.1 Polymorphic ISWIM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137
Chapter 15: Type Inference
141
15.1 Type-Inferred ISWIM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141
15.1.1 Constraint Generation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142
15.1.2 Unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 143
15.2 Inferring Polymorphism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145
Chapter 16: Recursive Types
147
16.1 Fixed-points of Type Abstractions
. . . . . . . . . . . . . . . . . . . . . . . . . . 147
16.2 Equality Between Recursive Types . . . . . . . . . . . . . . . . . . . . . . . . . . 148
16.3 Isomorphisms Between Recursive Types . . . . . . . . . . . . . . . . . . . . . . . 149
16.4 Using Iso-Recursive Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 150
Chapter 17: Data Abstraction and Existential Types
153
17.1 Data Abstraction in Clients . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153
17.2 Libraries that Enforce Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . 154
17.3 Existential ISWIM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155
17.4 Modules and Existential Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157
Chapter 18: Subtyping
159
18.1 Records and Subtypes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 159
18.2 Subtypes and Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162
18.3 Subtypes and Fields
18.4 From Records to Objects
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162
Chapter 19: Objects and Classes
165
19.1 MiniJava Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165
19.2 MiniJava Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 168
19.3 MiniJava Type Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169
19.4 MiniJava Soundness
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 171
19.5 MiniJava Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177
IV Appendices
181
Appendix 20: Structural Induction
183
20.1 Detecting the Need for Structural Induction . . . . . . . . . . . . . . . . . . . . . 183
20.2 Definitions with Ellipses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185
20.3 Induction on Proof Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185
6
20.4 Multiple Structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 186
20.5 More Definitions and More Proofs
. . . . . . . . . . . . . . . . . . . . . . . . . . 187
Preface
These notes are a work in progress, but you may find them useful.
7
8
相关推荐
2023年江西萍乡中考道德与法治真题及答案.doc
2012年重庆南川中考生物真题及答案.doc
2013年江西师范大学地理学综合及文艺理论基础考研真题.doc
2020年四川甘孜小升初语文真题及答案I卷.doc
2020年注册岩土工程师专业基础考试真题及答案.doc
2023-2024学年福建省厦门市九年级上学期数学月考试题及答案.doc
2021-2022学年辽宁省沈阳市大东区九年级上学期语文期末试题及答案.doc
2022-2023学年北京东城区初三第一学期物理期末试卷及答案.doc
2018上半年江西教师资格初中地理学科知识与教学能力真题及答案.doc
2012年河北国家公务员申论考试真题及答案-省级.doc
2020-2021学年江苏省扬州市江都区邵樊片九年级上学期数学第一次质量检测试题及答案.doc
2022下半年黑龙江教师资格证中学综合素质真题及答案.doc
