扫一扫
关注中图网
官方微博
本类五星书更多>
-
>
全国计算机等级考试最新真考题库模拟考场及详解·二级MSOffice高级应用
-
>
决战行测5000题(言语理解与表达)
-
>
软件性能测试.分析与调优实践之路
-
>
第一行代码Android
-
>
C Primer Plus 第6版 中文版
-
>
深度学习
-
>
MATLAB计算机视觉与深度学习实战-赠在线交流卡和本书源码
现代类型论的发展与应用 版权信息
- 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
展开全部
书友推荐
- >
中国人在乌苏里边疆区:历史与人类学概述
中国人在乌苏里边疆区:历史与人类学概述
¥40.8¥48.0 - >
随园食单
随园食单
¥37.0¥48.0 - >
小考拉的故事-套装共3册
小考拉的故事-套装共3册
¥35.4¥68.0 - >
推拿
推拿
¥12.2¥32.0 - >
诗经-先民的歌唱
诗经-先民的歌唱
¥15.1¥39.8 - >
唐代进士录
唐代进士录
¥26.7¥39.8 - >
企鹅口袋书系列·伟大的思想20:论自然选择(英汉双语)
企鹅口袋书系列·伟大的思想20:论自然选择(英汉双语)
¥8.4¥14.0 - >
人文阅读与收藏·良友文学丛书:一天的工作
人文阅读与收藏·良友文学丛书:一天的工作
¥27.3¥45.8
本类畅销
-
2022图书×抽奖盲袋
¥9.9¥25 -
2023读书月阅读盲盒——天黑，闭眼，刀谁？
¥42.3¥158 -
-
2022读者节纪念徽章-三星会员专属
¥45¥45.6 -
2023读书月阅读盲盒——我什么场面没见过？
¥42.3¥158 -
2023读书月阅读盲盒——去码头整点什么薯条？
¥42.3¥158
浏览历史
儿童护理:::
¥49.0¥68.0恐龙全景图伶盗龙 /恐龙全景图
¥7.7¥18.0鲁班工坊纵览与博观
¥62.4¥86.6基础英语1000词贴纸书
¥22.8¥60.05年级-小学生课堂同步作文专家辅导-适用各版本语文教材
¥7.6¥19.9
