實用編程語言理論基礎（原書第2版）

第一部分判斷和規則
第1章抽象語法 2
1.1抽象語法樹 2
1.2抽象綁定樹 4
1.3注記 8
習題 8
第2章歸納定義 10
2.1判斷 10
2.2推理規則 10
2.3推導 11
2.4規則歸納 13
2.5反覆運算歸納定義和聯立歸納定義 14
2.6用規則定義函數 15
2.7注記 15
習題 16
第3章假言判斷與一般性判斷 17
3.1假言判斷 17
3.1.1可導性 17
3.1.2可納性 18
3.2假言歸納定義 20
3.3一般性判斷 21
3.4泛型歸納定義 22
3.5注記 23
習題 23
 
第二部分靜態語義和動態語義
第4章靜態語義 28
4.1語法 28
4.2類型系統 29
4.3結構性質 30
4.4注記 31
習題 31
第5章動態語義 33
5.1轉換系統 33
5.2結構化動態語義 34
5.3上下文動態語義 36
5.4等式動態語義 37
5.5注記 39
習題 39
第6章類型安全 40
6.1保持性 40
6.2進展性 41
6.3執行階段錯誤 42
6.4注記 43
習題 43
第7章求值動態語義 44
7.1求值動態語義 44
7.2結構化動態語義和求值動態語義的關係 45
7.3重溫類型安全 45
7.4成本動態語義 46
7.5注記 47
習題 47
 
第三部分全函數
第8章函式定義和值 50
8.1一階函數 50
8.2高階函數 51
8.3求值動態語義和定義等同 53
8.4動態作用域 54
8.5注記 55
習題 55
第9章高階遞迴的系統T 56
9.1靜態語義 56
9.2動態語義 57
9.3可定義性 58
9.4不可定義性 59
9.5注記 61
習題 61
 
第四部分有限資料類型
第10章積類型 64
10.1空積與二元積 64
10.2有限積 65
10.3原始互遞迴 66
10.4注記 67
習題 67
第11章和類型 69
11.1空和與二元和 69
11.2有限和 70
11.3和類型的應用 71
11.3.1void和unit 71
11.3.2布林類型 72
11.3.3枚舉 72
11.3.4選擇 73
11.4注記 74
習題 74
 
第五部分類型和命題
第12章構造邏輯 78
12.1構造語義 78
12.2構造邏輯 79
12.2.1可證性 79
12.2.2證明項 81
12.3證明的動態語義 82
12.4命題即類型 83
12.5注記 83
習題 83
第13章經典邏輯 85
13.1經典邏輯 85
13.1.1可證性和可反駁性 86
13.1.2證明和反駁 87
13.2推導消去形式 89
13.3證明的動態語義 90
13.4排中律 91
13.5雙重否定翻譯 92
13.6注記 93
習題 94
 
第六部分無限資料類型
第14章泛型程式設計 96
14.1引言 96
14.2多項式類型運算元 96
14.3正類型運算元 98
14.4注記 99
習題 99
第15章歸納類型與餘歸納類型 101
15.1示例 101
15.2靜態語義 104
15.2.1類型 104
15.2.2運算式 105
15.3動態語義 105
15.4求解類型等式 106
15.5注記 107
習題 107
 
第七部分變數類型
第16章多態類型的系統F 110
16.1多態抽象 110
16.2多態的可定義性 113
16.2.1積與和 113
16.2.2自然數 114
16.3參數化概述 115
16.4注記 116
習題 116
第17章抽象類別型 117
17.1存在類型 117
17.1.1靜態語義 118
17.1.2動態語義 118
17.1.3安全性 118
17.2資料抽象 119
17.3存在類型的可定義性 120
17.4表示獨立性 120
17.5注記 122
習題 122
第18章高階種類 123
18.1構造器和種類 123
18.2構造器等同 125
18.3運算式和類型 126
18.4注記 126
習題 127
 
第八部分部分性和遞迴類型
第19章遞迴函數的系統PCF 130
19.1靜態語義 131
19.2動態語義 132
19.3可定義性 133
19.4有限資料結構和無限資料結構 135
19.5 性與部分性 135
19.6注記 136
習題 136
第20章遞迴類型的系統FPC 138
20.1求解類型等式 138
20.2歸納類型和餘歸納類型 139
20.3自指/自引用 141
20.4狀態的起源 142
20.5注記 143
習題 143
 
第九部分動態類型
第21章無類型的λ演算 146
21.1λ演算 146
21.2可定義性 147
21.3Scott定理 149
21.4無類型意味著單類型 150
21.5注記 151
習題 151
第22章動態定型 153
22.1動態類型化PCF 153
22.2變體和擴展 156
22.3動態定型的批判 158
22.4注記 158
習題 159
第23章混合定型 160
23.1一個混合語言 160
23.2動態語義作為靜態定型 162
23.3動態定型的優化 162
23.4靜態定型和動態定型的對比 164
23.5注記 165
習題 165
 
第十部分子定型
第24章結構化子定型 168
24.1包含規則 168
24.2各種子定型 169
24.2.1數數值型別 169
24.2.2積類型 169
24.2.3和類型 170
24.2.4動態類型 170
24.3變體 171
24.3.1積類型與和類型 171
24.3.2部分函數類型 171
24.3.3遞迴類型 172
24.3.4量化類型 173
24.4動態語義和安全性 174
24.5注記 175
習題 176
第25章行為定型 177
25.1靜態語義 177
25.2布林盲 183
25.3細化的安全性 184
25.4注記 185
習題 186
 
