现代类型论的发展与应用

图书标准信息

• 作者 （英）罗朝晖
• 出版社 清华大学出版社
• 出版时间 2024-04
• 版次 1
• ISBN 9787302660354
• 定价 68.00元
• 装帧 其他
• 开本 16开
• 页数 213页

【内容简介】

本书是关于现代类型论的专著。与集合论类似，现代类型论是数学及诸多领域的 
基础语言。本书介绍了现代类型论(及其元理论)，并以自然语言语义学和计算机辅助 
推理为例对以现代类型论为基础的应用领域进行深入浅出的讨论。作为基础语言，现 
代类型论一方面提供了丰富的描述机制，另一方面便于理解与实现，因此与集合论相 
比有着多方面的优势。这些优点在实际运用中展示出来：作为范例，书中深入研究了 
基于现代类型论的自然语言语义学，以加深读者对此的理解。书中还介绍了以现代类 
型论为基础的交互式证明技术在数学形式化、计算机程序验证及自然语言推理诸方面 
的应用，进一步展示了使用现代类型论作为基础语言的优势。 

本书适合研究自然语言语义学、计算机科学和逻辑学等领域的学者及研究生和 
对相关内容感兴趣的读者。

【作者简介】

:
    罗朝晖，现为伦敦大学皇家霍洛威学院计算机系教授，曾就读于国防科技大学，于1990年在英国爱丁堡大学获博士学位，之后在爱丁堡大学、杜伦大学和伦敦大学就职，毕其一生精力研究现代类型论及其应用，是该领域的学术带头人之一，取得了卓越的研究成果，原创作品包括研究统一类型论的《计算与推理》（1994年由牛津大学出版社出版）和研究自然语言语义学的《基于现代类型论的形式语义学》（2020年由Wiley出版社出版）。本书是作者将多年的研究成果精选后写成的中文专著，它的出版将有效地推动国内逻辑学、计算机科学、自然语言语义学及有关交叉领域的进一步发展。

【目录】

章现代类型论及其应用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.1prop：逻辑命题的非直谓类型空间27

2.4.2直谓类型空间及其描述方式29

2.4.3类型空间应用举例33

……