邏輯、語言與計算暑期研習營
Formosan Summer School on Logic, Language, and Computation, 20228/1-8/12 09:00-17:00
地點：國立臺灣大學新生教學館 202 教室
Formosan Summer School on Logic, Language, and Computation, 2022本課程將講授程式語言領域之入門理論與知識，希望培養學生以型式邏輯進行清晰思考的能力，了解邏輯與程式語言、型別系統的密切關係，以及型別系統在程式語言中扮演的角色，使學生能以遞迴／迭構方式理解並解決程式設計問題，能運用軟體工具輔助邏輯推理及證明程式正確性，並具備進一步探索程式語言相關領域的知識基礎。
函數程式雖然常被說成是沒有副作用的，但是其實藉由函數以及型別的抽象化，尤其是藉由著名的 Monad 概念，可以更精準、更廣泛地表達並駕馭各種副作用。 我們先介紹 Monad 的原理，再說明幾種歷久彌新的應用，包括搜尋、句法分析、機率運算等。 我們也會跟人工智慧扯上關係，因為不論是要用「自動微分」把機器學習普及化，還是要把清晰易懂的模型變成跑得動的程式，都免不了對副作用進行推理。
本課程以 Haskell 為工具，概述函數程式設計相關的一些必備知識，以便與其他課程銜接。 由歸納法開始，我們將談資料結構與函數的歸納定義，發現函數的定義可依循資料結構的定義。 而若欲證明該函數的性質，又可使用歸納法，其證明可依循函數的定義。 接著我們會談到摺 (fold) 的觀念，發現摺可視為一種歸納法的抽象。 最後以紅黑樹 (red-black tree) 為例演練程式設計與歸納證明，並為之後的依值型別課程做準備。
數學證明建立於有效的推論結構之上， 而型式邏輯學的目的是以嚴謹符號表達這些推論結構並研究其性質。 這門課聚焦於命題直構邏輯 (propositional intuitionistic logic) 的自然演繹系統 (natural deduction)，討論型式邏輯學裡基本的語法 (syntactic) 和語意 (semantic) 證明方法，並點出邏輯與計算的密切關係，銜接至依值型別課程。 透過對推論結構的型式化學習，這門課也為其他課程所需的數學證明基礎作好準備。
現今許多語言如 Haskell、Agda 都會以 λ-算則 （λ-calculus，其中 λ 唸作 lam-da /ˈlæmdə/）的變形作為語言的模型，因此在課程中我們將從數學角度探討 λ-calculus 以及程式語言各種基本概念跟性質。例如定義何謂計算以及計算上相等的程式證明相關性質；加入型別討論並證明一個有型別沒有副作用的程式是如何能保證計算時一定會算出結果；除了學理上的興趣外，我們也會討論具體實務上應用於許多語言中解決程式碼重複的語言特性—多型（polymorphism）。這門課將延伸至依值型別課程，應用 Agda 實作與證明語言的性質。
依值型別的表達能力遠超過主流語言的型別系統，一些原先需要另外證明的程式性質可直接編寫為依值型別，程式只要通過型別檢查即可保證性質成立。 當我們透過依值型別提供更多資訊給型別檢查器，後者就能反過來隨時告訴我們當下已知與尚待滿足的條件，互動地寫出正確程式。 依值型別語言也可用於數學型式化，數學定理與證明在依值型別語言中表達出來後，不僅能保證推論過程正確無誤，還一定具有計算意義。 在此數學、邏輯、計算融為一體，形成新世代程式語言設計的堅實基礎。
| 第一週 | 星期一 | 星期二 | 星期三 | 星期四 | 星期五 |
|---|---|---|---|---|---|
| 上午 | 函數程設 0Inductive definitions | 函數程設 1Folds | λ-算則 0Untyped λ-Calculus | λ-算則 1Simply typed λ-Calculus | λ-算則 2Polymorphic λ-Calculus |
| 下午 | 邏輯 0Propositional logic & natural deduction | 邏輯 1Classical semantics of propositional logic | 函數程設 2Red-black trees | 邏輯 2Curry–Howard correspondence | 討論Discussion |
| 第二週 | 星期一 | 星期二 | 星期三 | 星期四 | 星期五 |
|---|---|---|---|---|---|
| 上午 | Monad 與副作用 0Dualism: Pure programming with effects, monad, type classes | Monad 與副作用 1Choices: Nondeterministic search & lazy sharing, parsing, probabability | Monad 與副作用 2AI: Gradient descent, automatic differentiation, equational reasoning | Monad 與副作用 3Optional topics | 考試Exam |
| 下午 | 依值型別 0Indexed datatypes & dependent pattern matching | 依值型別 1Shallow embedding of higher-order logic & deep embedding of propositional logic | 依值型別 2Formalisation of simply typed λ-Calculus | 討論 Discussion |