課程介紹

本課程將講授程式語言領域之入門理論與知識,希望培養學生以型式邏輯進行清晰思考的能力,了解邏輯與程式語言、型別系統的密切關係, 以及型別系統在程式語言中扮演的角色,使學生能以遞迴/迭構方式理解並解決程式設計問題,能運用軟體工具輔助邏輯推理及證明程式正確性, 並具備進一步探索程式語言相關領域的知識基礎。

公告事項

特別講題:Monad 與副作用

函數編程雖然常被說成是沒有副作用的,但是其實藉由函數以及型別的抽象化,尤其是藉由著名的 Monad 概念,可以更精準、更廣泛地表達並駕馭各種副作用。我們先介紹 Monad 的原理,再說明幾種歷久彌新的應用,包括搜尋、句法分析、機率運算等。我們也會跟人工智慧扯上關係,因為不論是要用「自動微分」把機器學習普及化,還是要把清晰易懂的模型變成跑得動的程式,都免不了對副作用進行推理。

重要日期

  1. 03/10
    網站上線
  2. 07/17
    外地實習生報名截止
  3. 07/20
    外校學生修課報名截止
  4. 07/25
    臺大學生報名截止
  5. 08/01
    課程開始
  6. 08/12
    課程結束

課程

函數編程

講師

穆信成
中央研究院資訊科學研究所

教學資源

講義
原始檔
練習解答
考試範圍

邏輯

講師

柯向上
中央研究院資訊科學研究所

教學資源

投影片
考試範圍

λ-Calculus

講師

陳亮廷
中央研究院資訊科學研究所

教學資源

投影片
補充資料
習題解答
考試範圍

依值型別編程

講師

穆信成
中央研究院資訊科學研究所
柯向上
中央研究院資訊科學研究所
陳亮廷
中央研究院資訊科學研究所

教學資源

Agda 安裝指南
Unicode 符號對照表
原始檔
考試範圍

Monad 與副作用

講師

單中杰
Department of Computer Science, Indiana University

教學資源

原始檔
考試範圍

課表

第一週 星期一 星期二 星期三 星期四 星期五
上午 函數編程 0Opening & wholemeal programming 函數編程 1Inductive definitions λ-Calculus 0Untyped λ-Calculus λ-Calculus 1Simply Typed λ-Calculus λ-Calculus 2Polymorphic λ-Calculus
下午 邏輯 0Propositional logic & natural deduction 邏輯 1Classical semantics of propositional logic 函數編程 2Fold fusion 邏輯 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