課程資訊

What’s New

以函數語言為起點，瞭解程式語言在語法、語意、與實務面向的課題。

本課程為「程式語言(Programming Languages)」系列課程之一，著眼點並不是教特定程式語言，而是以函數語言(functional language)為媒介，討論設計程式解決問題的思考方式、設計程式使用的數學與邏輯基礎、以及程式語言與形式符號在其中扮演的角色。其核心概念包括：

程式語言是一種形式語言，作為思考的工具。我們用程式語言表達概念，也用程式語言中的形式規則檢驗程式的正確性。
函數程設(functional programming)是一種相當簡化的程式設計模型。因為簡單，有更多易於掌握的性質，可作為討論程式語言的基礎。
有一整套奠基於歸納法(induction)之上的程式設計理論。資料結構可用歸納法定義，其上的程式可用歸納寫成，關於該程式的性質也可用歸納法證明。與之相對的是餘歸納(coinduction).
上述兩種方法都不足以定義出所有程式 – 為此我們將需要允許遞迴 (general recursion) 的模型. 然而，表達力變強大也意味著我們將失去一些好性質。
程式設計與定理證明是密切相關、相輔相成的活動。
函數語言這樣的簡單模型允許我們做等式推導，可作為一種程式設計方法 – 將程式「算」出來。
好的型別系統常有「只要型別對，程式就會對」的特性。
型別系統與邏輯有密切關係：邏輯陳述相當於型別，具有該型別的程式則是該邏輯陳述的證明。
型別系統能幫助我們確立程式的正確性，甚至輔助我們寫程式。
更強大的型別系統相當於更具表達力的邏輯。同樣地，邏輯變強大的同時，我們也犧牲掉一些好掌握的性質。

關鍵字：函數程設 functional programming 程式推導 program derivation 歸納法 induction 證明 proofs 邏輯 logic 型別系統 type systems

僅採計期中考、期末考成績，比率機動調整。課堂中將發習題，但不計入學期分數。出席不計。

詳見工具.