鏈接：https://pan.baidu.com/s/1t2aWQ7QflYF2lUjNAQNYyA?pwd=ezbf?

提取碼：ezbf

本書提出了一種基于類型系統(tǒng)和結(jié)構(gòu)操作語(yǔ)義的編程語(yǔ)言理論。第2版經(jīng)過(guò)全面修訂，幾乎每章都包含習(xí)題，并新增一章討論類型細(xì)化。本書涉及的概念廣泛，包括：基本數(shù)據(jù)類型，多態(tài)和抽象類型，動(dòng)態(tài)定型，動(dòng)態(tài)分派，子類型和類型細(xì)化，符號(hào)和動(dòng)態(tài)分類，并行和成本語(yǔ)義，并發(fā)和分布。書中對(duì)不同編程語(yǔ)言的特性做了分析、證明和比較，所提供的方法可直接應(yīng)用于語(yǔ)言的實(shí)現(xiàn)、程序推理邏輯的研發(fā)以及語(yǔ)言特性的形式化驗(yàn)證，具有較高的實(shí)用性。本書不僅可以作為高等學(xué)校計(jì)算機(jī)相關(guān)專業(yè)的編程語(yǔ)言理論課程教材，也可供相關(guān)領(lǐng)域的科研人員和技術(shù)人員參考閱讀。

作者簡(jiǎn)介

---作者簡(jiǎn)介---
羅伯特·哈珀(Robert Harper) 卡內(nèi)基·梅隆大學(xué)計(jì)算機(jī)科學(xué)系教授，他的主要研究興趣是類型論在編程語(yǔ)言的設(shè)計(jì)與實(shí)現(xiàn)中的應(yīng)用，以及其元理論的機(jī)械化。Harper是Allen Newell卓越研究獎(jiǎng)?wù)潞虷erbert A. Simon卓越教學(xué)獎(jiǎng)的獲得者，并且是ACM會(huì)士。

---譯者簡(jiǎn)介---
張昱 博士，中國(guó)科學(xué)技術(shù)大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院、網(wǎng)絡(luò)空間安全學(xué)院副教授。研究興趣包括程序設(shè)計(jì)語(yǔ)言、操作系統(tǒng)和并行計(jì)算等，特別是面向人工智能和量子計(jì)算等新領(lǐng)域的編程系統(tǒng)、軟件分析、異構(gòu)計(jì)算與系統(tǒng)優(yōu)化等。

胡明哲 中國(guó)科學(xué)技術(shù)大學(xué)網(wǎng)絡(luò)空間安全學(xué)院博士研究生。主要研究方向?yàn)槎嗾Z(yǔ)言軟件的程序分析。

目錄

