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

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