本网讯（通讯员时尚）5月8日晚，伦敦大学皇家霍洛威学院罗朝晖教授通过线上方式作了题为“现代类型论及其应用”的讲座。罗朝晖教授毕其一生精力研究现代类型论及其应用，是该领域的学术带头人之一。本次讲座由我院程勇教授主持，皖西学院石运宝副教授评议，线上参与者达500余人次。

讲座分为两部分，第一部分是关于现代类型论的发展历史、基本构成的简要介绍，第二部分是现代类型论的两个应用。

在第一部分，罗朝晖教授首先介绍了现代类型论(Modern Type Theory)的起源及其元理论等内容。现代类型论起源于对集合论中悖论的研究。为了解决这些悖论，Russell创立了分支类型论(Ramified type theory)，Ramsey等人将其简化创立了简单类型论(Simple type theory)。20世纪后半叶Martin-Löf引入了”judgements”等全新的概念，开创了现代类型论。之后罗朝晖教授介绍了类型论中的一些基础概念，讲解了依赖类型(dependent types)等例子助于观众理解，以及类型论中“命题即类型”原则(proposition-as-types)的含义——“一个命题由它的证明构成的类型所决定”。然后罗教授阐释了类型论与集合论在逻辑层面的区别：公理集合论实际上是一阶逻辑的一个理论；类型论并不是一种逻辑的理论，它本身便是一种自然的推理系统，类型论中的“命题”类型对象可以组成逻辑。

接下来罗朝晖教授介绍了类型论的元理论。类型论的元理论都是非常复杂的，会包含大量的定理，这使得元理论的研究难度很大。通过使用ZFC作为元语言我们可以证明类型论的一致性，Caveat等逻辑学家提出是否可以不使用集合论而直接证明其一致性，因此创立了意义论(theories of meaning)。罗朝晖教授介绍了在不同哲学观点下提出的不同的意义论。然后罗朝晖教授展示了类型论和计算机科学的联系。很多“Proof assistants”都是基于类型论研发的，研究者们通过使用“Proof assistants”解决了如“四色定理”等数学和计算机科学中的问题。

在第二部分，罗朝晖教授主要介绍了类型论的两个应用——“单价基础与同伦类型论”和“现代类型论语义学”。学者们利用类型论解决了很多数学、逻辑中的问题，在应用的过程中也对类型论有了更多的理解。一百多年来数学家都是把集合论视为标准的数学基础理论，“单价基础”(univalent foundations)是一种新的理论。单价基础最早由俄国数学家、菲尔兹奖得主Voevodsky在2005年左右研究。Voevodsky的主要思想有三条：一、证明应该可以被验证；二、集胚(groupoid)概念是研究高维数学的合适工具；三、使用类型论来描述集胚。现代类型论语义学是一种区别与传统的蒙太古语义、基于现代类型论的语义学。它的产生是因为很多学者认识到，丰富的类型结构有助于我们描述自然语言。之后罗朝晖教授通过一些例子讲解了现代类型论语义的构成、描述的能力、子类型的概念等等。

在评论互动环节，石运宝副教授作了简要的总结和评论，并提问“同伦类型论是否可以归为现代类型论”。罗教授给出了肯定的回答，表示现代类型论可以理解为区分于简单类型论的类型论。之后程勇教授提问不同的类型论以及不同的proof assistant的共性和区别体现在哪些方面。罗教授表示不同的类型论其实共性更多，区别体现在具体的研究问题。交流环节中罗教授也提到类型论是一个不断发展的充满活力的学科，近些年也解决了许多新的问题、产生了许多新的积极结果。

（编辑：邓莉萍  审稿：刘慧）