深入研究編譯器、程序設計語言理論須要學習哪些數理邏輯學的內容？

PLT中好像充滿了xxx推導, yyy演算

---

xx推導、xx演算，以及其他程序語言理論涉及的，可能不只是數理邏輯，下面簡要說說自己的體會。

首先最好要有一定的集合論，抽象代數（群、環、域這些），數理邏輯，和圖論的基礎。正巧，《離散數學》上面這幾個都有。 最後再補充一下類型論的知識，type theory建議找綜述性的論文，要能把基本的type rule看懂吧。

進一步，很可能會用到的：

形式語言與自動機導論 。

面向計算機科學的數理邏輯系統建模與推理。建立對Hoare Logic, model checking等的理解。

Types and Programming Languages 。

Formal semantic的也可以找些材料了解。

其實上面這些東西，內容上有些是交叉的，光看文獻也比較枯燥。有了一定的基礎，可以從具體的項目/問題入手，遇到需要的再翻大部頭、找相關論文。 比如你要做程序分析的工具，需要從control flow graph，program dependent graph等各種」圖「中提取信息，離不開圖論的知識；」形式化「地建立那些分析的模型，需要用到抽象代數的格、域等（尤其是抽象解釋中）。如果對程序驗證比較感興趣，就需要多了解Curry-Howard同構、Hoare logic、Model checking

等東西，這也是PL方向最接近」理論CS「的了。。

最後，範疇論、Homotopy Type Theory、遞歸論中比較「難」的部分，這些其實屬於比較小眾/新潮的，PL很多研究/應用都用不上。都會的話自然是最好。。

下面推薦兩本書，都是由多位作者共同撰寫的。

Advanced Topics in Types and Programming Languages

SSA Book （完成度比較低。。）

想到再補充。

，

---

---

PLT領域對數理邏輯的依賴並不多，不用為了理解PLT的東西重學MaLo(mathematical logic)。你提到的推導和演算你能理解表面意思就夠了，沒有太深的東西。

MaLo一般會有分成First Order和Second Order來講。大部分面向計算機系的書或者課程只講First Order，因為它是完備的（情況比較簡單，好理解）。我實在想不到PLT有什麼場景需要涉及不完備的二階邏輯，所以你就找本教材把FO logic看了就行了，核心是圍繞公理化系統，重點和難點理解公理化相關的問題。

如果你看完覺得不甘心，想了解一些不完備的東西，建議你去看可計算理論的教材，而不是去學二階邏輯，可計算理論中的「不可判定」就是二階邏輯不完備的一個實例。想明白幾種模型計算能力的層級問題就夠了。

---

推薦閱讀：