掃一掃
關(guān)注中圖網(wǎng)
官方微博
現(xiàn)代類(lèi)型論的發(fā)展與應(yīng)用
作者：[英]羅朝暉
開(kāi)本：
其他
頁(yè)數(shù)：
213
本類(lèi)榜單：計(jì)算機(jī)/網(wǎng)絡(luò)銷(xiāo)量榜
本類(lèi)五星書(shū)更多>
-
>
決戰(zhàn)行測(cè)5000題(言語(yǔ)理解與表達(dá))
-
>
軟件性能測(cè)試.分析與調(diào)優(yōu)實(shí)踐之路
-
>
第一行代碼Android
-
>
深度學(xué)習(xí)
-
>
Unreal Engine 4藍(lán)圖完全學(xué)習(xí)教程
-
>
深入理解計(jì)算機(jī)系統(tǒng)-原書(shū)第3版
-
>
Word/Excel PPT 2013辦公應(yīng)用從入門(mén)到精通-(附贈(zèng)1DVD.含語(yǔ)音視頻教學(xué)+辦公模板+PDF電子書(shū))
中圖價(jià):¥53.0
加入購(gòu)物車(chē)
現(xiàn)代類(lèi)型論的發(fā)展與應(yīng)用 版權(quán)信息
- ISBN：9787302660354
- 條形碼：9787302660354 ; 978-7-302-66035-4
- 裝幀：平裝-膠訂
- 冊(cè)數(shù)：暫無(wú)
- 重量：暫無(wú)
- 所屬分類(lèi)：>
現(xiàn)代類(lèi)型論的發(fā)展與應(yīng)用 本書(shū)特色
本書(shū)作者是現(xiàn)代類(lèi)型論的**專(zhuān)家及國(guó)際學(xué)術(shù)帶頭人。此書(shū)基于作者多年的研究成果，深度介紹現(xiàn)代類(lèi)型論，闡述其理論，應(yīng)用及發(fā)展前景。目前尚無(wú)關(guān)于現(xiàn)代類(lèi)型論和以此為基礎(chǔ)的自然語(yǔ)言語(yǔ)義學(xué)的中文專(zhuān)著，此書(shū)的出版將進(jìn)一步推動(dòng)計(jì)算機(jī)科學(xué)及人工智能在各領(lǐng)域更廣泛的應(yīng)用。
現(xiàn)代類(lèi)型論的發(fā)展與應(yīng)用 內(nèi)容簡(jiǎn)介
本書(shū)是關(guān)于現(xiàn)代類(lèi)型論的專(zhuān)著。與集合論類(lèi)似，現(xiàn)代類(lèi)型論是數(shù)學(xué)及諸多領(lǐng)域的 基礎(chǔ)語(yǔ)言。本書(shū)介紹了現(xiàn)代類(lèi)型論(及其元理論)，并以自然語(yǔ)言語(yǔ)義學(xué)和計(jì)算機(jī)輔助 推理為例對(duì)以現(xiàn)代類(lèi)型論為基礎(chǔ)的應(yīng)用領(lǐng)域進(jìn)行深入淺出的討論。作為基礎(chǔ)語(yǔ)言，現(xiàn) 代類(lèi)型論一方面提供了豐富的描述機(jī)制，另一方面便于理解與實(shí)現(xiàn)，因此與集合論相 比有著多方面的優(yōu)勢(shì)。這些優(yōu)點(diǎn)在實(shí)際運(yùn)用中展示出來(lái)：作為范例，書(shū)中深入研究了 基于現(xiàn)代類(lèi)型論的自然語(yǔ)言語(yǔ)義學(xué)，以加深讀者對(duì)此的理解。書(shū)中還介紹了以現(xiàn)代類(lèi) 型論為基礎(chǔ)的交互式證明技術(shù)在數(shù)學(xué)形式化、計(jì)算機(jī)程序驗(yàn)證及自然語(yǔ)言推理諸方面 的應(yīng)用，進(jìn)一步展示了使用現(xiàn)代類(lèi)型論作為基礎(chǔ)語(yǔ)言的優(yōu)勢(shì)。 本書(shū)適合研究自然語(yǔ)言語(yǔ)義學(xué)、計(jì)算機(jī)科學(xué)和邏輯學(xué)等領(lǐng)域的學(xué)者及研究生和 對(duì)相關(guān)內(nèi)容感興趣的讀者。
現(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
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
展開(kāi)全部
現(xiàn)代類(lèi)型論的發(fā)展與應(yīng)用 作者簡(jiǎn)介
羅朝暉，現(xiàn)為倫敦大學(xué)皇家霍洛威學(xué)院計(jì)算機(jī)系教授，曾就讀于國(guó)防科技大學(xué)，于1990年在英國(guó)愛(ài)丁堡大學(xué)獲博士學(xué)位，之后在愛(ài)丁堡大學(xué)、杜倫大學(xué)和倫敦大學(xué)就職，畢其一生精力研究現(xiàn)代類(lèi)型論及其應(yīng)用，是該領(lǐng)域的學(xué)術(shù)帶頭人之一，取得了卓越的研究成果，原創(chuàng)作品包括研究統(tǒng)一類(lèi)型論的《計(jì)算與推理》（1994年由牛津大學(xué)出版社出版）和研究自然語(yǔ)言語(yǔ)義學(xué)的《基于現(xiàn)代類(lèi)型論的形式語(yǔ)義學(xué)》（2020年由Wiley出版社出版）。本書(shū)是作者將多年的研究成果精選后寫(xiě)成的中文專(zhuān)著，它的出版將有效地推動(dòng)國(guó)內(nèi)邏輯學(xué)、計(jì)算機(jī)科學(xué)、自然語(yǔ)言語(yǔ)義學(xué)及有關(guān)交叉領(lǐng)域的進(jìn)一步發(fā)展。
書(shū)友推薦
- >
名家?guī)阕x魯迅:朝花夕拾
- >
羅庸西南聯(lián)大授課錄
- >
唐代進(jìn)士錄
- >
煙與鏡
- >
李白與唐代文化
- >
小考拉的故事-套裝共3冊(cè)
- >
莉莉和章魚(yú)
- >
隨園食單
本類(lèi)暢銷(xiāo)