譯者序
第2版前言
第1版前言
第一部分　判斷和規(guī)則
第1章　抽象語(yǔ)法 2
1.1　抽象語(yǔ)法樹 2
1.2　抽象綁定樹 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　類型系統(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章　類型安全 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　重溫類型安全 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ù)類型
第10章　積類型 64
10.1　空積與二元積 64
10.2　有限積 65
10.3　原始互遞歸 66
10.4　注記 67
習(xí)題 67
第11章　和類型 69
11.1　空和與二元和 69
11.2　有限和 70
11.3　和類型的應(yīng)用 71
11.3.1　void和unit 71
11.3.2　布爾類型 72
11.3.3　枚舉 72
11.3.4　選擇 73
11.4　注記 74
習(xí)題 74
第五部分　類型和命題
第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　命題即類型 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ù)類型
第14章　泛型編程 96
14.1　引言 96
14.2　多項(xiàng)式類型算子 96
14.3　正類型算子 98
14.4　注記 99
習(xí)題 99
第15章　歸納類型與余歸納類型 101
15.1　示例 101
15.2　靜態(tài)語(yǔ)義 104
15.2.1　類型 104
15.2.2　表達(dá)式 105
15.3　動(dòng)態(tài)語(yǔ)義 105
15.4　求解類型等式 106
15.5　注記 107
習(xí)題 107
第七部分　變量類型
第16章　多態(tà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章　抽象類型 117
17.1　存在類型 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　存在類型的可定義性 120
17.4　表示獨(dú)立性 120
17.5　注記 122
習(xí)題 122
第18章　高階種類 123
18.1　構(gòu)造器和種類 123
18.2　構(gòu)造器等同 125
18.3　表達(dá)式和類型 126
18.4　注記 126
習(xí)題 127
第八部分　部分性和遞歸類型
第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章　遞歸類型的系統(tǒng)FPC 138
20.1　求解類型等式 138
20.2　歸納類型和余歸納類型 139
20.3　自指/自引用 141
20.4　狀態(tài)的起源 142
20.5　注記 143
習(xí)題 143
第九部分　動(dòng)態(tài)類型
第21章　無(wú)類型的λ演算 146
21.1　λ演算 146
21.2　可定義性 147
21.3　Scott定理 149
21.4　無(wú)類型意味著單類型 150
21.5　注記 151
習(xí)題 151
第22章　動(dòng)態(tài)定型 153
22.1　動(dòng)態(tài)類型化PCF 153
22.2　變體和擴(kuò)展 156
22.3　動(dòng)態(tài)定型的批判 158
22.4　

查看全部↓

前言/序言

就像構(gòu)建軟件系統(tǒng)的第2版會(huì)有風(fēng)險(xiǎn)一樣，為教材編寫第2版也會(huì)帶來(lái)風(fēng)險(xiǎn)：很難在避免過(guò)度修改和不破壞原有基礎(chǔ)的情況下做出實(shí)質(zhì)性改進(jìn)。為了避免“第二系統(tǒng)效應(yīng)”，我試圖通過(guò)更正、修訂、擴(kuò)展和刪除來(lái)提高內(nèi)容的一致性，刪除一些偏離主題的話題，增加一些第1版中遺漏的話題，并為每一章引入習(xí)題。
此次修訂刪除了許多印刷錯(cuò)誤，糾正了一些重大錯(cuò)誤（特別是并行抽象機(jī)和Algol并發(fā)性的公式），并改進(jìn)了全書的表述。一些章節(jié)被刪除（一般模式匹配和極化、多態(tài)的受限形式），一些章節(jié)被完全重寫（關(guān)于高階種類的章節(jié)），一些章節(jié)被大幅修改（一般的和參數(shù)化歸納定義、并發(fā)和分布式 Algol），一些章節(jié)被重組（以更好地區(qū)分部分類型論和完全類型論），另外還新增了一章（關(guān)于類型細(xì)化）。本次修訂刪除了一些章節(jié)中對(duì)資料來(lái)源的不清晰引用，以避免混淆這些話題當(dāng)前和原有的表述。全書引入了一套新的(可發(fā)音的）語(yǔ)言名稱系統(tǒng)。習(xí)題試圖擴(kuò)展正文中的思想，而其解答往往涉及值得研究的重要技術(shù)思想。在課后作業(yè)中，盡量不包含按部就班的常規(guī)練習(xí)。
撰寫本書的目的是建立一個(gè)全面闡述和分析編程語(yǔ)言中各種思想的框架。語(yǔ)言設(shè)計(jì)和編程方法要從手工制作發(fā)展到嚴(yán)密的學(xué)科，首先必須要有正確的定義。只有這樣，才能進(jìn)行有意義的分析和整合。我希望能幫助建立這樣的基礎(chǔ)。
感謝Stephen Brookes、Evan Cavallo、Karl Crary、Jon Sterling、James R. Wilcox和Todd Wilson對(duì)本版書稿的評(píng)審，并感謝他們提出的修訂建議。感謝我的系主任Frank Pfenning對(duì)我完成本版工作的支持。還要感謝編輯Ada Brunstein和