邏輯、語言與計算暑期研習營
Formosan Summer School on Logic, Language, and Computation, 20247/1-7/12 09:10-12:10, 13:20–16:20
地點：國立臺灣大學管理學院一號館103教室
Formosan Summer School on Logic, Language, and Computation, 2024本課程將講授程式語言領域之入門理論與知識，希望培養學生以型式邏輯進行清晰思考的能力，了解邏輯與程式語言、型別系統的密切關係，以及型別系統在程式語言中扮演的角色，使學生能以遞迴／迭構方式理解並解決程式設計問題，能運用軟體工具輔助邏輯推理及證明程式正確性，並具備進一步探索程式語言相關領域的知識基礎。
FLOLAC 2024 很榮幸邀請到劍橋大學 Neel Krishnaswami 教授擔任特別講師，講題為 Programming with Modal Types，內容簡介如下：
著名的 Curry-Howard 對應闡述形式邏輯和函式程設之間深刻的對應：邏輯命題與型別相對應，命題的證明與該型別的程式亦相對應。然而幾個世紀以來，邏輯學家認識到邏輯系統並非只有一種，而是存在許多不同的邏輯系統。在過去的幾十年中，電腦科學家已經理解到這些邏輯系統可以反過來為程式語言提供新的見解。
傳統邏輯最重要的擴充之一是模態邏輯（modal logic）。這將形式邏輯拓展到對於相對情境下斷言的研究。例如，我們不可能說「正在下雨」這個命題絕對是真或假，而是得取決於它被斷言的時間和地點。從電腦科學的角度來看，這表明我們可以將型別系統擴展到不單只是資料的形狀，而是關注到程式更深層次的行為特性。
本課程將探討模態邏輯在程式語言設計中的應用，從它們在型別理論中的表現開始，展示如何用於組織各種計算現象，包括反應式程式設計（reactive programming）、增量計算（incremental computing）、資料庫查詢語言（data query language），甚至是能力安全程式設計（capability-safe programming）。
本課程以 Haskell 為工具，概述函數程式設計相關的一些必備知識，以便與其他課程銜接。 由歸納法開始，我們將談資料結構與函數的歸納定義，發現函數的定義可依循資料結構的定義。 而若欲證明該函數的性質，又可使用歸納法，其證明可依循函數的定義。 接著我們會談到摺 (fold) 的觀念，發現摺可視為一種歸納法的抽象。
數學證明建立於有效的推論結構之上， 而型式邏輯學的目的是以嚴謹符號表達這些推論結構並研究其性質。 這門課聚焦於命題直構邏輯 (propositional intuitionistic logic) 的自然演繹系統 (natural deduction)，討論型式邏輯學裡基本的語法 (syntactic) 和語意 (semantic) 證明方法，並點出邏輯與計算的密切關係，最終引導至依值型別。 透過對推論結構的型式化學習，這門課也為其他課程所需的數學證明基礎作好準備。
現今許多語言如 Haskell、Agda 都會以 λ-算則 （λ-calculus，其中 λ 唸作 lam-da /ˈlæmdə/）的變形作為語言的模型，因此在課程中我們將從數學角度探討 λ-calculus 以及程式語言各種基本概念跟性質。例如定義何謂計算以及計算上相等的程式證明相關性質；加入型別討論並證明一個有型別沒有副作用的程式是如何能保證計算時一定會算出結果；除了學理上的興趣外，我們也會討論具體實務上應用於許多語言中解決程式碼重複的語言特性—多型（polymorphism）。
著名的 Curry-Howard 對應闡述形式邏輯和函式程設之間深刻的對應：邏輯命題與型別相對應，命題的證明與該型別的程式亦相對應。然而幾個世紀以來，邏輯學家認識到邏輯系統並非只有一種，而是存在許多不同的邏輯系統。在過去的幾十年中，電腦科學家已經理解到這些邏輯系統可以反過來為程式語言提供新的見解。
傳統邏輯最重要的擴充之一是模態邏輯（modal logic）。這將形式邏輯拓展到對於相對情境下斷言的研究。例如，我們不可能說「正在下雨」這個命題絕對是真或假，而是得取決於它被斷言的時間和地點。從電腦科學的角度來看，這表明我們可以將型別系統擴展到不單只是資料的形狀，而是關注到程式更深層次的行為特性。
本課程將探討模態邏輯在程式語言設計中的應用，從它們在型別理論中的表現開始，展示如何用於組織各種計算現象，包括反應式程式設計（reactive programming）、增量計算（incremental computing）、資料庫查詢語言（data query language），甚至是能力安全程式設計（capability-safe programming）。
| 第一週 | 星期一 | 星期二 | 星期三 | 星期四 | 星期五 |
|---|---|---|---|---|---|
| 上午 | 函數程設 0Definition and Proof by Induction | 函數程設 1Monads | λ-算則 0Untyped λ-Calculus | λ-算則 1Simple Types and their Extensions | λ-算則 2Parametric Polymorphism |
| 下午 | 邏輯 0Propositional Logic and Natural Deduction | 邏輯 1Classical Semantics of Propositional Logic | 函數程設 2Monads (Continued) | 邏輯 2The Curry–Howard Correspondence | 討論Discussion |
| 第二週 | 星期一 | 星期二 | 星期三 | 星期四 | 星期五 |
|---|---|---|---|---|---|
| 上午 | 模態型別 0Modal Logic | 模態型別 1Capability-Safety and Logical Relations | 模態型別 2 | 模態型別 3 | 考試Exam |
| 下午 | λ-算則 3Bidirectional Typing | 函數程設 3Monads (Rebooted) | 邏輯 3Dependently Typed Programming | 討論 Discussion |