本網訊（通訊員時尚）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的共性和區别體現在哪些方面。羅教授表示不同的類型論其實共性更多，區别體現在具體的研究問題。交流環節中羅教授也提到類型論是一個不斷發展的充滿活力的學科，近些年也解決了許多新的問題、産生了許多新的積極結果。

（編輯：鄧莉萍  審稿：劉慧）