Lambda calculus引論(目錄)

前言:

函數式編程作為與編程範式之一有著相當長的歷史, 它的發展伴隨著計算機科學特別是計算理論與語言理論的發展. 函數式編程可以說是編程語言里一個相當重要的領域, 相關的理論成為了各類研究的基石, 這裡為大家介紹函數式編程中最基礎的λ-calculus與類型論等的相關的理論.

這個"引論"系列不是真正準備給零基礎初學者的, 攤手. 叫引論只是因為這一系列的文章主要是基於λ-calculus講解與其相關的最基礎的理論知識. 所以不是對相關領域比較熟悉或有興趣的小夥伴們對不起啦喵. 想要真正入門的小夥伴可以去閱讀一些稍微入門點的材料, 有什麼問題也歡迎隨時來找我呀喵.

目錄

一. 規約求值

• λ-calculus的構成部分
• λ-calculus規約求值問題
• The Church-Rosser Theorem

二. 不動點

• 遞歸結構定義問題
• 不動點組合子
• 最小不動點定理
• 不動點邏輯

三. 不可判定

• 條件與分支
• 自然數系統
• 列表結構
• 拓展λ-calculus
• 哥德爾數
• De Bruijns index
• 遞歸函數
• 不可判定性

四. 規約策略

• The quasi-leftmost-reduction theorem
• λI-calculus
• βη-規約

五. 簡單類型

• Simply typed λ-calculus à la Curry
• Simply typed λ-calculus à la Church
• Church-Rosser property(for simply typed λ-calculus)

六. 正規化與類型重建

• 弱正規化定理
• 強正規化定理
• 類型檢查與重建

七. 柯里-霍華德同構

• 待定

八. 系統μ與Continuation

• 待定

九. 系統F與類型多態

• 待定

十. 依值類型

• 待定

十一. Cube與PTS

• 待定

十二. Advanced topic

• lambda模型(待定)
• 類型空間(待定)
• 笛卡兒閉範疇(待定)

(第七節以後的文章還沒寫好, 望見諒, 我會抽空把坑填上的. 另外關於Lambda calculus引論這個系列與專欄有什麼意見或疑問也歡迎來和我討論, 也歡迎相關話題的投稿)

推薦閱讀：