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

第1 章  現(xiàn)代類型論及其應(yīng)用 1
1.1  簡(jiǎn)單類型論與現(xiàn)代類型論發(fā)展概述 1
1.2  現(xiàn)代類型論概論及特點(diǎn)綜述. 4
1.2.1  基本概念概述  4
1.2.2  現(xiàn)代類型論的特點(diǎn)及其與其他形式系統(tǒng)的區(qū)別 6
1.3  現(xiàn)代類型論的若干應(yīng)用和本書概述 9
第2 章  現(xiàn)代類型論 12
2.1  判斷、上下文及定義性等式 12
2.2  類型構(gòu)造算子 15
2.2.1  函數(shù)的依賴類型（Π 類型）  15
2.2.2  序?qū)Φ囊蕾囶愋停?Sigma; 類型）  17
2.2.3  不相交并類型 20
2.2.4  有窮類型 21
2.3  歸納、遞歸及計(jì)算理論. 22
2.3.1  自然數(shù)類型 22
2.3.2  列表類型和向量類型 24
2.4  類型空間 27
2.4.1  Prop：邏輯命題的非直謂類型空間 27
2.4.2  直謂類型空間及其描述方式 29
2.4.3  類型空間應(yīng)用舉例 33
2.5  子類型理論 35
2.5.1  包含性子類型理論及其問題 36
2.5.2  強(qiáng)制性子類型理論 38
2.5.3  子類型類型空間、類型的（不）相交性和依賴性記錄類型   41
2.6  后記.  46
第3 章  基于現(xiàn)代類型論的自然語(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  豐富的類型結(jié)構(gòu)：通名的類型語(yǔ)義、選擇限制及其他.  60
3.3.4  子類型理論在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ǔ)義的說明   80
3.5.1  證明無(wú)關(guān)性及其在MTT 語(yǔ)義學(xué)中的重要性  80
3.5.2  關(guān)于驢句及回指語(yǔ)義的討論 82
3.6  后記   87
第4 章  現(xiàn)代類型論的擴(kuò)充及語(yǔ)義學(xué)研究   89
4.1  標(biāo)記：類型論的語(yǔ)境描述機(jī)制 90
4.1.1  標(biāo)記：常量的描述機(jī)制 90
4.1.2  標(biāo)記的引入及語(yǔ)境的描述 92
4.1.3  標(biāo)記中的子類型條目及定義性條目  93
4.2  同謂現(xiàn)象及其點(diǎn)類型語(yǔ)義 96
4.2.1  同謂現(xiàn)象 96
4.2.2  點(diǎn)類型的形式化及同謂現(xiàn)象的MTT 語(yǔ)義  97
4.2.3  通名的集胚語(yǔ)義：以涉及同謂及量詞的復(fù)雜語(yǔ)境為例 100
4.3  判斷語(yǔ)義的命題形式 104
4.3.1  判斷語(yǔ)義及其命題形式   105
4.3.2  異類等式及判斷語(yǔ)義之命題形式的形式化  108
4.3.3  避免生成過剩.  111
4.4  依賴類型在事件語(yǔ)義學(xué)中的應(yīng)用 113
4.4.1  事件語(yǔ)義學(xué)、它的優(yōu)勢(shì)及有關(guān)問題   114
4.4.2  依賴事件類型（I）：簡(jiǎn)單類型論的擴(kuò)充 116
4.4.3  依賴事件類型（II）：MTT 事件語(yǔ)義學(xué) 119
4.5  依賴性范疇語(yǔ)法 123
4.5.1  依賴性子結(jié)構(gòu)類型論   124
4.5.2  語(yǔ)法分析的例子   126
4.6 后記  128
第5 章  基于現(xiàn)代類型論的交互式推理 129
5.1  現(xiàn)代類型論與交互式證明系統(tǒng)  129
5.2  程序規(guī)范與驗(yàn)證 132
5.2.1  命令式程序及其規(guī)范的形式化及驗(yàn)證  132
5.2.2  類型論中函數(shù)式程序的規(guī)范及驗(yàn)證   136
5.2.3  程序的模塊化開發(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)代類型論的元理論 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 定義類型論  156
6.2.3  歸納模式   159
6.3  現(xiàn)代類型論的形式化描述及元理論研究.  161
6.3.1  統(tǒng)一類型論（UTT）  161
6.3.2  強(qiáng)制性子類型理論  166
6.3.3  標(biāo)記類型論   170
6.4  關(guān)于意義理論的討論 174
6.5  后記  175
結(jié)語(yǔ)   176
附錄A  有關(guān)上下文和定義性等式的推理規(guī)則 177
附錄B  類型構(gòu)造算子的推理規(guī)則   178
B.1   Π 類型  178
B.2   Σ 類型  179
B.3  不相交并類型 179
B.4  有窮類型. 180
B.5  自然數(shù)類型、列表類型和向量類型  181
附錄C  Prop 及邏輯算子   185
C.1  Prop. 185
C.2  邏輯算符  186
附錄D  簡(jiǎn)單類型論   187
D.1   的推理規(guī)則 187
D.2   中的邏輯運(yùn)算符   188
附錄E  依賴性子結(jié)構(gòu)類型論  189
參考文獻(xiàn).  192
索引.  206