掃一掃
關注中圖網
官方微博
本類五星書更多>
-
>
全國計算機等級考試最新真考題庫模擬考場及詳解·二級MSOffice高級應用
-
>
決戰行測5000題(言語理解與表達)
-
>
軟件性能測試.分析與調優實踐之路
-
>
第一行代碼Android
-
>
JAVA持續交付
-
>
EXCEL最強教科書(完全版)(全彩印刷)
-
>
深度學習
現代類型論的發展與應用 版權信息
- ISBN：9787302660354
- 條形碼：9787302660354 ; 978-7-302-66035-4
- 裝幀：平裝-膠訂
- 冊數：暫無
- 重量：暫無
- 所屬分類：>
現代類型論的發展與應用 本書特色
本書作者是現代類型論的**專家及國際學術帶頭人。此書基于作者多年的研究成果，深度介紹現代類型論，闡述其理論，應用及發展前景。目前尚無關于現代類型論和以此為基礎的自然語言語義學的中文專著，此書的出版將進一步推動計算機科學及人工智能在各領域更廣泛的應用。
現代類型論的發展與應用 內容簡介
本書是關于現代類型論的專著。與集合論類似，現代類型論是數學及諸多領域的 基礎語言。本書介紹了現代類型論(及其元理論)，并以自然語言語義學和計算機輔助 推理為例對以現代類型論為基礎的應用領域進行深入淺出的討論。作為基礎語言，現 代類型論一方面提供了豐富的描述機制，另一方面便于理解與實現，因此與集合論相 比有著多方面的優勢。這些優點在實際運用中展示出來：作為范例，書中深入研究了 基于現代類型論的自然語言語義學，以加深讀者對此的理解。書中還介紹了以現代類 型論為基礎的交互式證明技術在數學形式化、計算機程序驗證及自然語言推理諸方面 的應用，進一步展示了使用現代類型論作為基礎語言的優勢。 本書適合研究自然語言語義學、計算機科學和邏輯學等領域的學者及研究生和 對相關內容感興趣的讀者。
現代類型論的發展與應用 目錄
第1 章 現代類型論及其應用 1
1.1 簡單類型論與現代類型論發展概述 1
1.2 現代類型論概論及特點綜述. 4
1.2.1 基本概念概述 4
1.2.2 現代類型論的特點及其與其他形式系統的區別 6
1.3 現代類型論的若干應用和本書概述 9
第2 章 現代類型論 12
2.1 判斷、上下文及定義性等式 12
2.2 類型構造算子 15
2.2.1 函數的依賴類型（Π 類型） 15
2.2.2 序對的依賴類型（Σ 類型） 17
2.2.3 不相交并類型 20
2.2.4 有窮類型 21
2.3 歸納、遞歸及計算理論. 22
2.3.1 自然數類型 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 章 基于現代類型論的自然語言語義學 49
3.1 形式語義學的基礎語言 50
3.2 蒙太古語義學 52
3.3 MTT 語義學：概述及特征. 55
3.3.1 MTT 語義學發展簡史. 55
3.3.2 MTT 語義學簡例. 57
3.3.3 豐富的類型結構：通名的類型語義、選擇限制及其他. 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 關于時態形容詞的討論 79
3.5 證明無關性及關于回指語義的說明 80
3.5.1 證明無關性及其在MTT 語義學中的重要性 80
3.5.2 關于驢句及回指語義的討論 82
3.6 后記 87
第4 章 現代類型論的擴充及語義學研究 89
4.1 標記：類型論的語境描述機制 90
4.1.1 標記：常量的描述機制 90
4.1.2 標記的引入及語境的描述 92
4.1.3 標記中的子類型條目及定義性條目 93
4.2 同謂現象及其點類型語義 96
4.2.1 同謂現象 96
4.2.2 點類型的形式化及同謂現象的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 事件語義學、它的優勢及有關問題 114
4.4.2 依賴事件類型（I）：簡單類型論的擴充 116
4.4.3 依賴事件類型（II）：MTT 事件語義學 119
4.5 依賴性范疇語法 123
4.5.1 依賴性子結構類型論 124
4.5.2 語法分析的例子 126
4.6 后記 128
第5 章 基于現代類型論的交互式推理 129
5.1 現代類型論與交互式證明系統 129
5.2 程序規范與驗證 132
5.2.1 命令式程序及其規范的形式化及驗證 132
5.2.2 類型論中函數式程序的規范及驗證 136
5.2.3 程序的模塊化開發及驗證 137
5.3 自然語言語義的形式化及推理 142
5.3.1 在Coq 中實現MTT 語義學 142
5.3.2 形容詞修飾語義 143
5.3.3 Most 和驢句的語義 145
5.3.4 MTT 事件語義學 146
5.4 后記 149
第6 章 現代類型論的元理論 150
6.1 元理論諸重要性質概述 150
6.1.1 與上下文有關的元理論性質 151
6.1.2 有關計算的重要性質 151
6.2 邏輯框架與歸納模式 154
6.2.1 邏輯框架LF 154
6.2.2 用LF 定義類型論 156
6.2.3 歸納模式 159
6.3 現代類型論的形式化描述及元理論研究. 161
6.3.1 統一類型論（UTT） 161
6.3.2 強制性子類型理論 166
6.3.3 標記類型論 170
6.4 關于意義理論的討論 174
6.5 后記 175
結語 176
附錄A 有關上下文和定義性等式的推理規則 177
附錄B 類型構造算子的推理規則 178
B.1 Π 類型 178
B.2 Σ 類型 179
B.3 不相交并類型 179
B.4 有窮類型. 180
B.5 自然數類型、列表類型和向量類型 181
附錄C Prop 及邏輯算子 185
C.1 Prop. 185
C.2 邏輯算符 186
附錄D 簡單類型論 187
D.1 的推理規則 187
D.2 中的邏輯運算符 188
附錄E 依賴性子結構類型論 189
參考文獻. 192
索引. 206
1.1 簡單類型論與現代類型論發展概述 1
1.2 現代類型論概論及特點綜述. 4
1.2.1 基本概念概述 4
1.2.2 現代類型論的特點及其與其他形式系統的區別 6
1.3 現代類型論的若干應用和本書概述 9
第2 章 現代類型論 12
2.1 判斷、上下文及定義性等式 12
2.2 類型構造算子 15
2.2.1 函數的依賴類型（Π 類型） 15
2.2.2 序對的依賴類型（Σ 類型） 17
2.2.3 不相交并類型 20
2.2.4 有窮類型 21
2.3 歸納、遞歸及計算理論. 22
2.3.1 自然數類型 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 章 基于現代類型論的自然語言語義學 49
3.1 形式語義學的基礎語言 50
3.2 蒙太古語義學 52
3.3 MTT 語義學：概述及特征. 55
3.3.1 MTT 語義學發展簡史. 55
3.3.2 MTT 語義學簡例. 57
3.3.3 豐富的類型結構：通名的類型語義、選擇限制及其他. 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 關于時態形容詞的討論 79
3.5 證明無關性及關于回指語義的說明 80
3.5.1 證明無關性及其在MTT 語義學中的重要性 80
3.5.2 關于驢句及回指語義的討論 82
3.6 后記 87
第4 章 現代類型論的擴充及語義學研究 89
4.1 標記：類型論的語境描述機制 90
4.1.1 標記：常量的描述機制 90
4.1.2 標記的引入及語境的描述 92
4.1.3 標記中的子類型條目及定義性條目 93
4.2 同謂現象及其點類型語義 96
4.2.1 同謂現象 96
4.2.2 點類型的形式化及同謂現象的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 事件語義學、它的優勢及有關問題 114
4.4.2 依賴事件類型（I）：簡單類型論的擴充 116
4.4.3 依賴事件類型（II）：MTT 事件語義學 119
4.5 依賴性范疇語法 123
4.5.1 依賴性子結構類型論 124
4.5.2 語法分析的例子 126
4.6 后記 128
第5 章 基于現代類型論的交互式推理 129
5.1 現代類型論與交互式證明系統 129
5.2 程序規范與驗證 132
5.2.1 命令式程序及其規范的形式化及驗證 132
5.2.2 類型論中函數式程序的規范及驗證 136
5.2.3 程序的模塊化開發及驗證 137
5.3 自然語言語義的形式化及推理 142
5.3.1 在Coq 中實現MTT 語義學 142
5.3.2 形容詞修飾語義 143
5.3.3 Most 和驢句的語義 145
5.3.4 MTT 事件語義學 146
5.4 后記 149
第6 章 現代類型論的元理論 150
6.1 元理論諸重要性質概述 150
6.1.1 與上下文有關的元理論性質 151
6.1.2 有關計算的重要性質 151
6.2 邏輯框架與歸納模式 154
6.2.1 邏輯框架LF 154
6.2.2 用LF 定義類型論 156
6.2.3 歸納模式 159
6.3 現代類型論的形式化描述及元理論研究. 161
6.3.1 統一類型論（UTT） 161
6.3.2 強制性子類型理論 166
6.3.3 標記類型論 170
6.4 關于意義理論的討論 174
6.5 后記 175
結語 176
附錄A 有關上下文和定義性等式的推理規則 177
附錄B 類型構造算子的推理規則 178
B.1 Π 類型 178
B.2 Σ 類型 179
B.3 不相交并類型 179
B.4 有窮類型. 180
B.5 自然數類型、列表類型和向量類型 181
附錄C Prop 及邏輯算子 185
C.1 Prop. 185
C.2 邏輯算符 186
附錄D 簡單類型論 187
D.1 的推理規則 187
D.2 中的邏輯運算符 188
附錄E 依賴性子結構類型論 189
參考文獻. 192
索引. 206
展開全部
現代類型論的發展與應用 作者簡介
羅朝暉，現為倫敦大學皇家霍洛威學院計算機系教授，曾就讀于國防科技大學，于1990年在英國愛丁堡大學獲博士學位，之后在愛丁堡大學、杜倫大學和倫敦大學就職，畢其一生精力研究現代類型論及其應用，是該領域的學術帶頭人之一，取得了卓越的研究成果，原創作品包括研究統一類型論的《計算與推理》（1994年由牛津大學出版社出版）和研究自然語言語義學的《基于現代類型論的形式語義學》（2020年由Wiley出版社出版）。本書是作者將多年的研究成果精選后寫成的中文專著，它的出版將有效地推動國內邏輯學、計算機科學、自然語言語義學及有關交叉領域的進一步發展。
書友推薦
- >
山海經
- >
大紅狗在馬戲團-大紅狗克里弗-助人
- >
史學評論
- >
羅庸西南聯大授課錄
- >
朝聞道
- >
李白與唐代文化
- >
伊索寓言-世界文學名著典藏-全譯本
- >
經典常談
本類暢銷