第十一部分動態分派
第26章類與方法 188
26.1分派矩陣 188
26.2基於類的組織 190
26.3基於方法的組織 191
26.4自指 192
26.5注記 194
習題 194
第27章繼承 196
27.1類與方法擴展 196
27.2基於類的繼承 197
27.3基於方法的繼承 198
27.4注記 198
習題 199
 
第十二部分控制流
第28章控制棧 202
28.1機器定義 202
28.2安全性 203
28.3機器K的正確性 204
28.3.1完備性 205
28.3.2可靠性 205
28.4注記 206
習題 207
第29章異常 208
29.1失敗 208
29.2異常 209
29.3異常值 210
29.4注記 211
習題 211
第30章延續 213
0.1概述 213
30.2延續的動態語義 214
30.3用延續構造協程 216
30.4注記 218
習題 218
 
第十三部分符號資料
第31章符號 222
31.1符號聲明 222
31.1.1有作用域的動態語義 223
31.1.2無作用域的動態語義 224
31.2符號引用 224
31.2.1靜態語義 225
31.2.2動態語義 225
31.2.3安全性 225
31.3注記 226
習題 226
第32章流動綁定 227
32.1 靜態語義 227
32.2動態語義 228
32.3類型安全 229
32.4一些微妙之處 229
32.5流動引用 231
32.6注記 231
習題 232
第33章動態分類 233
33.1動態類 233
33.1.1靜態語義 233
33.1.2動態語義 234
33.1.3安全性 234
33.2類引用 234
33.3動態類的可定義性 235
33.4動態分類的應用 236
33.4.1秘密分類 236
33.4.2異常值 237
33.5注記 237
習題 237
 
第十四部分可變狀態
第34章現代化的Algol 240
34.1基本命令 240
34.1.1靜態語義 241
34.1.2動態語義 241
34.1.3安全性 243
34.2一些程式設計習語 243
34.3類型化的命令和類型化的可賦值對象 245
34.4注記 247
習題 247
第35章可賦值對象的引用 250
35.1能力 250
35.2有作用域的可賦值物件 251
35.3自由的可賦值對象 252
35.4安全性 254
35.5良性效應 256
35.6注記 257
習題 257
第36章惰性求值 258
36.1按需的PCF 258
36.2按需的PCF的安全性 260
36.3按需的FPC 262
36.4懸掛類型 263
36.5注記 264
習題 264
 
第十五部分並行
第37章嵌套並行 268
37.1二叉fork-join 268
37.2成本動態語義 270
37.3多叉fork-join 273
37.4有界實現 274
37.5調度 277
37.6注記 279
習題 279
第38章未來與投機 280
38.1未來 280
38.1.1靜態語義 280
38.1.2順序動態語義 281
38.2投機 281
38.2.1靜態語義 81
38.2.2順序動態語義 282
38.3並行動態語義 282
38.4未來流水線 284
38.5注記 285
習題 285
 
第十六部分併發與分散式
第39章進程演算 288
39.1動作與事件 288
39.2交互 289
39.3複製 291
39.4分配通道 292
39.5通信 294
39.6通道傳遞 296
39.7普適性 297
39.8注記 299
習題 299
第40章併發Algol 301
40.1併發Algol 301
40.2廣播通信 303
40.3選擇性通信 305
40.4自由的可賦值物件作為進程 307
40.5注記 308
習題 308
第41章分散式Algol 309
41.1靜態語義 309
41.2動態語義 312
41.3安全性 313
41.4注記 314
習題 314
 
第十七部分模組化
第42章模組化與連結 316
42.1簡單單元與連結 316
42.2初始化和效果 317
42.3注記 318
第43章單例種類和子種類 319
43.1概述 319
43.2單例 320
43.3依賴種類 322
43.4高階單例 324
43.5注記 325
習題 326
第44章類型抽象與類型類 327
44.1類型抽象 328
44.2類型類 329
44.3模組語言 331
44.4一等模組和二等模組 334
44.5注記 335
習題 335
第45章層次結構和參數化 337
45.1層次結構 337
45.2抽象 339
45.3層次結構和抽象 341
45.4應用函子 343
45.5注記 344
習題 344
 
第十八部分等式推理
第46章系統T的相等性 346
46.1觀測等價 346
46.2邏輯等價 349
46.3邏輯等價和觀測等價重合 350
46.4一些相等性定律 352
46.4.1一般定律 352
46.4.2相等性定律 353
46.4.3歸納定律 353
46.5注記 353
第47章系統PCF的相等性 354
47.1觀測等價 354
47.2邏輯等價 354
47.3邏輯等價和觀測等價重合 355
47.4緊致性 357
47.5惰性自然數 360
47.6注記 361
第48章參數化 362
48.1概述 362
48.2觀測等價 362
48.3邏輯等價 364
48.4參數化性質 368
48.5重溫表示獨立性 370
48.6注記 371
第49章進程等價 372
49.1進程演算372
49.2強等價 374
49.3弱等價 376
49.4注記 377
 
附錄A有限集的背景 378
參考文獻 379