Lambda Calculus 歷史 -- AI 偵探風格#

以「推理探案」的方式，追查 λ 演算從 1928 年誕生至今的每一步： 前因是什麼？線索在哪裡？推理如何展開？後果又如何改變了整個計算科學？

起源期（1920s–1930s）#

• 1928-Church發明λ演算.md -- λ 符號的誕生
• 1932-Church邏輯系統.md -- 以 λ 為基礎的邏輯嘗試
• 1934-Kleeneλ可定義函數.md -- 遞迴函數與 λ 的交會
• 1935-KleeneRosser矛盾.md -- 悖論擊潰 Church 系統
• 1936-判定問題不可判定性.md -- Entscheidungsproblem 的審判
• 1936-Church編碼.md -- 用純 λ 項寫出數字與布林
• 1937-Turing等價性證明.md -- 兩大計算模型的會師

發展期（1940s–1960s）#

• 1940-簡單型別λ演算.md -- 用型別封鎖悖論
• 1941-Church的書.md -- The Calculi of Lambda-Conversion
• 1958-LISP.md -- λ 記法第一次進入程式語言
• 1958-Curry組合邏輯.md -- 沒有變數的 λ 演算
• 1963-SECD機器.md -- Landin 的抽象執行引擎
• 1964-ISWIM.md -- 函數式語言的祖先

型別理論期（1970s–1980s）#

• 1965-CurryHoward對應.md -- 命題即型別、證明即程式
• 1969-ScottD∞模型.md -- λ 演算終於有了數學語義
• 1972-SystemF.md -- Girard 的多型 λ 演算
• 1972-指稱語義.md -- Scott 與 Strachey 的語義學
• 1973-ML語言.md -- Hindley–Milner 型別推論問世
• 1980-MartinLöf依賴型別.md -- 型別承載命題的極限
• 1985-Barendregt標準參考書.md -- λ 演算的聖經

現代應用期（1990s–至今）#

• 1989-Coq.md -- 證明即程式的實作
• 1990-Haskell.md -- 以 Curry 命名的純函數式語言
• 現代-匿名函數.md -- λ 演算進入主流程式設計