2009年11月11日下午，伦敦大学皇家霍洛威学院计算机科学系罗朝晖教授应邀请来我中心作了题为“Type-Theoretical Semantics with Coercive Subtyping” 的报告。

罗教授首先简要地介绍了类型论：在定义类型的时候，包含了计算，即在判定一个元素是否属于一个类型时，可以通过计算它的值是否恰是该类型中的某个最简元素。如同集合在集合论中的那样基本，类型在数学中是很基本的概念。类型论有着许多良好的性质，例如正常化（可判定性+一致性）、Subject Reduction、Church-Rosser 等等。类型论的方法已经被应用证明工具上，例如 ALF/Agda、Coq、Lego/Plastic、Matita、NuPRL 等等。

随后罗教授重点介绍了他的工作，Coercive Subtyping 理论及其在自然语言研究中的应用，并对比了其他的语义学方法，例如蒙太古语法。蒙太古语法把通名和动词都解释为实体上的函数子集，形容词则被解释为子集到子集的函数。类型论方法则把通名看做是类型，动词和形容词看作是函数子集，被形容词修饰着的通名则解释为Sigma 类型。为了处理蒙太古语法中的困难：被形容词修饰的通名和无修饰的通名之间的关系，罗教授引入了coersive subtyping 的概念，构造从 sigma 类型到类型之间的同构嵌入。Coersive Subtyping 的方法在给出一个好的类型论语义时作用至关重大，而在词汇语义学中也能够良好地模拟许多词汇现象。（陈星群）