課程介紹

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

公告事項

特別講題:Monad 與副作用

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

重要日期

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

課程

函數程設

本課程以 Haskell 為工具,概述函數程式設計相關的一些必備知識,以便與其他課程銜接。由歸納法開始,我們將談資料結構與函數的歸納定義,發現函數的定義可依循資料結構的定義。而若欲證明該函數的性質,又可使用歸納法,其證明可依循函數的定義。接著我們會談到摺 (fold) 的觀念,發現摺可視為一種歸納法的抽象。最後以紅黑樹 (red-black tree) 為例演練程式設計與歸納證明,並為之後的依值型別課程做準備。

課程講師

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

教學資源

講義
講義
原始檔
習題
習題解答
補充資料

邏輯

數學證明建立於有效的推論結構之上,而型式邏輯學的目的是以嚴謹符號表達這些推論結構並研究其性質。這門課聚焦於命題直構邏輯 (propositional intuitionistic logic) 的自然演繹系統 (natural deduction),討論型式邏輯學裡基本的語法 (syntactic) 和語意 (semantic) 證明方法,並點出邏輯與計算的密切關係,銜接至依值型別課程。透過對推論結構的型式化學習,這門課也為其他課程所需的數學證明基礎作好準備。

課程講師

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

教學資源

投影片

λ-算則

現今許多語言如 Haskell、Agda 都會以 λ-算則 (λ-calculus,其中 λ 唸作 lam-da /ˈlæmdə/)的變形作為語言的模型,因此在課程中我們將從數學角度探討 λ-calculus 以及程式語言各種基本概念跟性質。例如定義何謂計算以及計算上相等的程式證明相關性質;加入型別討論並證明一個有型別沒有副作用的程式是如何能保證計算時一定會算出結果;除了學理上的興趣外,我們也會討論具體實務上應用於許多語言中解決程式碼重複的語言特性—多型(polymorphism)。這門課將延伸至依值型別課程,應用 Agda 實作與證明語言的性質。

課程講師

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

教學資源

投影片

依值型別

依值型別的表達能力遠超過主流語言的型別系統,一些原先需要另外證明的程式性質可直接編寫為依值型別,程式只要通過型別檢查即可保證性質成立。當我們透過依值型別提供更多資訊給型別檢查器,後者就能反過來隨時告訴我們當下已知與尚待滿足的條件,互動地寫出正確程式。依值型別語言也可用於數學型式化,數學定理與證明在依值型別語言中表達出來後,不僅能保證推論過程正確無誤,還一定具有計算意義。在此數學、邏輯、計算融為一體,形成新世代程式語言設計的堅實基礎。

課程講師

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

教學資源

Agda 安裝指南
Unicode 符號對照表
原始檔

特別講題:Monad 與副作用

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

課程講師

單中杰
Department of Computer Science, Indiana University

教學資源

投影片
習題

課表

第一週 星期一 星期二 星期三 星期四 星期五
上午 函數程設 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