Cartesian Closed Categories 與簡單型別論 (二)

型別理論

簡單型別（simple type theory）由一部份的 lambda term 以及函數型別構成，我們先從基本的名稱開始講起。

Cartesian Closed Categories 與簡單型別論 (一)

介紹

範疇論對理論電腦科學影響重大，其中一個應用提供各種型別理論（複數以上 type theories）的模型語意。為了解釋這兩者之間的關係，我們以 simply-typed lambda calculus $\lambda_\to$（或簡稱 simple type theory、STT）為例，討論其範疇上的詮釋。在 STT 中只討論最基本的函數型別（function type）以及變數型別，具體來看是非常簡單的函數式語言，型別系統只負責處理 function application 是否合適。

這題材預計分做兩篇，首先解釋 Cartesian closed category （簡稱 CCC）跟 simply typed lambda calculus 的定義跟基本性質，接著談論如何聯繫 CCC 與 simply typed lambda calculus 兩者。