現(xiàn)代類(lèi)型論的發(fā)展與應(yīng)用

第1 章  現(xiàn)代類(lèi)型論及其應(yīng)用 1
1.1  簡(jiǎn)單類(lèi)型論與現(xiàn)代類(lèi)型論發(fā)展概述 1
1.2  現(xiàn)代類(lèi)型論概論及特點(diǎn)綜述. 4
1.2.1  基本概念概述  4
1.2.2  現(xiàn)代類(lèi)型論的特點(diǎn)及其與其他形式系統(tǒng)的區(qū)別 6
1.3  現(xiàn)代類(lèi)型論的若干應(yīng)用和本書(shū)概述 9
第2 章  現(xiàn)代類(lèi)型論 12
2.1  判斷、上下文及定義性等式 12
2.2  類(lèi)型構(gòu)造算子 15
2.2.1  函數(shù)的依賴(lài)類(lèi)型（Π 類(lèi)型）  15
2.2.2  序?qū)Φ囊蕾?lài)類(lèi)型（Σ 類(lèi)型）  17
2.2.3  不相交并類(lèi)型 20
2.2.4  有窮類(lèi)型 21
2.3  歸納、遞歸及計(jì)算理論. 22
2.3.1  自然數(shù)類(lèi)型 22
2.3.2  列表類(lèi)型和向量類(lèi)型 24
2.4  類(lèi)型空間 27
2.4.1  Prop：邏輯命題的非直謂類(lèi)型空間 27
2.4.2  直謂類(lèi)型空間及其描述方式 29
2.4.3  類(lèi)型空間應(yīng)用舉例 33
2.5  子類(lèi)型理論 35
2.5.1  包含性子類(lèi)型理論及其問(wèn)題 36
2.5.2  強(qiáng)制性子類(lèi)型理論 38
2.5.3  子類(lèi)型類(lèi)型空間、類(lèi)型的（不）相交性和依賴(lài)性記錄類(lèi)型   41
2.6  后記.  46
第3 章  基于現(xiàn)代類(lèi)型論的自然語(yǔ)言語(yǔ)義學(xué)   49
3.1  形式語(yǔ)義學(xué)的基礎(chǔ)語(yǔ)言  50
3.2  蒙太古語(yǔ)義學(xué)  52
3.3  MTT 語(yǔ)義學(xué)：概述及特征.  55
3.3.1  MTT 語(yǔ)義學(xué)發(fā)展簡(jiǎn)史.  55
3.3.2  MTT 語(yǔ)義學(xué)簡(jiǎn)例.  57
3.3.3  豐富的類(lèi)型結(jié)構(gòu)：通名的類(lèi)型語(yǔ)義、選擇限制及其他.  60
3.3.4  子類(lèi)型理論在MTT 語(yǔ)義學(xué)中的應(yīng)用 64
3.4  形容詞修飾語(yǔ)義的研究. 70
3.4.1  相交形容詞 73
3.4.2  下屬形容詞 74
3.4.3  否定性形容詞 76
3.4.4  非承諾形容詞 78
3.4.5  關(guān)于時(shí)態(tài)形容詞的討論 79
3.5  證明無(wú)關(guān)性及關(guān)于回指語(yǔ)義的說(shuō)明   80
3.5.1  證明無(wú)關(guān)性及其在MTT 語(yǔ)義學(xué)中的重要性  80
3.5.2  關(guān)于驢句及回指語(yǔ)義的討論 82
3.6  后記   87
第4 章  現(xiàn)代類(lèi)型論的擴(kuò)充及語(yǔ)義學(xué)研究   89
4.1  標(biāo)記：類(lèi)型論的語(yǔ)境描述機(jī)制 90
4.1.1  標(biāo)記：常量的描述機(jī)制 90
4.1.2  標(biāo)記的引入及語(yǔ)境的描述 92
4.1.3  標(biāo)記中的子類(lèi)型條目及定義性條目  93
4.2  同謂現(xiàn)象及其點(diǎn)類(lèi)型語(yǔ)義 96
4.2.1  同謂現(xiàn)象 96
4.2.2  點(diǎn)類(lèi)型的形式化及同謂現(xiàn)象的MTT 語(yǔ)義  97
4.2.3  通名的集胚語(yǔ)義：以涉及同謂及量詞的復(fù)雜語(yǔ)境為例 100
4.3  判斷語(yǔ)義的命題形式 104
4.3.1  判斷語(yǔ)義及其命題形式   105
4.3.2  異類(lèi)等式及判斷語(yǔ)義之命題形式的形式化  108
4.3.3  避免生成過(guò)剩.  111
4.4  依賴(lài)類(lèi)型在事件語(yǔ)義學(xué)中的應(yīng)用 113
4.4.1  事件語(yǔ)義學(xué)、它的優(yōu)勢(shì)及有關(guān)問(wèn)題   114
4.4.2  依賴(lài)事件類(lèi)型（I）：簡(jiǎn)單類(lèi)型論的擴(kuò)充 116
4.4.3  依賴(lài)事件類(lèi)型（II）：MTT 事件語(yǔ)義學(xué) 119
4.5  依賴(lài)性范疇語(yǔ)法 123
4.5.1  依賴(lài)性子結(jié)構(gòu)類(lèi)型論   124
4.5.2  語(yǔ)法分析的例子   126
4.6 后記  128
第5 章  基于現(xiàn)代類(lèi)型論的交互式推理 129
5.1  現(xiàn)代類(lèi)型論與交互式證明系統(tǒng)  129
5.2  程序規(guī)范與驗(yàn)證 132
5.2.1  命令式程序及其規(guī)范的形式化及驗(yàn)證  132
5.2.2  類(lèi)型論中函數(shù)式程序的規(guī)范及驗(yàn)證   136
5.2.3  程序的模塊化開(kāi)發(fā)及驗(yàn)證   137
5.3  自然語(yǔ)言語(yǔ)義的形式化及推理  142
5.3.1  在Coq 中實(shí)現(xiàn)MTT 語(yǔ)義學(xué) 142
5.3.2  形容詞修飾語(yǔ)義   143
5.3.3  Most 和驢句的語(yǔ)義 145
5.3.4  MTT 事件語(yǔ)義學(xué)  146
5.4  后記 149
第6 章  現(xiàn)代類(lèi)型論的元理論 150
6.1  元理論諸重要性質(zhì)概述  150
6.1.1  與上下文有關(guān)的元理論性質(zhì)   151
6.1.2  有關(guān)計(jì)算的重要性質(zhì)  151
6.2  邏輯框架與歸納模式 154
6.2.1  邏輯框架LF  154
6.2.2  用LF 定義類(lèi)型論  156
6.2.3  歸納模式   159
6.3  現(xiàn)代類(lèi)型論的形式化描述及元理論研究.  161
6.3.1  統(tǒng)一類(lèi)型論（UTT）  161
6.3.2  強(qiáng)制性子類(lèi)型理論  166
6.3.3  標(biāo)記類(lèi)型論   170
6.4  關(guān)于意義理論的討論 174
6.5  后記  175
結(jié)語(yǔ)   176
附錄A  有關(guān)上下文和定義性等式的推理規(guī)則 177
附錄B  類(lèi)型構(gòu)造算子的推理規(guī)則   178
B.1   Π 類(lèi)型  178
B.2   Σ 類(lèi)型  179
B.3  不相交并類(lèi)型 179
B.4  有窮類(lèi)型. 180
B.5  自然數(shù)類(lèi)型、列表類(lèi)型和向量類(lèi)型  181
附錄C  Prop 及邏輯算子   185
C.1  Prop. 185
C.2  邏輯算符  186
附錄D  簡(jiǎn)單類(lèi)型論   187
D.1   的推理規(guī)則 187
D.2   中的邏輯運(yùn)算符   188
附錄E  依賴(lài)性子結(jié)構(gòu)類(lèi)型論  189
參考文獻(xiàn).  192
索引.  206