Let’s play Agda：把抽象的數學證明當成程式來執行#

本網站的目的，是幫助你學習 Agda 這個函數式證明語言。它是為 2025 年在帕多瓦大學 （University of Padova）開設的一門課程而製作的。

從這裡開始： Agda 作為程式語言

簡單來說：Agda 是一種程式語言……#

• 🧊 純函數式，沒有可變狀態
• 🐑 語法與風格類似 Haskell
• 🧱 靜態型別，讓許多錯誤在編譯期就被抓到
• 🌳 熟悉的型別，例如整數、串列、……
• 🧭 型別推論，讓我們專心處理真正重要的型別

舉例來說，插入排序（insertion sort）的實作大概長這樣：

sort : List ℕ → List ℕ
sort []       = []
sort (x ∷ xs) = insert x (sort xs)

我們也可以想像具有下列型別簽名（type signature）的函數……

fibonacci : ℕ → ℕ                                   -- 費氏數
pi        : ℝ                                       -- 任意精度的常數
size      : {X : Set} → Tree X → ℕ                  -- 二元樹的大小
replicate : {X : Set} (len : ℕ) → X → Vector len X  -- 由相同元素組成的向量

……同時也是一種證明語言……#

• 🧾 見證的型別（types of witnesses），把證明與寫程式這兩種活動統一起來
• ✨ 情境輔助（context assistance），用互動的方式一步步建構證明
• 🎨 表達力足以涵蓋大部分的數學
• 🤹 以 hole 驅動的開發（hole-driven development）

在 Agda 中，我們藉由建構一個能算出適當見證（witness）的程式，來證明一個命題。這種作法就是 著名的 propositions as types（命題即型別）哲學：

grande-teorema   : 2 + 2 ≡ 4
binomial-theorem : (x : ℕ) (y : ℕ) → (x + y) ² ≡ x ² + 2 · x · y + y ²
sort-correct     : (xs : List ℕ) → IsSorted (sort xs)

舉例來說，存在著下列這些見證的型別……

• 證明 2 + 2 等於 4 （這個型別非空，也就是有居民 inhabited）；
• 證明 2 + 2 等於 5 （這個型別是空的）；
• 證明存在大於 42 的質數 （這個型別包含無限多個值，例如序對 (43 , p)，其中 p 是「43 是大於 42 的質數」的見證）；
• 證明質數有無限多個；
• 證明某個給定的排序函數 sort 運作正確 （這個型別包含的函數，會讀入任意串列 xs 作為輸入，並輸出一個見證， 證明 sort xs 是由小到大排好的）；
• 證明連續統假設（continuum hypothesis）成立；
• 諸如此類。

……並且協助我們……#

• ✅ 驗證證明的正確性
• 🧮 實作演算法
• 💭 整理數學思路
• ⚙️ 從計算的角度欣賞數學
• 🚀 協力打造數學函式庫