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